dinatural transformations

Stream: maths

[Scott Morrison]

@fosco, you may want to start here:

import category_theory.products.basic

open opposite

namespace category_theory

variables {C D : Type*} [category C] [category D]

structure dinat_trans (F G : Cᵒᵖ × C ⥤ D) :=
(app := Π X, F.obj (op X, X) ⟶ G.obj (op X, X))
/- ... axioms ... -/

end category_theory

[fosco]

ok, a very basic question.

structure dinat_trans (F G : Cᵒᵖ × C ⥤ D) :=
  (app := Π X, F.obj (op X, X) ⟶ G.obj (op X, X))
  (dinaturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    F.map (op f, 𝟙 X) ≫ app X ≫ G.map (op 𝟙 X, f) = F.map (op 𝟙 Y,f) ≫ app Y ≫ G (op f, 𝟙 Y) . obviously)

this gives me an error,

  prod.mk (op f)
term
  op f
has type
  (X ⟶ Y)ᵒᵖ
but is expected to have type
  ?m_1.fst ⟶ ?m_2.fst

and this is telling me that I'm not building the morphism in C^op x C correctly. What is the correct syntax to refer to the morphism $(f, 1_Y)$ in $C^{op}\times C$?

[fosco]

(PS: it's night time for me in my timezone ;-) I'll get back at it tomorrow)

[Reid Barton]

For a morphism, it should be f.op, I think.

[fosco]

Same error if I change to f.op

[Reid Barton]

Exactly the same?

[Reid Barton]

Well, there is a second op f

[fosco]

type mismatch at application
  prod.mk f.op
term
  f.op
has type
  op Y ⟶ op X
but is expected to have type
  ?m_1.fst ⟶ ?m_2.fst

where is ?m_1 implicitly defined?

[Reid Barton]

Aha I didn't read the whole error message. It is closer now, though!

[fosco]

Same error message, but $\epsilon$ less mistake :grinning:

[Reid Barton]

For these metavariables like ?m_1 (as far as I know) you just have to guess, so here probably it is the implicit source object argument of F.map

[fosco]

is at least (f,g) the right way to define a morphism in a product category? Initially I thought I had to use angle brackets..

[Reid Barton]

That is, I'm not sure if Lean is smart enough here to guess what objects (f.op, 𝟙 X) is meant to be a map between... you can tell it explicitly, but it's a bit inconvenient

[fosco]

how do you tell it explicitly?

[Reid Barton]

Something like (f.op, 𝟙 X) : (op Y, X) ⟶ (op X, X) (if I got it right)

[Reid Barton]

I'm not sure it will help, but it might

[fosco]

And where should I specify this typing?

[fosco]

I thought given the type of f there's a unique way to infer the type of (f.op, 1 X)...

[Reid Barton]

It has a unique type in the sense that its type is known to be prod blah blah but in principle there could be various pairs of objects of Cᵒᵖ × C between which the type of maps is that specific type... which is a bit annoying.

[Reid Barton]

F.map ((f.op, 𝟙 X) : (op Y, X) ⟶ (op X, X))

[Reid Barton]

Based on src#category_theory.bifunctor.diagonal it seems like this is what you're meant to write

[Reid Barton]

Probably there should be something like F.map_prod f g to make this easier.

[Reid Barton]

I see the file I linked above is from 2017 so maybe it already exists... but I looked there because it seemed like the logical place for it

[fosco]

open opposite

namespace category_theory

variables {C D : Type*} [category C] [category D]

structure dinat_trans (F G : Cᵒᵖ × C ⥤ D) :=
  (app : Π X, F.obj (op X, X) ⟶ G.obj (op X, X))
  (dinaturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    F.map ((f.op, 𝟙 X) : (op Y, X) ⟶ (op X, X)) ≫ app X ≫ G.map (((𝟙 X).op, f) : (op X,X) ⟶ (op X,Y)) = F.map (((𝟙 Y).op, f) : (op Y,X) ⟶ (op Y,Y)) ≫ app Y ≫ G.map (f.op, 𝟙 Y) . obviously)

end category_theory

no errors!

[fosco]

:smile: tomorrow, co/wedges!

[Scott Morrison]

