preserving terminal objects at all universe levels

Stream: maths

[Emily Riehl]

I've added a lot of junk to PR #25010 to move from a proof that a functor preserves terminal objects at universe level zero to conclude the same at all universe levels. Eg, in the test code below I have a much easier construction of the given but had to add a lot to generalize this to a proof of the goal.

import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
import Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
import Mathlib.CategoryTheory.Limits.Preserves.Basic
import Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

namespace CategoryTheory

open Limits SSet

universe u

variable (F : SSet.{u} ⥤ Cat.{u, u})

/-- In the PR there is a relatively easy proof of this. -/
def given : hoFunctor.obj (⊤_ SSet.{0}) ≅ ⊤_ Cat.{0, 0} := sorry

/-- It takes a lot more work to prove this. But can I conclude it somehow from `given`? -/
def goal : hoFunctor.obj (⊤_ SSet.{u}) ≅ ⊤_ Cat.{u, u} := by
  let thing := given
  sorry

end CategoryTheory

I'm wondering if there is a way to move from the given to the goal directly?

[Emily Riehl]

In case anyone cares, I'll give more details about the current construction in #25010. Golfing advice would be very welcome!

Essentially the proof chains together five isomorphisms:
(hoFunctor.obj (⊤_ SSet)) ≅ hoFunctor.obj Δ[0] ≅ hoFunctor.obj (nerve (ULiftFin 1)) ≅ ULiftFin 1 ≅ Cat.of (Discrete PUnit) ≅ (⊤_ Cat)

[Emily Riehl]

We start by lifting the finite ordinal categories to arbitrary universe levels:

/-- An alias for the underlying type of the category `Fin n` lifted to an object of `Cat.{v, u}`. -/
def ULiftFin (n : ℕ) : Type u := (ULiftHom.{v,u} (ULift.{u} (Fin n)))

[Emily Riehl]

The first is obtained by proving that the 0-simplex is terminal.

The second requires a generalization of a recent result of @Thomas Murrills to arbitrary universes:

/-- The Yoneda embedding from the `SimplexCategory` into simplicial sets is naturally
isomorphic to `SimplexCategory.toCat ⋙ nerveFunctor` with component isomorphisms
`Δ[n] ≅ nerve (Fin (n + 1))`. -/
def simplexIsNerve (n : ℕ) : Δ[n] ≅ nerve (Fin (n + 1)) := NatIso.ofComponents <| fun n ↦
    Equiv.toIso stdSimplex.objEquiv ≪≫ SimplexCategory.homIsoFunctor

-- TODO: generalize from universe level 0 to arbitrary universes.
def simplexIsNerve' (n : ℕ) : Δ[n] ≅ nerve (ULiftFin (n + 1)) := sorry

The third iso is something in mathlib (phew).

The final two isomorphisms connect the abstract defined terminal object in Cat to an explicitly described unit category at any universe level. Then we connect this explicit categorty to ULiftFin 1:

