## Stream: maths

### Topic: category theory

#### Kenny Lau (Apr 02 2018 at 10:02):

@[reducible] def Set.Prod_Hom (B : Type u) : adjunction examples.Set examples.Set :=
(examples.Set.product_functor B)
(examples.Set.Hom_functor_right B)
(λ A C f x, f x.1 x.2)
(λ A C f x y, f (x, y))
(λ A₁ A₂ C₁ C₂ f g t, rfl)
(λ A₁ A₂ C₁ C₂ f g t, rfl)
(λ A C f, funext $λ ⟨t₁, t₂⟩, rfl) (λ A C f, rfl)  #### Kenny Lau (Apr 02 2018 at 10:02): so natural #### Kenny Lau (Apr 02 2018 at 10:20): @[reducible] def Top_Set : adjunction examples.Top examples.Set := adjunction.free_forgetful _ examples.Top.discrete examples.Top.forgetful (λ S T f, ⟨f, continuous_top⟩) (λ S T f, f.1) (λ T₁ T₂ S₁ S₂ f g t z, rfl) (λ T₁ T₂ S₁ S₂ f g t, subtype.eq rfl) (λ S T f, subtype.eq rfl) (λ S T f, rfl) @[reducible] def Set_Top : adjunction examples.Set examples.Top := adjunction.make _ _ examples.Top.forgetful examples.Top.indiscrete (λ S T f, f.1) (λ S T f, ⟨f, continuous_bot⟩) (λ T₁ T₂ S₁ S₂ f g t, subtype.eq rfl) (λ T₁ T₂ S₁ S₂ f g t, rfl) (λ S T f, rfl) (λ S T f, subtype.eq rfl)  #### Kenny Lau (Apr 02 2018 at 10:20): that moment when they're adjoint to each other #### Kenny Lau (Apr 07 2018 at 17:25): for a set S, denoting by L(S) the transitive closure of S, we see that for any transitive set T with S ⊆ T, then L(S) ⊆ T #### Kenny Lau (Apr 07 2018 at 17:25): I wonder if this is the left adjoint of some forgetful functor #### Kenny Lau (Apr 07 2018 at 17:26): well, working in the category of sets with inclusion as morphism, we see that Hom_Trans(L(S),T) = Hom_Set(S,R(T)), where Trans is the category of transitive sets #### Kevin Buzzard (Apr 07 2018 at 18:43): What does this even mean? What is a transitive set? #### Kenny Lau (Apr 07 2018 at 18:44): A set X is transitive if for every x and y such that x∈y∈X, we have x∈X #### Kenny Lau (Apr 07 2018 at 18:45): if the transitive closure is indeed a left adjoint, then we get right-exactness for free #### Kevin Buzzard (Apr 07 2018 at 18:49): Eew. I think I saw that notion in undergraduate set theory nearly 30 years ago, and I'm not sure I've seen it since. Maybe I saw it in the context of ordinals, which is something else I've not seen since. #### Kevin Buzzard (Apr 07 2018 at 18:53): Are you making an assertion here? What is R(T)? #### Kenny Lau (Apr 07 2018 at 18:53): the forgetful functor that forgets the fact that T is transitive #### Kevin Buzzard (Apr 07 2018 at 18:53): Is what you write true? #### Kenny Lau (Apr 07 2018 at 18:53): I believe so #### Kevin Buzzard (Apr 07 2018 at 18:54): If S and T are both transitive, then you're asserting that the transitive maps from S to T are the same as the maps from S to T then? #### Kenny Lau (Apr 07 2018 at 18:54): yes, since here the morphisms are just inclusions, so there is only one morphism per pair of sets #### Kevin Buzzard (Apr 07 2018 at 18:55): What does Hom_Set mean then? #### Kenny Lau (Apr 07 2018 at 18:55): oh, inclusion #### Kevin Buzzard (Apr 07 2018 at 18:57): Do you have a question? #### Kenny Lau (Apr 07 2018 at 18:57): is my belief right #### Kevin Buzzard (Apr 07 2018 at 18:58): What does Hom_Trans mean? #### Kenny Lau (Apr 07 2018 at 18:58): subcategory #### Kevin Buzzard (Apr 07 2018 at 18:58): I don't know what anything means. It feels like you have made these categories up. #### Kevin Buzzard (Apr 07 2018 at 18:59): It also seems that you are just as capable of writing down a proof of your assertion as I am. Why not check it in Lean? ;-) #### Kenny Lau (Apr 07 2018 at 18:59): because to hell with the category of sets in Lean #### Kevin Buzzard (Apr 07 2018 at 18:59): What does Hom_Trans mean? #### Kenny Lau (Apr 07 2018 at 18:59): the inclusion in the category of transitive sets #### Kevin Buzzard (Apr 07 2018 at 18:59): So at most one map between two sets? #### Kenny Lau (Apr 07 2018 at 19:00): yes #### Kevin Buzzard (Apr 07 2018 at 19:00): " we see that for any transitive set T with S ⊆ T, then L(S) ⊆ T ". Is that your question? #### Kenny Lau (Apr 07 2018 at 19:00): well that's the UMP of transitive closure #### Kenny Lau (Apr 07 2018 at 19:00): which should be right #### Kevin Buzzard (Apr 07 2018 at 19:01): But what is your question if it is not precisely that statement? #### Kenny Lau (Apr 07 2018 at 19:01): no idea #### Kevin Buzzard (Apr 07 2018 at 19:01): We might be done then :-) #### Kenny Lau (Apr 07 2018 at 19:02): interesting #### Reid Barton (Sep 01 2018 at 21:06): Scott I guess I'll keep you updated on what I'm doing by sending pastebin links for now. #### Reid Barton (Sep 01 2018 at 21:07): https://pastebin.com/WmdNgPdx is limits and colimits in types (nice and easy) and small and filtered categories (also easy). #### Reid Barton (Sep 01 2018 at 21:08): Next I plan to try to show that small limits commute with filtered colimits #### Reid Barton (Sep 01 2018 at 21:08): Probably I won't finish that in the next few days. #### Scott Morrison (Sep 01 2018 at 22:45): Thanks, Reid, that patch has been applied! #### Reid Barton (Sep 02 2018 at 15:54): I defined the limit functor but the proofs aren't as concise as they should be, especially map_id'. https://pastebin.com/QDM9H7TX #### Reid Barton (Sep 02 2018 at 15:55): Scott -- maybe the simp lemmas could be set up so that map_id' can be proved by obviously? map_comp' is more complicated, since you have to use associativity (backwards) #### Scott Morrison (Sep 02 2018 at 22:10): @Reid Barton, in fact I already had this, obscurely hidden in universal/complete/default.lean, with slightly different proofs. I've incorporated some changes from yours, but left my proofs for now. Curiously, obviously does just fine for map_comp', but fails on map_id' because for some reason simp won't apply limit.lift_π. #### Scott Morrison (Sep 02 2018 at 22:13): I guess it was hiding in that directory because I wrote it for the sake of https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/universal/complete/functor_category.lean, a still incomplete proof that C \lea D has limits if D does. #### Kenny Lau (Oct 20 2018 at 15:59): @Scott Morrison Will you change some of the mathlib files to use category theory? #### Kenny Lau (Oct 20 2018 at 16:00): what's the plan for category theory? #### Scott Morrison (Oct 20 2018 at 16:00): I think at first, not much. Things like has_products CommRing can first live under category_theory/, as we get used to them. #### Kenny Lau (Oct 20 2018 at 16:01): will they gradually assimilate into the main mathlib library? #### Scott Morrison (Oct 20 2018 at 16:01): Eventually such facts should move out to their natural homes, immediately following where the underlying lemmas are actually proved. #### Kenny Lau (Oct 20 2018 at 16:01): nice #### Scott Morrison (Oct 20 2018 at 16:01): I suspect in the long run a lot of files will want to import category_theory.isomorphism, to avoid having to define their own custom version of equiv for the structure at hand. #### Kenny Lau (Nov 02 2018 at 09:58): @Scott Morrison The new module will be: class module (α : out_param$ Type u) (β : Type v) [out_param \$ ring α]
[add_comm_group β] extends semimodule α β


How will your category theory library deal with this?

#### Scott Morrison (Nov 02 2018 at 11:02):

Mostly users will just want the category of R-modules for some fixed R. After you've fixed the ring this is no more or less scary than bundling any other algebraic typeclass, I think.

#### Kenny Lau (Nov 02 2018 at 11:15):

@Scott Morrison I don't see how bundle can solve this

#### Scott Morrison (Nov 02 2018 at 11:16):

Oh, I didn't imply that we should use bundled. It's only intended for the simplest cases.

#### Scott Morrison (Nov 02 2018 at 11:18):

But structure Module (a : Type) [ring a] := (b : Type) (m : module a b), is presumably fine.

#### Scott Morrison (Nov 02 2018 at 11:18):

Maybe you haven't actually said what you're concerned about?

#### Kenny Lau (Nov 02 2018 at 11:18):

and actually that's all I'm concerned about

#### Scott Morrison (Nov 02 2018 at 11:19):

So structure Module (a : Type) [ring a] := (b : Type) (g : add_comm_group b) (m : module a b)...?

#### Kenny Lau (Nov 02 2018 at 11:22):