Make sure in a ``` block that you start with a new line. Otherwise zulip swallows the first line and tries to interpret it as a language instruction for the code block.

[Scott Morrison]

This is slightly terser:

import category_theory.products.basic

open opposite

namespace category_theory

variables {C D E : Type*} [category C] [category D] [category E]

-- TODO move to category_theory.products.bifunctor, and make use of there
/-- A synonym for `F.map (f, g)`, helpful because Lean struggles to typecheck `(f, g)`. -/
def functor.map_prod (F : C × D ⥤ E) {W X : C} {Y Z : D} (f : W ⟶ X) (g : Y ⟶ Z) :
  F.obj (W, Y) ⟶ F.obj (X, Z) :=
F.map (f, g)

structure dinat_trans (F G : Cᵒᵖ × C ⥤ D) :=
(app : Π X, F.obj (op X, X) ⟶ G.obj (op X, X))
(dinaturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
  F.map_prod f.op (𝟙 _) ≫ app X ≫ G.map_prod (𝟙 _) f =
  F.map_prod (𝟙 _) f ≫ app Y ≫ G.map_prod f.op (𝟙 _) . obviously)

end category_theory

using Reid's map_prod suggestion.

[Scott Morrison]

Note also that by writing (𝟙 _) I can avoid having to write (𝟙 X).op.

[Scott Morrison]

(Note also Lean's style guide says no indenting for structure fields, and no long lines. :-)

[fosco]

def constant_functor (X : D) : C ⥤ D :=
{ obj := λ Y, X,
  map := λ Y Y' f, 𝟙 X, }

def promote_covariant (F : C ⥤ D) : (Cᵒᵖ × C ⥤ D) :=
{ obj := λ Z, F.obj Z.snd,
  map := λ Z W f, F.map f.snd, }

def promote_contravariant (F : Cᵒᵖ ⥤ D) : (Cᵒᵖ × C ⥤ D) :=
{ obj := λ Z, F.obj Z.fst,
  map := λ Z W f, F.map f.fst, }

def wedge (F : Cᵒᵖ × C ⥤ D) (X : D) : dinat_trans (promote_covariant (constant_functor X)) F := sorry

def cowedge (F : Cᵒᵖ × C ⥤ D) (X : D) : dinat_trans F  (promote_covariant (constant_functor X)) := sorry

a few other definitions; I'm not sure wedge and cowedge are definitions though: they are _functions_ eating a functor $F : C^{op}\times C \to D$ and an object of $D$, and giving back the category of dinatural transformations between the two. So, $Dinat(F,G)$ is a type! I'm not sure this is the best design choice.

[Johan Commelin]

I hope that functor.const exists already.

[Johan Commelin]

And promote_covariant should be something like functor.snd ⋙ F

[fosco]

Sure. I am just trying to reinvent the wheel to get a grip on the basic defs
(I should also have a look at cone and cocone...)

[fosco]

Johan Commelin said:

And promote_covariant should be something like functor.snd ⋙ F

unknown identifier 'category_theory.functor.snd'

[Johan Commelin]

Ooh, it's probably just category_theory.snd, sorry. It is category_theory.prod.snd

[Johan Commelin]

docs#category_theory.prod.snd

[Johan Commelin]

Voila :this:

[fosco]

Now I see a complaint for \ggg

type mismatch at application
  functor.comp prod.snd
term
  prod.snd
has type
  Π (C : Type ?) [_inst_1 : category C] (D : Type ?) [_inst_2 : category D], C × D ⥤ D : Type (max
        (?+1)
        (max ? (?+1))
        (?+1)
        (max ? (?+1))
        (max ? ?)
        ?
        ?
        ?)
but is expected to have type
  Cᵒᵖ × C ⥤ ?m_1 : Type (max u_4 ? u_1 ?)

[Johan Commelin]

Aah, prod.snd takes to arguments (namely the factors)

[Johan Commelin]

So prod.snd _ _ ⋙ F should work

[fosco]

perfect

[Johan Commelin]

Sorry, I should have tested my code before commenting

[fosco]

Nah, it's me, I should start from the beginning, be more systematic. Instead I am learning the syntax along the way.

[Johan Commelin]

It's a lot more fun that way. I also jumped straight in (-;

[Scott Morrison]

@fosco, I think your definition of wedge is on the wrong track. You don't want D as a parameter, but rather as a field of the wedge.

[Scott Morrison]

You could write

def wedge (F : Cᵒᵖ × C ⥤ D)  := \Sigma X : D, dinat_trans ... F := sorry

but better would be

structure wedge (F : Cᵒᵖ × C ⥤ D) :=
(X : D)
(\a : dinat_trans ... F)

and then instance (F) : category (wedge F) := ...

[Scott Morrison]

(Probably before the instance you want to enter the wedge namespace and define hom, presumably as another structure.)

[fosco]

I agree; also, promotes are redundant, lean figures out alone that the domain of the constant functor must be $C^{op}\times C$.

[fosco]

What is hom?

In fact, I would like to define the twisted arrow category of $\hom_C$:

• objects : the morphisms of $C$
• morphisms $f \to g$ : the pairs $u : src(g) \to src(f), v : trg(f) \to trg(g)$ such that the obvious square commutes

is this a structure that then I have to prove is a category?

Again, I am discovering the syntax along the way :smile: be patient...

[fosco]

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) := sorry

this seems to work (it only complains for the sorry)

[fosco]

Now I would love to have something similar to agda's ctrl-R to auto-generate the fields I have to fill (hom, id, comp)... wishful thinking?

[Ruben Van de Velde]

Replace the sorry by an underscore, and if you're in vs code, a lightbulb should show up

[Johan Commelin]

Ctrl-. will open the lightbulb menu. Then hit <Up>-<Up>-<Enter> and you will have your skeleton :laughing:

[fosco]

I know very little as you can see! :smile:

[fosco]

structure wedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans (constant_functor tip) F)

structure cowedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans F (constant_functor tip))

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, U.tip ⟶ V.tip,
  id   := λ X, eq_to_hom rfl,
  comp := λ X Y Z f g, f ≫ g, }

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom  := λ U V, U.tip ⟶ V.tip,
  id   := λ X, eq_to_hom rfl,
  comp := λ X Y Z f g, f ≫ g, }

[fosco]

Now for the twisted arrow category...

[fosco]

Hmmm, I am having a hard time again, figuring out how to define it

[fosco]

instance twisted : category (C.hom) :=
  { hom := _,
  id := _,
  comp := _,
  id_comp' := _,
  comp_id' := _,
  assoc' := _ }

I would like to say: if $C$ is a category, there is a category having objects the class of morphisms of $C$, and morphisms the pairs (u,v) as above; I have two problems: first, I can't figure out where to put the information that the class of objects of $Tw(C)$ is $\hom(C)$; second, I want just some pairs of morphisms (u,v): how does one consider just some pairs (u,v), subject to a certain condition?

[Scott Morrison]

Before you go too far: please use the existing functor.const, rather than rolling your own.

[Scott Morrison]

In wedge, I'd suggest for now calling tip instead X. It's not great, but it will be consistent with the terminology for cone and cocone. If you feel strongly about it, we can make a PR to update cone and cocone later. :-)

[Scott Morrison]

I'm confused. Your category instances for wedge and cowedge are wrong. The morphisms aren't just morphisms between the tips, but morphisms satisfying some condition.

[Scott Morrison]

This is why you need to create a structure wedge.hom := ...

[Scott Morrison]

Which will carry the morphism and this condition. See how this is implemented for comma or cone.

[fosco]

Scott Morrison said:

Before you go too far: please use the existing functor.const, rather than rolling your own.

Replacing constant_functor with functor.const doesn't work...

[Scott Morrison]

Let's see: src#functor.const.

[Scott Morrison]

Nope, that's wrong.

[fosco]

Scott Morrison said:

I'm confused. Your category instances for wedge and cowedge are wrong. The morphisms aren't just morphisms between the tips, but morphisms satisfying some condition.

Indeed: because I don't know how to specify a condition that the morphisms have to satisfy. I'll look into cone

[Scott Morrison]

src#category_theory.functor.const

[fosco]

type mismatch at application
  functor.const tip
term
  tip
has type
  D : Type u_2
but is expected to have type
  Type ? : Type (?+1)

[Scott Morrison]

There's functor.const for you. You'll have to import category_theory.const to get it. Note that it is set up to be functorial, so you'll need to see how it is used.

[Scott Morrison]

Read the module doc-string in the link I just gave you to see how to use functor.const.

[Scott Morrison]

(Later you will be happy that functor.const is functorial in the constant. :-)

[Scott Morrison]

(The doc-string for functor.const could be more helpful, I see. At least the module doc-string explains it.)

[fosco]

it seems to me that this should work

structure wedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans (functor.const tip) F)

but it doesn't

[Scott Morrison]

As I've been saying in the message above, functor.const takes more arguments than you are giving it.

[Scott Morrison]

(Because it is set up to be functorial.)

[Scott Morrison]

To see how to set up wedge.hom you should look at src#category_theory.limits.cone_morphism.

[Scott Morrison]

You probably just need (functor.const _).obj tip

[Scott Morrison]

(And if you write open functor higher up in your file you can just write const, rather than functor.const.

[Scott Morrison]

Error messages of the form

type mismatch at application
  functor.const tip
has type
  D : Type u_2
but is expected to have type
  Type ? : Type (?+1)

are super useful, and worth learning how to interpret. It's saying that that first argument of functor.const is not an object of a category, but actually a type.

[Scott Morrison]

It is expecting to be given the name of the "source category" for the constant functor that you want.

[Scott Morrison]

Notice in your earlier constant_functor the source category was an "implicit" argument (i.e. given via curly braces { }). This means you can leave them out, but Lean has to be able to guess the correct value from context. That's not always a good idea, so the mathlib version functor.const has to be told the source category "explicitly".

[fosco]

so, const (domain) (object) ?

[Scott Morrison]

The next difference is that functor.const C doesn't just take an object of D and spit out a functor C \func D. It is actually giving you a functor from C to C \func D.

[Scott Morrison]

Hence we have to write (const domain).obj object to apply it to an object.

[Scott Morrison]

(You could write (const domain).map morphism to apply it to a morphism (obtaining, of course, the identity morphism on your chosen constant.)

[Scott Morrison]

Eventually you need all these functoriality statements (even if automation takes care of plugging them in at the right places), so we tend to package them all up at the beginning, rather than thinking of them as separate constructions.

[fosco]

I'm starting to understand, but I am still confused

1. How can I possibly know how many arguments, and in what order, are needed by const, looking at its type here?

def const : C ⥤ (J ⥤ C) :=
{ obj := λ X,
  { obj := λ j, X,
    map := λ j j' f, 𝟙 X },
  map := λ X Y f, { app := λ j, f } }

2. I understand that this const gives a functor from C to C \func D, which is different from what I defined. Yet, const (Cᵒᵖ × C) tip gives the same type mismatch.

[Scott Morrison]

Note that functors are not functions!

[Scott Morrison]

If F : C ⥤ D, and X : C, you can't just write F X.

[Scott Morrison]

You need to write F.obj X.

[Scott Morrison]

So you need to write (const (Cᵒᵖ × C)).obj tip

[fosco]

Scott Morrison said:

So you need to write (const (Cᵒᵖ × C)).obj tip

Doesn't work! I tried.

[Scott Morrison]

Show me the error message?

[fosco]

invalid field notation, type is not of the form (C ...) where C is a constant
  const (Cᵒᵖ × C)
has type
  Type ? → Type u_1

[Scott Morrison]

Might need to post the #mwe.

[fosco]

structure wedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans ((const (Cᵒᵖ × C)).obj tip) F)

[Scott Morrison]

Are you sure this const is category_theory.functor.const?

[Scott Morrison]

(i.e. if you right-click on it and go-to-definition you land in the right place)

[Scott Morrison]

It's possible you're seeing some other const, because I don't think it should have type Type ? → Type u_1.

[Scott Morrison]

Maybe you can post your whole file?

[Scott Morrison]

Sorry to derail you by suggesting using functor.const instead of your own. In the long run it will pay off but I appreciate it is annoying now. :-)

[fosco]

Now it works, if I write functor.const; for some reason opening functor at the beginning doesn't work

[fosco]

Here's the whole file anyway

import category_theory.products.basic
import category_theory.const

open opposite
open functor

namespace category_theory

variables {C D E : Type*} [category C] [category D] [category E]

def functor.map_prod (F : C × D ⥤ E) {W X : C} {Y Z : D} (f : W ⟶ X) (g : Y ⟶ Z) :
  F.obj (W, Y) ⟶ F.obj (X, Z) :=
F.map (f, g)

structure dinat_trans (F G : Cᵒᵖ × C ⥤ D) :=
(app : Π X, F.obj (op X, X) ⟶ G.obj (op X, X))
(dinaturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
  F.map_prod f.op (𝟙 _) ≫ app X ≫ G.map_prod (𝟙 _) f =
  F.map_prod (𝟙 _) f ≫ app Y ≫ G.map_prod f.op (𝟙 _) . obviously)

namespace wedge

structure wedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans ((functor.const (Cᵒᵖ × C)).obj tip) F)

structure cowedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans F ((functor.const (Cᵒᵖ × C)).obj tip))

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, U.tip ⟶ V.tip,
  id   := λ X, eq_to_hom rfl,
  comp := λ X Y Z f g, f ≫ g, }

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom  := λ U V, U.tip ⟶ V.tip,
  id   := λ X, eq_to_hom rfl,
  comp := λ X Y Z f g, f ≫ g, }

-- instance twisted : category (hom C) :=
--   { hom := _,
--   id := _,
--   comp := _,
--   id_comp' := _,
--   comp_id' := _,
--   assoc' := _ }

end wedge

end category_theory

[Scott Morrison]

Ah --- did you open functor inside or outside the namespace category_theory?

[fosco]

outside

[Scott Morrison]

The problem is that the Haskell programmers put functor in the root namespace, to mean a type level functor like programmers like.

[Scott Morrison]

And the real functor is only in the category_theory namespace.

[Scott Morrison]

So you accidentally picked up the other one.

[fosco]

Scott Morrison said:

The problem is that the Haskell programmers put functor in the root namespace, to mean a type level functor like programmers like.

It's always haskellers' fault :grinning:

[Scott Morrison]

I've been wanting to trying move the programmers' functor into a namespace, as control.functor.

[Scott Morrison]

But never did it.

[Scott Morrison]

Maybe I'll go investigate that again.

[fosco]

yet the same thing happens if I move the open functor inside the category_theory namespace

[Scott Morrison]

In any case, if you move the open inside, or write open category_theory.functor, you should be good.

[fosco]

yes, open category_theory.functor works.

[fosco]

Whew!

[Scott Morrison]

Next up:
get rid of your instance : category (wedge ...), and instead first define structure wedge.hom (...) := ...

[Kevin Buzzard]

By the way one answer to "how do I figure out what inputs are implicit and what are explicit" is "just hover over the function definition and its type will pop up" and another is #check @const

[Scott Morrison]

The complication here was that it wasn't either explicit or implicit: it was functorial.

[Scott Morrison]

Okay, well I'm off for now @fosco. Good luck. Reading some examples like arrow categories, comma categories, and categories of cones will be helpful for what you are doing next.

[fosco]

Thanks for your help!

[fosco]

This should be nearer to what you were suggesting:

structure wedge_morphism (U V : wedge T) :=
(hom : U.tip ⟶ V.tip)
(w'  : ∀ j : C, hom ≫ V.α.app j = U.α.app j . obviously)

structure cowedge_morphism (U V : cowedge T) :=
(hom : U.tip ⟶ V.tip)
(w'  : ∀ j : C, U.α.app j ≫ hom = V.α.app j . obviously)

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, wedge_morphism U V,
  id   := λ X, eq_to_hom rfl,
  comp := λ X Y Z f g, f ≫ g, }

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom  := λ U V, cowedge_morphism U V
  id   := λ X, eq_to_hom rfl,
  comp := λ X Y Z f g, f ≫ g, }

[fosco]

(I added [T : Cᵒᵖ × C ⥤ D] among the variables)

[Kevin Buzzard]

Another thing you might want to try @fosco (if you didn't already) is doing Scott's problem sheet in LFTCM2020: clone https://github.com/leanprover-community/lftcm2020 with leanproject get lftcm2020, open the lftcm2020 folder with VS Code, make your way to src/exercises_sources/thursday/category_theory/ and try filling in the sorrys. Beforehand you might want to watch the accompanying video.

[fosco]

I watched part of Scott's video :smile: it motivated me to enter here.

[Kevin Buzzard]

oh nice!

[Scott Morrison]

Excellent!

[Kevin Buzzard]

I'm glad that people can find their way to that stuff independently of being pointed there from here

[Scott Morrison]

Don't forgot to:

restate_axiom wedge_morphism.w'     -- this will make a copy called `w`, and clean up some mess `. obviously` leaves
attribute [simp] wedge_morphism.w

[Scott Morrison]

It's important as you build new structures that you simultaneously define simp lemmas which make use of the bundled axioms. If you do this right, you can avoid lots of boring proofs!

[fosco]

I feel I need a more systematic approach to understand this kind of subtlety.

[Scott Morrison]

Hmm... before we go there. I don't think

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, wedge_morphism U V,
  id   := λ X, eq_to_hom rfl,
  comp := λ X Y Z f g, f ≫ g, }

can possibly be working.

[Scott Morrison]

Because id and comp should be constructing new wedge_morphisms.

[Scott Morrison]

After all, you need to check the condition holds for the composition of two wedge morphisms, using the conditions for the two wedge morphisms!

[Scott Morrison]

(Or rather, we hope that we don't need to check this, but that Lean will check it for us.)

[fosco]

uh, probably they were auto-filled sorrys; the problem though is earlier

[fosco]

in the definition of hom

[fosco]

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  F

[fosco]

I just copied from the definition of cone_category

[Scott Morrison]

Hrmm... we need to sort that out first.

[Scott Morrison]

Now, you said above that you introduced T as a variable, but you put it in square brackets. That was wrong -- square brackets are only for typeclasses.

[Scott Morrison]

(A good rule of thumb, by the way, is to always fix the first error in the file first, and to not proceed past errors! sorry is okay, but an error higher up can really obscure what's going on.)

[Scott Morrison]

Changing the square brackets to { } on T will give you the correct error message now.

[Scott Morrison]

So you want something more like:

variables {T : Cᵒᵖ × C ⥤ D}

structure wedge_morphism (U V : wedge T) :=
(hom : U.tip ⟶ V.tip)
(w'  : ∀ j : C, hom ≫ V.α.app j = U.α.app j . obviously)

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, wedge_morphism U V,
  id   := λ X, ⟨𝟙 _⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom⟩, }

This still has an error, but notice that in the id field we didn't need to provide the proof of w'! Hooray, Lean did it for us.

[Scott Morrison]

However in the comp field Lean complains that it can't prove w'.

[Scott Morrison]

But if you add

restate_axiom wedge_morphism.w'
attribute [simp] wedge_morphism.w

then that error goes away too! Hooray!

[Scott Morrison]

But there are still more errors: the id and comp fields both typecheck, but there's an error on the { of the instance. If you read the messages, you'll see that it's failing to prove the comp_id' id_comp' and assoc' fields of category.

[Scott Morrison]

The reason here is that we haven't explained to Lean how one checks that two wedge_morphisms are equal: you check that their homs are equal!

[Scott Morrison]

So we add

@[ext]
lemma wedge_morphis.ext {U V : wedge T} (f g : wedge_morphism U V) (w : f.hom = g.hom) : f = g :=
by { cases f, cases g, tidy, }

[Scott Morrison]

The @[ext] annotation here says: "if automation is trying to prove things are equal by the strategy of proving they are equal "componentwise" in some sense, try using this lemma!"

[Scott Morrison]

After this,

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, wedge_morphism U V,
  id   := λ X, ⟨𝟙 _⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom⟩, }

compiles with no errors.

[Scott Morrison]

Okay, but now I am really leaving for the night. :-) Have fun.

[fosco]

:-) sure, I will.

Thanks again

[fosco]

the same solution, for cowedges, does not work:

@[ext]
lemma wedge_morphism.ext {U V : wedge T} (f g : wedge_morphism U V) (w : f.hom = g.hom) : f = g :=
by { cases f, cases g, tidy, }

@[ext]
lemma cowedge_morphism.ext {U V : cowedge T} (f g : cowedge_morphism U V) (w : f.hom = g.hom) : f = g :=
by { cases f, cases g, tidy, }

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, wedge_morphism U V,
  id   := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom⟩, }

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom := λ U V, cowedge_morphism U V,
  id := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom⟩ }

[fosco]

There is an unsolved goal showing that the composition of the hom parts of is a cowedge; something I would easily prove with a couple of congs in agda, but here I have no idea how to move

[fosco]

...I guess I should move to simpler exercises.

[Kevin Buzzard]

Can you paste everything you have so far as a #mwe? I'm only half-watching this thread and so I'm missing all the imports/opens etc, but I can try to help.

[Kevin Buzzard]

import category_theory.products.basic
import category_theory.const

open opposite

namespace category_theory

open category_theory.functor

variables {C D E : Type*} [category C] [category D] [category E]

def functor.map_prod (F : C × D ⥤ E) {W X : C} {Y Z : D} (f : W ⟶ X) (g : Y ⟶ Z) :
  F.obj (W, Y) ⟶ F.obj (X, Z) :=
F.map (f, g)

structure dinat_trans (F G : Cᵒᵖ × C ⥤ D) :=
(app : Π X, F.obj (op X, X) ⟶ G.obj (op X, X))
(dinaturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
  F.map_prod f.op (𝟙 _) ≫ app X ≫ G.map_prod (𝟙 _) f =
  F.map_prod (𝟙 _) f ≫ app Y ≫ G.map_prod f.op (𝟙 _) . obviously)

structure wedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans ((const (Cᵒᵖ × C)).obj tip) F)

structure cowedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans F ((const (Cᵒᵖ × C)).obj tip))


variables {T : Cᵒᵖ × C ⥤ D}

structure wedge_morphism (U V : wedge T) :=
(hom : U.tip ⟶ V.tip)
(w'  : ∀ j : C, hom ≫ V.α.app j = U.α.app j . obviously)

structure cowedge_morphism (U V : cowedge T) :=
(hom : U.tip ⟶ V.tip)
(w'  : ∀ j : C, U.α.app j ≫ hom = V.α.app j . obviously)

restate_axiom wedge_morphism.w'
attribute [simp] wedge_morphism.w

restate_axiom cowedge_morphism.w'
attribute [simp] cowedge_morphism.w

@[ext]
lemma wedge_morphism.ext {U V : wedge T} (f g : wedge_morphism U V) (w : f.hom = g.hom) : f = g :=
by { cases f, cases g, tidy, }

@[ext]
lemma cowedge_morphism.ext {U V : cowedge T} (f g : cowedge_morphism U V) (w : f.hom = g.hom) : f = g :=
by { cases f, cases g, tidy, }

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, wedge_morphism U V,
  id   := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom⟩, }

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom := λ U V, cowedge_morphism U V,
  id := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom⟩ }

-- instance twisted : category (hom C) :=
--   { hom := _,
--   id := _,
--   comp := _,
--   id_comp' := _,
--   comp_id' := _,
--   assoc' := _ }

end category_theory

[Kevin Buzzard]

So if I click just before the red underline then I see that the goal is

⊢ ∀ (j : C), X.α.app j ≫ f.hom ≫ g.hom = Z.α.app j

[Kevin Buzzard]

so in the definition of composition of morphisms in this cowedge category, so far you have said "let X, Y, Z be objects of cowedge F and say f : X -> Y and g : Y -> Z are morphisms." We now want to define a morphism from X to Z and right now to do that Lean's understanding is that you need to prove (some statement about a diagram commuting)

[Kevin Buzzard]

which looks odd to me

[Kevin Buzzard]

oh this looks like w'

[Kevin Buzzard]

oh, so Lean is complaining that it can't prove w'

[Kevin Buzzard]

automation is failing to do your diagram chase

[Kevin Buzzard]

Is it true?

[Kevin Buzzard]

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom := λ U V, cowedge_morphism U V,
  id := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom, begin
    intro j,
    sorry
  end⟩ }

gives you the goal

F : Cᵒᵖ × C ⥤ D
X Y Z : cowedge F
f : X ⟶ Y
g : Y ⟶ Z
j : C
⊢ X.α.app j ≫ f.hom ≫ g.hom = Z.α.app j

Is that goal true?

[Kevin Buzzard]

yeah I can prove it

[Kevin Buzzard]

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom := λ U V, cowedge_morphism U V,
  id := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom, begin
    intro j,
    cases f with f_hom f_w,
    cases g with g_hom g_w,
    specialize f_w j,
    specialize g_w j,
    simp [← g_w, ← f_w],
  end⟩ }

[Kevin Buzzard]

Scott's obviously tactic seems to find the analogous proof for wedge F but not for this one. I have no idea how the automation works but there's a hand-constructed proof. It might be the case that with some more magic you can get Lean to find this proof itself

[Kevin Buzzard]

and here's what the proof looked like before I golfed it (so you can see my thought process):

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom := λ U V, cowedge_morphism U V,
  id := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom, begin
    intro j,
    cases f with f_hom f_w,
    cases g with g_hom g_w,
    simp,
    specialize f_w j,
    specialize g_w j,
    rw ← g_w,
    rw ← f_w,
    rw category.assoc,
  end⟩ }

[Kevin Buzzard]

and after:

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom := λ U V, cowedge_morphism U V,
  id := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom, λ j, begin
    cases f with _ f_w,
    cases g with _ g_w,
    simp [← f_w j, ← g_w j],
  end⟩ }

[fosco]

Amazing!

[fosco]

So, when I define a structure like wedge_morphism, cases allows me to access its fields (hom and w' in this case)

[Kevin Buzzard]

Yes, and unfortunately (because we are trying to be clever with automation) you can see that the type of f_w is auto_param (∀ (j : C), X.α.app j ≫ f_hom = Y.α.app j) (name.mk_string "obviously" name.anonymous), but I have seen that sufficiently often to know that what it actually says is just ∀ (a : C), X.α.app a ≫ f_hom = Y.α.app a so I could just feed j into that function and get X.α.app j ≫ f_hom = Y.α.app j

[Kevin Buzzard]

I am bewildered why simp at f_w doesn't get rid of the auto_param. rw auto_param_eq at f_w, gives

rewrite tactic failed, did not find instance of the pattern in the target expression
  auto_param ?m_1 ?m_2
state:
...
f_w : auto_param (∀ (j : C), X.α.app j ≫ f_hom = Y.α.app j) (name.mk_string "obviously" name.anonymous),
...

[Kevin Buzzard]

Oh I am a fool, it does work, it just leaves the old one behind because it's in the goal (the error above is because there's a second f_w later on in the context)

[Kevin Buzzard]

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom := λ U V, cowedge_morphism U V,
  id := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom, λ j, begin
    cases f with _ f_w,
    cases g with _ g_w,
    simp at ⊢ f_w g_w,
    -- local context now looks nice
    -- `obviously` still fails though
    simp [← f_w j, ← g_w j],
  end⟩ }

[Adam Topaz]

This works fine for me...

import category_theory.products.basic
import category_theory.const

open opposite

namespace category_theory

open category_theory.functor

variables {C D E : Type*} [category C] [category D] [category E]

def functor.map_prod (F : C × D ⥤ E) {W X : C} {Y Z : D} (f : W ⟶ X) (g : Y ⟶ Z) :
  F.obj (W, Y) ⟶ F.obj (X, Z) :=
F.map (f, g)

structure dinat_trans (F G : Cᵒᵖ × C ⥤ D) :=
(app : Π X, F.obj (op X, X) ⟶ G.obj (op X, X))
(dinaturality' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
  F.map_prod f.op (𝟙 _) ≫ app X ≫ G.map_prod (𝟙 _) f =
  F.map_prod (𝟙 _) f ≫ app Y ≫ G.map_prod f.op (𝟙 _) . obviously)

restate_axiom dinat_trans.dinaturality'
attribute [simp, reassoc] dinat_trans.dinaturality

structure wedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans ((const (Cᵒᵖ × C)).obj tip) F)

structure cowedge (F : Cᵒᵖ × C ⥤ D) :=
(tip : D)
(α : dinat_trans F ((const (Cᵒᵖ × C)).obj tip))


variables {T : Cᵒᵖ × C ⥤ D}

structure wedge_morphism (U V : wedge T) :=
(hom : U.tip ⟶ V.tip)
(w'  : ∀ j : C, hom ≫ V.α.app j = U.α.app j . obviously)

structure cowedge_morphism (U V : cowedge T) :=
(hom : U.tip ⟶ V.tip)
(w'  : ∀ j : C, U.α.app j ≫ hom = V.α.app j . obviously)

restate_axiom wedge_morphism.w'
attribute [simp, reassoc] wedge_morphism.w

restate_axiom cowedge_morphism.w'
attribute [simp, reassoc] cowedge_morphism.w

@[ext]
lemma wedge_morphism.ext {U V : wedge T} (f g : wedge_morphism U V) (w : f.hom = g.hom) : f = g :=
by { cases f, cases g, tidy, }

@[ext]
lemma cowedge_morphism.ext {U V : cowedge T} (f g : cowedge_morphism U V) (w : f.hom = g.hom) : f = g :=
by { cases f, cases g, tidy, }

instance (F : Cᵒᵖ × C ⥤ D) : category (wedge F) :=
{ hom  := λ U V, wedge_morphism U V,
  id   := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom⟩, }

instance (F : Cᵒᵖ × C ⥤ D) : category (cowedge F) :=
{ hom := λ U V, cowedge_morphism U V,
  id := λ X, ⟨ 𝟙 _ ⟩,
  comp := λ X Y Z f g, ⟨f.hom ≫ g.hom⟩ }

-- instance twisted : category (hom C) :=
--   { hom := _,
--   id := _,
--   comp := _,
--   id_comp' := _,
--   comp_id' := _,
--   assoc' := _ }

end category_theory

[fosco]

The missing part was this

restate_axiom dinat_trans.dinaturality'
attribute [simp, reassoc] dinat_trans.dinaturality

[Adam Topaz]

I also added the reassoc attribute to the other simp lemmas

[Adam Topaz]

But I don't know exactly what made it work :)

[fosco]

lean magic

[fosco]

Now: the next step is defining a category having object the hom-class of another given category

[fosco]

(probably there is a ton of other things to do, but the twisted arrow category seems to be the next logical step)

[Adam Topaz]

We do have docs#category_theory.arrow and docs#category_theory.comma

[fosco]

perfect: Tw(C) is the comma category of the terminal functor $* \to Set$ and of the hom functor of $C$

[fosco]

Now, is this an instance or a definition?

[Adam Topaz]

docs#category_theory.comma is itself a structure, which is endowed with a category instance

[fosco]

I would like to write "given a category C, there is a category Tw(C) done so and so"

[fosco]

is this an instance of category, or the definition of a new category?

[Johan Commelin]

It's a definition, and you put a category instance on top of it

[Johan Commelin]

@[derive category]
def twisted (C : Type*) [category C] := comma _ _ -- fill in the functors

[fosco]

It doesn't work:

don't know how to synthesize placeholder
context:
C : Type u_1,
_inst_4 : category C
⊢ Sort ?

[fosco]

(also, unknown identifier comma, but that's going to be solved with the right open I guess)

[Adam Topaz]

You're probably missing an import

[Adam Topaz]

What are the two functors precisely? The initial one from *, but what do you mean by the hom functor?

[Adam Topaz]

The one from Cop x C to Set?

[fosco]

the functor $\hom : C^{op} \times C \to Set$ sending $(X,Y)$ to $\hom(X,Y)$ and $(u,v)$ to the function $f\mapsto vfu$

[fosco]

but I would like to re-define these basic objects, and refactor later using more high-level stuff... I feel I'm losing the grip of the problem.

[fosco]

I need baby steps. How do I define a category with a single object and a single morphism?

[fosco]

how do I define a functor from said category to Set, picking the singleton set?

[fosco]

when I have these blocks, and the hom functor above, I can try to define twisted

[Adam Topaz]

Gotcha. So we have the constant functor as you already know, and for the hom functor we can use docs#category_theory.yoneda and docs#category_theory.uncurry (and docs#category_theory.prod.swap if needed)

[fosco]

yoneda + uncurry gives hom, I understand, but what about the terminal category?

[Adam Topaz]

docs#category_theory.discrete and docs#punit

[Adam Topaz]

so category_theory.discrete punit is the terminal category

[fosco]

def hom_functor : Cᵒᵖ × C ⥤ Type* :=
uncurry yoneda

def terminal_category : category unit :=
category_theory.discrete punit

I have no idea what I'm doing :grinning:

[fosco]

(mostly because I have no idea how to write the generic "this is of type that")

[Johan Commelin]

@fosco what do you mean?

[Johan Commelin]

def terminal_category : category unit :=
category_theory.discrete_category punit

:this: should be instance. You are instructing lean how to put a category structure on the type unit.

[Johan Commelin]

But you can also just use category_theory.discrete punit, as Adam suggested.
category_theory.discrete is a function that eats a type, and spits out that same type (the identity, ha!)
But the upshot is that if a type is wrapped in this identity function, then Lean endows it with the category structure that has no homs except for the identity homs.

[fosco]

No: category_theory.discrete punit throws a mismatch

[fosco]

category_theory.discrete_category punit does not

[fosco]

Johan Commelin said:

fosco what do you mean?

I mean that I have no idea how to turn into Lean the definition I have in mind

[fosco]

I see there's a lot of stuff already written, but I feel like I'm the passenger in a bus; when the trip is finished I don't remember the road I took. I learn by driving.

[fosco]

My problem is small, and I want an elementary solution; I don't care there is a library that does it already, I need to see how to write down the definition I want

[fosco]

You are helping a lot, but it is exhausting to say the least.

[fosco]

I want to define a category with a single object and a single morphism. I want to define a functor from it to Set, that picks the singleton

[Johan Commelin]

So you write

instance : category unit :=
_

And use the :bulb: to get a skeleton.

[Johan Commelin]

After that, you write

def terminal_functor : unit ⥤ Type :=
_

etc...

[fosco]

ok, I'll give it a try. But now I need a break

Thanks!

[Adam Topaz]

I made you a video explaining how to construct these things:
2021-10-02_10-31-46.mkv

[fosco]

wow, many thanks!

[Adam Topaz]

No problem. There are a few subtleties with universe parameters, as you can see...

[fosco]

heh, yeah :grinning: I would have lost a few hours after those...

[Scott Morrison]

Just coming back to explain why the reassoc attribute Adam suggested is useful!

[Scott Morrison]

The goal automation was stuck on was

F : Cᵒᵖ × C ⥤ D
X Y Z : cowedge F
f : X ⟶ Y
g : Y ⟶ Z
j : C
⊢ X.α.app j ≫ f.hom ≫ g.hom = Z.α.app j

[Scott Morrison]

You might wonder: surely f.w : X.α.app j ≫ f.hom = Y.α.app j, which is a @[simp] lemma, should fire here when automation calls simp, reducing the goal to Y.α.app j ≫ g.hom = Z.α.app j, which is in turn solvable by simp using g.w.

[Scott Morrison]

The problem is associativity: the goal is actually X.α.app j ≫ (f.hom ≫ g.hom) = Z.α.app j and so f.w` doesn't immediately apply.

