Preserves terminal

Stream: mathlib4

[Kenny Lau]

What is the idiomatic way to say that a defined functor preserves terminal objects?

[Aaron Liu]

The definition you linked states it as "preserves the empty limit" so I guess that's it?

[Calle Sönne]

Aaron Liu said:

The definition you linked states it as "preserves the empty limit" so I guess that's it?

I'm not familiar with this part of the category theory library, but this says it preserves an arbitrary choice of empty limit. I'm guessing maybe what kenny is looking for is something like preserving IsTerminal or IsEmptyLimit or something similar (whatever this is called if it exists)

[Kenny Lau]

ah ok i think i know now, PreservesLimit would be the standard way for using, but for proving the standard way would be something about mapCone

[Kenny Lau]

and I guess it's fine that there's no separate abbrev for all of the shapes that we need

[Aaron Liu]

Calle Sönne said:

I'm not familiar with this part of the category theory library, but this says it preserves an arbitrary choice of empty limit.

Any two choices of empty limit are isomorphic :)

[Kenny Lau]

Aaron Liu said:

Calle Sönne said:

I'm not familiar with this part of the category theory library, but this says it preserves an arbitrary choice of empty limit.

Any two choices of empty limit are isomorphic :)

but not defeq :slight_smile:

[Adam Topaz]

I would use PreservesLimitsOfShape

[Kenny Lau]

Adam Topaz said:

I would use PreservesLimitsOfShape

It doesn't seem to be the preferred way in the file I linked

[Adam Topaz]

the instance in your link is PreservesLimit ... and PreservesLimitsOfShape would imply that.

[Adam Topaz]

import Mathlib

open CategoryTheory Limits

variable (C D : Type*) [Category C] [Category D] (F : C ⥤ D)
  [PreservesLimitsOfShape (Discrete PEmpty) F]
  [HasTerminal C] [HasTerminal D]

noncomputable
example : F.obj (⊤_ C) ≅ ⊤_ D := PreservesTerminal.iso _

[Adam Topaz]

I would also specify universes explicitly in this case.

[Kenny Lau]

How would you prove this?

import Mathlib

open CategoryTheory Limits

universe w v v' u u'

variable (C : Type u) (D : Type u') [Category.{v} C] [Category.{v'} D] (F : C ⥤ D)

instance (h : ∀ T : C, IsTerminal T → IsTerminal (F.obj T)) :
    PreservesLimitsOfShape (Discrete PEmpty.{w+1}) F :=
  sorry

[Kenny Lau]

This is a bit weird, I feel like there are definitely missing lemmas.

[Adam Topaz]

Here's a (nu-cleaned-up) proof (essentially every step was found with exact? after specifying the type)

import Mathlib

open CategoryTheory Limits

universe w v v' u u'

variable (C : Type u) (D : Type u') [Category.{v} C] [Category.{v'} D] (F : C ⥤ D)

lemma foo (h : ∀ T : C, IsTerminal T → IsTerminal (F.obj T)) : PreservesLimit (Functor.empty.{0} C) F where
  preserves := by
    intro c hc
    let d := F.mapCone c
    let ec : c ≅ asEmptyCone c.pt := Cones.ext (Iso.refl _)
    let G : Functor.empty D ≅ Functor.empty C ⋙ F :=
      (Functor.empty D).emptyExt (Functor.empty C ⋙ F)
    let ed : d ≅ (Cones.postcompose G.hom).obj (asEmptyCone d.pt) := Cones.ext (Iso.refl _)
    constructor
    suffices IsLimit ((Cones.postcompose G.hom).obj (asEmptyCone d.pt)) by
      exact this.ofIsoLimit ed.symm
    let qq : IsLimit (asEmptyCone d.pt) ≃ IsLimit ((Cones.postcompose G.hom).obj (asEmptyCone d.pt)) :=
      (IsLimit.postcomposeHomEquiv G (asEmptyCone d.pt)).symm
    apply qq.toFun
    apply h
    exact hc.ofIsoLimit ec

lemma bar (h : ∀ T : C, IsTerminal T → IsTerminal (F.obj T)) : PreservesLimitsOfShape (Discrete Empty) F := by
  constructor
  intro K
  let e : Discrete Empty ≌ Discrete PEmpty.{1} :=
    equivalenceOfIsEmpty (Discrete Empty) (Discrete PEmpty.{1})
  let ee : K ≅ e.functor ⋙ Functor.empty.{0} C := K.isEmptyExt (e.functor ⋙ Functor.empty C)
  suffices PreservesLimit (e.functor ⋙ Functor.empty.{0} C) F from
    preservesLimit_of_iso_diagram F ee.symm
  suffices PreservesLimit (Functor.empty.{0} C) F from Functor.Initial.comp_preservesLimit e.functor
  apply foo
  assumption

