1-limits in Cat

Stream: maths

[Joseph Hua]

Hi! I'm spending this week proving that Cat is complete (as a 1-category). Whilst this is "evil" somehow since Cat is really a 2-category, I think the results are worth having in mathlib. The non-master branch of my repo currently contains constructions of binary products and equalizers in Cat. https://github.com/Jlh18/discrete_fibrations/tree/Joseph is this worth a PR?

[Adam Topaz]

Ping @Junyan Xu

[Reid Barton]

This doesn't look too bad as far as eq_to_hom stuff is concerned, but I wonder if we have to deal with eq_to_hom anyways, maybe we can get a bigger payoff, like proving Cat is equivalent to some presentation of the 1-category of categories that doesn't involve dependent types.

[Reid Barton]

For example the presentation in terms of objects and morphisms with source and target maps and partially defined composition (which is the models of an essentially algebraic theory), or even the presentation as a reflective subcategory of simplicial sets.

[Junyan Xu]

Golfed the product part; why didn't you do it with arbitrary product? Because we don't have a category structure on the pi type yet? Will think about equalizers tomorrow; wondering whether using heq instead of eq in the definition of hom could lead to easier proofs.

[Joseph Hua]

oh wow, thanks for that @Junyan Xu . I am going to prove things about arbitrary product today! I did binary products first because I wanted to first get used to the category theory library with an easier exercise.

I am not familiar with the theory that you mention @Reid Barton , so I probably won't be doing that... So the conclusion is that this is not good PR material, given that this alternative is available?

[Joseph Hua]

hext is amazing

[Junyan Xu]

Using hext results in a goal without eq_to_hom, which is simpler in some sense, but there are very few lemmas about == (heq), for example there's no analogue of prod.ext for heq in mathlib, so I need to do dsimp [prod_map, (≫)], cases F.map f, refl instead of just prod.ext rfl rfl (in fact the types are defeq as I realized today and heq_of_eq (prod.ext rfl rfl) works). eq_to_hom is used to flush everything into the same type, and then heq can be expressed using = (eq), and all lemmas about eq can be used. It's not too bad to work with heq in this case, as many things involved are "almost defeq", i.e. Lean can recognized them to be defeq once the structures are broken down into its components using cases.

[Joseph Hua]

I'm struggling to find the right definition for equalizers using heq. The objects should just be as I originally had, requiring F.obj x = G.obj x, but it seems like requiring F.map f == G.map f for morphisms is not a good idea, since I can't do cases on a proof of the statement.

[Joseph Hua]

okay i showed that the category of small category has all small limits. I'm still confused about how equalizers should work using heq

[Junyan Xu]