I'm not really sure how all of this works, because last time in my own category repo, I was wrestling with sigma

#### Scott Morrison (Nov 02 2018 at 11:27):

Yeah, I think just building custom structures, and then a few lemmas that peel back out the typeclasses as needed, is easiest.

#### Scott Morrison (Nov 02 2018 at 11:27):

I'll make a few more examples.

thanks

#### Kenny Lau (Nov 02 2018 at 16:46):

@Scott Morrison is bundled category a category? If not, what's the proper name?

#### Johan Commelin (Nov 02 2018 at 19:54):

I have a natural transformation a from F to G, and Lean is looking for a natural transformation from G.op to F.op. So I would like to provide a.op but this is not defined yet. What is the natural place to add this definition? In opposites.lean or in natural_transformation.lean?

#### Reid Barton (Nov 02 2018 at 20:00):

I think it makes sense to keep category/functor/natural_transformation "at the bottom" and so put a.op in opposites like F.op

#### Johan Commelin (Nov 02 2018 at 20:05):

Ok... fine with me. I could also imagine opposites being pretty "fundamental".

#### Kenny Lau (Nov 02 2018 at 20:09):

It would be quite interesting if we know that functors form a category but not that categories form a category...

#### Kenny Lau (Nov 02 2018 at 20:09):

I've searched all the files

#### Mario Carneiro (Nov 02 2018 at 20:10):

the problem is that categories form a 2-category

#### Mario Carneiro (Nov 02 2018 at 20:10):

so "categories form a category" is true but mostly useless

#### Reid Barton (Nov 02 2018 at 20:10):

Categories also form a perfectly good category, we just don't have it yet

#### Johan Commelin (Nov 02 2018 at 20:19):

Ok, I'm testing out a heresy:

def cocone (F : J ⥤ C) := cone F.op


The first problem I hit is that for c : cocone F the tip of the cocone c.X is now an object of C\op instead of C. Can this somehow be fixed? I would rather just write f : c.X \hom X instead of

f : @category.hom C _ c.X X


#### Reid Barton (Nov 02 2018 at 20:27):

I actually have this problem in ordinary informal math as well: it's hard to talk about both C and C^op at the same time.
Sometimes I write things like $\overline{A}$ for the object of C^op corresponding to the object $A$ of C, but I'm not really fond of it.

#### Kenny Lau (Nov 02 2018 at 20:28):

"ordinary informal math" = category

#### Johan Commelin (Nov 02 2018 at 20:30):

Sure, so we could write X.op for such objects. But this problem is different. With my definition c.X lives in C^op by definition. But I'dd rather have it live in C... And somehow just writing f : (c.X : C) \hom X doesn't cut it....

#### Johan Commelin (Nov 02 2018 at 20:30):

Hmmm... I have to run. See y'all later.

#### Reid Barton (Nov 02 2018 at 20:52):

Perhaps we could have unop : C\op \to C?

#### Kenny Lau (Nov 02 2018 at 20:56):

or maybe an equivalence of categories C\op\op \cong C?

#### Kenny Lau (Nov 02 2018 at 21:22):

import algebra.module
import category_theory.examples.rings category_theory.opposites

universes u v w

variables (R : Type u) [ring R]

class Module (M : Type v) extends add_comm_group M, module R M

def Module.is_linear_map {M N : Type v} [Module R M] [Module R N] (f : M → N) : Prop :=
is_linear_map f

open category_theory category_theory.examples

instance Module.concrete_category : concrete_category (@Module.is_linear_map R _) :=
⟨λ _ _, by constructor; intros; refl,
λ _ _ _ _ _ _ _ _ hf hg, by cases hf; cases hg; constructor; intros; simp only [(∘), *]⟩

@[reducible] def Mod := bundled (Module R)

@[reducible] def Cat := bundled category

instance : category Cat :=
{ hom := λ C D, @category_theory.functor C.1 C.2 D.1 D.2,
id := λ C, @functor.id C.1 C.2,
comp := λ C D E, @category_theory.functor.comp C.1 C.2 D.1 D.2 E.1 E.2,
id_comp' := λ C D f, by cases f; refl,
comp_id' := λ C D f, by cases f; refl }

def Mod : Ringᵒᵖ ⥤ Cat :=
{ obj := λ R, bundled.mk _ (Mod R.1),
map' := λ R S φ, concrete_functor (begin end) (begin end) }


#### Reid Barton (Nov 02 2018 at 21:34):

This looks good, but then the real test is whether it's convenient to use objects of Mod R as modules and vice versa, and the same for Cat

#### Reid Barton (Nov 02 2018 at 21:36):

At a minimum you want the instance that gets you the Module back out from x : Mod R

#### Reid Barton (Nov 02 2018 at 21:37):

analogous to instance (x : Ring) : ring x := x.str

#### Kenny Lau (Nov 02 2018 at 21:37):

that's just interface

#### Kenny Lau (Nov 02 2018 at 21:37):

anyone can write an interface

#### Reid Barton (Nov 02 2018 at 21:38):

anyone can define Cat, too

#### Reid Barton (Nov 02 2018 at 21:38):

Finding a good interface is the important thing

#### Chris Hughes (Nov 02 2018 at 21:38):

Interfaces are hard.

#### Kenny Lau (Nov 02 2018 at 21:40):

I think opposite can have a better interface

#### Kenny Lau (Nov 02 2018 at 22:36):

@Scott Morrison how should we define an additive category?

#### Scott Morrison (Nov 02 2018 at 22:36):

ugh, yeah, defining enriched categories may take a lot of work to do in general. :-(

#### Scott Morrison (Nov 02 2018 at 22:37):

If you _just_ want additive categories (which is very reasonable, later we can retrofit them as special cases of enriched categories)

#### Scott Morrison (Nov 02 2018 at 22:38):

then I don't think it's too bad

ok, then how?

#### Scott Morrison (Nov 02 2018 at 22:38):

Just have a new typeclass [additive_category C], with fields hom_abelian : add_comm_group (X \hom Y) and comp_bilinear : ...

#### Scott Morrison (Nov 02 2018 at 22:39):

and then some defs that create instances from these fields

#### Kenny Lau (Nov 02 2018 at 22:39):

can we instead declare it as a functor from the Hom category to the Ab category

#### Kenny Lau (Nov 02 2018 at 22:40):

such that some triangle commutes

#### Kenny Lau (Nov 02 2018 at 22:40):

I guess Hom isn't a category

#### Scott Morrison (Nov 02 2018 at 22:40):

yeah, I'm not sure what you mean

#### Kenny Lau (Nov 02 2018 at 22:41):

there must be a way to do this category-theoretically...

#### Scott Morrison (Nov 02 2018 at 22:41):

Well... I think often it's better to have the definitions "explicit" and then have lemmas saying "you can interpret this in categorical terms"

sure

#### Scott Morrison (Nov 02 2018 at 22:41):

In particular, for monoidal categories (or 2-categories), which I really want to get back to,

#### Scott Morrison (Nov 02 2018 at 22:42):

it turns out to be a really bad idea to say that a monoidal category is a category equipped with a functor (C x C) \func C, such that ...

#### Kenny Lau (Nov 02 2018 at 22:42):

why isn't Lean ready for a category theory library?

#### Scott Morrison (Nov 02 2018 at 22:42):

and instead you should do everything grossly: a function tensorObjects, a function tensorMorphisms, and then have a lemma saying these form that functor

#### Scott Morrison (Nov 02 2018 at 22:43):

This sounds like a really bad idea, but the way lean's notation system and elaborator work, you run into endless misery making the functor the "primary" description of the tensor product.

#### Scott Morrison (Nov 02 2018 at 22:43):

It's very unfortunate. :-(

#### Scott Morrison (Nov 02 2018 at 22:45):

why isn't Lean ready for a category theory library?

Speaking to mathematicians, Lean, like every other ITP system, is not ready to do mathematics in. :-)

Lean is terrible, just less terrible than all the others!

#### Reid Barton (Nov 02 2018 at 23:17):

I don't know whether this would be easier or harder, but you don't actually need monoidal categories to do enriched categories; you could enrich in a multicategory instead

#### Kevin Buzzard (Nov 02 2018 at 23:23):

I've found it quite good fun doing abstract maths in Lean. I've not used categories though. But stuff like commutative algebra seems to come out nicely.

#### Kenny Lau (Nov 02 2018 at 23:24):

right, until the module thing came along

#### Chris Hughes (Nov 02 2018 at 23:27):

Lean is often good at abstract stuff. I think maybe abstract usually means it has to be done on paper more formally, because there's less real world intuition.

#### Scott Morrison (Nov 03 2018 at 07:16):

But stuff like commutative algebra seems to come out nicely.

Stockholm syndrome. :-)

#### Reid Barton (Nov 05 2018 at 00:44):

Scott, are you attached to the name category_theory.embedding?
How about fully_faithful?

#### Reid Barton (Nov 05 2018 at 00:47):

embedding is ambiguous, I feel. Someone may think it implies "injective on objects" for example. The nlab gives a variety of definitions.

#### Reid Barton (Nov 05 2018 at 00:48):

(Also it collides with the top-level embedding of topological spaces, which is not category_theory's fault but it did cause some extremely confusing behavior during one of my lean-homotopy-theory mathlib version bumps.)

#### Scott Morrison (Nov 05 2018 at 02:00):

Yes, we should definitely change this.

#### Johan Commelin (Nov 05 2018 at 18:52):

@Scott Morrison Do you have any idea why this would fail?

failed to synthesize type class instance for
X : Type u₁,
𝒳 : category X,
U : X,
f : covering_family U,
p : f.index × f.index
⊢ category (Xᵒᵖ ⥤ Type v₁)


#### Scott Morrison (Nov 05 2018 at 18:54):

either you're missing the import, or something is weird with universe levels?

#### Johan Commelin (Nov 05 2018 at 18:55):

I have

def presheaf := Xᵒᵖ ⥤ C

variables {X} {C}

instance : category (presheaf X C) := by unfold presheaf; apply_instance


in the same file.

#### Scott Morrison (Nov 05 2018 at 18:57):

Turn on pp.universes?

#### Johan Commelin (Nov 05 2018 at 18:57):

I'll try that. I also see

[class_instances] (0) ?x_0 : category (Xᵒᵖ ⥤ Type v₁) := @functor.category ?x_40 ?x_41 ?x_42 ?x_43
failed is_def_eq


in the trace.

#### Johan Commelin (Nov 05 2018 at 19:00):

Ok, that gave me

failed to synthesize type class instance for
X : Type u₁,
𝒳 : category.{u₁ v₁} X,
U : X,
f : covering_family.{u₁ v₁} U,
p : f.index × f.index
⊢ category.{(max u₁ (v₁+1)) v₁} (Xᵒᵖ ⥤ Type v₁)


#### Johan Commelin (Nov 05 2018 at 19:00):

Maybe I don't understand universes well enough...

#### Johan Commelin (Nov 05 2018 at 19:00):

Should that last v_1 be a v_1 + 1?

#### Reid Barton (Nov 05 2018 at 19:02):

I think it should be max u_1 v_1, if I calculated right

#### Reid Barton (Nov 05 2018 at 19:03):

Ah, Scott was kind enough to write out the universe parameters in instance functor.category.

#### Reid Barton (Nov 05 2018 at 19:03):

My guess: perhaps you are doing something where you actually need X to be a small category?

#### Reid Barton (Nov 05 2018 at 19:04):

it's hard to say what to do without knowing where that goal is coming from

#### Johan Commelin (Nov 05 2018 at 19:04):

But in yoneda Scott is doing the same thing as I'm doing. Now I'm really confused.

variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C]
include 𝒞

def yoneda : C ⥤ ((Cᵒᵖ) ⥤ (Type v₁)) :=


#### Reid Barton (Nov 05 2018 at 19:05):

Sure you can write down X\op \func Type v_1, but it might not have v_1-small hom sets.

#### Mario Carneiro (Nov 05 2018 at 19:07):

how big are the homsets of the functor category?

#### Scott Morrison (Nov 05 2018 at 19:08):

variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₂) [𝒟 : category.{u₂ v₂} D]
include 𝒞 𝒟

