category theory

Stream: maths

[Kenny Lau]

https://github.com/kckennylau/category-theory/blob/master/src/adjunction_examples.lean

[Kenny Lau]

@[reducible] def Set.Prod_Hom (B : Type u) : adjunction examples.Set examples.Set :=
adjunction.make _ _
  (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]

so natural

[Kenny Lau]

@[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]

that moment when they're adjoint to each other

[Kenny Lau]

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]

I wonder if this is the left adjoint of some forgetful functor

[Kenny Lau]

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]

What does this even mean? What is a transitive set?

[Kenny Lau]

A set X is transitive if for every x and y such that x∈y∈X, we have x∈X

[Kenny Lau]

if the transitive closure is indeed a left adjoint, then we get right-exactness for free

[Kevin Buzzard]

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]

Are you making an assertion here? What is R(T)?

[Kenny Lau]

the forgetful functor that forgets the fact that T is transitive

[Kevin Buzzard]

Is what you write true?

[Kenny Lau]

I believe so

[Kevin Buzzard]

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]

yes, since here the morphisms are just inclusions, so there is only one morphism per pair of sets

[Kevin Buzzard]

What does Hom_Set mean then?

[Kenny Lau]

oh, inclusion

[Kevin Buzzard]

Do you have a question?

[Kenny Lau]

is my belief right

[Kevin Buzzard]

What does Hom_Trans mean?

[Kenny Lau]

subcategory

[Kevin Buzzard]

I don't know what anything means. It feels like you have made these categories up.

[Kevin Buzzard]

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]

because to hell with the category of sets in Lean

[Kevin Buzzard]

What does Hom_Trans mean?

[Kenny Lau]

the inclusion in the category of transitive sets

[Kevin Buzzard]

So at most one map between two sets?

[Kenny Lau]

yes

[Kevin Buzzard]

" we see that for any transitive set T with S ⊆ T, then L(S) ⊆ T ". Is that your question?

[Kenny Lau]

well that's the UMP of transitive closure

[Kenny Lau]

which should be right

[Kevin Buzzard]

But what is your question if it is not precisely that statement?

[Kenny Lau]

no idea

[Kevin Buzzard]

We might be done then :-)

[Kenny Lau]

interesting

[Reid Barton]

Scott I guess I'll keep you updated on what I'm doing by sending pastebin links for now.

[Reid Barton]

https://pastebin.com/WmdNgPdx is limits and colimits in types (nice and easy) and small and filtered categories (also easy).

[Reid Barton]

Next I plan to try to show that small limits commute with filtered colimits

[Reid Barton]

Probably I won't finish that in the next few days.

[Scott Morrison]

Thanks, Reid, that patch has been applied!

[Reid Barton]

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]

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]

@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]

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]

@Scott Morrison Will you change some of the mathlib files to use category theory?

[Kenny Lau]

what's the plan for category theory?

[Scott Morrison]

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]

will they gradually assimilate into the main mathlib library?

[Scott Morrison]

Eventually such facts should move out to their natural homes, immediately following where the underlying lemmas are actually proved.

[Kenny Lau]

nice

[Scott Morrison]

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]

@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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kenny Lau]

well you forgot the add_comm_group

[Kenny Lau]

and actually that's all I'm concerned about

[Scott Morrison]

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

[Kenny Lau]

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]

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

[Scott Morrison]

I'll make a few more examples.

[Kenny Lau]

thanks

[Kenny Lau]

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

[Johan Commelin]

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]

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]

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

[Kenny Lau]

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

[Kenny Lau]

I've searched all the files

[Mario Carneiro]

the problem is that categories form a 2-category

[Mario Carneiro]

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

[Reid Barton]

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

[Johan Commelin]

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]

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]

"ordinary informal math" = category

[Johan Commelin]

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]

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

[Reid Barton]

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

[Kenny Lau]

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

[Kenny Lau]

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]

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]

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

[Reid Barton]

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

[Kenny Lau]