lemma baz (h : ∀ T : C, IsTerminal T → IsTerminal (F.obj T)) : PreservesLimitsOfShape (Discrete PEmpty.{w+1}) F := by
  let ee : Discrete PEmpty.{w+1} ≌ Discrete Empty := equivalenceOfIsEmpty
    (Discrete PEmpty.{w + 1}) (Discrete Empty)
  suffices PreservesLimitsOfShape (Discrete Empty) F from
    preservesLimitsOfShape_of_equiv ee.symm F
  apply bar
  assumption

This is a complete mess because some parts of the library use Empty and some use PEmpty.{w+1}.

[Kenny Lau]

It sounds like we have missing lemmas

[Adam Topaz]

Well, I think the real issue is that we don't have any consistency in how we talk about terminal objects.

[Adam Topaz]

Or in how we talk about functors from the empty category.

[Bhavik Mehta]

Adam Topaz said:

Well, I think the real issue is that we don't have any consistency in how we talk about terminal objects.

I'm not sure this is fair, we have IsTerminal and HasTerminal to solve precisely this problem, and there's already the existence and uniqueness for functors from the empty category. I think this is a universes issue, it looks like some of the statements to do the above aren't universe polymorphic enough (likely because they were written before limits became more universe polymorphic)

[Bhavik Mehta]

Specifically, https://github.com/leanprover-community/mathlib4/blob/f3731eaabfa91f8610f09b48be38213d6c16d171/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean#L38 is restricted to universe level 0, and that's the part which is making the proof above so long, making that universe polymorphic means it can be done a lot shorter, or (more likely) a lemma switching to a more general universe

[Bhavik Mehta]

in fact I take that back too: with an extra definition about mapCone (which I'm sure already exists but I couldn't find it), it's a combination of three two-line proofs. So I think we're not missing that much API here.

import Mathlib

open CategoryTheory Limits

universe w v v' u u'

variable (C : Type u) (D : Type u') [Category.{v} C] [Category.{v'} D] (F : C ⥤ D)

def mapConeIso {J : Type u''} [Category.{v''} J] {K : J ⥤ C} {c d : Cone K} (h : c ≅ d) :
    F.mapCone c ≅ F.mapCone d :=
  Cones.ext (F.mapIso ((Cones.forget _).mapIso h)) <| by simp [← Functor.map_comp]

def preservesLimit_empty_of_isTerminal_imp_isTerminal
    (h : ∀ T : C, IsTerminal T → IsTerminal (F.obj T)) :
    PreservesLimit (Functor.empty.{0} C) F where
  preserves {c} hc :=
    have hc' : c ≅ asEmptyCone c.pt := Cones.ext (Iso.refl _)
    ⟨((isLimitMapConeEmptyConeEquiv F c.pt).2 (h _ (hc.ofIsoLimit hc'))).ofIsoLimit (mapConeIso _ _ _ hc'.symm)⟩

def preservesLimitsOfShape_of_isTerminal_imp_isTerminal'
    (h : ∀ T : C, IsTerminal T → IsTerminal (F.obj T)) :
    PreservesLimitsOfShape (Discrete PEmpty.{1}) F where
  preservesLimit {K} :=
    let _ := preservesLimit_empty_of_isTerminal_imp_isTerminal _ _ _ h
    preservesLimit_of_iso_diagram _ K.uniqueFromEmpty.symm

def preservesLimitsOfShape_of_isTerminal_imp_isTerminal
    (h : ∀ T : C, IsTerminal T → IsTerminal (F.obj T)) :
    PreservesLimitsOfShape (Discrete PEmpty.{w+1}) F :=
  let _ := preservesLimitsOfShape_of_isTerminal_imp_isTerminal' _ _ _ h
  preservesLimitsOfShape_of_equiv emptyEquivalence F

[Bhavik Mehta]

Note that the theorem you asked for is basically the converse of https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.html#CategoryTheory.Limits.IsTerminal.isTerminalObj, and both of these are basically just chaining equivs, so it shouldn't be surprising after seeing that that the API all basically already existed

[Kenny Lau]

@Bhavik Mehta mapConeIso is something with Functoriality.cones.mapIso but I do agree that it should be a separate definition