instance functor.category :
category.{(max u₁ v₁ u₂ v₂) (max u₁ v₂)} (C ⥤ D) :=


#### Scott Morrison (Nov 05 2018 at 19:08):

I wrote the universe levels explicitly in the definition, as documentation for just these moments. :-)

#### Johan Commelin (Nov 05 2018 at 19:09):

Thanks! I'm probably dense, but I'm still confused why Scott could write what he wrote for yoneda, and now I want to apply it and Lean complains...

#### Scott Morrison (Nov 05 2018 at 19:10):

The danger is always the u1 appearing the morphism universe level.

#### Reid Barton (Nov 05 2018 at 19:10):

Apply what how? What is the actual math?

#### Scott Morrison (Nov 05 2018 at 19:10):

So in Yoneda, we don't care about the universe level of the morphisms in the resulting category.

#### Scott Morrison (Nov 05 2018 at 19:10):

But you _do_ care.

#### Scott Morrison (Nov 05 2018 at 19:11):

You need a category category.{(max u₁ (v₁+1)) v₁} (Xᵒᵖ ⥤ Type v₁)

#### Johan Commelin (Nov 05 2018 at 19:11):

Ooops... I crashed the machine I was logged into...

#### Johan Commelin (Nov 05 2018 at 19:11):

I was working on the sheaf branch.

#### Johan Commelin (Nov 05 2018 at 19:12):

https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheaf.lean#L41

#### Scott Morrison (Nov 05 2018 at 19:13):

But with category.{u1 v1} X, you're going to find Xop \func Type v1 only has a category structure with

#### Scott Morrison (Nov 05 2018 at 19:13):

objects in universe max u1 (v1+1) (which is fine)

#### Scott Morrison (Nov 05 2018 at 19:13):

and morphisms in universe max u1 v1

#### Johan Commelin (Nov 05 2018 at 19:14):

I see. So now I should convince Lean that it should be looking for a more relaxed constraint...

#### Johan Commelin (Nov 05 2018 at 19:16):

First need to build mathlib on a new machine. (What is the emoji for compiling?)

#### Johan Commelin (Nov 05 2018 at 19:19):

I propose :fencing: for compiling because of https://www.xkcd.com/303/

#### Reid Barton (Nov 05 2018 at 19:24):

I guess this is one of the points where one uses universes in a more serious way

#### Mario Carneiro (Nov 05 2018 at 19:26):

is this what representable functors are for?

#### Reid Barton (Nov 05 2018 at 19:27):

In math one could just pass to a universe in which X is a small category

#### Kevin Buzzard (Nov 05 2018 at 19:27):

is this what representable functors are for?

They're used in the Fermat's Last Theorem proof to produce rings out of thin air.

#### Reid Barton (Nov 05 2018 at 19:31):