Sorry to make you confused. I was just wondering whether heq would make equalizer simpler as well, given that it works well with products; but it turns out not to be the case. Although generally speaking heq between morphisms is equivalent to eq between morphisms conjugated by eq_to_hom, heq has less library support and most lemmas are stated in terms of eq_to_hom. (eq_to_hom seems to play well with simp lemmas, while proofs involving heq often requires the generalize tactic and that may be hard to automate, and if you want to compose to non-defeq'ly composable morphisms, you have to use eq_to_hom; these are possibly why people invented eq_to_hom and mostly abandoned heq.) Though I'm able to define the equalizer category using heq, it's complicated and this is the best I can get:

equalizer.str'

def equalizer.str' : category.{v} { c : C // F.obj c = G.obj c } :=
{ hom := λ x y, { f : x.1 ⟶ y.1 // F.map f == G.map f },
  id := λ x, ⟨𝟙 x, by erw [F.map_id, G.map_id, x.2]⟩,
  comp := λ x y z f g, ⟨ f.1 ≫ g.1, by { rw [F.map_comp, G.map_comp],
    have hf := f.2, have hg := g.2,
    generalize_hyp : F.map f.1 = Ff at ⊢ hf, generalize_hyp : G.map f.1 = Gf at ⊢ hf,
    generalize_hyp : F.map g.1 = Fg at ⊢ hg, generalize_hyp : G.map g.1 = Gg at ⊢ hg,
    clear f g, have hx := x.2, have hy := y.2, have hz := z.2,
    generalize_hyp : F.obj x.1 = Fx at Ff hx ⊢,
    generalize_hyp : F.obj y.1 = Fy at Ff Fg hy ⊢,
    generalize_hyp : F.obj z.1 = Fz at Fg hz ⊢,
    cases hx, cases hy, cases hz, apply heq_of_eq,
    rw [eq_of_heq hf, eq_of_heq hg] } ⟩ }

and here is a proof that the heq condition is equivalent to the "eq to conjugation by eq_to_hom" condition:

heq_iff_eq_conj_eq_to_hom

lemma heq_iff_eq_conj_eq_to_hom {c₁ c₂ : C} (h₁ : F.obj c₁ = G.obj c₁) (h₂ : F.obj c₂ = G.obj c₂)
  (f : c₁ ⟶ c₂) : F.map f = eq_to_hom h₁ ≫ G.map f ≫ eq_to_hom h₂.symm ↔ F.map f == G.map f :=
by { generalize : F.map f = Ff, generalize : G.map f = Gf, clear f,
  generalize_hyp : F.obj c₁ = F₁ at h₁ Ff ⊢, generalize_hyp : F.obj c₂ = F₂ at h₂ Ff ⊢,
  cases h₁, cases h₂, simp }

Now that limits are done, are you proceeding to colimits?

[Junyan Xu]

Seems we don't have the forgetful functor from Cat to Type (taking the object part). We'd like to show it preserves (co)limits.

[Joseph Hua]

Junyan Xu said:

Sorry to make you confused. I was just wondering whether heq would make equalizer simpler as well, given that it works well with products; but it turns out not to be the case. Although generally speaking heq between morphisms is equivalent to eq between morphisms conjugated by eq_to_hom, heq has less library support and most lemmas are stated in terms of eq_to_hom. (eq_to_hom seems to play well with simp lemmas, while proofs involving heq often requires the generalize tactic and that may be hard to automate, and if you want to compose to non-defeq'ly composable morphisms, you have to use eq_to_hom; these are possibly why people invented eq_to_hom and mostly abandoned heq.) Though I'm able to define the equalizer category using heq, it's complicated and this is the best I can get:

equalizer.str'

def equalizer.str' : category.{v} { c : C // F.obj c = G.obj c } :=
{ hom := λ x y, { f : x.1 ⟶ y.1 // F.map f == G.map f },
  id := λ x, ⟨𝟙 x, by erw [F.map_id, G.map_id, x.2]⟩,
  comp := λ x y z f g, ⟨ f.1 ≫ g.1, by { rw [F.map_comp, G.map_comp],
    have hf := f.2, have hg := g.2,
    generalize_hyp : F.map f.1 = Ff at ⊢ hf, generalize_hyp : G.map f.1 = Gf at ⊢ hf,
    generalize_hyp : F.map g.1 = Fg at ⊢ hg, generalize_hyp : G.map g.1 = Gg at ⊢ hg,
    clear f g, have hx := x.2, have hy := y.2, have hz := z.2,
    generalize_hyp : F.obj x.1 = Fx at Ff hx ⊢,
    generalize_hyp : F.obj y.1 = Fy at Ff Fg hy ⊢,
    generalize_hyp : F.obj z.1 = Fz at Fg hz ⊢,
    cases hx, cases hy, cases hz, apply heq_of_eq,
    rw [eq_of_heq hf, eq_of_heq hg] } ⟩ }

and here is a proof that the heq condition is equivalent to the "eq to conjugation by eq_to_hom" condition:

heq_iff_eq_conj_eq_to_hom

lemma heq_iff_eq_conj_eq_to_hom {c₁ c₂ : C} (h₁ : F.obj c₁ = G.obj c₁) (h₂ : F.obj c₂ = G.obj c₂)
  (f : c₁ ⟶ c₂) : F.map f = eq_to_hom h₁ ≫ G.map f ≫ eq_to_hom h₂.symm ↔ F.map f == G.map f :=
by { generalize : F.map f = Ff, generalize : G.map f = Gf, clear f,
  generalize_hyp : F.obj c₁ = F₁ at h₁ Ff ⊢, generalize_hyp : F.obj c₂ = F₂ at h₂ Ff ⊢,
  cases h₁, cases h₂, simp }

Now that limits are done, are you gonna proceed to colimits? Seems eq.rec is inevitable to define homs for the sigma category ... Oh it's actually Grothendieck construction with base a discrete category ... Maybe the Grothendieck construction yields the colimit for arbitrary diagram ...

Ah okay - yeah I couldn't figure out how to generalize the data F.map f to eliminate it. I'll try to see if this definition could tidy up my work. Thanks a lot!

About coproducts: it seems to me that category_theory.elements and category_theory.sigma are kind of duplicates of the same Grothendieck construction. Would it be nicer to make the sigma version from the elements version by making the indexing type I a discrete category? Either way, I will use this both for making pullbacks (which I would like to have a direct construction for) and maybe I'll do colimits too.

[Junyan Xu]

Oh I didn't know that category_theory.sigma.basic and category_theory.pi.basic exist! It seems sigma works for a functor from a discrete category to Cat, while elements works for a functor from an arbitrary category to Type, so they are complementary instead of special case of one another (and there is also grothendieck that works for a functor from any category to Cat, which I've generalized to oplax functors). sigma defines the homs not via another sigma type, but directly as an inductive type, which may or may not be easy to work with, and it would be interesting to try.

[Bhavik Mehta]

I found it a lot easier to work with the homs for sigma as an inductive type rather than a sigma type, because it avoids eq.rec and eq_to_hom sorts of things showing up everywhere and it made the proofs more awkward than usual to work with! My original method was to use a standard sigma type though

[Joseph Hua]

I just finished golfing the equalizer proof using heq and refactoring maps into the limit @Junyan Xu . There are a bunch of irrelevant comments about authenticity (I'm submitting this as coursework) so please ignore them.

[Joseph Hua]

Also made a couple of lemmas for composition working with heq

[Joseph Hua]

oh right elements is for functors into Type u silly me

[Kevin Buzzard]

Joseph -- is this for the assessment "prove a theorem at 1st year undergraduate level" due in on Friday? :laughing:

[Junyan Xu]

Just want to note that map_comp_heq has an easy proof using congr' as in

equalizer.str'

def equalizer.str' : category.{v} { c // F.obj c = G.obj c } :=
{ hom := λ x y, { f : x.1 ⟶ y.1 // F.map f == G.map f },
  id := λ x, ⟨ 𝟙 x , by erw [F.map_id, G.map_id, x.2] ⟩,
  comp := λ x y z f g, ⟨ f.1 ≫ g.1 , by { rw [F.map_comp, G.map_comp],
    congr' 1, exacts [x.2, y.2, z.2, f.2, g.2] } ⟩ }

[Joseph Hua]

Junyan Xu said:

Just want to note that map_comp_heq has an easy proof using congr' as in

equalizer.str'

def equalizer.str' : category.{v} { c // F.obj c = G.obj c } :=
{ hom := λ x y, { f : x.1 ⟶ y.1 // F.map f == G.map f },
  id := λ x, ⟨ 𝟙 x , by erw [F.map_id, G.map_id, x.2] ⟩,
  comp := λ x y z f g, ⟨ f.1 ≫ g.1 , by { rw [F.map_comp, G.map_comp],
    congr' 1, exacts [x.2, y.2, z.2, f.2, g.2] } ⟩ }

oh wow that's slick. but why does it work? I don't see how being "less aggressive at breaking down the goal" helps

[Junyan Xu]

If you try congr you'll see it's too aggressive and produces five identical goals F = G which isn't necessarily true...

[Junyan Xu]

and this is the output of show_term { congr' 1, exacts [x.2, y.2, z.2, f.2, g.2] }:

exact eq.rec
  (λ [self : category_struct ↥D] (self' : category_struct ↥D) (e_1 : self == self'),
     eq.rec
       (λ {X : ↥D} (X' : ↥D) (e_2 : X == X'),
          eq.rec
            (λ {Y : ↥D} (Y' : ↥D) (e_3 : Y == Y'),
               eq.rec
                 (λ {Z : ↥D} (Z' : ↥D) (e_4 : Z == Z'),
                    eq.rec
                      (λ (ᾰ ᾰ' : X ⟶ Y) (e_5 : ᾰ == ᾰ'),
                         eq.rec
                           (λ (ᾰ_1 ᾰ' : Y ⟶ Z) (e_6 : ᾰ_1 == ᾰ'),
                              eq.rec (heq.refl (ᾰ ≫ ᾰ_1)) (eq_of_heq e_6))
                           (eq_of_heq e_5))
                      (eq_of_heq e_4))
                 (eq_of_heq e_3))
            (eq_of_heq e_2))
       (eq_of_heq e_1))
  (eq.refl ↥D)
  category.to_category_struct
  (heq_of_eq (eq.refl category.to_category_struct))
  (G.obj x.val)
  (heq_of_eq x.property)
  (G.obj y.val)
  (heq_of_eq y.property)
  (G.obj z.val)
  (heq_of_eq z.property)
  (F.map f.val)
  (G.map f.val)
  f.property
  (F.map g.val)
  (G.map g.val)
  g.property

[Joseph Hua]

yeah i used show_term to have a look too. I guess it first looks for proofs of equality then tries to compare the terms, rather than looking to compare the terms, then checking equality (which fails)?

[Junyan Xu]

I don't quite get the question. Are you asking why congr fails? It doesn't actually fail but produces goals you won't be able to prove. For example congr' 1 produces F.obj x.val = G.obj x.val, but congr breaks it down one step further to get F = G, which is too much. It seems congr does recognize equalities in the context (but not the ones buried in a structure like subtype) but doesn't automatically apply them: if you do have := x.2 before congr you see that the first resulting goal becomes F.obj x.val = G.obj x.val (which is the type of x.2 but not automatically solved) but the other four goals remain F = G. congr' in contrast automatically uses equalities to solve resulting goals: if you do have := x.2, have := y.2, have := z.2, have := f.2, have := g.2, congr' 1 then goals accomplished.

[Joseph Hua]

you answered my question with yes haha, that is what I vaguely had in mind