[Scott Morrison]

We could deal with this problem by hand, by rewriting using category.assoc to rebracket and then using f.w and g.w.

[Scott Morrison]

However we could also realise that it would be helpful if there was a lemma f.w_assoc : ∀ h, X.α.app j ≫ (f.hom ≫ h) = Y.α.app j ≫ h, where we are quantifying over some arbitrary other morphism h.

[Scott Morrison]

If this were a @[simp] lemma, then simp could discharge the original goal by using f.w_assoc g.hom, and then using g.w.

[Scott Morrison]

Writing attribute [reassoc] wedge_morphism.w achieves exactly this! The reassoc attribute causes Lean to go away and inspect the lemma, realise it is an equation in a category involving a composition on the LHS, and automatically generate the additional lemma wedge_morphism.w_assoc.

[Scott Morrison]

In fact, you should try writing #print wedge_morphism.w_assoc to verify that this lemma was automatically created, and behaves as I indicated.

[Scott Morrison]

This trick largely ameliorates dealing with associativity in 1-categories. We can work with all our expressions in "simp normal form", here meaning "all associated to the right", but lemmas about compositions have automatically generated helper lemmas that allow them to apply in the middle of a composition.

[Scott Morrison]

(Sadly we have not implemented the planar-graph-pattern-matching that would be required to do this in 2-categories / monoidal categories. :-) One day!)