• Assume X is a small_category.{v_1}
• Have sieve take values in presheaves valued in Type (max u_1 v_1)
• Redesign limits so that you can talk about the limit of a w-sized diagram in a category.{u v} (but I don't think this sounds like a good idea)

#### Reid Barton (Nov 05 2018 at 19:33):

The first two are both versions of the math "just pick a universe in which X looks small", and it's a matter of where you want to put that shift of universe

#### Kevin Buzzard (Nov 05 2018 at 19:33):

The fpqc topology has some issues with large limits. @Johan Commelin are you planning on writing something sufficently general to deal with the fpqc topology?

Yes.

#### Johan Commelin (Nov 05 2018 at 19:33):

I want to do sheaves in the biggest generality possible.

#### Kevin Buzzard (Nov 05 2018 at 19:33):

Conrad would argue that the fpqc topology "does not exist"

#### Johan Commelin (Nov 05 2018 at 19:34):

I think I'll go for option 2.

#### Reid Barton (Nov 05 2018 at 19:34):

Are they actual issues or just issues for people who don't believe in universes?

#### Kevin Buzzard (Nov 05 2018 at 19:34):

I don't fully understand the issues

#### Johan Commelin (Nov 05 2018 at 19:35):

I think a little bit of both. You need to do resizing at some point. Like we were discussing kappa-small stuff a while ago.

#### Reid Barton (Nov 05 2018 at 19:35):

I think if you express any topology other than the Zariski one naturally in Lean it will have the same issues as the fpqc topology--otherwise you will need to manually replace your category with an essentially equivalent small one

#### Kevin Buzzard (Nov 05 2018 at 19:35):

I do understand that the issue with an fpqc cover is that you can't make a set of all fpqc covers

#### Kevin Buzzard (Nov 05 2018 at 19:35):

I'm not sure this is accurate Reid

#### Kevin Buzzard (Nov 05 2018 at 19:36):

With the etale topology there is in some formal sense not a set of etale covers

#### Kevin Buzzard (Nov 05 2018 at 19:36):

but there is a set of etale covers such that every etale cover is isomorphic to a cover in your set

#### Kevin Buzzard (Nov 05 2018 at 19:36):

with fpqc the problem is genuinely worse

#### Kevin Buzzard (Nov 05 2018 at 19:36):

because an arbitrary morphism of fields is fpqc

#### Kevin Buzzard (Nov 05 2018 at 19:37):

so there is not even a set of isomorphism classes of etale covers of spec(field)

#### Kevin Buzzard (Nov 05 2018 at 19:37):

I don't know whether thinking about things in a more universey way makes these two problems become the same

#### Kevin Buzzard (Nov 05 2018 at 19:38):

but in ZFC I've always had the impression that they were not the same

#### Reid Barton (Nov 05 2018 at 19:38):

Right, that is what I mean--you would not be able to define etale covers as just "a scheme with an etale map to X", because that will live in a too large universe--you need to manually replace the category with an equivalent small one with some kind of cardinality argument

right

#### Kevin Buzzard (Nov 05 2018 at 19:38):

but you can't do that for fpqc

right

#### Reid Barton (Nov 05 2018 at 19:39):

so there are two kinds of issues which could arise then

#### Reid Barton (Nov 05 2018 at 19:40):

one is if you don't accept the universe axiom, then you can't talk about such large collections like the category of sheaves for the fpqc topology on X at all

#### Kevin Buzzard (Nov 05 2018 at 19:40):

I believe Conrad is strictly ZFC so rejects the fpqc topology

#### Reid Barton (Nov 05 2018 at 19:40):

but that's not an issue if you do accept universes

#### Scott Morrison (Nov 05 2018 at 19:41):

@Johan Commelin I pushed my (inconclusive) changes to the sheaf branch. Now my dog insists on a walk (in the rain).

#### Reid Barton (Nov 05 2018 at 19:41):

but then a second issue which might come up is: you need to take a limit of sets or something, but because the indexing diagram of the limit is large it could take you outside the category you called Set. And that is a real issue even if you believe in universes

#### Johan Commelin (Nov 05 2018 at 19:46):

@Scott Morrison Thanks! I'll take a look!

#### Kevin Buzzard (Nov 05 2018 at 19:49):

Looking through old emails I've exchanged with Conrad on the fpqc matter, he basically says "fppf is enough for everything, and anyone who wants to work with fpqc -- well, that's their problem, and they can work out the details for themselves"

#### Reid Barton (Nov 05 2018 at 19:54):

Another possible approach is https://ncatlab.org/nlab/show/small+presheaf

#### Reid Barton (Nov 05 2018 at 19:57):

I think you can also think of this as like Ind, but with no restriction on the indexing diagrams you allow

#### Reid Barton (Nov 05 2018 at 19:58):

However I don't know whether this is useful for applications in algebraic geometry

#### Reid Barton (Nov 05 2018 at 19:58):

https://ncatlab.org/nlab/show/large+site is a not particularly encouraging page

#### Johan Commelin (Nov 05 2018 at 20:09):

@Reid Barton Hmmzz, I'm not really making any progress...

#### Reid Barton (Nov 05 2018 at 20:09):

I expect you will have other problems, too :slight_smile:

#### Johan Commelin (Nov 05 2018 at 20:09):

/me is not designed to think about universe issues...

#### Johan Commelin (Nov 05 2018 at 20:10):

What do you think is the best solution for now? Making X small?

#### Reid Barton (Nov 05 2018 at 20:11):

certainly easiest for the time being

#### Reid Barton (Nov 05 2018 at 20:11):

and you don't really lose any generality

#### Johan Commelin (Nov 05 2018 at 20:11):

Ok, then I'll leave the headaches for the sheaves refactor that Mario will work on next summer (-;

#### Reid Barton (Nov 05 2018 at 20:12):

I think your next problem was going to be: you have some coproducts indexed on a Type v_1, but now the morphism size is max u_1 v_1

#### Reid Barton (Nov 05 2018 at 20:12):

so you would need to add some ulift to align them

#### Johan Commelin (Nov 05 2018 at 20:17):

You're completely right.

#### Johan Commelin (Nov 05 2018 at 20:18):

So I want my indexing type to be small small

#### Johan Commelin (Nov 05 2018 at 20:18):

In which universe should the indexing type of a covering family live?

#### Johan Commelin (Nov 05 2018 at 20:19):

max u_1 v_1?

#### Reid Barton (Nov 05 2018 at 20:19):

I thought you were going to make X small instead

so u_1 = v_1

#### Reid Barton (Nov 05 2018 at 20:19):

if not, then I'm not sure

#### Johan Commelin (Nov 05 2018 at 20:22):

Yes, I am going to do that. So then I should just take u_1, right?

#### Reid Barton (Nov 05 2018 at 20:24):

Whatever the universe level of X is. It seems we tend to call it v in category_theory

#### Reid Barton (Nov 05 2018 at 20:28):

Well, or u

#### Johan Commelin (Nov 05 2018 at 21:01):

@Scott Morrison Wouldn't it be useful to have has_pullbacks_of_has_limits be an instance in general?

#### Scott Morrison (Nov 05 2018 at 21:02):

I'm afraid of doing that before we know that the pullbacks thus produced are "nice enough".

Ok, I see.

#### Scott Morrison (Nov 05 2018 at 21:02):

I suspect that you'll only want that instance "in desperation", when you don't have access to a construction of pullbacks that is defeq to something easier to work with than the general limit.

Hmmm, ok

#### Johan Commelin (Nov 05 2018 at 21:03):

So now I've made two small edits to sheaf.

#### Johan Commelin (Nov 05 2018 at 21:04):

Do you have a minute to look at the errors that remain? I'm very bad at fighting these universe issues.

#### Scott Morrison (Nov 05 2018 at 21:08):

hah, we've been duplicating effort :-)

#### Johan Commelin (Nov 05 2018 at 21:11):

Well, I didn't do much...

#### Johan Commelin (Nov 05 2018 at 21:13):

Do you think the library is ready for this? Or am I making too big a jump?

#### Scott Morrison (Nov 05 2018 at 21:14):

We're almost there. :-)

#### Scott Morrison (Nov 05 2018 at 21:14):

And this is exactly the sort of stress testing of limits that we need.

#### Scott Morrison (Nov 05 2018 at 21:14):

I committed a little, but it's still badly broken, and I have to get the kids to school/me to work.

#### Johan Commelin (Nov 05 2018 at 21:14):

Sure, those are more important than silly sheaves (-;

See you later

#### Kevin Buzzard (Nov 05 2018 at 21:19):

I've just been reading SGA4 in the bath

As you do

#### Kevin Buzzard (Nov 05 2018 at 21:20):

And very early on when talking about limits and colimits

#### Kevin Buzzard (Nov 05 2018 at 21:20):

They assume that the diagram is u-small

#### Kevin Buzzard (Nov 05 2018 at 21:21):

ie isomorphic to an element of the universe u

#### Kevin Buzzard (Nov 05 2018 at 21:21):

Their categories are u-categories

#### Kevin Buzzard (Nov 05 2018 at 21:21):

Ie hom sets are all in u

#### Kevin Buzzard (Nov 05 2018 at 21:22):

But the limits are over u-small diagrams consistently

#### Kevin Buzzard (Nov 05 2018 at 21:28):

Example theorem : the category of u-abelian groups has u-limits. This means that you take the category whose objects are abelian groups in some universe, and then take a limit but only over a category which is itself an element of u

#### Reid Barton (Nov 05 2018 at 21:31):

That's essentially our setup too, see https://github.com/leanprover-community/mathlib/blob/limits-others-new/category_theory/limits/limits.lean#L21-L22

#### Johan Commelin (Nov 05 2018 at 21:39):

@Scott Morrison In things like coequalizer.desc should the argument w get an auto_param obviously?

#### Scott Morrison (Nov 05 2018 at 21:45):

Yes, that seems plausible.

#### Johan Commelin (Nov 05 2018 at 21:50):

@Scott Morrison I just pushed some more silly stuff. Didn't make fundamental progress.

#### Johan Commelin (Nov 06 2018 at 07:37):

@Scott Morrison I don't think functor.const should be in cones. It is more fundamental. Should this be moved to functor or something?

Sounds good.

#### Reid Barton (Nov 10 2018 at 17:08):

@Johan Commelin did you ever find a setup for typing the functor arrow in emacs?

#### Johan Commelin (Nov 10 2018 at 18:04):

Nah, haven't looked into it yet. Sorry. Maybe some other emacs user can tell us how to fix this. @Sebastian Ullrich ?

#### Gabriel Ebner (Nov 10 2018 at 18:21):

The input abbreviations for emacs are defined here: https://github.com/leanprover/lean-mode/blob/9d6b8471e2044310b4cd7cd3213b1fc8f78ec499/lean-input.el#L407 It should be straightforward to submit a PR adding the new arrows (you might also want to add Scott's calligraphic symbols).

#### Gabriel Ebner (Nov 10 2018 at 18:25):

These are the relevant changes in the vscode extension:
\McB, etc. https://github.com/leanprover/vscode-lean/commit/46ef6b277f4b90ef440730e3b2f73f9381aa08b0#diff-7c2385f0b8db521fe81e3d20489e5f12
\bbA, etc. https://github.com/leanprover/vscode-lean/commit/0080ed0f7c80b199abf31212a7eb9356d3cbc896#diff-7c2385f0b8db521fe81e3d20489e5f12
\functor https://github.com/leanprover/vscode-lean/commit/d3988d9fae1ab4a7e4785486a08c5eddcd33c575#diff-7c2385f0b8db521fe81e3d20489e5f12

#### Gabriel Ebner (Nov 10 2018 at 18:25):

In the long term, we might want to have a common source for these abbreviations that is shared by the editor extensions.

#### Johan Commelin (Nov 10 2018 at 18:25):

@Gabriel Ebner Thanks a lot for the links! Once I find some time, I hope to add a PR.

#### Johan Commelin (Nov 15 2018 at 13:04):

Do we know that composition of functors is associative? I can't find it...

#### Reid Barton (Nov 15 2018 at 13:07):

I don't think so, but it is true by defeq at least

#### Johan Commelin (Nov 15 2018 at 13:11):

I see. So I guess this should be added sooner rather than later.

#### Scott Morrison (Nov 15 2018 at 19:56):

It's in lean-category-theory, under functor_categories/isomorphisms.lean.

#### Scott Morrison (Nov 15 2018 at 19:56):

At least -- it constructs the equality as a natural isomorphism.

#### Scott Morrison (Nov 15 2018 at 19:56):

I thought it would be good to also prove the the unitors and associator for functors satisfy the triangles and pentagon equations, but didn't do that.

#### Scott Morrison (Nov 15 2018 at 20:45):

@Johan Commelin, it turned out this was easy to do, so there's a new PR adding unitors and associators for functors, as well as checking the pentagon and triangle. (These will be necessary one day when we want an example of a 2-category!)

#### Johan Commelin (Nov 16 2018 at 05:35):

@Scott Morrison @Reid Barton I have a question about yoneda. I find the yoneda.lean file a bit confusing. Is there an easy way to extract that F.obj U is canonically the same as yoneda.obj ⟹ F, where U : X and F : presheaf X? Or is this something that we have to add to this file?

#### Reid Barton (Nov 16 2018 at 05:42):

In the adjunctions branch I just sort of ignored most of the contents of yoneda.lean and added an equiv which I could actually understand

#### Reid Barton (Nov 16 2018 at 05:42):

though I feel this approach isn't ideal either

#### Johan Commelin (Nov 16 2018 at 08:09):

@Scott Morrison I don't think this is in your Yoneda file in an equivalent form, is it?

@[simp] lemma yoneda_sections (U : X) (F : presheaf X) :
(yoneda.obj U ⟹ F) ≅ F.obj U :=
{ hom := show (yoneda.obj U ⟹ F) → (F.obj U), from λ α, α.app U (𝟙 U),
inv := show F.obj U → yoneda.obj U ⟹ F, from λ s,
{ app := λ V, show _ → F.obj V, from λ i, F.map i s,
naturality' := λ V₁ V₂ i, by tidy; erw F.map_comp; tidy },
hom_inv_id' :=
begin
ext α V i,
tidy {trace_result := tt},
have := congr (α.naturality i),
dsimp at this,
erw ←(this rfl),
simp
end,
inv_hom_id' := by tidy; erw F.map_id; tidy }


That hom_inv_id' is particularly nasty. Would tidy + rewrite_search be able to deal with that?

#### Scott Morrison (Nov 16 2018 at 08:16):

No, we've already got this. This iso is just a component of the natural isomorphism produced in yoneda_lemma.

#### Scott Morrison (Nov 16 2018 at 08:16):

@[simp] lemma yoneda_sections (X : C) (F : Cᵒᵖ ⥤ Type v₁) : (yoneda.obj X ⟹ F) ≅ ulift.{u₁} (F.obj X) :=
nat_iso.app (yoneda_lemma C) (X, F)


should do it.

#### Scott Morrison (Nov 16 2018 at 08:17):

If you're already working in a small category you can remove the ulift.

#### Scott Morrison (Nov 16 2018 at 08:18):

yoneda_lemma is the natural isomorphism between the two functors starting with (X, F). You can either embed X into presheafs, via the yoneda embedding, and then take hom, or you can just evaluate F on X.

#### Scott Morrison (Nov 16 2018 at 08:25):

And

omit 𝒞
def ulift_trivial (V : Type u₁) : ulift.{u₁} V ≅ V := by tidy

@[simp] def yoneda_sections_small {C : Type u₁} [small_category C] (X : C) (F : Cᵒᵖ ⥤ Type u₁) : (yoneda.obj X ⟹ F) ≅ F.obj X :=
nat_iso.app (yoneda_lemma C) (X, F) ≪≫ ulift_trivial _


gives you the version you want, for small categories.

#### Scott Morrison (Nov 16 2018 at 08:25):

Shall I just push this as a separate PR?

#### Scott Morrison (Nov 16 2018 at 08:26):

Sorry, it was an obvious omission in writing yoneda.lean, just writing out the main result in components.

#### Scott Morrison (Nov 16 2018 at 08:53):

This is available at https://github.com/leanprover/mathlib/pull/480.

#### Scott Morrison (Nov 16 2018 at 08:53):

It depends on the limits PR, because it's not worth backporting, but you're welcome to merge into the sheaf branch.

#### Johan Commelin (Nov 16 2018 at 16:18):

@Scott Morrison Ok cool! I kept on struggling with that product category. But this looks really nice!

#### Johan Commelin (Nov 17 2018 at 07:46):

@Scott Morrison Is iso_of_is_iso missing in the library?

#### Scott Morrison (Nov 17 2018 at 07:46):

Yes, lots of iso stuff is missing, that I've just been discovering now. :-)

#### Scott Morrison (Nov 17 2018 at 07:46):

I've been filling it in the monoidal categories repository, which is where I need it immediately.

#### Scott Morrison (Nov 17 2018 at 07:47):

Is it holding you up? I can make yet another PR to mathlib with some improvements to the iso and is_iso interface.

#### Johan Commelin (Nov 17 2018 at 07:49):

def iso_of_is_iso {X Y : C} {f : X ⟶ Y} (h : is_iso f) : X ≅ Y :=
{ hom := f,
..h}


That's whay I have at the top of my file now.

#### Scott Morrison (Nov 17 2018 at 07:50):

Ok, if that's keeping you afloat for now, I'll finish up a few things before making a "fixing isos" PR. It turns out there are at least a dozen other things missing too. :-)

#### Scott Morrison (Nov 17 2018 at 07:51):

As I'm sure Mario has told us many times before, you actually have to use this stuff!

#### Johan Commelin (Nov 17 2018 at 08:29):

@Scott Morrison I just pushed a whole bunch of stuff to the sheaf branch. If you want more data points for how stuff is used...

#### Johan Commelin (Nov 17 2018 at 08:29):

I'm gathering stuff that should move elsewhere at the top of the file. If it fits into PRs that you are preparing, please take it.

#### David Michael Roberts (Nov 20 2018 at 23:42):

I do understand that the issue with an fpqc cover is that you can't make a set of all fpqc covers

The issue is that there is not even a set of fpqc covers whose elements refine all possible fpqc covers, whereas for fppf and coarser this is true, even when there's not a set of isomorphism classes of covers. This is a genuine problem, and there is a model of ZF whose category of sets forms a large site with this 'feature' (with covers=surjective functions).

#### David Michael Roberts (Nov 20 2018 at 23:44):

One can of course consider whether a given presheaf is a fpqc sheaf or not, but forget trying to fpcq-sheafify in general. The hypotheses of the general adjoint functor theorem are not satisfied, so one cannot construct the left adjoint to Sh_fpqc(Aff) --> PreSh(Aff).

#### Johan Commelin (Nov 27 2018 at 14:10):

I currently have

@[simp] lemma map_left_id : map_left R (nat_trans.id L) ≅ functor.id _ :=
{ hom :=
{ app := λ X, { left := 𝟙 _, right := 𝟙 _ } },
inv :=
{ app := λ X, { left := 𝟙 _, right := 𝟙 _ } } }


but that is a worthless simp-lemma because of ≅. I think that in fact equality should hold:

@[simp] lemma map_left_id' : map_left R (nat_trans.id L) = functor.id _ := sorry


But I have no idea how to prove that two terms of a structure are equal. Is it true that they are equal if all their fields are equal? Is this somewhere in mathlib?

#### Reid Barton (Nov 27 2018 at 14:13):

This is generally what extensionality lemmas do... but you're probably going to have a bad time working with equality of functors

#### Reid Barton (Nov 27 2018 at 14:14):

what's map_left?

#### Reid Barton (Nov 27 2018 at 14:15):

Never mind, I figured it out from one of your other messages

#### Patrick Massot (Nov 27 2018 at 14:16):

Not sure it will help, but your question looks like the classic:

structure johan :=
(a : ℕ)
(aone : a = 1)

lemma johan.ext (X Y : johan) (h : X.a = Y.a) : X = Y :=
begin
cases X,
cases Y,
congr ; assumption
end


#### Patrick Massot (Nov 27 2018 at 14:17):

sorry about the silly example, but I wanted a structure including at least one data and one proof field

#### Johan Commelin (Nov 27 2018 at 14:19):

@Patrick Massot Thanks, I should have thought about cases.

#### Reid Barton (Nov 27 2018 at 14:19):

I think what you have now is the best way

#### Johan Commelin (Nov 27 2018 at 14:19):

@Reid Barton Well, but working with natural isomorphisms is also a massive pain atm.

#### Reid Barton (Nov 27 2018 at 14:21):

I guarantee it is not as bad as rewriting morphisms across equalities of objects and then trying to reason about the result

#### Patrick Massot (Nov 27 2018 at 14:23):

We should really setup a FAQ somewhere

#### Johan Commelin (Nov 27 2018 at 19:48):

@Scott Morrison I have no idea if this makes any sense, but I regularly get errors like these:

type mismatch at application
colimit.pre_map (comma.fst yoneda (functor.of_obj X) ⋙ F) ((comma.map_right_id' yoneda (functor.of_obj X)).hom)
term
(comma.map_right_id' yoneda (functor.of_obj X)).hom
has type
comma.map_right yoneda (𝟙 (functor.of_obj X)) ⟶ functor.id (comma yoneda (functor.of_obj X)) : Type (max
(max ? v)
v
?)
but is expected to have type
?m_3 ⟹ ?m_4 : Type v


Would it help to just get rid of the notation ⟹, and always speak of natural transformations as homs in the functor category?

#### Johan Commelin (Nov 27 2018 at 19:48):

Or is this a stupid universe issue again? (I just realise there are annoying ? in the error...)

#### Johan Commelin (Nov 27 2018 at 19:50):

Ok, never mind. It's a universe issue.

#### Kenny Lau (Nov 27 2018 at 20:20):

@Johan Commelin how do you get that many colours

#### Johan Commelin (Nov 27 2018 at 20:22):

I had less syntax, instead of lean :upside_down: @Kenny Lau

#### Scott Morrison (Nov 27 2018 at 20:40):

I guarantee it is not as bad as rewriting morphisms across equalities of objects and then trying to reason about the result

Yes. This. Please don't prove equalities between functors, you are just setting yourself up for suffering.

#### Reid Barton (Nov 27 2018 at 21:50):

Would it help to just get rid of the notation ⟹, and always speak of natural transformations as homs in the functor category?

I have actually wondered about this too, after a few minor annoyances involving the difference between nat_trans.vcomp and category.comp.

#### Reid Barton (Nov 27 2018 at 21:50):

It's hard to predict which one you will get once you start talking about colimits in categories of presheaves, as Johan has probably also experienced.

#### Reid Barton (Nov 27 2018 at 21:57):

It might be a rather invasive change though, or even not workable for some reason

#### Scott Morrison (Nov 27 2018 at 22:33):

I've experienced the same pain, but haven't tried removing ⟹. It seems a reasonable experiment, however.

#### Johan Commelin (Nov 28 2018 at 08:12):

I don't like the idea of setting myself up for suffering.

#### Johan Commelin (Nov 28 2018 at 08:12):

But I'm suffering hard at the moment.

#### Johan Commelin (Nov 28 2018 at 08:13):

After all functor.id ⋙ F is not defeq to F, and so we need some natural isomorphisms, and I just get the general feeling that we are walking headfirst into nasty 2-categorical territory.

#### Johan Commelin (Nov 28 2018 at 08:14):

Because, say what you like, but Lean isn't very good at working with the canonical natural isomorphism between functor.id ⋙ F and F.

#### Johan Commelin (Nov 28 2018 at 08:15):

I've got the following context:

C : Type v,
𝒞 : small_category C,
D : Type u,
𝒟 : category D,
F : C ⥤ D,
_inst_1 : has_colimits D,
X : presheaf C
⊢ colimit.pre (comma.fst yoneda (functor.of_obj X) ⋙ F) (comma.map_right yoneda (𝟙 (functor.of_obj X))) =
𝟙 (colimit (comma.fst yoneda (functor.of_obj X) ⋙ F))


This might look a bit daunting, but (comma.map_right yoneda (𝟙 (functor.of_obj X))) is naturally isomorphic to functor.id _

#### Johan Commelin (Nov 28 2018 at 08:16):

@Scott Morrison I'm really lost here. The maths is trivial. But Lean is fighting back hard.

#### Scott Morrison (Nov 28 2018 at 08:27):

Want to point me to a file and a commit?

#### Johan Commelin (Nov 28 2018 at 08:31):

Maybe I still don't know how to let the library do the heavy lifting for me...

#### Scott Morrison (Nov 28 2018 at 08:38):

woah, checking out that branch is like stepping into the future. adjunctions, cocompletions, groupoids, oh my.

#### Johan Commelin (Nov 28 2018 at 08:40):

Well, most of that is by Reid.

#### Johan Commelin (Nov 28 2018 at 08:41):

Or I should say: all of that is by Reid.

#### Scott Morrison (Nov 28 2018 at 08:43):

Can we not call functors f, when they could perfectly well be F?

#### Scott Morrison (Nov 28 2018 at 08:44):

Also, I feel you're slightly overusing variables. Things like map and map' should have the variable F : C \func D visible right there at the definition.

#### Scott Morrison (Nov 28 2018 at 08:45):

variables are great for implicit arguments, or even the primary argument if they are the sole primary argument for 20 definitions in a row...

#### Johan Commelin (Nov 28 2018 at 08:45):

Sure. I was using F for presheaves, but I decided that maybe I shouldn't yet do that.

#### Johan Commelin (Nov 28 2018 at 08:47):

Anyway, you shouldn't look too much at the sheaf.lean file. It will need a major rewrite once I have working presheaves.

#### Scott Morrison (Nov 28 2018 at 08:49):

Lots of stuff doesn't compile?

#### Scott Morrison (Nov 28 2018 at 08:49):

In the imports of presheaf.lean

#### Johan Commelin (Nov 28 2018 at 08:50):

Hmmm... I thought those were fine... but maybe stuff broke.

#### Johan Commelin (Nov 28 2018 at 08:51):

limits should work, but maybe it broke after I merged in Reid's branch

#### Scott Morrison (Nov 28 2018 at 08:51):

Ok, I see the thing you probably need, which is naturality in the second argument of colimit.pre

#### Scott Morrison (Nov 28 2018 at 08:51):

I can try to provide you that, and you can try to get stuff to compile :-)

#### Johan Commelin (Nov 28 2018 at 08:53):

Ok, so I have colimit.pre_map

#### Scott Morrison (Nov 28 2018 at 08:53):

yes, but that's naturality in the first argument, which isn't what you need

#### Johan Commelin (Nov 28 2018 at 08:53):

But I guess we need to upgrade pre into a functor?

#### Scott Morrison (Nov 28 2018 at 08:53):

unfortunately I think that might need to wait for 2-categories, I'm not sure. :-)

#### Johan Commelin (Nov 28 2018 at 08:54):

Right... but it is where this stuff is sucking us into, not?

#### Scott Morrison (Nov 28 2018 at 08:54):

I'm actually not sure where I should do this work. The main limits branch is now a bit stranded, as Reid has been pulling stuff out into separate PRs.

#### Scott Morrison (Nov 28 2018 at 08:54):

Doing work on the limits branch now may get orphaned, I'm not sure.

#### Johan Commelin (Nov 28 2018 at 08:54):

Maybe dump it into sheafy_preamble

#### Johan Commelin (Nov 28 2018 at 08:55):

I've been using that file to collect all sorts of facts that I need.

#### Scott Morrison (Nov 28 2018 at 08:56):

Yeah, I'm worried about that getting orphaned too. :-)

#### Scott Morrison (Nov 28 2018 at 08:56):

We're playing a bit fast and loose with our branches at the moment.

Very much.

#### Johan Commelin (Nov 28 2018 at 08:57):

So what exactly is the statement that you are trying to prove?

#### Scott Morrison (Nov 28 2018 at 08:57):

@Reid Barton, I'd really like to straighten out the limits branches a bit. What is the best way to "rebase" (possibly by hand) everything remaining on top of limits-2? Is this a bad thing to want to do?

#### Scott Morrison (Nov 28 2018 at 08:58):

No idea :-) I hadn't even started.

#### Scott Morrison (Nov 28 2018 at 08:59):

Say we have a natural transformation a : E \natt E'.

#### Scott Morrison (Nov 28 2018 at 09:00):

colim.map (a >>> F) gives a map from colim (E >>> F) to colim (E' >>> F)

#### Scott Morrison (Nov 28 2018 at 09:00):

presumably the triangle, obtained by mapping both of those to colim F via colim.pre, commutes?

#### Scott Morrison (Nov 28 2018 at 09:01):

So then if a is invertible, we have colim.pre F E = colim.map (a^{-1} >>> F) >> colim.pre F E' >> colim.map (a >>> F).

#### Scott Morrison (Nov 28 2018 at 09:02):

and hopefully now if E' is the identity, as in your case, everything quickly simplifies from there

#### Johan Commelin (Nov 28 2018 at 09:03):

So pre_map is saying that this triangle commutes.

#### Scott Morrison (Nov 28 2018 at 09:04):

No. pre_map is about changing the functor F, not the functor E.

#### Johan Commelin (Nov 28 2018 at 09:04):

But if E' = functor.id _ it still doesn't simplify, because functor.id _ >>> F is not F. For example colimit.pre F (functor.id _) = \b1 (colimit F) does not typecheck :sad:

#### Scott Morrison (Nov 28 2018 at 09:04):

I've just been looking at the history of the sheaf branch.

#### Johan Commelin (Nov 28 2018 at 09:05):

@Scott Morrison I think you are confusing map_pre and pre_map.

#### Scott Morrison (Nov 28 2018 at 09:05):

And ... you're up shit creek without a paddle. :-)

#### Johan Commelin (Nov 28 2018 at 09:05):

pre_map is something I added. It is in sheafy_preamble.lean

#### Scott Morrison (Nov 28 2018 at 09:05):

Getting sheaf back on top of master after limits-2 is merged is going to suck.

#### Johan Commelin (Nov 28 2018 at 09:06):

@Scott Morrison I will probably just copy-paste stuff into a new branch...

#### Scott Morrison (Nov 28 2018 at 09:06):

I'm looking at

lemma colimit.pre_map {K : Type v} [small_category K] [has_colimits_of_shape K C] (E : K ⥤ J) :
colimit.pre F E ≫ colim.map α = colim.map (whisker_left E α) ≫ colimit.pre G E :=
by ext; rw [←assoc, colimit.ι_pre, colim.ι_map, ←assoc, colim.ι_map, assoc, colimit.ι_pre]; refl


in limits-2.

#### Scott Morrison (Nov 28 2018 at 09:07):

I see. But yes, your pre_map is what we need. :-)

#### Johan Commelin (Nov 28 2018 at 09:07):

Aaahrg... so the names have changed...

#### Johan Commelin (Nov 28 2018 at 09:08):

What is called pre_map in limits-2 used to be map_pre on your old limits branch.

#### Johan Commelin (Nov 28 2018 at 09:08):

Ok, so in presheaf.lean you can see that I already erwd the pre_map-thingy.

#### Scott Morrison (Nov 28 2018 at 09:08):

I see. :-) Reid must have fixed it. :-) As I said, up a creek! :-)

#### Scott Morrison (Nov 28 2018 at 09:08):

Well, I can't see that, because nothing compiles. :-)

#### Scott Morrison (Nov 28 2018 at 09:09):

So, you need to keep the colim.map in there for the unitor.

#### Johan Commelin (Nov 28 2018 at 09:09):

Sorry, I need to run to a seminar...

#### Johan Commelin (Nov 28 2018 at 09:10):

And I'm sorry that stuff doens't compile. I still have some sort of interactive VScode when I work on this...

#### Johan Commelin (Nov 28 2018 at 09:10):

Maybe I should just wait till limits are merged, and then start from scratch.

#### Scott Morrison (Nov 28 2018 at 09:10):

You just want to know that

colimit.pre F (functor.id _) = colimit.map (left_unitor F)


(that's not meant to be real code).

#### Scott Morrison (Nov 28 2018 at 09:12):

Okay, in any case, keep bugging me about this. I'd both like to help, and like to see the resolution. I think it's going to be fine. :-)

#### Johan Commelin (Nov 28 2018 at 11:06):

@Scott Morrison Thanks for all your comments. I'll see if I can make any progress.

#### Reid Barton (Nov 28 2018 at 12:46):

Oh yeah, I noticed all the limit. lemmas had names of the form limit.foo_bar if the left-hand side looked like limit.foo ... >> limit.bar ..., and so I reversed the components of all the names of the corresponding colimit lemmas because they have the composition on the left-hand side in the other order.

#### Reid Barton (Nov 28 2018 at 12:47):

Actually I just copied and pasted the limit lemmas to make colimit versions, I ignored whatever was there before (which I think was not a full set of matching lemmas)

#### Johan Commelin (Nov 28 2018 at 12:51):

@Scott Morrison I fixed a bunch of compile issues, which we due to functor.const being picked from the wrong namespace (even though category_theory seems to be open). I really hope Lean 4 will kick a lot of these things out of the root namespace, because these conflicts are quite annoying.

#### Reid Barton (Nov 28 2018 at 12:52):

Yeah I encountered that same functor.const issue too, not sure what caused it to crop up suddenly

#### Keeley Hoek (Nov 28 2018 at 12:55):

Does @[priority] affect that kind of resolution?

#### Reid Barton (Nov 28 2018 at 13:18):

I can try to produce a rebased version of my adjunctions branch, that shouldn't take too long.

#### Reid Barton (Nov 28 2018 at 13:48):

It looks like Johan has mostly just been working on one file, so probably easiest to just copy the sheaf branch into a new branch indeed

#### Reid Barton (Nov 28 2018 at 13:53):

Oh, also the specific shape limit stuff isn't in limits-2 yet. I do have a copy that at least builds on top of limits-2 though, so I can push that somewhere as a temporary measure for you, Johan

#### Johan Commelin (Nov 28 2018 at 13:55):

I think it's best to fix it after limits-2 is merged.

#### Reid Barton (Nov 28 2018 at 13:59):

Ah, fair enough. I'll hold off on these things then

#### Johan Commelin (Nov 28 2018 at 15:48):

I thought I understood rfl by now. But apparently this is not rfl. If someone can explain this mystery, I would be very grateful.

#### Gabriel Ebner (Nov 28 2018 at 15:51):

map_right_id' should be a def. Theorems don't unfold (except for special circumstances / options).

#### Johan Commelin (Nov 28 2018 at 15:52):

Aaah, it should certainly be a def. Let me try again.

#### Johan Commelin (Nov 28 2018 at 15:53):

@Gabriel Ebner Cool! Now it works.

#### Kevin Buzzard (Nov 28 2018 at 17:12):

Computer scientists have such weird ideas about what a theorem is :-)