that's just interface

[Kenny Lau]

anyone can write an interface

[Reid Barton]

anyone can define Cat, too

[Reid Barton]

Finding a good interface is the important thing

[Chris Hughes]

Interfaces are hard.

[Kenny Lau]

I think opposite can have a better interface

[Kenny Lau]

@Scott Morrison how should we define an additive category?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

then I don't think it's too bad

[Kenny Lau]

ok, then how?

[Scott Morrison]

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

[Scott Morrison]

and then some defs that create instances from these fields

[Kenny Lau]

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

[Kenny Lau]

such that some triangle commutes

[Kenny Lau]

I guess Hom isn't a category

[Scott Morrison]

yeah, I'm not sure what you mean

[Kenny Lau]

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

[Scott Morrison]

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

[Kenny Lau]

sure

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

It's very unfortunate. :-(

[Scott Morrison]

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]

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]

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]

right, until the module thing came along

[Chris Hughes]

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]

But stuff like commutative algebra seems to come out nicely.

Stockholm syndrome. :-)

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

(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]

Yes, we should definitely change this.

[Johan Commelin]

@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]

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

[Johan Commelin]

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]

Turn on pp.universes?

[Johan Commelin]

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]

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]

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

[Johan Commelin]

Should that last v_1 be a v_1 + 1?

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Johan Commelin]

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]

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

[Reid Barton]

Which is what your goal is asking for

[Mario Carneiro]

how big are the homsets of the functor category?

[Scott Morrison]

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]

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

[Johan Commelin]

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]

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

[Reid Barton]

Apply what how? What is the actual math?

[Scott Morrison]

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

[Scott Morrison]

But you _do_ care.

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

I was working on the sheaf branch.

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

and morphisms in universe max u1 v1

[Scott Morrison]

which breaks your constraint

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Mario Carneiro]

is this what representable functors are for?

[Reid Barton]

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

[Kevin Buzzard]

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]

I think your options are

• 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]

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]

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?

[Johan Commelin]

Yes.

[Johan Commelin]

I want to do sheaves in the biggest generality possible.

[Kevin Buzzard]

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

[Johan Commelin]

I think I'll go for option 2.

[Reid Barton]

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

[Kevin Buzzard]

I don't fully understand the issues

[Johan Commelin]

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]

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]

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

[Kevin Buzzard]

I'm not sure this is accurate Reid

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

with fpqc the problem is genuinely worse

[Kevin Buzzard]

because an arbitrary morphism of fields is fpqc

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

right

[Kevin Buzzard]

but you can't do that for fpqc

[Reid Barton]

right

[Reid Barton]

so there are two kinds of issues which could arise then

[Reid Barton]

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]

I believe Conrad is strictly ZFC so rejects the fpqc topology

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

certainly easiest for the time being

[Reid Barton]

and you don't really lose any generality

[Johan Commelin]

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

[Reid Barton]

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]

so you would need to add some ulift to align them

[Johan Commelin]

You're completely right.

[Johan Commelin]

So I want my indexing type to be small small

[Johan Commelin]

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

[Johan Commelin]

max u_1 v_1?

[Reid Barton]

I thought you were going to make X small instead

[Reid Barton]

so u_1 = v_1

[Reid Barton]

if not, then I'm not sure

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

Well, or u

[Johan Commelin]

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

[Scott Morrison]

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

[Johan Commelin]

Ok, I see.

[Scott Morrison]

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.

[Johan Commelin]

Hmmm, ok

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

hah, we've been duplicating effort :-)

[Johan Commelin]

Well, I didn't do much...

[Johan Commelin]

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

[Scott Morrison]

We're almost there. :-)

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

See you later

[Kevin Buzzard]

I've just been reading SGA4 in the bath

[Kevin Buzzard]

As you do

[Kevin Buzzard]

And very early on when talking about limits and colimits

[Kevin Buzzard]

They assume that the diagram is u-small

[Kevin Buzzard]

