feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case) (#18137)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: joelriou

Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean

@@ -9,7 +9,7 @@ import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 # Uniqueness of morphisms in the category of iterations of functors
 
 Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`,
-we shall show in this file that there exists a unique morphism (TODO)
+we show in this file that there exists a unique morphism
 between two arbitrary objects in the category `Functor.Iteration ε j`
 when `j : J` and `J` is a well orderered set.
 
@@ -30,8 +30,6 @@ namespace Iteration
 
 namespace Hom
 
-variable (j : J)
-
 /-- The (unique) morphism between two objects in `Iteration ε ⊥` -/
 def mkOfBot (iter₁ iter₂ : Iteration ε (⊥ : J)) : iter₁ ⟶ iter₂ where
   natTrans :=
@@ -136,8 +134,114 @@ noncomputable def mkOfSucc
       rfl
     · simp [mkOfSuccNatTransApp_eq_of_le hi φ k (by rfl)]
 
+variable {j : J} {iter₁ iter₂ : Iteration ε j}
+
+section
+
+variable (φ : ∀ (i : J) (hi : i < j), iter₁.trunc hi.le ⟶ iter₂.trunc hi.le)
+  [WellFoundedLT J] (hj : Order.IsSuccLimit j)
+
+/-- Auxiliary definition for `mkOfLimit`. -/
+def mkOfLimitNatTransApp (i : J) (hi : i ≤ j) :
+    iter₁.F.obj ⟨i, hi⟩ ⟶ iter₂.F.obj ⟨i, hi⟩ :=
+  if h : i < j
+    then
+      (φ i h).natTrans.app ⟨i, by simp⟩
+    else by
+      obtain rfl : i = j := by
+        obtain h' | rfl := hi.lt_or_eq
+        · exfalso
+          exact h h'
+        · rfl
+      exact (iter₁.isColimit i hj (by simp)).desc (Cocone.mk _
+        { app := fun ⟨k, hk⟩ => (φ k hk).natTrans.app ⟨k, by simp⟩ ≫
+            iter₂.F.map (homOfLE (by exact hk.le))
+          naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by
+            have hf : k₁ ≤ k₂ := by simpa using leOfHom f
+            dsimp
+            rw [comp_id, congr_app (φ k₁ hk₁) ((truncFunctor ε hf).map (φ k₂ hk₂))]
+            erw [natTrans_naturality_assoc (φ k₂ hk₂) k₁ k₂ hf (by rfl)]
+            dsimp
+            rw [← Functor.map_comp, homOfLE_comp] })
+
+lemma mkOfLimitNatTransApp_eq_of_lt (i : J) (hi : i < j) :
+    mkOfLimitNatTransApp φ hj i hi.le = (φ i hi).natTrans.app ⟨i, by simp⟩ :=
+  dif_pos hi
+
+lemma mkOfLimitNatTransApp_naturality_top (i : J) (hi : i < j) :
+    iter₁.F.map (homOfLE (by simpa using hi.le) : ⟨i, hi.le⟩ ⟶ ⟨j, by simp⟩) ≫
+      mkOfLimitNatTransApp φ hj j (by rfl) =
+      mkOfLimitNatTransApp φ hj i hi.le ≫ iter₂.F.map (homOfLE (by simpa using hi.le)) := by
+  rw [mkOfLimitNatTransApp_eq_of_lt φ hj i hi, mkOfLimitNatTransApp, dif_neg (by simp)]
+  exact (iter₁.isColimit j hj (by rfl)).fac _ ⟨i, hi⟩
+
+/-- Auxiliary definition for `mkOfLimit`. -/
+@[simps]
+def mkOfLimitNatTrans : iter₁.F ⟶ iter₂.F where
+  app := fun ⟨k, hk⟩ => mkOfLimitNatTransApp φ hj k hk
+  naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by
+    have hk : k₁ ≤ k₂ := leOfHom f
+    obtain h₂ | rfl := hk₂.lt_or_eq
+    · dsimp
+      rw [mkOfLimitNatTransApp_eq_of_lt _ hj k₂ h₂,
+        mkOfLimitNatTransApp_eq_of_lt _ hj k₁ (lt_of_le_of_lt hk h₂),
+        congr_app (φ k₁ (lt_of_le_of_lt hk h₂)) ((truncFunctor ε hk).map (φ k₂ h₂))]
+      exact natTrans_naturality (φ k₂ h₂) k₁ k₂ hk (by rfl)
+    · obtain h₁ | rfl := hk₁.lt_or_eq
+      · exact mkOfLimitNatTransApp_naturality_top _ hj _ h₁
+      · obtain rfl : f = 𝟙 _ := rfl
+        simp only [map_id, id_comp, comp_id]
+
+/-- The (unique) morphism between two objects in `Iteration ε j` when `j` is a limit element,
+assuming we have a morphism between the truncations to `Iteration ε i` for all `i < j`. -/
+def mkOfLimit : iter₁ ⟶ iter₂ where
+  natTrans := mkOfLimitNatTrans φ hj
+  natTrans_app_zero := by
+    simp [mkOfLimitNatTransApp_eq_of_lt φ _ ⊥ (by simpa only [bot_lt_iff_ne_bot] using hj.ne_bot)]
+  natTrans_app_succ i h := by
+    dsimp
+    have h' := hj.succ_lt h
+    rw [mkOfLimitNatTransApp_eq_of_lt φ hj _ h',
+      (φ _ h').natTrans_app_succ i (Order.lt_succ_of_not_isMax (not_isMax_of_lt h)),
+      mkOfLimitNatTransApp_eq_of_lt φ _ _ h,
+      congr_app (φ i h) ((truncFunctor ε (Order.le_succ i)).map (φ (Order.succ i) h'))]
+    dsimp
+
+end
+
+variable [WellFoundedLT J]
+
+instance : Nonempty (iter₁ ⟶ iter₂) := by
+  let P := fun (i : J) => ∀ (hi : i ≤ j),
+    Nonempty ((truncFunctor ε hi).obj iter₁ ⟶ (truncFunctor ε hi).obj iter₂)
+  suffices ∀ i, P i from this j (by rfl)
+  intro i
+  induction i using SuccOrder.limitRecOn with
+  | hm i hi =>
+    obtain rfl : i = ⊥ := by simpa using hi
+    exact fun hi' ↦ ⟨Hom.mkOfBot _ _⟩
+  | hs i hi hi' =>
+    exact fun hi'' ↦ ⟨Hom.mkOfSucc _ _ hi (hi' ((Order.le_succ i).trans hi'')).some⟩
+  | hl i hi hi' =>
+    exact fun hi'' ↦ ⟨Hom.mkOfLimit (fun k hk ↦ (hi' k hk (hk.le.trans hi'')).some) hi⟩
+
+noncomputable instance : Unique (iter₁ ⟶ iter₂) :=
+  uniqueOfSubsingleton (Nonempty.some inferInstance)
+
 end Hom
 
+variable [WellFoundedLT J] {j : J} (iter₁ iter₂ iter₃ : Iteration ε j)
+
+/-- The canonical isomorphism between two objects in the category `Iteration ε j`. -/
+noncomputable def iso : iter₁ ≅ iter₂ where
+  hom := default
+  inv := default
+
+@[simp]
+lemma iso_refl : iso iter₁ iter₁ = Iso.refl _ := by aesop_cat
+
+lemma iso_trans : iso iter₁ iter₂ ≪≫ iso iter₂ iter₃ = iso iter₁ iter₃ := by aesop_cat
+
 end Iteration
 
 end Functor