instance DiscretePUnit.isTerminal : IsTerminal (Cat.of (Discrete PUnit)) :=
  IsTerminal.ofUniqueHom (fun C ↦ star C) (fun _ _ => punit_ext' _ _)

/-- As a terminal object, `Discrete PUnit` is isomorphic to the terminal object in `Cat.` -/
noncomputable def TerminalCatDiscretePUnitIso : ⊤_ Cat.{u,u} ≅ Cat.of (Discrete.{u} PUnit) :=
  terminalIsoIsTerminal DiscretePUnit.isTerminal

/-- An isomorphism between `ULiftFin 1` and `Discrete PUnit`. -/
def ULiftFinDiscretePUnitIso : Cat.of (ULiftFin 1) ≅ Cat.of (Discrete PUnit) where
  hom := toCatHom (star (ULiftFin 1))
  inv := toCatHom (fromPUnit (ULift.up 0))
  hom_inv_id := by
    apply (Function.RightInverse.injective ULiftFin.of_toComposableArrows)
    exact ComposableArrows.ext₀ rfl
  inv_hom_id := rfl

[Robin Carlier]

I am not sure if this helps directly for this, but docs#CategoryTheory.Limits.Types.isTerminalEquivUnique says an object in Type u is terminal iff it has a Unique structure. Perhaps it would be good to introduce a similar thing for Cat, saying that an object is terminal iff the underlying type has a Unique structure and the category has a IsDiscrete instance?

[Robin Carlier]

Then you’d "just" need to prove that hoFunctor.obj (⊤_ SSet) has a single object (should be "easy", as this is a quotient of a one-object type?) and, only one morphisms between those.

[Emily Riehl]

Interesting idea. The single object would be clear enough but I'm scared to attempt a proof that requires getting into the details of the construction of hoFunctor. Though in this case perhaps it wouldn't be too terrible...

[Robin Carlier]

In any cases, I believe a characterization of terminal object in Cat as "Unique + IsDiscrete" would be nice to have on its own.

[Emily Riehl]

We have a file CategoryTheory.Category.Cat.Limit (constructing limits in Cat) so could this go in CategoryTheory.Category.Cat.Terminal?

[Robin Carlier]

I’ll leave it to a maintainer to give a definite answer, but for Type, it’s in a file CategoryTheory.Limits.Types.Shapes, that records "explicit" constructions for co/limits of types, so I guess CategoryTheory.Limits.Cat.Shapes or CategoryTheory.Category.Cat.Limit.Shape might be appropriate?
(Though ....Terminal is perhaps best suited if the file only deal with terminal objects...)

[Robin Carlier]

I need to run for today, so I apologize for the unfinished stuff, but if you add things like

instance [Unique C] : Unique (Quotient r) where
  uniq a := by ext; subsingleton

instance [∀ (x y : C), Subsingleton (x ⟶ y)] (x y : Quotient r) :
    Subsingleton (x ⟶ y) := (full_functor r).map_surjective.subsingleton

around line 129 in CategoryTheory.Quotient, and

@[simp]
lemma FreeRefl.quotientFunctor_id (V) [ReflQuiver V] (X : V) :
    (FreeRefl.quotientFunctor V).map (𝟙rq X).toPath = 𝟙 _ := by
  apply Quotient.sound
  exact .mk

instance (V : Type*) [ReflQuiver V] [Unique V] : Unique (FreeRefl V) :=
  letI : Unique (Paths V) := inferInstanceAs (Unique V)
  inferInstanceAs (Unique (Quotient _))

instance (V : Type*) [ReflQuiver V] [Unique V]
    [∀ (x y : V), Unique (x ⟶ y)] (x y : FreeRefl V) :
    Unique (x ⟶ y) where
  default := (FreeRefl.quotientFunctor V).map ((Paths.of V).map default)
  uniq f := by
    letI : Unique (Paths V) := inferInstanceAs (Unique V)
    induction f using Quotient.induction with | @h x y f =>
    symm
    induction f using Paths.induction with
    | id =>
      apply Quotient.sound
      obtain rfl : x = y := by subsingleton
      conv =>
        arg 3
        equals (𝟙rq _).toPath => congr; subsingleton
      exact .mk
    | @comp x y z f g hrec =>
        obtain rfl : x = z := by subsingleton
        obtain rfl : x = y := by subsingleton
        obtain rfl : g = 𝟙rq _ := by subsingleton
        -- rw below can be avoided if you turn FreeRefl.quotientFunctor into an abbrev.
        -- and then also the simp call works better
        rw [← FreeRefl.quotientFunctor]
        simp only [Paths.of_obj, ↓hrec, Paths.of_map, Functor.map_comp,
          FreeRefl.quotientFunctor_id, Category.comp_id]
        rfl

in Mathlib.CategoryTheory.ReflQuiv, after line 142, (the last proof is certainly golfable...), then with just the right amount of unfolding on hoFunctor it should be doable to prove that hoFunctor.obj (⊤_ SSet.{u}) has a single object and a unique morphism between that single object, provided that you give Unique _ and [∀ (x y : _), Unique (x ⟶ y)] instances on oneTruncation₂ ((truncation 2).obj ⊤_ SSet.{u}), which should hopefully be doable. Then, the thing I mentionned about terminal objects in Cat should finish the thing.
Perhaps for better defeq properties, it might be better to show this for hoFunctor.obj (𝟙_ SSet.{u}) first, and then use an abstract isomorphism with ⊤_ SSet.{u} though.

[Emily Riehl]

@Robin Carlier is this the sort of thing you had in mind?

import Mathlib.CategoryTheory.Category.Cat.Limit
import Mathlib.CategoryTheory.Limits.Shapes.Terminal
import Mathlib.CategoryTheory.PUnit

universe v u v' u'

open CategoryTheory Limits Functor

namespace CategoryTheory

namespace Cat

section
variable {T : Type u} [Category.{v} T] [Unique T] [IsDiscrete T]

/-- The unique functor to the discrete category on a unique object. -/
def toDiscreteUnique (X : Type u') [Category.{v'} X] : X ⥤ T where
  obj := fun _ ↦ default
  map := fun _ ↦ 𝟙 _