[fosco]

Thanks a lot! So, next step is define the twisted arrow category of C

[fosco]

I need

1. the hom functor: $\hom_C : C^{op}\times C \to Set$
2. the terminal functor, $* \to Set$ choosing the singleton
3. a comma construction.

I have 2. 1 can be obtained uncurrying yoneda. 3 is already there

[fosco]

This is not what I initially wanted to use to define Tw(C), but nevermind, maybe there will be a theorem later.

[Scott Morrison]

Remember that Set is called Type now. :-)

[Scott Morrison]

See category_theory.hom_functor: src#category_theory.functor.hom

[Scott Morrison]

We also have src#category_theory.category_of_elements.

[Scott Morrison]

which might give you a one-liner definition of the twisted arrow category!

[fosco]

The problem is always the same, I don't know the syntax with which I can invoke the right definition

[fosco]

Plus, copy-pasting the definition of hom results in errors

[fosco]

failed to synthesize type class instance for
C : Type u_1,
_inst_1 : category C,
p : Cᵒᵖ × C
⊢ quiver C

[Scott Morrison]

That's weird!

[Scott Morrison]

Can you post a #mwe?

[Scott Morrison]

Or try set_option pp.universes true and see what the error message becomes?

[fosco]

Where should I put it?

[Kevin Buzzard]

