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.

noncomputable def CategoryTheory.SmallObject.SuccStruct.iter {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] (j : J) : Φ.Iteration j

Given Φ : SuccStruct C and an element j : J in a well-ordered type, this is the unique element in Φ.Iteration j.

Equations

• Φ.iter j = Classical.arbitrary (Φ.Iteration j)

noncomputable def CategoryTheory.SmallObject.SuccStruct.iterationFunctor {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : Functor J C

Given Φ : SuccStruct C and a well-ordered type J, this is the functor J ⥤ C which gives the iterations of Φ indexed by J.

Equations

• Φ.iterationFunctor J = { obj := fun (j : J) => (Φ.iter j).F.obj ⟨j, ⋯⟩, map := fun {X Y : J} (f : X ⟶ Y) => (Φ.iter X).mapObj (Φ.iter Y) ⋯ ⋯ ⋯ ⋯, map_id := ⋯, map_comp := ⋯ }

noncomputable def CategoryTheory.SmallObject.SuccStruct.iteration {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : C

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 : J ⥤ C.

Equations

• Φ.iteration J = CategoryTheory.Limits.colimit (Φ.iterationFunctor J)

noncomputable def CategoryTheory.SmallObject.SuccStruct.iterationCocone {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : Limits.Cocone (Φ.iterationFunctor J)

The colimit cocone expressing that Φ.iteration J is the colimit of Φ.iterationFunctor J.

Equations

• Φ.iterationCocone J = CategoryTheory.Limits.colimit.cocone (Φ.iterationFunctor J)

@[simp]

theorem CategoryTheory.SmallObject.SuccStruct.iterationCocone_pt {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : (Φ.iterationCocone J).pt = Φ.iteration J

noncomputable def CategoryTheory.SmallObject.SuccStruct.isColimitIterationCocone {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : Limits.IsColimit (Φ.iterationCocone J)

Φ.iteration J identifies to the colimit of Φ.iterationFunctor J.

Equations

• Φ.isColimitIterationCocone J = CategoryTheory.Limits.colimit.isColimit (Φ.iterationFunctor J)

theorem CategoryTheory.SmallObject.SuccStruct.iterationFunctor_obj {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] (i : J) {j : J} (iter : Φ.Iteration j) (hi : i ≤ j) : (Φ.iterationFunctor J).obj i = iter.F.obj ⟨i, hi⟩

theorem CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) {j : J} (iter : Φ.Iteration j) (hj : i₂ ≤ j) : Arrow.mk ((Φ.iterationFunctor J).map (homOfLE h₁₂)) = Arrow.mk (iter.F.map (homOfLE h₁₂))

instance CategoryTheory.SmallObject.SuccStruct.instIsWellOrderContinuousIterationFunctor {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : (Φ.iterationFunctor J).IsWellOrderContinuous

noncomputable def CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjBotIso {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : (Φ.iterationFunctor J).obj ⊥ ≅ Φ.X₀

The isomorphism (Φ.iterationFunctor J).obj ⊥ ≅ Φ.X₀.

Equations

• Φ.iterationFunctorObjBotIso J = CategoryTheory.eqToIso ⋯

noncomputable def CategoryTheory.SmallObject.SuccStruct.ιIterationFunctor {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : (Functor.const J).obj Φ.X₀ ⟶ Φ.iterationFunctor J

The natural map Φ.X₀ ⟶ (Φ.iterationFunctor J).obj j.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.SmallObject.SuccStruct.ιIteration {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : Φ.X₀ ⟶ Φ.iteration J

The canonical map Φ.X₀ ⟶ Φ.iteration J which is the Jth-transfinite composition of maps Φ.toSucc.

Equations

• Φ.ιIteration J = CategoryTheory.CategoryStruct.comp (Φ.iterationFunctorObjBotIso J).inv (CategoryTheory.Limits.colimit.ι (Φ.iterationFunctor J) ⊥)

noncomputable def CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : Φ.prop.TransfiniteCompositionOfShape J (Φ.ιIteration J)

The inclusion Φ.ιIteration J is a transfinite composition of shape J of morphisms in Φ.prop.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_F {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : (Φ.transfiniteCompositionOfShapeιIteration J).F = Φ.iterationFunctor J

@[simp]

theorem CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_isoBot {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : (Φ.transfiniteCompositionOfShapeιIteration J).isoBot = Φ.iterationFunctorObjBotIso J

@[simp]

theorem CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_incl {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : (Φ.transfiniteCompositionOfShapeιIteration J).incl = (Φ.iterationCocone J).ι

@[simp]

theorem CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_isColimit {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : (Φ.transfiniteCompositionOfShapeιIteration J).isColimit = Φ.isColimitIterationCocone J

theorem CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) : Φ.prop ((Φ.iterationFunctor J).map (homOfLE ⋯))

noncomputable def CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjSuccIso {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) : (Φ.iterationFunctor J).obj (Order.succ j) ≅ Φ.succ ((Φ.iterationFunctor J).obj j)

When j is not a maximal element, then (Φ.iterationFunctor J).obj (Order.succ j) is isomorphic to Φ.succ ((Φ.iterationFunctor J).obj j).

Equations

• Φ.iterationFunctorObjSuccIso j hj = CategoryTheory.eqToIso ⋯

theorem CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) : (Φ.iterationFunctor J).map (homOfLE ⋯) = CategoryStruct.comp (Φ.toSucc ((Φ.iterationFunctor J).obj j)) (Φ.iterationFunctorObjSuccIso j hj).inv

theorem CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ_assoc {C : Type u} [Category.{v, u} C] (Φ : SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) {Z : C} (h : (Φ.iterationFunctor J).obj (Order.succ j) ⟶ Z) : CategoryStruct.comp ((Φ.iterationFunctor J).map (homOfLE ⋯)) h = CategoryStruct.comp (Φ.toSucc ((Φ.iterationFunctor J).obj j)) (CategoryStruct.comp (Φ.iterationFunctorObjSuccIso j hj).inv h)