#### Johan Commelin (Nov 28 2018 at 17:25):

@Scott Morrison @Reid Barton I suggest we replace of_obj with of.obj after defining

namespace functor
variables {C : Type u} [𝒞 : category.{u v} C]
include 𝒞

def of : C ⥤ (punit ⥤ C) := const punit

namespace of
@[simp] lemma obj_obj (X : C) : (of.obj X).obj = λ _, X := rfl
@[simp] lemma obj_map (X : C) : (of.obj X).map = λ _ _ _, 𝟙 X := rfl
@[simp] lemma map_app {X Y : C} (f : X ⟶ Y) : (of.map f).app = λ _, f := rfl
end of

end functor


Is that ok?

#### Reid Barton (Nov 28 2018 at 17:28):

Yes, that seems sensible

#### Reid Barton (Nov 28 2018 at 22:27):

@Scott Morrison I fixed a bunch of compile issues, which we due to functor.const being picked from the wrong namespace (even though category_theory seems to be open). I really hope Lean 4 will kick a lot of these things out of the root namespace, because these conflicts are quite annoying.

If someone could track this down, it would be super helpful. I'm not sure what changed here.

#### Johan Commelin (Nov 30 2018 at 13:33):

@Reid Barton @Scott Morrison Do you think we need something like this? I find it extremely annoying that Lean refuses some of my morphisms because the come from an opposite category. I understand why Lean complains, but getting it to accept the arrow is extremely annoying. This might help...