Before the error

[Kevin Buzzard]

Outside any structure def or theorem

[Kevin Buzzard]

But you should please get into the habit of posting #mwe s. Errors by themselves are not easy to interpret

[fosco]

import category_theory.products.basic
import category_theory.const
import category_theory.comma
import category_theory.discrete_category

open opposite

namespace category_theory

open category_theory.functor

variables {C D E : Type*} [category C] [category D] [category E]

definition hom : Cᵒᵖ × C ⥤ Type :=
{ obj       := λ p, unop p.1 ⟶ p.2,
  map       := λ X Y f, λ h, f.1.unop ≫ h ≫ f.2 }

end category_theory

[fosco]

image.png

[Scott Morrison]

Ah, but you didn't copy and paste.

[Scott Morrison]

You wrote Type as the target.

[Scott Morrison]

The problem is that [category C] introduces a universe variable for the morphism level.

[Scott Morrison]

import category_theory.products.basic
import category_theory.const
import category_theory.comma
import category_theory.discrete_category

open opposite

namespace category_theory

open category_theory.functor

variables {C D E : Type*} [category C] [category D] [category E]

definition hom : Cᵒᵖ × C ⥤ Type* :=
{ obj       := λ p, unop p.1 ⟶ p.2,
  map       := λ X Y f, λ h, f.1.unop ≫ h ≫ f.2 }

