extensionality for functors

Stream: mathlib4

[Dean Young]

Can someone direct me towards extensionality for functors?

[Eric Wieser]

Did you try searching for those two words on the #docs? (try "functor ext" in the search box)

[Eric Wieser]

It's a bit confusing because we have both docs#CategoryTheory.Functor and docs#Functor, but hopefully you know which one you want!

[Dean Young]

@Eric Wieser This is a pretty good category library.

I kind of want vertical composition to infer that two functors are equal (perhaps with a type class) by first applying some rewrite rules (Id₁ Id₂ and associativity in Cat). Is that something this library can do?

[Dean Young]

For instance, in many triangle identities I end up having to add in a natural transformation to handle simply associativity of functors, and I think it would be good to try to have it infer that equality on its own so I don't have to add in these extra natural transformations in the rewrite system.

[Dean Young]

Such normal forms for natural transformations and functors could make things a lot easier.

[Jason Rute]

If using the existing category theory library, try docs#CategoryTheory.Functor.ext and docs#CategoryTheory.Functor.hext

[Jason Rute]

Based on your PA post (and my currently wrong answer), I think the second is likely what you want.

[Jason Rute]

Also, I don't know much about the category theory library, but you might want to play with it more (instead of developing your own). I think they do have a lot of automation of various forms already in use. I think the tidy tactic was originally developed for this library, and it looks like now they are using the aesop tactic.

[Jason Rute]