/-- Any two functors to a discrete category on a unique object are *equal*. -/
theorem toDiscreteUnique_ext {X : Type u'} [Category.{v'} X] (F G : X ⥤ T) : F = G :=
  Functor.ext fun X => by simp only [eq_iff_true_of_subsingleton]

def isDiscreteUnique.isTerminal : IsTerminal (Cat.of T) :=
  IsTerminal.ofUniqueHom (fun X ↦ toDiscreteUnique (T := T) X)
    (fun _ _ ↦ toDiscreteUnique_ext (T := T) _ _)

end

[Emily Riehl]

I also built some isomorphisms (continuing the above):

/-- Any `T : Cat.{u, u}` with a unique object and discrete homs is isomorphic to `⊤_ Cat.{u, u}.` -/
noncomputable def terminalDiscreteUniqueIso
    {T : Type u} [Category.{u} T] [Unique T] [IsDiscrete T] : ⊤_ Cat.{u, u} ≅ Cat.of T :=
  terminalIsoIsTerminal isDiscreteUnique.isTerminal

/-- The discrete category on `PUnit` is terminal. -/
def DiscretePUnit.isTerminal : IsTerminal (Cat.of (Discrete PUnit)) :=
  isDiscreteUnique.isTerminal

section

variable {T : Type u} [Category.{u} T] (H : IsTerminal (Cat.of T))

/-- Any terminal object `T : Cat.{u, u}` is isomorphic to `Cat.of (Discrete PUnit)`. -/
def isTerminalDiscretePUnitIso : Cat.of T ≅ Cat.of (Discrete PUnit) := by
  refine (IsTerminal.uniqueUpToIso H DiscretePUnit.isTerminal)

end

end Cat

end CategoryTheory

[Emily Riehl]

The code above (your suggestions and my work in progress) is now in a draft PR #25459. I accidentally merged in the other approach (manually constructing a bunch of isomorphisms, without using an abstract characterization of terminal objects). I could prune this or leave it there for reference.

I got stuck on a lot of basic things when constructing the two instances of uniqueness involving one-truncations. Morally these are just types of maps into the terminal object in the simplex category but Lean doesn't agree... :(

[Robin Carlier]

Yes, these kind of lemmas about Cat are what I had in mind.
I took the liberty to push sorry-free versions of the Unique instances on OneTruncation₂ in #25459, which basically works by forcing Lean to see these are "just" maps to a terminal object, feel free to rework it if you want!

[Emily Riehl]