end category_theory

works fine.

[Scott Morrison]

Alternatively if we write

import category_theory.products.basic
import category_theory.const
import category_theory.comma
import category_theory.discrete_category

open opposite

namespace category_theory

open category_theory.functor

variables {C D E : Type*} [category C] [category D] [category E]

set_option pp.universes true

definition hom : Cᵒᵖ × C ⥤ Type :=
{ obj       := λ p, unop p.1 ⟶ p.2,
  map       := λ X Y f, λ h, f.1.unop ≫ h ≫ f.2 }

end category_theory

[Scott Morrison]

we get a useful error message:

[Scott Morrison]

failed to synthesize type class instance for
C : Type u_1,
_inst_1 : category.{u_4 u_1} C,
p : Cᵒᵖ × C
⊢ quiver.{1 u_1} C

[Scott Morrison]

From which you can see that there is a universe level problem! There is a category instance with universe levels .{u_4 u_1}, but the quiver instance you need is .{1 u_1}.

[Scott Morrison]

and the reason for this is exactly that you changed the codomain of hom to Type.

[Kevin Buzzard]

You have to ask yourself whether you want to work with a category C whose objects form a set in some Grothendieck universe u1 and whose hom sets all live in another Grothendieck universe u2, and then whether D has objects in u3 etc etc. That's what you're doing right now