namespace category.hom
variables {C : Type u} [𝒞 : category.{u v} C]
include 𝒞

def op {X Y : C} (f : X ⟶ Y) : @category.hom _ category_theory.opposite Y X := f
def deop {X Y : Cᵒᵖ} (f : X ⟶ Y) : @category.hom _ 𝒞 Y X := f

@[simp] lemma op_deop {X Y : C} (f : X ⟶ Y) : f.op.deop = f := rfl
@[simp] lemma deop_op {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.deop.op = f := rfl

end category.hom


#### Scott Morrison (Nov 30 2018 at 23:51):

This sounds fine to me. I agree dealing with opposites is gross. :-(

#### Johan Commelin (Dec 03 2018 at 15:38):

@Reid Barton Have you had similar experiences? What is your opinion on my proposed solution?

#### Scott Morrison (Dec 04 2018 at 09:55):

Hi @Johan Commelin, I am experimenting with making op irreducible, and thus _requiring_ the use of op or deop (and corresponding op_obj and deop_obj on objects).

#### Scott Morrison (Dec 04 2018 at 09:55):

It is slightly grosser, but I think we've all discovered that too much can go mysteriously wrong with the current implementation of opposites.

#### Johan Commelin (Dec 04 2018 at 10:00):

@Scott Morrison Aah, that sounds like a good idea!

#### Johan Commelin (Dec 04 2018 at 10:01):

I hadn't thought about making it irreducible. Those boundaries are useful, but I'm not yet aware of how to make the system help us.

#### Johan Commelin (Dec 04 2018 at 10:01):

So yes, I think it is very good if we have to be explicit about oping and deoping.

#510

#### Johan Commelin (Dec 04 2018 at 11:53):

@Scott Morrison Looks good to me. I do wonder if we can remove the _obj suffix to make things a bit shorter. We could rename the existing op to op_cat.

#### Johan Commelin (Dec 04 2018 at 11:53):

I think this is a good PR, but I regret that a lot of stuff is also becoming somewhat uglier.

#### Kevin Buzzard (Dec 11 2018 at 16:53):

@Ramon Fernandez Mir is making me engage with the category theory stuff! Is there a name for this map: (λ f r, f r : (FF.obj x ⟶ FF.obj y) → (FF.obj x → FF.obj y)) ? I'm changing a long arrow to a short one. The target of the functor FF is the category CommRing, so I want to take an abstract element of the hom set and actually produce the ring hom. There's a coercion that does it magically, but I actually have a set of abstract homs and want a set of concrete homs and I have to feed set.image something.

#### Johan Commelin (Dec 11 2018 at 17:18):

@Kevin Buzzard Could you provide slightly more context? I typically get away without doing anything.

#### Kevin Buzzard (Dec 11 2018 at 17:26):

We had a functor FF from a small category J to CommRing and two objects x and y of J, and we wanted the set of maps from $FF(x)$ to $FF(y)$ coming from J.

#### Johan Commelin (Dec 11 2018 at 17:28):

I see, and FF.obj x \hom FF.obj y is a subtype, but you want a set?

#### Johan Commelin (Dec 11 2018 at 17:28):

Is that correct? If so, I think subtype.val would be the function you are looking for.

#### Johan Commelin (Dec 11 2018 at 17:29):

I don't know by heart how CommRing is defined.

#### Kevin Buzzard (Dec 11 2018 at 17:31):

I'm trying to get from category_theory.category.hom R S to R -> S

#### Kevin Buzzard (Dec 11 2018 at 17:32):

I can just evaluate a term of type category_theory.category.hom R S at r and get s : S

#### Kevin Buzzard (Dec 11 2018 at 17:34):

but I was wondering what the name of the coercion was, because I needed to refer to the map itself when doing something else.

#### Johan Commelin (Dec 11 2018 at 17:55):

@Kevin Buzzard On line 90 of category.lean you can find

{ hom   := λa b, subtype (hom a.2 b.2),


(This is in the instance of concrete_category --> category.) So the map you want is called subtype.val.

#### Reid Barton (Dec 11 2018 at 18:13):

I think there is (or should be?) some more high-level name for this, like forget

#### Johan Commelin (Dec 11 2018 at 18:26):

@Kevin Buzzard That's right. As Reid mentioned, there is a forgetful functor. You will have to

import category_theory.types


#### Reid Barton (Dec 11 2018 at 18:29):

Ah that's where it is

#### Reid Barton (Dec 14 2018 at 05:15):

@Kevin Buzzard did you end up using forget? I'm inclined to make its "C" argument implicit, would that help or hurt you?

#### Kevin Buzzard (Dec 14 2018 at 06:51):

I didn't do anything. I was talking about it with Ramon at our last meeting and haven't thought about it since

#### Kevin Buzzard (Dec 14 2018 at 06:52):

I am completely snowed under with teaching and reference writing

#### Ramon Fernandez Mir (Dec 23 2018 at 19:05):

@Reid Barton sorry I just saw this. I was playing with that code a few days ago and I didn't manage to make it work with forget. What is the "C" argument meant to be?

#### Gun Pinyo (Aug 07 2019 at 21:23):

In https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category.lean,
Could anyone tells me why objects are not a field but a parameter to the definition of category? What is the advantage of it? Also, why the definition of a category is a class rather than an ordinary structure?

#### Kenny Lau (Aug 07 2019 at 21:24):

It allows us to say that the "set" of all groups have a category structure on it

#### Kenny Lau (Aug 07 2019 at 21:24):

so given two groups G and H, Lean can infer what G \hom H means

#### Kenny Lau (Aug 07 2019 at 21:25):

structure instances can't be automatically inferred

#### Gun Pinyo (Aug 07 2019 at 21:30):

Ok, but what if want to say something like "let C be a category" I need to explicitly state its object and become "let C be a category that has objects as blah". I find this quite wired.

I know that this can be solved using Σ obj : Type*, category obj but this is a little bit ad-hoc, does mathlib has a definition for this?

#### Kenny Lau (Aug 07 2019 at 21:31):

Let X be a type that has a category structure C on it

#### Gun Pinyo (Aug 07 2019 at 21:38):

This way of defining a category really see a category as an underlining structure of some type. However, many interesting categories focus more on the morphism whereas object carries almost no information e.g. the category of simplexes in which I believe that it has type as category ℕ.

#### Kenny Lau (Aug 07 2019 at 21:39):

This is an interesting example.

#### Kenny Lau (Aug 07 2019 at 21:40):

I don't know what to do with it.

#### Scott Morrison (Aug 07 2019 at 21:49):

You just do something like def \Delta := \nat, and then instance : category \Delta. This is what type synonyms are for.

#### Scott Morrison (Aug 07 2019 at 21:49):

But yes, my initial starts on the category theory library did use bundled categories.

#### Scott Morrison (Aug 07 2019 at 21:50):

The payoff, which has not yet been realised in mathlib, of using unbundled categories is that it would allow us to use uniform notation \iso, \hom, \otimes etc across all examples.

#### Scott Morrison (Aug 07 2019 at 21:51):

Mostly this hasn't happened because the category theoretic notion of iso between rings, say, would only allow talking about isomorphisms between rings in the same universe.

#### Scott Morrison (Aug 07 2019 at 21:51):

This distinction matters, I think for equiv (rather than just using iso in category Type), where it's pretty common to want to shift universes.

#### Scott Morrison (Aug 07 2019 at 21:52):

On the other hand it's rare that one deals with isomorphisms of rings in different universes.

#### Scott Morrison (Aug 07 2019 at 21:52):

(but it does happen, sure)

#### Scott Morrison (Aug 07 2019 at 21:53):

If I were king, I'd use iso instead of mul_equiv, algebra_equiv, homeomorphism, etc. etc., and even use iso in Type, adding an extra pequiv for talking about equivalences that cross universe levels.

#### Scott Morrison (Aug 07 2019 at 21:54):

@Gun Pinyo, there is src/category_theory/Cat.lean, which defines bundled categories in mathlib, although doesn't do very much with them.

#### Kevin Buzzard (Aug 07 2019 at 22:49):

(but it does happen, sure)

Why do you say this? In maths I never leave Type. This universe polymorphism is just something which the CS people want to make us use and this is one point where it adds to the confusion.

#### Mario Carneiro (Aug 08 2019 at 00:05):

Is Cat a category? If so, you aren't working in Type

#### Mario Carneiro (Aug 08 2019 at 00:07):

Maybe that's not the best example, but Type (u+1) makes several appearances in mathlib

#### Mario Carneiro (Aug 08 2019 at 00:08):

Perhaps you don't think it's important to have ordinals or cardinals or surreals or a model of ZFC

#### Mario Carneiro (Aug 08 2019 at 00:13):

Probably the only one of those you use regularly are cardinals. Of course there are ways to do cardinals in ZFC as well, but the question is not whether it's possible but whether it is easy to work that way. Jeremy told me today that he believes that FLT can probably be proven in primitive recursive arithmetic (PRA), a weak subsystem of Peano arithmetic, but such a proof would obviously look almost unrecognizable compared to Wiles' proof

#### Gun Pinyo (Aug 08 2019 at 00:18):

You just do something like def \Delta := \nat, and then instance : category \Delta. This is what type synonyms are for.

Well, def \Delta := \nat is the abuse of notation, what if I want to define the category of cubes then I should do def \square := \nat then suddenly we have \Delta = \square which shouldn't be true.

#### Gun Pinyo (Aug 08 2019 at 00:26):

@Scott Morrison If the advantage of unbundled categories couldn't be used in practice, should we go back and use bundled one (as the main def) as before?

#### Scott Morrison (Aug 08 2019 at 01:35):

@Gun Pinyo, I don't think you should think of that as abuse of notation. It is used all over mathlib, and is just part of how typeclasses are used in dependent type theory. After building the API for \Delta or for \square, one should then mark \Delta as [irreducible], preventing people from seeing the implementation detail that it is definitionally equal to nat.

#### Scott Morrison (Aug 08 2019 at 01:35):

I don't think that the advantages of unbundled categories can't be used in practice, we're just not there yet. :-)

#### Scott Morrison (Aug 08 2019 at 01:36):

The algebraists are currently busy bundling ring homs and similar gadgets, and this actually makes it easier to use the uniform notions provided by the the category theory library.

#### Scott Morrison (Aug 08 2019 at 01:37):

@Kevin Buzzard

Why do you say this? In maths I never leave Type.

So let's get rid of ring_equiv and friends... :-) If you're happy not being able to change universe levels across a ring_equiv, there's not much advantage over just using the uniform iso.

#### Scott Morrison (Aug 08 2019 at 01:39):

There is the point that in an iso you need to explicitly say that both directions are ring homomorphisms, while the default constructor of ring_equiv only asks that you prove this in one direction, but solving this is just a tiny bit of plumbing. (i.e. we can provide an alternative constructor for isomorphisms of rings, etc)

#### Johan Commelin (Aug 08 2019 at 05:20):

@Gun Pinyo Just for the record, I think that @Johannes Hölzl also developped some stuff with cubes. In particular he had a definition of cubical homology, I think. @Johannes Hölzl do you still have this code somewhere?

#### Kevin Buzzard (Dec 23 2019 at 00:47):

import category_theory.natural_isomorphism category_theory.limits.limits

open category_theory category_theory.limits

universes v u

example (C : Type u) [𝒞 : category.{v} C] [has_limits.{v} C] (J : Type v) [small_category J] (F G : J ⥤ C)
(h : F ≅ G) : limit F ≅ limit G :=
begin
sorry
end


Is that true? [remark: in my application, F and G are equal but not defeq :-/ ]

#### Kenny Lau (Dec 23 2019 at 06:13):

import category_theory.natural_isomorphism category_theory.limits.limits

open category_theory category_theory.limits

universes v u

example (C : Type u) [𝒞 : category.{v} C] [has_limits.{v} C] (J : Type v) [small_category J] (F G : J ⥤ C)
(h : F ≅ G) : limit F ≅ limit G :=
{ hom := limit.lift G ⟨limit F, λ X, limit.π F X ≫ h.1.1 X, λ X Y f, by simp; rw [← limit.w F f, category.assoc, h.1.2 f]; obviously⟩,
inv := limit.lift F ⟨limit G, λ X, limit.π G X ≫ h.2.1 X, λ X Y f, by simp; rw [← limit.w G f, category.assoc, h.2.2 f]; obviously⟩ }


#### Kenny Lau (Dec 23 2019 at 06:13):

surely there's a better proof

#### Johan Commelin (Dec 23 2019 at 10:14):

I think this stuff is already in mathlib

#### Kevin Buzzard (Dec 23 2019 at 10:15):

I couldn't find the one I posted but I can quite believe I missed it. Library_search couldn't find it either

#### Johan Commelin (Dec 23 2019 at 10:15):

It's probably not exactly this, but a slight variant

Last updated: May 18 2021 at 08:14 UTC