diff --git a/Mathlib.lean b/Mathlib.lean index 25b6753d6ca64..6eb498aa7d06b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2178,8 +2178,8 @@ import Mathlib.CategoryTheory.SmallObject.Construction import Mathlib.CategoryTheory.SmallObject.Iteration.Basic import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone +import Mathlib.CategoryTheory.SmallObject.Iteration.Iteration import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty -import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom import Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting import Mathlib.CategoryTheory.SmallObject.WellOrderInductionData import Mathlib.CategoryTheory.Square diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean index d739917e114af..2c101474727ed 100644 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean @@ -4,54 +4,65 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ import Mathlib.CategoryTheory.Category.Preorder -import Mathlib.CategoryTheory.Limits.IsLimit +import Mathlib.CategoryTheory.Limits.HasLimits import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Order.SuccPred.Limit -/-! # Transfinite iterations of a functor - -In this file, given a functor `Φ : C ⥤ C` and a natural transformation -`ε : 𝟭 C ⟶ Φ`, we shall define the transfinite iterations of `Φ` (TODO). - -Given `j : J` where `J` is a well ordered set, we first introduce -a category `Iteration ε j`. An object in this category consists of -a functor `F : Set.Iic j ⥤ C ⥤ C` equipped with the data -which makes it the `i`th-iteration of `Φ` for all `i` such that `i ≤ j`. -Under suitable assumptions on `C`, we shall show that this category -`Iteration ε j` is equivalent to the punctual category (TODO). -In this file, we show that the there is at most one morphism between -two objects. In `SmallObject.Iteration.UniqueHom`, we shall show -that there does always exist a unique morphism between -two objects (TODO). Then, we shall show the existence of -an object (TODO). In these proofs, which are all done using -transfinite induction, we have to treat three cases separately: -* the case `j = ⊥`; -* the case `j` is a successor; -* the case `j` is a limit element. +/-! # Transfinite iterations of a construction + +In this file, we introduce the structure `SuccStruct` on a category `C`. +It consists of the data of an object `X₀ : C`, a successor map `succ : C → C` +and a morphism `toSucc : X ⟶ succ X` for any `X : C`. The map `toSucc` +does not have to be natural in `X`. For any element `j : J` in +well-ordered type `J`, we would like to define +the iteration of `Φ : SuccStruct C`, as a functor `F : J ⥤ C` +such that `F.obj ⊥ = X₀`, `F.obj j ⟶ F.obj (Order.succ j)` is `toSucc (F.obj j)` +when `j` is not maximal, and when `j` is limit, `F.obj j` should be the +colimit of the `F.obj k` for `k < j`. + +In the small object argument, we shall apply this to the iteration of +a functor `F : C ⥤ C` equipped with a natural transformation `ε : 𝟭 C ⟶ F`: +this will correspond to the case of +`SuccStruct.ofTrans ε : SuccStruct (C ⥤ C)`, for which `X₀ := 𝟭 C`, +`succ G := G ⋙ F` and `toSucc G : G ⟶ G ⋙ F` is given by `whiskerLeft G ε`. + +The construction of the iteration of `Φ : SuccStruct C` is done +by transfinite induction, under an assumption `HasIterationOfShape C J`. +However, for a limit element `j : J`, the definition of `F.obj j` +does not involve only the objects `F.obj i` for `i < j`, but it also +involves the maps `F.obj i₁ ⟶ F.obj i₂` for `i₁ ≤ i₂ < j`. +Then, this is a straightforward application of definitions by +transfinite induction. In order to solve this technical difficulty, +we introduce a structure `Φ.Iteration j` for any `j : J`. This +structure contains all the expected data and properties for +all the indices that are `≤ j`. In this file, we show that +`Φ.Iteration j` is a subsingleton. The uniqueness shall ne +obtained in the file `SmallObject.Iteration.Nonempty`, and +the construction of the functor `Φ.iterationFunctor J : J ⥤ C` +and of its colimit `Φ.iteration J : C` is done in the +file `SmallObject.Iteration.Iteration`. + +The map `Φ.toSucc X : X ⟶ Φ.succ X` does not have to be natural +(and it is not in certain applications). Then, two isomorphic +objects `X` and `Y` may have non isomorphic successors. This is +the reason why we make an extensive use of equalities of objects +in the definitions. -/ -universe u +universe w v u namespace CategoryTheory open Category Limits -variable {C : Type*} [Category C] {Φ : C ⥤ C} (ε : 𝟭 C ⟶ Φ) {J : Type u} +variable {C : Type u} [Category.{v} C] {J : Type w} -namespace Functor +namespace SmallObject -namespace Iteration - -variable [Preorder J] {j : J} (F : Set.Iic j ⥤ C) - -/-- The map `F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩` when `F : Set.Iic j ⥤ C` -and `i : J` is such that `i < j`. -/ -noncomputable abbrev mapSucc' [SuccOrder J] (i : J) (hi : i < j) : - F.obj ⟨i, hi.le⟩ ⟶ F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ := - F.map <| homOfLE <| Subtype.mk_le_mk.2 <| Order.le_succ i +section -variable {i : J} (hi : i ≤ j) +variable [Preorder J] {j : J} (F : Set.Iic j ⥤ C) {i : J} (hi : i ≤ j) /-- The functor `Set.Iio i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C` when `i ≤ j`. -/ @@ -89,187 +100,280 @@ lemma restrictionLE_obj (k : J) (hk : k ≤ i) : lemma restrictionLE_map {k₁ k₂ : Set.Iic i} (φ : k₁ ⟶ k₂) : (restrictionLE F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl -end Iteration - -/-- The category of `j`th iterations of a functor `Φ` equipped with a natural -transformation `ε : 𝟭 C ⟶ Φ`. An object consists of the data of all iterations -of `Φ` for `i : J` such that `i ≤ j` (this is the field `F`). Such objects are -equipped with data and properties which characterizes the iterations up to a unique -isomorphism for the three types of elements: `⊥`, successors, limit elements. -/ -structure Iteration [Preorder J] [OrderBot J] [SuccOrder J] (j : J) where - /-- The data of all `i`th iterations for `i : J` such that `i ≤ j`. -/ - F : Set.Iic j ⥤ C ⥤ C - /-- The zeroth iteration is the identity functor. -/ - isoZero : F.obj ⟨⊥, bot_le⟩ ≅ 𝟭 C - /-- The iteration on a successor element is obtained by composition of - the previous iteration with `Φ`. -/ - isoSucc (i : J) (hi : i < j) : F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅ F.obj ⟨i, hi.le⟩ ⋙ Φ - /-- The natural map from an iteration to its successor is induced by `ε`. -/ - mapSucc'_eq (i : J) (hi : i < j) : - Iteration.mapSucc' F i hi = whiskerLeft _ ε ≫ (isoSucc i hi).inv - /-- If `i` is a limit element, the `i`th iteration is the colimit - of `k`th iterations for `k < i`. -/ - isColimit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : - IsColimit (Iteration.coconeOfLE F hij) - -namespace Iteration - -variable {ε} -variable {j : J} - -section - -variable [Preorder J] [OrderBot J] [SuccOrder J] (iter : Φ.Iteration ε j) - -/-- For `iter : Φ.Iteration.ε j`, this is the map -`iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨Order.succ i, _⟩` if `i : J` is such that `i < j`. -/ -noncomputable abbrev mapSucc (i : J) (hi : i < j) : - iter.F.obj ⟨i, hi.le⟩ ⟶ iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ := - mapSucc' iter.F i hi - -lemma mapSucc_eq (i : J) (hi : i < j) : - iter.mapSucc i hi = whiskerLeft _ ε ≫ (iter.isoSucc i hi).inv := - iter.mapSucc'_eq _ hi - end section -variable [Preorder J] [OrderBot J] [SuccOrder J] (iter₁ iter₂ : Φ.Iteration ε j) - -/-- A morphism between two objects `iter₁` and `iter₂` in the -category `Φ.Iteration ε j` of `j`th iterations of a functor `Φ` -equipped with a natural transformation `ε : 𝟭 C ⟶ Φ` consists of a natural -transformation `natTrans : iter₁.F ⟶ iter₂.F` which is compatible with the -isomorphisms `isoZero` and `isoSucc`. -/ -structure Hom where - /-- A natural transformation `iter₁.F ⟶ iter₂.F` -/ - natTrans : iter₁.F ⟶ iter₂.F - natTrans_app_zero : - natTrans.app ⟨⊥, bot_le⟩ = iter₁.isoZero.hom ≫ iter₂.isoZero.inv := by aesop_cat - natTrans_app_succ (i : J) (hi : i < j) : - natTrans.app ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = (iter₁.isoSucc i hi).hom ≫ - whiskerRight (natTrans.app ⟨i, hi.le⟩) _ ≫ (iter₂.isoSucc i hi).inv := by aesop_cat - -namespace Hom +variable [Preorder J] -attribute [simp, reassoc] natTrans_app_zero +variable (C J) in +/-- A category `C` has iterations of shape `J` when certain shapes +of colimits exists. When `J` is well ordered, this assumption is used in +order to show that the category `Iteration ε j` is nonempty for any `j : J`, +see the file `CategoryTheory.SmallObject.Nonempty`. -/ +class HasIterationOfShape : Prop where + hasColimitsOfShape_of_isSuccLimit (j : J) (hj : Order.IsSuccLimit j) : + HasColimitsOfShape (Set.Iio j) C := by infer_instance + hasColimitsOfShape : HasColimitsOfShape J C := by infer_instance -/-- The identity morphism in the category `Φ.Iteration ε j`. -/ -@[simps] -def id : Hom iter₁ iter₁ where - natTrans := 𝟙 _ - -variable {iter₁ iter₂} +attribute [instance] HasIterationOfShape.hasColimitsOfShape --- Note: this is not made a global ext lemma because it is shown below --- that the type of morphisms is a subsingleton. -lemma ext' {f g : Hom iter₁ iter₂} (h : f.natTrans = g.natTrans) : f = g := by - cases f - cases g - subst h - rfl +variable (C) in +lemma hasColimitOfShape_of_isSuccLimit [HasIterationOfShape C J] (j : J) + (hj : Order.IsSuccLimit j) : + HasColimitsOfShape (Set.Iio j) C := + HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit j hj -attribute [local ext] ext' +end -/-- The composition of morphisms in the category `Iteration ε j`. -/ +variable (C) in +/-- A successor structure () on a category consists of the +data of an object `succ X` for any `X : C`, a map `toSucc X : X ⟶ toSucc X` +(which does not need to be natural), and a zeroth object `X₀`. +-/ +structure SuccStruct where + /-- the zeroth object -/ + X₀ : C + /-- the successor of an object -/ + succ (X : C) : C + /-- the map to the successor -/ + toSucc (X : C) : X ⟶ succ X + +namespace SuccStruct + +/-- Given a functor `Φ : C ⥤ C`, a natural transformation of the form `𝟭 C ⟶ Φ` +induces a successor structure. -/ @[simps] -def comp {iter₃ : Iteration ε j} (f : Hom iter₁ iter₂) (g : Hom iter₂ iter₃) : - Hom iter₁ iter₃ where - natTrans := f.natTrans ≫ g.natTrans - natTrans_app_succ i hi := by simp [natTrans_app_succ _ _ hi] - -instance : Category (Iteration ε j) where - Hom := Hom - id := id - comp := comp - -instance {J} {j : J} [PartialOrder J] [OrderBot J] [WellFoundedLT J] [SuccOrder J] - {iter₁ iter₂ : Iteration ε j} : - Subsingleton (iter₁ ⟶ iter₂) where - allEq f g := by - apply ext' - suffices ∀ i hi, f.natTrans.app ⟨i, hi⟩ = g.natTrans.app ⟨i, hi⟩ by - ext ⟨i, hi⟩ : 2 - apply this - intro i - induction i using SuccOrder.limitRecOn with - | hm j H => - obtain rfl := H.eq_bot - simp [natTrans_app_zero] - | hs j H IH => - intro hj - simp [Hom.natTrans_app_succ, IH, (Order.lt_succ_of_not_isMax H).trans_le hj] - | hl j H IH => - refine fun hj ↦ (iter₁.isColimit j H hj).hom_ext ?_ - rintro ⟨k, hk⟩ - simp [IH k hk] - -end Hom +def ofNatTrans {F : C ⥤ C} (ε : 𝟭 C ⟶ F) : SuccStruct (C ⥤ C) where + succ G := G ⋙ F + toSucc G := whiskerLeft G ε + X₀ := 𝟭 C -@[simp] -lemma natTrans_id : Hom.natTrans (𝟙 iter₁) = 𝟙 _ := rfl +lemma congr_toSucc (Φ : SuccStruct C) {X Y : C} (h : X = Y) : + Φ.toSucc X = eqToHom (by rw [h]) ≫ Φ.toSucc Y ≫ eqToHom (by rw [h]) := by + subst h + simp + +variable (Φ : SuccStruct C) [LinearOrder J] [OrderBot J] [SuccOrder J] + [HasIterationOfShape C J] + +/-- The category of `j`th iterations of a succesor structure `Φ : SuccStruct C`. +An object consists of the data of all iterations of `Φ` for `i : J` such +that `i ≤ j` (this is the field `F`). Such objects are +equipped with data and properties which characterizes uniquely the iterations +on three types of elements: `⊥`, successors, limit elements. -/ +@[ext] +structure Iteration [WellFoundedLT J] (j : J) where + /-- The data of all `i`th iterations for `i : J` such that `i ≤ j`. -/ + F : Set.Iic j ⥤ C + /-- The zeroth iteration is the zeroth object . -/ + obj_bot : F.obj ⟨⊥, bot_le⟩ = Φ.X₀ + /-- The iteration on a successor element identifies to the successor. -/ + obj_succ (i : J) (hi : i < j) : + F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = Φ.succ (F.obj ⟨i, hi.le⟩) + /-- The natural map from an iteration to its successor is induced by `toSucc`. -/ + map_succ (i : J) (hi : i < j) : + F.map (homOfLE (Order.le_succ i) : ⟨i, hi.le⟩ ⟶ ⟨Order.succ i, Order.succ_le_of_lt hi⟩) = + Φ.toSucc _ ≫ eqToHom (by rw [obj_succ _ hi]) + /-- If `i` is a limit element, the `i`th iteration is the colimit + of `k`th iterations for `k < i`. -/ + obj_limit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : + letI := hasColimitOfShape_of_isSuccLimit C i hi + F.obj ⟨i, hij⟩ = colimit (restrictionLT F hij) + map_eq_ι (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) + (k : J) (hk : k < i) : + letI := hasColimitOfShape_of_isSuccLimit C i hi + F.map (homOfLE hk.le : ⟨k, hk.le.trans hij⟩ ⟶ ⟨i, hij⟩) = + colimit.ι (restrictionLT F hij) ⟨k, hk⟩ ≫ + eqToHom (by rw [obj_limit i hi]) + +variable [WellFoundedLT J] -variable {iter₁ iter₂} +namespace Iteration -@[simp, reassoc] -lemma natTrans_comp {iter₃ : Iteration ε j} (φ : iter₁ ⟶ iter₂) (ψ : iter₂ ⟶ iter₃) : - (φ ≫ ψ).natTrans = φ.natTrans ≫ ψ.natTrans := rfl +variable {Φ} +variable {j : J} -@[reassoc] -lemma natTrans_naturality (φ : iter₁ ⟶ iter₂) (i₁ i₂ : J) (h : i₁ ≤ i₂) (h' : i₂ ≤ j) : - iter₁.F.map (by exact homOfLE h) ≫ φ.natTrans.app ⟨i₂, h'⟩ = - φ.natTrans.app ⟨i₁, h.trans h'⟩ ≫ iter₂.F.map (by exact homOfLE h) := by - apply φ.natTrans.naturality +section -variable (ε) in -/-- The evaluation functor `Iteration ε j ⥤ C ⥤ C` at `i : J` when `i ≤ j`. -/ -@[simps] -def eval {i : J} (hi : i ≤ j) : Iteration ε j ⥤ C ⥤ C where - obj iter := iter.F.obj ⟨i, hi⟩ - map φ := φ.natTrans.app _ - -/-- Given `iter : Iteration ε j` and `i : J` such that `i ≤ j`, this is the -induced element in `Iteration ε i`. -/ -@[simps F isoZero isoSucc] -def trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) : Iteration ε i where +variable (iter : Φ.Iteration j) + +/-- The isomorphism `iter.F.obj ⟨⊥, bot_le⟩ ≅ Φ.X₀`. -/ +def isoBot : iter.F.obj ⟨⊥, bot_le⟩ ≅ Φ.X₀ := + eqToIso (by rw [obj_bot]) + +/-- The object `iter.F.obj ⟨Order.succ i, _⟩` identifies to +the successor of `iter.F.obj ⟨i, _⟩` when `i < j`. -/ +def isoSucc (i : J) (hi : i < j) : + iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅ + Φ.succ (iter.F.obj ⟨i, hi.le⟩) := + eqToIso (by rw [obj_succ _ i hi]) + +/-- Variant of `map_succ'` involving the isomorphism `isoSucc`. -/ +lemma map_succ' (i : J) (hi : i < j) : + iter.F.map (homOfLE (Order.le_succ i) : + ⟨i, hi.le⟩ ⟶ ⟨Order.succ i, Order.succ_le_of_lt hi⟩) = + Φ.toSucc _ ≫ (iter.isoSucc i hi).inv := + iter.map_succ i hi + +/-- When `i : J` is limit, `iter.F.obj ⟨i, _⟩` identifies +to the colimit of the restriction of `iter.F` to `Set.Iio i`. -/ +noncomputable def isColimit (i : J) + (hi : Order.IsSuccLimit i) (hij : i ≤ j) : + IsColimit (coconeOfLE iter.F hij) := by + have := hasColimitOfShape_of_isSuccLimit C i hi + exact IsColimit.ofIsoColimit (colimit.isColimit _) + (Cocones.ext (eqToIso (iter.obj_limit i hi hij).symm) + (fun ⟨k, hk⟩ ↦ (iter.map_eq_ι i hi hij k hk).symm)) + +/-- The element in `Φ.Iteration i` that is deduced from an element +in `Φ.Iteration j` when `i ≤ j`. -/ +@[simps F] +def trunc (iter : Φ.Iteration j) {i : J} (hi : i ≤ j) : Φ.Iteration i where F := restrictionLE iter.F hi - isoZero := iter.isoZero - isoSucc k hk := iter.isoSucc k (lt_of_lt_of_le hk hi) - mapSucc'_eq k hk := iter.mapSucc'_eq k (lt_of_lt_of_le hk hi) - isColimit k hk' hk := iter.isColimit k hk' (hk.trans hi) - -variable (ε) in -/-- The truncation functor `Iteration ε j ⥤ Iteration ε i` when `i ≤ j`. -/ -@[simps obj] -def truncFunctor {i : J} (hi : i ≤ j) : Iteration ε j ⥤ Iteration ε i where - obj iter := iter.trunc hi - map {iter₁ iter₂} φ := - { natTrans := whiskerLeft _ φ.natTrans - natTrans_app_succ := fun k hk => φ.natTrans_app_succ k (lt_of_lt_of_le hk hi) } - -@[simp] -lemma truncFunctor_map_natTrans_app - (φ : iter₁ ⟶ iter₂) {i : J} (hi : i ≤ j) (k : J) (hk : k ≤ i) : - ((truncFunctor ε hi).map φ).natTrans.app ⟨k, hk⟩ = - φ.natTrans.app ⟨k, hk.trans hi⟩ := rfl + obj_bot := iter.obj_bot + obj_succ k hk := iter.obj_succ k (lt_of_lt_of_le hk hi) + obj_limit k hk hk' := iter.obj_limit k hk (hk'.trans hi) + map_succ k hk := iter.map_succ k (lt_of_lt_of_le hk hi) + map_eq_ι k hk hki l hl := iter.map_eq_ι k hk (hki.trans hi) l hl end -namespace Hom - -variable [PartialOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] - {iter₁ iter₂ : Φ.Iteration ε j} - -lemma congr_app (φ φ' : iter₁ ⟶ iter₂) (i : J) (hi : i ≤ j) : - φ.natTrans.app ⟨i, hi⟩ = φ'.natTrans.app ⟨i, hi⟩ := by - obtain rfl := Subsingleton.elim φ φ' - rfl - -end Hom +omit [OrderBot J] [SuccOrder J] [WellFoundedLT J] in +lemma congr_colimit_ι {F G : Set.Iio j ⥤ C} (h : F = G) (hj : Order.IsSuccLimit j) + (i : Set.Iio j) : + letI := hasColimitOfShape_of_isSuccLimit C j hj + colimit.ι F i = by + refine eqToHom (by rw [h]) ≫ colimit.ι G i ≫ eqToHom (by rw [h]) := by + subst h + simp + +/-! Auxiliary definitions for the proof of `Subsingleton (Φ.Iteration j)`. -/ + +namespace subsingleton + +variable {F G : Set.Iic j ⥤ C} (hobj : F.obj = G.obj) + +omit [OrderBot J] [SuccOrder J] [WellFoundedLT J] + +/-- Given two functors `Set.Iic j ⥤ C` that are equal on objects, +this is the condition that they coincide on a given map. -/ +def MapEq (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j) : Prop := + F.map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩) = + eqToHom (by rw [hobj]) ≫ + G.map (homOfLE h₁₂ : ⟨i₁, _⟩ ⟶ ⟨i₂, _⟩) ≫ eqToHom (by rw [hobj]) + +omit [HasIterationOfShape C J] in +lemma mapEq_of_eq {k : J} (hkj : k ≤ j) (h : restrictionLE F hkj = restrictionLE G hkj) + (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ k) : + MapEq hobj i₁ i₂ h₁₂ (h₂.trans hkj) := by + exact Functor.congr_hom h (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩) + +omit [HasIterationOfShape C J] + +lemma mapEq_rfl (i : J) (h : i ≤ j) : MapEq hobj i i (by simp) h := by + simp [MapEq] + +variable {hobj} in +lemma mapEq_trans {i₁ i₂ i₃ : J} (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) {h₃ : i₃ ≤ j} + (m₁₂ : MapEq hobj i₁ i₂ h₁₂ (h₂₃.trans h₃)) (m₂₃ : MapEq hobj i₂ i₃ h₂₃ h₃) : + MapEq hobj i₁ i₃ (h₁₂.trans h₂₃) h₃ := by + dsimp [MapEq] at m₁₂ m₂₃ ⊢ + rw [← homOfLE_comp (X := Set.Iic j) (x := ⟨i₁, _⟩) + (y := ⟨i₂, h₂₃.trans h₃⟩) (z := ⟨i₃, _⟩) h₁₂ h₂₃, Functor.map_comp, + Functor.map_comp, m₁₂, m₂₃] + simp + +lemma functor_eq (hmap : ∀ (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j), MapEq hobj i₁ i₂ h₁₂ h₂) : + F = G := + Functor.ext (by simp [hobj]) (by + rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f + exact hmap i₁ i₂ (leOfHom f) h₂) + +end subsingleton + +open subsingleton in +instance subsingleton : Subsingleton (Φ.Iteration j) where + allEq iter₁ iter₂ := by + suffices iter₁.F = iter₂.F by aesop + revert iter₁ iter₂ + induction j using SuccOrder.limitRecOn with + | hm j h => + intro iter₁ iter₂ + obtain rfl := h.eq_bot + fapply Functor.ext + · rintro ⟨i, hi⟩ + obtain rfl : i = ⊥ := by simpa using hi + simp only [obj_bot] + · rintro ⟨i, hi⟩ ⟨i', hi'⟩ f + obtain rfl : i = ⊥ := by simpa using hi + obtain rfl : i' = ⊥ := by simpa using hi' + obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _ + simp + | hs j hj₁ hj₂ => + intro iter₁ iter₂ + have hobj : iter₁.F.obj = iter₂.F.obj := by + ext ⟨i, hi⟩ + wlog h : i ≤ j generalizing i + · obtain hi | rfl := hi.lt_or_eq + · exact this _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).mp hi) + · simp only [obj_succ _ _ (Order.lt_succ_of_not_isMax hj₁), this _ _ (by rfl)] + exact Functor.congr_obj (hj₂ (iter₁.trunc (Order.le_succ _)) + (iter₂.trunc (Order.le_succ _))) ⟨i, h⟩ + have hsucc : MapEq hobj _ _ (Order.le_succ j) (by simp) := by + simp only [MapEq, map_succ _ _ (Order.lt_succ_of_not_isMax hj₁), + Φ.congr_toSucc (congr_fun hobj ⟨j, _⟩), assoc, eqToHom_trans] + apply functor_eq hobj + intro i₁ i₂ + wlog hi₂ : i₂ ≤ j generalizing i₂ + · intro h₁₂ h₂ + obtain h₂ | rfl := h₂.lt_or_eq + · exact (hi₂ ((Order.lt_succ_iff_of_not_isMax hj₁).mp h₂)).elim + · by_cases hi₁ : i₁ ≤ j + · exact mapEq_trans _ _ (this j (by simp) hi₁ (Order.le_succ j)) hsucc + · obtain rfl : i₁ = Order.succ j := + le_antisymm h₁₂ ((Order.succ_le_iff_of_not_isMax hj₁).mpr (by simpa using hi₁)) + apply mapEq_rfl + intro h₁₂ h₂ + exact mapEq_of_eq hobj (Order.le_succ j) + (hj₂ (iter₁.trunc (Order.le_succ j)) (iter₂.trunc (Order.le_succ j))) _ _ _ hi₂ + | hl j h₁ h₂ => + intro iter₁ iter₂ + have hobj : iter₁.F.obj = iter₂.F.obj := by + ext ⟨i, hi⟩ + wlog h : i < j generalizing i + · obtain rfl : j = i := le_antisymm (by simpa using h) hi + simp only [obj_limit _ _ h₁] + congr 1 + fapply Functor.ext + · rintro ⟨i, hi⟩ + exact this _ _ hi + · rintro ⟨i₁, hi₁⟩ ⟨i₂, hi₂⟩ f + exact Functor.congr_hom (h₂ i₂ hi₂ (iter₁.trunc hi₂.le) (iter₂.trunc hi₂.le)) + (homOfLE (leOfHom f) : ⟨i₁, leOfHom f⟩ ⟶ ⟨i₂, by simp⟩) + exact Functor.congr_obj (h₂ i h (iter₁.trunc h.le) (iter₂.trunc h.le)) ⟨i, by simp⟩ + apply functor_eq hobj + intro i₁ i₂ h₁₂ hi₂ + by_cases h₃ : i₂ < j + · exact mapEq_of_eq hobj hi₂ + (h₂ _ h₃ (iter₁.trunc h₃.le) (iter₂.trunc h₃.le)) _ _ _ (by rfl) + · obtain rfl : j = i₂ := le_antisymm (by simpa using h₃) hi₂ + by_cases h₄ : i₁ < j + · dsimp [MapEq] + have : restrictionLT iter₁.F hi₂ = restrictionLT iter₂.F hi₂ := + Functor.ext (fun k ↦ congr_fun hobj ⟨k.1, k.2.le⟩) (by + rintro ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f + exact Functor.congr_hom (h₂ k₂ hk₂ (iter₁.trunc hk₂.le) (iter₂.trunc hk₂.le)) + (homOfLE (leOfHom f) : ⟨k₁, leOfHom f⟩ ⟶ ⟨k₂, by simp⟩)) + simp only [map_eq_ι _ _ h₁ _ _ h₄, assoc, eqToHom_trans, + congr_colimit_ι this h₁] + · obtain rfl : i₁ = j := le_antisymm h₁₂ (by simpa using h₄) + exact mapEq_rfl hobj i₁ hi₂ end Iteration -end Functor +end SuccStruct + +end SmallObject end CategoryTheory diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean index 166469022df52..634e98a242ca7 100644 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean @@ -20,7 +20,7 @@ universe u namespace CategoryTheory -open Category +open Category SmallObject namespace Functor @@ -37,14 +37,22 @@ it sends `Order.succ j` to the given object `X`. -/ def obj (i : Set.Iic (Order.succ j)) : C := if hij : i.1 ≤ j then F.obj ⟨i.1, hij⟩ else X +lemma obj_eq (i : Set.Iic j) : + obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ = F.obj i := dif_pos i.2 + /-- The isomorphism `obj F X ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j`. -/ def objIso (i : Set.Iic j) : - obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := eqToIso (dif_pos i.2) + obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := + eqToIso (obj_eq _ _ _) + +include hj in +lemma obj_succ_eq : obj F X ⟨Order.succ j, by simp⟩ = X := + dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj) /-- The isomorphism `obj F X ⟨Order.succ j, _⟩ ≅ X`. -/ def objSuccIso : obj F X ⟨Order.succ j, by simp⟩ ≅ X := - eqToIso (dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj)) + eqToIso (obj_succ_eq hj _ _) variable {X} @@ -116,11 +124,19 @@ def extendToSucc : Set.Iic (Order.succ j) ⥤ C where map_id _ := extendToSucc.map_id _ F τ _ _ map_comp {i₁ i₂ i₃} f g := extendToSucc.map_comp hj F τ i₁ i₂ i₃ (leOfHom f) (leOfHom g) i₃.2 +lemma extendToSucc_obj_eq (i : Set.Iic j) : + (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ = F.obj i := + extendToSucc.obj_eq F X i + /-- The isomorphism `(extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j` -/ def extendToSuccObjIso (i : Set.Iic j) : (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := extendToSucc.objIso F X i +lemma extendToSucc_obj_succ_eq : + (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ = X := + extendToSucc.obj_succ_eq hj F X + /-- The isomorphism `(extendToSucc hj F τ).obj ⟨Order.succ j, _⟩ ≅ X`. -/ def extendToSuccObjSuccIso : (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ ≅ X := @@ -138,12 +154,12 @@ lemma extendToSuccObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi /-- The isomorphism expressing that `extendToSucc hj F τ` extends `F`. -/ @[simps!] def extendToSuccRestrictionLEIso : - Iteration.restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F := + restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F := NatIso.ofComponents (extendToSuccObjIso hj F τ) (by rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f apply extendToSuccObjIso_hom_naturality) -lemma extentToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : +lemma extendToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : (extendToSucc hj F τ).map (homOfLE hi : ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) = (extendToSuccObjIso hj F τ ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) ≫ diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean index 35b3bf90ea04c..3c601d1afeffd 100644 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean @@ -19,7 +19,7 @@ universe u namespace CategoryTheory -open Category Limits +open Category Limits SmallObject namespace Functor @@ -92,11 +92,19 @@ def ofCocone : Set.Iic j ⥤ C where map_id i := ofCocone.map_id _ _ i.2 map_comp {_ _ i₃} _ _ := ofCocone.map_comp _ _ _ _ _ _ i₃.2 +lemma ofCocone_obj_eq (i : J) (hi : i < j) : + (ofCocone c).obj ⟨i, hi.le⟩ = F.obj ⟨i, hi⟩ := + dif_pos hi + /-- The isomorphism `(ofCocone c).obj ⟨i, _⟩ ≅ F.obj ⟨i, _⟩` when `i < j`. -/ def ofCoconeObjIso (i : J) (hi : i < j) : (ofCocone c).obj ⟨i, hi.le⟩ ≅ F.obj ⟨i, hi⟩ := ofCocone.objIso c _ _ +lemma ofCocone_obj_eq_pt : + (ofCocone c).obj ⟨j, by simp⟩ = c.pt := + dif_neg (by simp) + /-- The isomorphism `(ofCocone c).obj ⟨j, _⟩ ≅ c.pt`. -/ def ofCoconeObjIsoPt : (ofCocone c).obj ⟨j, by simp⟩ ≅ c.pt := @@ -127,14 +135,14 @@ lemma ofCoconeObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ when `c : Cocone F`. -/ @[simps!] def restrictionLTOfCoconeIso : - Iteration.restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F := + restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F := NatIso.ofComponents (fun ⟨i, hi⟩ ↦ ofCoconeObjIso c i hi) (by intros; apply ofCoconeObjIso_hom_naturality) variable {c} in /-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (Preorder.le_refl j)`. -/ def isColimitCoconeOfLEOfCocone (hc : IsColimit c) : - IsColimit (Iteration.coconeOfLE (ofCocone c) (Preorder.le_refl j)) := + IsColimit (coconeOfLE (ofCocone c) (Preorder.le_refl j)) := (IsColimit.precomposeInvEquiv (restrictionLTOfCoconeIso c) _).1 (IsColimit.ofIsoColimit hc (Cocones.ext (ofCoconeObjIsoPt c).symm (fun ⟨i, hi⟩ ↦ by diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Iteration.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Iteration.lean new file mode 100644 index 0000000000000..3aa25e1015337 --- /dev/null +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Iteration.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2024 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ + +import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty + +/-! +# The transfinite iteration of a successor structure + +Given a successor structure `Φ : SuccStruct C` (see the file `SmallObject.Iteration.Basic`) +and a well-ordered type `J`, we define the iteration `Φ.iteration J : C`. It is +defined as the colimit of a functor `Φ.iterationFunctor J : J ⥤ C`. + +-/ + +universe w v u + +namespace CategoryTheory.SmallObject.SuccStruct + +open Limits + +variable {C : Type u} [Category.{v} C] (Φ : SuccStruct C) + (J : Type u) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] + [HasIterationOfShape C J] + +variable {J} in +/-- Given `Φ : SuccStruct C` and an element `j : J` in a well-ordered type, +this is the unique element in `Φ.Iteration j`. -/ +noncomputable def iter (j : J) : Φ.Iteration j := Classical.arbitrary _ + +/-- Given `Φ : SuccStruct C` and a well-ordered type `J`, this +is the functor `J ⥤ C` which gives the iterations of `Φ` indexed by `J`. -/ +@[simps (config := .lemmasOnly)] +noncomputable def iterationFunctor : J ⥤ C where + obj j := (Φ.iter j).F.obj ⟨j, by simp⟩ + map f := Iteration.mapObj _ _ (leOfHom f) _ _ (leOfHom f) + +/-- Given `Φ : SuccStruct C` and a well-ordered type `J`, +this is an object of `C` which is the iteration of `Φ` to the power `J`: +it is defined as the colimit of the functor `Φ.iterationFunctor J`. -/ +noncomputable def iteration : C := colimit (Φ.iterationFunctor J) + +/-- The colimit cocone expressing that `Φ.iteration J` is the colimit +of `Φ.iterationFunctor J`. -/ +noncomputable def iterationCocone : Cocone (Φ.iterationFunctor J) := + colimit.cocone _ + +@[simp] +lemma iterationCocone_pt : (Φ.iterationCocone J).pt = Φ.iteration J := rfl + +/-- `Φ.iteration J` identifies to the colimit of `Φ.iterationFunctor J`. -/ +noncomputable def isColimitIterationCocone : IsColimit (Φ.iterationCocone J) := + colimit.isColimit _ + +end CategoryTheory.SmallObject.SuccStruct diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean index 80bdbaec34cea..416b8382c34e1 100644 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean @@ -3,18 +3,16 @@ Copyright (c) 2024 Joël Riou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ +import Mathlib.CategoryTheory.SmallObject.Iteration.Basic import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc +import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone /-! -# Existence of objects in the category of iterations of functors +# Existence of the iteration of a successor structure -Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`, -we shall show in this file that for any well ordered set `J`, -and `j : J`, the category `Functor.Iteration ε j` is nonempty. -As we already know from the main result in `SmallObject.Iteration.UniqueHom` -that such objects, if they exist, are unique up to a unique isomorphism, -we shall show the existence of a term in `Functor.Iteration ε j` by -transfinite induction. +Given `Φ : SuccStruct C`, we show by transfinite induction +that for any element `j` in a well ordered set `J`, +the type `Φ.Iteration j` is nonempty. -/ @@ -22,76 +20,238 @@ universe u namespace CategoryTheory -open Category Limits +namespace SmallObject + +namespace SuccStruct -variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ} - {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] +open Category Limits -namespace Functor +variable {C : Type*} [Category C] (Φ : SuccStruct C) + {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] + [HasIterationOfShape C J] namespace Iteration -variable (ε J) in +variable (J) in /-- The obvious term in `Iteration ε ⊥`: it is given by the identity functor. -/ -def mkOfBot : Iteration ε (⊥ : J) where - F := (Functor.const _).obj (𝟭 C) - isoZero := Iso.refl _ - isoSucc _ h := by simp at h - mapSucc'_eq _ h := by simp at h - isColimit x hx h := by - exfalso - refine hx.not_isMin (by simpa using h) - -/-- When `j : J` is not maximal, this is the extension as `Iteration ε (Order.succ j)` -of any `iter : Iteration ε j`. -/ -noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Iteration ε j) : - Iteration ε (Order.succ j) where - F := extendToSucc hj iter.F (whiskerLeft _ ε) - isoZero := (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨⊥, by simp⟩).trans iter.isoZero - isoSucc i hi := - if hij : i < j then - extendToSuccObjIso _ _ _ ⟨Order.succ i, Order.succ_le_of_lt hij⟩ ≪≫ - iter.isoSucc i hij ≪≫ (isoWhiskerRight (extendToSuccObjIso _ _ _ ⟨i, hij.le⟩).symm _) - else - have hij' : i = j := le_antisymm - (by simpa only [Order.lt_succ_iff_of_not_isMax hj] using hi) (by simpa using hij) - eqToIso (by subst hij'; rfl) ≪≫ extendToSuccObjSuccIso hj iter.F (whiskerLeft _ ε) ≪≫ - isoWhiskerRight ((extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨j, by simp⟩).symm.trans - (eqToIso (by subst hij'; rfl))) _ - mapSucc'_eq i hi := by - obtain hi' | rfl := ((Order.lt_succ_iff_of_not_isMax hj).mp hi).lt_or_eq - · ext X - have := iter.mapSucc_eq i hi' - dsimp [mapSucc, mapSucc'] at this ⊢ - rw [extentToSucc_map _ _ _ _ _ _ (Order.succ_le_of_lt hi'), this, dif_pos hi'] - dsimp - rw [assoc, assoc] - erw [ε.naturality_assoc] - · ext X - dsimp [mapSucc'] - rw [dif_neg (gt_irrefl i), extendToSucc_map_le_succ] - dsimp - rw [id_comp, comp_id] - erw [ε.naturality_assoc] - isColimit i hi hij := by - have hij' : i ≤ j := by - obtain hij | rfl := hij.lt_or_eq - · exact (Order.lt_succ_iff_of_not_isMax hj).1 hij - · exfalso - exact Order.not_isSuccLimit_succ_of_not_isMax hj hi - refine (IsColimit.precomposeHomEquiv - (isoWhiskerLeft (monotone_inclusion_lt_le_of_le hij').functor - (extendToSuccRestrictionLEIso hj iter.F (whiskerLeft _ ε))).symm _).1 - (IsColimit.ofIsoColimit (iter.isColimit i hi hij') - (Iso.symm (Cocones.ext (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨i, hij'⟩) - (fun ⟨k, hk⟩ ↦ ?_)))) - dsimp - rw [assoc, extendToSuccObjIso_hom_naturality hj iter.F (whiskerLeft _ ε)] - dsimp - rw [Iso.inv_hom_id_assoc] +def mkOfBot : Φ.Iteration (⊥ : J) where + F := (Functor.const _).obj Φ.X₀ + obj_bot := rfl + obj_succ _ h := by simp at h + map_succ _ h := by simp at h + obj_limit x hx h := (hx.not_isMin (by simpa using h)).elim + map_eq_ι _ _ h₁ _ h₂ := by + obtain rfl := le_bot_iff.1 h₁ + simp at h₂ + +variable {Φ} + +open Functor in +/-- When `j : J` is not maximal, this is the extension as `Φ.Iteration (Order.succ j)` +of any `iter : Φ.Iteration j`. -/ +noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Φ.Iteration j) : + Φ.Iteration (Order.succ j) where + F := extendToSucc hj iter.F (Φ.toSucc _) + obj_bot := by rw [extendToSucc_obj_eq _ _ _ ⟨⊥, bot_le⟩, obj_bot] + obj_succ i hi₁ := by + have hi₂ := (Order.lt_succ_iff_of_not_isMax hj).1 hi₁ + rw [extendToSucc_obj_eq _ _ _ ⟨i, hi₂⟩] + by_cases hi₃ : i < j + · rw [extendToSucc_obj_eq _ _ _ ⟨Order.succ i, Order.succ_le_of_lt hi₃⟩, obj_succ _ _ hi₃] + · obtain rfl : i = j := le_antisymm hi₂ (by simpa using hi₃) + rw [extendToSucc_obj_succ_eq] + map_succ i hi₁ := by + rw [Order.lt_succ_iff_of_not_isMax hj] at hi₁ + by_cases hi₂ : i < j + · simp [extendToSucc_map _ _ _ _ _ _ (Order.succ_le_of_lt hi₂), map_succ _ _ hi₂, + extendToSuccObjIso, extendToSucc.objIso, + Φ.congr_toSucc (extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨i, hi₂.le⟩)] + · obtain rfl : j = i := le_antisymm (by simpa using hi₂) hi₁ + simp [extendToSucc_map_le_succ, + Φ.congr_toSucc (extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨j, by simp⟩), + extendToSuccObjIso, extendToSucc.objIso, + extendToSuccObjSuccIso, extendToSucc.objSuccIso] + obj_limit i hi hij := by + rw [Order.IsSuccLimit.le_succ_iff hi] at hij + rw [extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨i, hij⟩, obj_limit _ _ hi] + congr 1 + fapply Functor.ext + · rintro ⟨k, hk⟩ + exact (extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨k, _⟩).symm + · rintro ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f + simp [extendToSucc_map _ _ _ k₁ k₂ (leOfHom f) (hk₂.le.trans hij), + extendToSuccObjIso, extendToSucc.objIso, + extendToSuccObjSuccIso, extendToSucc.objSuccIso] + map_eq_ι i hi hij k hk := by + have hij' := (Order.IsSuccLimit.le_succ_iff hi).1 hij + have : restrictionLT iter.F hij' = + restrictionLT (extendToSucc hj iter.F (Φ.toSucc _)) hij := by + fapply Functor.ext + · rintro ⟨l, hl⟩ + exact (extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨l, _⟩).symm + · rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f + simp [extendToSucc_map _ _ _ l₁ l₂ (leOfHom f) (hl₂.le.trans hij'), + extendToSuccObjIso, extendToSucc.objIso] + simp [extendToSucc_map _ _ _ _ _ _ hij', map_eq_ι _ i hi _ _ hk, + congr_colimit_ι this hi, extendToSuccObjIso, extendToSucc.objIso] + +lemma congr_obj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + (k : J) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) : + iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩ := by + wlog h : j₁ ≤ j₂ generalizing j₁ j₂ + · exact (this iter₂ iter₁ h₂ h₁ (le_of_lt (by simpa using h))).symm + rw [Subsingleton.elim iter₁ (iter₂.trunc h)] + dsimp + +lemma congr_map {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) : + iter₁.F.map (homOfLE h : ⟨k₁, h.trans h₁⟩ ⟶ ⟨k₂, h₁⟩) = + eqToHom (congr_obj iter₁ iter₂ k₁ (h.trans h₁) (h.trans h₂)) ≫ + iter₂.F.map (homOfLE h) ≫ + eqToHom (congr_obj iter₁ iter₂ k₂ h₁ h₂).symm := by + wlog hj : j₁ ≤ j₂ generalizing j₁ j₂ + · simp [this iter₂ iter₁ h₂ h₁ ((not_le.1 hj).le)] + exact Functor.congr_hom (congr_arg F (Subsingleton.elim iter₁ (iter₂.trunc hj))) + (homOfLE h : ⟨k₁, _⟩ ⟶ ⟨k₂, _⟩) + +/-- Given `iter₁ : Φ.Iteration j₁` and `iter₂ : Φ.Iteration j₂`, with `j₁ ≤ j₂`, +if `k₁ ≤ k₂` are elements such that `k₁ ≤ j₁` and `k₂ ≤ k₂`, then this +is the canonical map `iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩`. -/ +def mapObj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂) : + iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩ := + eqToHom (congr_obj iter₁ iter₂ k₁ h₁ (h₁.trans hj)) ≫ + iter₂.F.map (homOfLE h₁₂) + +@[simp] +lemma mapObj_refl {j : J} (iter : Φ.Iteration j) + {k l : J} (h : k ≤ l) (h' : l ≤ j) : + mapObj iter iter h (h.trans h') h' (by rfl) = iter.F.map (homOfLE h) := by + simp [mapObj] + +@[reassoc (attr := simp)] +lemma mapObj_trans {j₁ j₂ j₃ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + (iter₃ : Φ.Iteration j₃) {k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂) (h₂₃ : k₂ ≤ k₃) + (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂) (h₂₃' : j₂ ≤ j₃) : + mapObj iter₁ iter₂ h₁₂ h₁ h₂ h₁₂' ≫ mapObj iter₂ iter₃ h₂₃ h₂ h₃ h₂₃' = + mapObj iter₁ iter₃ (h₁₂.trans h₂₃) h₁ h₃ (h₁₂'.trans h₂₃') := by + simp [mapObj, congr_map iter₂ iter₃ h₁₂ h₂ (h₂.trans h₂₃'), ← Functor.map_comp] + +namespace mkOfLimit + +open Functor + +variable {j : J} (hj : Order.IsSuccLimit j) (iter : ∀ (i : J), i < j → Φ.Iteration i) + +/-- Assuming `j : J` is a limit element and that we have `∀ (i : J), i < j → Φ.Iteration i`, +this is the inductive system `Set.Iio j ⥤ C` which sends `⟨i, _⟩` to +`(iter i _).F.obj ⟨i, _⟩`. -/ +@[simps] +noncomputable def inductiveSystem : Set.Iio j ⥤ C where + obj i := (iter i.1 i.2).F.obj ⟨i.1, by simp⟩ + map {i₁ i₂} f := mapObj (iter i₁.1 i₁.2) (iter i₂.1 i₂.2) (leOfHom f) + (by simp) (by simp) (leOfHom f) + +/-- The extension of `inductiveSystem iter` to a functor `Set.Iic j ⥤ C` which +sends the top element to the colimit of `inductiveSystem iter`. -/ +noncomputable def functor : Set.Iic j ⥤ C := + letI := hasColimitOfShape_of_isSuccLimit C j hj + ofCocone (colimit.cocone (inductiveSystem iter)) + +lemma functor_obj (i : J) (hi : i < j) {k : J} (iter' : Φ.Iteration k) (hk : i ≤ k) : + (functor hj iter).obj ⟨i, hi.le⟩ = iter'.F.obj ⟨i, hk⟩ := by + dsimp only [functor] + rw [ofCocone_obj_eq _ _ hi] + apply congr_obj + +lemma functor_obj_eq_colimit : + letI := hasColimitOfShape_of_isSuccLimit C j hj + (functor hj iter).obj ⟨j, by simp⟩ = colimit (inductiveSystem iter) := by + apply ofCocone_obj_eq_pt + +lemma functor_map {i₁ i₂ : J} (h₁₂ : i₁ ≤ i₂) (hi₂ : i₂ < j) + {k : J} (iter' : Φ.Iteration k) (hk : i₂ ≤ k) : + (functor hj iter).map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) = + eqToHom (functor_obj hj iter i₁ (lt_of_le_of_lt h₁₂ hi₂) iter' (h₁₂.trans hk)) ≫ + iter'.F.map (homOfLE h₁₂) ≫ + eqToHom (functor_obj hj iter i₂ hi₂ iter' hk).symm := by + simp [functor, ofCocone_map _ _ _ _ hi₂, congr_map (iter i₂ hi₂) iter' _ _ hk, + ofCoconeObjIso, ofCocone.objIso, mapObj] + +lemma restrictionLT_functor_of_lt {i : J} (hij : i < j) {k : J} (iter' : Φ.Iteration k) + (hk : i ≤ k) : + restrictionLT (functor hj iter) hij.le = restrictionLT iter'.F hk := by + fapply Functor.ext + · rintro ⟨l, hl⟩ + exact functor_obj hj _ _ (hl.trans hij) iter' _ + · rintro ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ f + exact functor_map hj _ _ (h₂.trans hij) _ _ + +lemma restrictionLT_functor : + restrictionLT (functor hj iter) (le_refl j) = inductiveSystem iter := by + fapply Functor.ext + · rintro ⟨l, hl⟩ + exact functor_obj hj _ _ hl _ _ + · rintro ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ f + simp [functor_map _ _ _ h₂ (iter l₂ h₂) (by rfl), mapObj] + +lemma functor_map_to_top (i : J) (hij : i < j) : + letI := hasColimitOfShape_of_isSuccLimit C j hj + (functor hj iter).map (homOfLE hij.le : ⟨i, hij.le⟩ ⟶ ⟨j, by simp⟩) = + eqToHom (functor_obj _ _ _ hij _ _) ≫ colimit.ι (inductiveSystem iter) ⟨i, hij⟩ ≫ + eqToHom (functor_obj_eq_colimit hj iter).symm := by + simp [functor, ofCocone_map_to_top _ _ hij, ofCoconeObjIso, ofCocone.objIso, + ofCoconeObjIsoPt, ofCocone.objIsoPt] + +end mkOfLimit + +open mkOfLimit in +/-- When `j` is a limit element, this is the element in `Φ.Iteration j` +that is constructed from elements in `Φ.Iteration i` for all `i < j`. -/ +noncomputable def mkOfLimit {j : J} (hj : Order.IsSuccLimit j) + (iter : ∀ (i : J), i < j → Φ.Iteration i) : + Φ.Iteration j where + F := functor hj iter + obj_bot := functor_obj hj iter ⊥ (Order.IsSuccLimit.bot_lt hj) (mkOfBot Φ J) (by rfl) + obj_succ i hi₁ := by + have hi₂ := (Order.IsSuccLimit.succ_lt_iff hj).2 hi₁ + rw [functor_obj hj iter (Order.succ i) hi₂ (iter (Order.succ i) hi₂) (by rfl), + functor_obj hj iter i hi₁ (iter (Order.succ i) hi₂) (Order.le_succ i), + obj_succ _ _ (Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi₁))] + map_succ i hi₁ := by + have hi₂ := (Order.IsSuccLimit.succ_lt_iff hj).2 hi₁ + simp [functor_map hj iter (Order.le_succ i) hi₂ (iter _ hi₂) (by rfl), + map_succ _ _ (Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi₁)), + Φ.congr_toSucc (functor_obj hj iter i hi₁ (iter _ hi₂) (Order.le_succ i))] + obj_limit i hi hij := by + obtain hij | rfl := hij.lt_or_eq + · rw [functor_obj hj iter i hij (iter _ hij) (by rfl), obj_limit _ i hi, + restrictionLT_functor_of_lt hj iter hij (iter i hij) (by rfl)] + · rw [functor_obj_eq_colimit, restrictionLT_functor] + map_eq_ι i hi hij := by + obtain hij | rfl := hij.lt_or_eq + · intro k hk + simp [functor_map hj iter _ hij (iter i hij) (by rfl), + map_eq_ι _ _ hi _ _ hk, + congr_colimit_ι (restrictionLT_functor_of_lt hj iter hij (iter i hij) (by rfl)) hi] + · intro k hk + simp [functor_map_to_top _ _ _ hk, + congr_colimit_ι (restrictionLT_functor hj iter) hi ⟨k, hk⟩] + +variable (Φ) + +instance nonempty (j : J) : Nonempty (Φ.Iteration j) := by + induction j using SuccOrder.limitRecOn with + | hm i hi => + obtain rfl : i = ⊥ := by simpa using hi + exact ⟨mkOfBot Φ J⟩ + | hs i hi hi' => exact ⟨mkOfSucc hi hi'.some⟩ + | hl i hi hi' => exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩ end Iteration -end Functor +end SuccStruct + +end SmallObject end CategoryTheory diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean deleted file mode 100644 index 5e804f4b55103..0000000000000 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean +++ /dev/null @@ -1,249 +0,0 @@ -/- -Copyright (c) 2024 Joël Riou. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joël Riou --/ -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 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. - --/ - -universe u - -namespace CategoryTheory - -open Category Limits - -variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ} - {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] - -namespace Functor - -namespace Iteration - -namespace Hom - -/-- The (unique) morphism between two objects in `Iteration ε ⊥` -/ -def mkOfBot (iter₁ iter₂ : Iteration ε (⊥ : J)) : iter₁ ⟶ iter₂ where - natTrans := - { app := fun ⟨i, hi⟩ => eqToHom (by congr; simpa using hi) ≫ iter₁.isoZero.hom ≫ - iter₂.isoZero.inv ≫ eqToHom (by congr; symm; simpa using hi) - naturality := fun ⟨i, hi⟩ ⟨k, hk⟩ φ => by - obtain rfl : i = ⊥ := by simpa using hi - obtain rfl : k = ⊥ := by simpa using hk - obtain rfl : φ = 𝟙 _ := rfl - simp } - natTrans_app_succ i hi := by simp at hi - -section - -variable {i : J} {iter₁ iter₂ : Iteration ε (Order.succ i)} - (hi : ¬IsMax i) (φ : iter₁.trunc (SuccOrder.le_succ i) ⟶ iter₂.trunc (SuccOrder.le_succ i)) - -/-- Auxiliary definition for `mkOfSucc`. -/ -noncomputable def mkOfSuccNatTransApp (k : J) (hk : k ≤ Order.succ i) : - iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩ := - if hk' : k = Order.succ i then - eqToHom (by subst hk'; rfl) ≫ (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫ - whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫ - (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv ≫ - eqToHom (by subst hk'; rfl) - else - φ.natTrans.app ⟨k, Order.le_of_lt_succ (by - obtain hk | rfl := hk.lt_or_eq - · exact hk - · tauto)⟩ - -lemma mkOfSuccNatTransApp_eq_of_le (k : J) (hk : k ≤ i) : - mkOfSuccNatTransApp hi φ k (hk.trans (Order.le_succ i)) = - φ.natTrans.app ⟨k, hk⟩ := - dif_neg (by rintro rfl; simpa using lt_of_le_of_lt hk (Order.lt_succ_of_not_isMax hi)) - -@[simp] -lemma mkOfSuccNatTransApp_succ_eq : - mkOfSuccNatTransApp hi φ (Order.succ i) (by rfl) = - (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫ - whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫ - (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv := by - dsimp [mkOfSuccNatTransApp] - rw [dif_pos rfl, comp_id, id_comp] - -/-- Auxiliary definition for `mkOfSucc`. -/ -@[simps] -noncomputable def mkOfSuccNatTrans : - iter₁.F ⟶ iter₂.F where - app := fun ⟨k, hk⟩ => mkOfSuccNatTransApp hi φ k hk - naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by - dsimp - have hk : k₁ ≤ k₂ := leOfHom f - obtain h₂ | rfl := hk₂.lt_or_eq - · replace h₂ : k₂ ≤ i := Order.le_of_lt_succ h₂ - rw [mkOfSuccNatTransApp_eq_of_le hi φ k₂ h₂, - mkOfSuccNatTransApp_eq_of_le hi φ k₁ (hk.trans h₂)] - exact natTrans_naturality φ k₁ k₂ hk h₂ - · obtain h₁ | rfl := hk.lt_or_eq - · have h₂ : k₁ ≤ i := Order.le_of_lt_succ h₁ - let f₁ : (⟨k₁, hk⟩ : { l | l ≤ Order.succ i}) ⟶ - ⟨i, Order.le_succ i⟩ := homOfLE h₂ - let f₂ : (⟨i, Order.le_succ i⟩ : Set.Iic (Order.succ i)) ⟶ - ⟨Order.succ i, by simp⟩ := homOfLE (Order.le_succ i) - obtain rfl : f = f₁ ≫ f₂ := rfl - rw [Functor.map_comp, Functor.map_comp, assoc, - mkOfSuccNatTransApp_eq_of_le hi φ k₁ h₂] - erw [← natTrans_naturality_assoc φ k₁ i h₂ (by rfl)] - rw [mkOfSuccNatTransApp_succ_eq] - dsimp - have ha : iter₁.F.map f₂ = iter₁.mapSucc i (Order.lt_succ_of_not_isMax hi) := rfl - have hb : iter₂.F.map f₂ = iter₂.mapSucc i (Order.lt_succ_of_not_isMax hi) := rfl - rw [ha, hb] - rw [iter₁.mapSucc_eq i, iter₂.mapSucc_eq i, assoc, - Iso.inv_hom_id_assoc] - ext X - dsimp - rw [← ε.naturality_assoc] - rfl - · obtain rfl : f = 𝟙 _ := rfl - rw [Functor.map_id, Functor.map_id, id_comp, comp_id] - -end - -/-- The (unique) morphism between two objects in `Iteration ε (Order.succ i)`, -assuming we have a morphism between the truncations to `Iteration ε i`. -/ -noncomputable def mkOfSucc - {i : J} (iter₁ iter₂ : Iteration ε (Order.succ i)) (hi : ¬IsMax i) - (φ : iter₁.trunc (SuccOrder.le_succ i) ⟶ iter₂.trunc (SuccOrder.le_succ i)) : - iter₁ ⟶ iter₂ where - natTrans := mkOfSuccNatTrans hi φ - natTrans_app_zero := by - dsimp - rw [mkOfSuccNatTransApp_eq_of_le _ _ _ bot_le, φ.natTrans_app_zero] - rfl - natTrans_app_succ k hk := by - obtain hk' | rfl := (Order.le_of_lt_succ hk).lt_or_eq - · dsimp - rw [mkOfSuccNatTransApp_eq_of_le hi φ k hk'.le, - mkOfSuccNatTransApp_eq_of_le hi φ (Order.succ k) (Order.succ_le_of_lt hk'), - φ.natTrans_app_succ _ hk'] - 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 - -end CategoryTheory