[Scott Morrison]

The one-liner for twisted_arrow is just:

import category_theory.elements

open category_theory

@[derive category]
def twisted_arrow (C : Type*) [category C] := (functor.hom C).elements

[fosco]

I see! Thanks.

[Kevin Buzzard]

Type is the smallest Grothendieck universe so you can't land in there in general unless you restrict to categories whose hom sets are there. Basically you have to decide what you mean by a category, is it small, large, or do you want to try to write code which works for both or even more general situations

[Kevin Buzzard]

Right now we choose a universe level for objects and a different one for morphisms

[Scott Morrison]

(Hopefully reading the note about universe levels in category_theory.category.basic will be helpful. It explains why we need to use two independent universe levels, in order to formalise small and large categories uniformly.)

[Patrick Massot]

https://leanprover-community.github.io/mathlib_docs/notes.html#category_theory%20universes

[fosco]

Kevin Buzzard said:

In lean we choose a universe level for objects and a different one for morphisms

Yes; whereas usually objects are in a universe more than the one where hom's live

[fosco]

anyway

[fosco]

now I have various choices for how to formalise next:

1. the end of F is the terminal object of its category of wedges
2. precomposing with the functor $Tw(F) \to C^{op}\times C$ sends $F : C^{op}\times C \to D$ to $\bar F : Tw(C) \to D$, and
3. $\int_c F\cong \lim \bar F$

[fosco]

1. I looked for "terminal object of a category", but I didn't find anything, only the statement that a category has a terminal object. I was thinking to something on the lines of "{Wd(F) has a terminal object, a choice of that object}"

2. does the category of elements construction allows to extract the functor immediately?

[Scott Morrison]

2. does the category of elements construction allows to extract the functor immediately?

Which functor?

[fosco]