ie isomorphic to an element of the universe u

[Kevin Buzzard]

Their categories are u-categories

[Kevin Buzzard]

Ie hom sets are all in u

[Kevin Buzzard]

But the limits are over u-small diagrams consistently

[Kevin Buzzard]

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]

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]

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

[Scott Morrison]

Yes, that seems plausible.

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

Sounds good.

[Reid Barton]

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

[Johan Commelin]

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

[Gabriel Ebner]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

@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]

@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]

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]

though I feel this approach isn't ideal either

[Johan Commelin]

@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]

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

[Scott Morrison]

@[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)

[Scott Morrison]

should do it.

[Scott Morrison]

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

[Scott Morrison]

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]

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]

Shall I just push this as a separate PR?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

@Scott Morrison Is iso_of_is_iso missing in the library?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

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

[Johan Commelin]

@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]

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]

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]

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]

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]

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

[Reid Barton]

what's map_left?

[Reid Barton]

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

[Patrick Massot]

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]

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

[Johan Commelin]

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

[Reid Barton]

I think what you have now is the best way

[Johan Commelin]

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

[Reid Barton]

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

[Patrick Massot]

We should really setup a FAQ somewhere

[Johan Commelin]

@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]

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

[Johan Commelin]

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

[Kenny Lau]

@Johan Commelin how do you get that many colours

[Johan Commelin]

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

[Scott Morrison]

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]

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]

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]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

But I'm suffering hard at the moment.

[Johan Commelin]

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]

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]

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]

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

[Scott Morrison]

Want to point me to a file and a commit?

[Johan Commelin]

@Scott Morrison https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/presheaf.lean#L69

[Johan Commelin]

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

[Scott Morrison]

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

[Johan Commelin]

Well, most of that is by Reid.

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Johan Commelin]

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]

Lots of stuff doesn't compile?

[Scott Morrison]

In the imports of presheaf.lean

[Johan Commelin]

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

[Scott Morrison]

e.g. limits/limits.lean and adjunctions.lean

[Johan Commelin]

adjunctions probably don't compile

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

Ok, so I have colimit.pre_map

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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]

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

[Johan Commelin]

Maybe dump it into sheafy_preamble

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

Very much.

[Johan Commelin]

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

[Scott Morrison]

@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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Johan Commelin]

So pre_map is saying that this triangle commutes.

[Scott Morrison]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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]

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]

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

[Reid Barton]

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]

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]

@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]

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

[Keeley Hoek]

Does @[priority] affect that kind of resolution?

[Reid Barton]

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

[Reid Barton]

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]

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]

Ooh, don't worry too much about this

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

I'm very confused about https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/commas.lean#L155-L156
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]

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

[Johan Commelin]

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

[Johan Commelin]

@Gabriel Ebner Cool! Now it works.

[Kevin Buzzard]

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

[Johan Commelin]

@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]

Yes, that seems sensible

[Reid Barton]

@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]

@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]

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

[Johan Commelin]

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

[Scott Morrison]

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]

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]

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

[Johan Commelin]

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]

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

[Scott Morrison]

#510

[Johan Commelin]

@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]

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

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

@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]

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

[Johan Commelin]

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

import category_theory.types

[Reid Barton]

Ah that's where it is

[Reid Barton]

@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]

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]

I am completely snowed under with teaching and reference writing

[Ramon Fernandez Mir]

@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]

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]

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

[Kenny Lau]

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

[Kenny Lau]

structure instances can't be automatically inferred

[Gun Pinyo]

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]

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

[Gun Pinyo]

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]

This is an interesting example.

[Kenny Lau]

I don't know what to do with it.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

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

[Scott Morrison]

(but it does happen, sure)

[Scott Morrison]

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]

@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]

(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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

@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]

@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]

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

[Scott Morrison]

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]

@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]

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]

@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]

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]

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]

surely there's a better proof

[Johan Commelin]

I think this stuff is already in mathlib

[Kevin Buzzard]

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]

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