I know Lean for the Curious Mathematician has a section on the category theory library complete with a tutorial and exercises to learn it better. The materials for the 2020 version is on github (https://github.com/leanprover-community/lftcm2020), but that is Lean 3. The 2023 version (in September) will cover Lean 4.

[Dean Young]

I think that's what I'll do, and it makes sense to assimilate their approach, but I was worried at first that I would pick up idiosyncrasies, such as that not having all of the fields of the various structures. I also needed to know which extensionality results are actually possible and which are limited in the way of HEq, though lack of CatExt is not critical. I'm more interested in not having to redo things three years from now. It would also help if the tutorials were more systematic, with completed tables and so on.

I think what I'm going to do is use their category, functor, natural transformation, and prove it makes an example of my "twocategory", of which my ℂ𝕒𝕥 is also an example. Going forward, I'll be able to switch to their ℂ𝕒𝕥.Obj, ℂ𝕒𝕥.Hom, ℂ𝕒𝕥.Idn, ℂ𝕒𝕥.Id₁, ℂ𝕒𝕥.Id₂, ℂ𝕒𝕥.Ass when I start to need more sophisticated maneuvers and help from the community.

I also have to check out their "Eilenberg Moore adjunction of a (co)monad", "(co)monad corresponding to (co)Eilenberg Moore adjunction". There are some requirements from what I'll need out of this (I need the canonical maps out of the (co)Eilenberg (co)Moore adjunctions as functors as well as a commutative triangle involving them).

[Scott Morrison]

The library already has bicategories, and the fact that categories/functors/natural transformations form a bicategory.

[Dean Young]

Bicategories, but I wanted strict two category.

[Scott Morrison]

Strict = suffering.

[Dean Young]

I took a look at the generators of the bicategory class. I do like how it uses the whiskers.

[Dean Young]

What is autoparam?

[Scott Morrison]

Run a tactic to try and fill in the field, so the user can omit it. Read the category theory library -- we don't give any boring proofs, because aesop can do them all.

[Dean Young]

Oh maybe I begin to see.

[Dean Young]

@Scott Morrison Suppose I wanted to compose two 2-morphisms f : F ⟶ G₁, g : G₂ ⟶ H, but G₁ and G₂ were only equal after applying associativity or a unit law for ordinary composition of functors. For instance, that happens when trying to build the triangle identities. Does this library have a way of inserting that cell on its own maybe or a type class for proving G₁ = G₂?

[Kevin Buzzard]

Can you make a #mwe ?

[Adam Topaz]

You can always compose with the associator/unitor or in the middle

[Dean Young]

Oh ok I get it, it's associator and leftUnitor rightUnitor like Adam says.

[Dean Young]

So basically those three are natural isomorphisms and its best to avoid the corresponding equalities.

[Adam Topaz]

These will introduce compositions with identity morphisms under the hood, but in practice simp will get rid of those in proofs.

[Scott Morrison]

You might like ⊗≫ in the monoidal category library, which automatically inserts associators and unitors when the composition doesn't otherwise typecheck. There is (I think?) a corresponding operator for bicategories as well.

[Yuma Mizuno]

Yes. For example, ⊗≫ composes 2-morphisms η and ε without inserting an associator in this image.
diagram.png

[Dean Young]

Does this work for Mathlib's bicategory of categories though?

[Dean Young]

Can you direct me to the bicategory of categories type?

[Adam Topaz]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Category/Cat.html#CategoryTheory.Cat.bicategory

[Dean Young]

In the implementation notes it says that "In the literature of category theory, a strict bicategory (usually called a strict 2-category) is often defined as a bicategory whose left unitors, right unitors, and associators are identities. We cannot use this definition directly here since the types of 2-morphisms depend on 1-morphisms. For this reason, we use eqToIso, which gives isomorphisms from equalities, instead of identities."

[Dean Young]

"Suppose I wanted to compose two 2-morphisms f : F ⟶ G₁, g : G₂ ⟶ H, but G₁ and G₂ were only equal after applying associativity or a unit law for ordinary composition of functors. For instance, that happens when trying to build the triangle identities. Does this library have a way of inserting that cell on its own maybe or a type class for proving G₁ = G₂?"

It looks like Adam has answered this.

My next goal is to construct an example of a bicategory.

[Dean Young]

@Yuma Mizuno Can you help me with those triangle unicode characters in your picture? What are the U####?

[Yuma Mizuno]

Do you mean the whiskering operators? I don't know the unicode numbers, but I'm typing them by \lhd and \rhd in VSCode.

[Dean Young]

oh ok awesome

[Scott Morrison]

Hovering over a unicode character in VSCode tells you how to type it.

[Dean Young]

Take a look at this... exactly what I wanted.

def ℂ𝕒𝕥 : (Bicategory Cat) := CategoryTheory.Cat.bicategory

#check Cat
#check ℂ𝕒𝕥
#check ℂ𝕒𝕥.Hom

notation G "∘" F => F ≫ G

variable {C D E: Cat}
variable {C₁ C₂ C₃ C₄ : Cat}
variable {D₁ D₂ D₃ D₄ : Cat}
notation C "⭢" D => C ⟶ D
variable {Dom : B₀}
variable {Cod : B₀}
variable {Fst : Dom ⭢ Cod}
variable {Snd : Cod ⭢ Dom}
variable {η :(𝟙 Dom) ⭢ (Snd ∘ Fst)}
variable {ε :(Fst ∘ Snd) ⭢ (𝟙 Cod)}



#check ℂ𝕒𝕥.whiskerLeft
notation F "◁" η => ℂ𝕒𝕥.whiskerLeft F η

#check ℂ𝕒𝕥.whiskerRight
notation η "▷" G => ℂ𝕒𝕥.whiskerRight η G

#check ℂ𝕒𝕥
#check ℂ𝕒𝕥.Hom
#check ℂ𝕒𝕥.id
#check ℂ𝕒𝕥.comp
#check ℂ𝕒𝕥.associator
#check ℂ𝕒𝕥.leftUnitor
#check ℂ𝕒𝕥.rightUnitor
#check ℂ𝕒𝕥.whiskerLeft_id
#check ℂ𝕒𝕥.whiskerLeft_comp
#check ℂ𝕒𝕥.id_whiskerLeft
#check ℂ𝕒𝕥.comp_whiskerLeft
#check ℂ𝕒𝕥.id_whiskerRight
#check ℂ𝕒𝕥.comp_whiskerRight
#check ℂ𝕒𝕥.whiskerRight_comp
#check ℂ𝕒𝕥.whiskerRight_id
#check ℂ𝕒𝕥.whisker_assoc
#check ℂ𝕒𝕥.whisker_exchange
#check ℂ𝕒𝕥.pentagon
#check ℂ𝕒𝕥.triangle

-- the first triangle identity
def AdjId₁
 (Dom : Cat)
 (Cod : Cat)
 (Fst : Dom ⭢ Cod)
 (Snd : Cod ⭢ Dom)
 (η :(𝟙 Dom) ⭢ (Snd ∘ Fst))
 (ε : (Fst ∘ Snd) ⭢ (𝟙 Cod)) : Prop := (((Fst ◁ ε) ∘ (η ▷ Fst)) = (𝟙 Fst))

-- the second triangle identity
def AdjId₂
 (Dom : Cat)
 (Cod : Cat)
 (Fst : Dom ⭢ Cod)
 (Snd : Cod ⭢ Dom)
 (η :(𝟙 Dom) ⭢ (Snd ∘ Fst))
 (ε : (Fst ∘ Snd) ⭢ (𝟙 Cod)) : Prop := ((ε ▷ Snd) ∘ (Snd ◁ η)) = (𝟙 Snd)

-- definition of an adjunction
structure adjunction where
  Dom : Cat
  Cod : Cat
  Fst : Dom ⭢ Cod
  Snd : Cod ⭢ Dom
  η :  (𝟙 Dom) ⭢ (Snd ∘ Fst)
  ε : (Fst ∘ Snd) ⭢ (𝟙 Cod)
  Id₁ : AdjId₁ Dom Cod Fst Snd η ε
  Id₂ : AdjId₂ Dom Cod Fst Snd η ε

[Dean Young]

def left_adjoint (f : adjunction) : f.Dom ⭢ f.Cod := f.Fst

notation f "ॱ" => left_adjoint f



def right_adjoint (f : adjunction) : f.Cod ⭢ f.Dom := f.Snd

notation f "𛲔" => right_adjoint f

[Dean Young]

That unicode dot pair is a hard find.

[Nicolas Rolland]

Jason Rute said:

I know Lean for the Curious Mathematician has a section on the category theory library complete with a tutorial and exercises to learn it better. The materials for the 2020 version is on github (https://github.com/leanprover-community/lftcm2020), but that is Lean 3. The 2023 version (in September) will cover Lean 4.

I hope the material will be on github and videos online as in past years !