there are various ways to call it; the "category of elements" construction turns a presheaf $F : C^{op} \to Set$ into a fibration over $C$; the functor I want is precisely that fibration

[Scott Morrison]

1.

src#category_theory.limits.is_terminal

[fosco]

it just forgets the "element" a in (X, a \in FX)

[Scott Morrison]

src#category_theory.category_of_elements.π

[Scott Morrison]

(or just read through category_theory.elements until you find it :-)

[fosco]

def twisted_fibration : twisted C ⥤ Cᵒᵖ × C :=
category_of_elements.π (twisted C)

I get a universe error.. let's see if I'm able to fix it alone

[fosco]

no, it's a type misatch

[fosco]

twisted C
has type
  Type (max u_1 u_4) : Type (max (u_1+1) (u_4+1))
but is expected to have type
  Cᵒᵖ × C ⥤ Type u_4 : Type (max u_4 u_1 (u_4+1))

[fosco]

def twisted_fibration : twisted C ⥤ Cᵒᵖ × C :=
category_of_elements.π (functor.hom C)

hooray!

[fosco]

Now:

/- TODO:
F : Cᵒᵖ × C ⥤ D (I'd be happy to do it just for D=Type* atm...)
end1 : the terminal object in Wd(F) (it exists, because Type is complete)
end2 : limit of (F ⋙ twisted_fibration C)
thm end1 ≅ end2 canonically
-/

[fosco]

( whoops, it's (twisted_fibration C ⋙ F) )

[Scott Morrison]

Oh dear, you've said the dread word "canonically"! What do you mean? :-)

[Scott Morrison]

Presumably it is some naturality statement with respect to C.

[fosco]

yes (it can be done later, or it can be avoided :grinning: I'm suffering enough)

[fosco]

def end1 (F : Cᵒᵖ × C ⥤ Type*) : Type* := sorry
def end2 (F : Cᵒᵖ × C ⥤ Type*) : Type* := sorry

[fosco]

these are the typings.

[Scott Morrison]

So yes, first challenge is to write down the statement of the isomorphism, with a sorry for the construction.

[fosco]

Whoops, no

[Scott Morrison]

We'd like to just be able to write ⊤ : wedge F to specify the terminal object. Probably we're going to have to do some amount of explaining so that Lean understands why the completeness of Type implies the existence of a terminal object in wedge F.

[fosco]

oh, so \top is a shorthand to refer to a terminal object?

[Scott Morrison]

Yes. It's used all over mathlib for the top element of a lattice, but we also use the same notation for terminal objects.

[fosco]

How comes I can't find it if I Ctrl-F the entire src/ folder?

[Scott Morrison]

Are you writing \top in the search box? You need to copy and paste the unicode symbol into the search box.

[fosco]

Yes, I did

[Scott Morrison]

Does searching for anything work?

[fosco]

Nevermind; in theory this should work

limits.terminal (wedge F)

but it complains because it wants a proof that Type* has enough limits (probably?)

[Scott Morrison]

No, it's not clever enough to want that. :-)

[Scott Morrison]

How is Lean going to know anything about any limits in wedge F?

[Scott Morrison]

As far as it is concerned it is some brand new category.

[Scott Morrison]

We need to tell it something. So --- why does wedge F have a terminal object?

[fosco]

it doesn't; but __if__ it does, that's the end.

[fosco]

Scott Morrison said:

How is Lean going to know anything about any limits in wedge F?

Of course :smile:

[fosco]

that's why I was thinking about something like {a proof that wedge(F) has a terminal object, a choice of that object}

[fosco]

but this is a.. structure?

[Scott Morrison]

So you need is_terminal

[fosco]

is_terminal eats an object of the codomain

[Scott Morrison]

def my_iso {F : Cᵒᵖ × C ⥤ D} (X : wedge F) (h : is_terminal X) : P ≅ Q := sorry

[Scott Morrison]

That says: "suppose I have a terminal wedge, called X, then I can construct an isomorphism between P and Q"

[Scott Morrison]

(obviously you will need to fill in P and Q here)

[fosco]

I don't understand...

[Scott Morrison]

Isn't this what you want to say? You want to say "Suppose there is a terminal object in wedge F. Then <some construction based on that object> is a limit for twisted_fibration C ⋙ F."

[fosco]

oh! I see; no, I'm stuck at a former step, defining the end of F. I took another approach, but it looks kinda stupid

def end1 (F : Cᵒᵖ × C ⥤ D) (X : wedge F) (h : limits.is_terminal X) : wedge F := X

[fosco]

at least it doesnt complain...

[Scott Morrison]

So maybe instead you want to write

def limit_cone_of_terminal_wedge {F : Cᵒᵖ × C ⥤ D} (X : wedge F) (h : is_terminal X) :
  cone (twisted_fibration C ⋙ F) :=
...
lemma is_limit_of_terminal_wedge {F : Cᵒᵖ × C ⥤ D} (X : wedge F) (h : is_terminal X) :
  is_limit (limit_cone_of_terminal_wedge X h) :=
...

[Scott Morrison]

Yeah, that end1 definition is not doing anything for you. :-)

[Scott Morrison]

And probably you want to factor that into more pieces:

def end_of_terminal_wedge {F : Cᵒᵖ × C ⥤ D} (X : wedge F) (h : is_terminal X) : D :=
sorry

@[simps]
def limit_cone_of_terminal_wedge {F : Cᵒᵖ × C ⥤ D} (X : wedge F) (h : is_terminal X) :
  cone (twisted_fibration C ⋙ F) :=
{ X := end_of_terminal_wedge X h,
  π := sorry, }

lemma is_limit_of_terminal_wedge {F : Cᵒᵖ × C ⥤ D} (X : wedge F) (h : is_terminal X) :
  is_limit (limit_cone_of_terminal_wedge X h) :=
...

[fosco]

well, technically the end of F is the whole wedge, an object of wedge F

[fosco]

usually you call "the end" just the tip

[fosco]

I need a break :grinning: thanks for your help so far!

[Scott Morrison]

@fosco, rather than this manual translation between terminal objects and limit cones, you should just directly prove the equivalence of categories between wedge F and cone (twisted_fibration C ⋙ F).

[Kevin Buzzard]

Yes; whereas usually objects are in a universe more than the one where hom's live

You're claiming that, but you're also talking about limits and for limits in large categories it's essential that the source category (the diagram) does not satisfy the condition you claim is usual. And limits are also "usual" right? Formalisation has to take these things into account and it's when you start formalising that you start noticing them.

[Kevin Buzzard]

The way Scott has set it up saves us from having to develop two parallel theories of small and large categories.

[Kevin Buzzard]

It is not true in lean that "every small category is large", for the same reason that it's not true in lean that every natural number is a real number. There's a "canonical" construction which eats one thing and spits out the other but it's a genuine function and needs to be applied (and then one has to check that it commutes with everything)