Thanks! Really appreciated. This would have taken me ages (if ever) to sort out.

I've cleaned up the rest of the PR so hopefully it will be ready to review soon. Feel free to make improvements/golf if you are so inspired but if you're ready to move onto other things, please accept my thanks now.

[Adam Topaz]

My inclination would be to prove that the various functors involved preserve limits of the appropriate shape.

[Emily Riehl]

@Robin Carlier the PR you helped me with is now #25781 on my fork. I had trouble with a few of the suggested changes, one of which I'm hoping you can help me with.

Joël suggested changing abbrev FreeRefl.quotientFunctor back to a def, but this breaks the instance

instance (V : Type*) [ReflQuiver V] [Unique V]
    [∀ (x y : V), Unique (x ⟶ y)] (x y : FreeRefl V) :
    Unique (x ⟶ y) where

in a way I don't understand. Supposedly the issue can be fixed by adding simp lemmas but I don't know how to figure out what statements would help.

[Robin Carlier]

I think the simp lemmas that we'd want from this def are already here (there’s just one and it’s FreeRefl.quotientFunctor_id).

I think the issue here is that we’re calling Quotient.induction, which creates goal using Quotient.functor .... I suggested making FreeRefl.quotientFunctor and abbrev so that it unifies with Quotient.functor.

So either we need a special induction principle for FreeReflQuiver (really, just a restatement/translation of the one for quotients), or, alternatively, immediately after calling Quotient.induction we can get everything back in the FreeRefl.quotientFunctorlanguage via a rewrite.
This diff should be working (works on my end at least).

diff --git a/Mathlib/CategoryTheory/Category/ReflQuiv.lean b/Mathlib/CategoryTheory/Category/ReflQuiv.lean
index 36935d8b291..0d8582630f2 100644
--- a/Mathlib/CategoryTheory/Category/ReflQuiv.lean
+++ b/Mathlib/CategoryTheory/Category/ReflQuiv.lean
@@ -129,7 +129,7 @@ instance (V) [ReflQuiver V] : Category (FreeRefl V) :=

 /-- The quotient functor associated to a quotient category defines a natural map from the free
 category on the underlying quiver of a refl quiver to the free category on the reflexive quiver. -/
-abbrev FreeRefl.quotientFunctor (V) [ReflQuiver V] : Paths V ⥤ FreeRefl V :=
+def FreeRefl.quotientFunctor (V) [ReflQuiver V] : Paths V ⥤ FreeRefl V :=
   Quotient.functor (C := Paths V) (FreeReflRel (V := V))

 /-- This is a specialization of `Quotient.lift_unique'` rather than `Quotient.lift_unique`, hence
@@ -156,6 +156,7 @@ instance (V : Type*) [ReflQuiver V] [Unique V]
   uniq f := by
     letI : Unique (Paths V) := inferInstanceAs (Unique V)
     induction f using Quotient.induction with | @h x y f =>
+    rw [← FreeRefl.quotientFunctor]
     symm
     induction f using Paths.induction with
     | id =>

[Robin Carlier]

Writing an induction principle specially for FreeRefl (combining Paths.Induction and Quotient.Induction) is probably the more principled approach though, it’s a bit longer but it’s what you want to go for if you intend to prove more stuff about FreeRefl.

[Robin Carlier]

I’m noticing that we also don’t have special induction principles for HomotopyCategory (at least I did not see any around the definition), FreeRefl is a bit of an intermediary construction but I think we definitely want some quality of life principles around HomotopyCategory. I’ll try writing one this weekend if I find the time.

[Emily Riehl]

Thanks both for the solution and for the explanation.

I'm about to go offline for a few days so I opted for the less principled more efficient solution. But I agree that having some quality of life principles for homotopy category would be great. We're about to have a strict bicategory of quasi-categories whose hom-categories are homotopy categories. I'd like to some day be able to calculate the 1-cells and 2-cells!