Documentation

Mathlib.CategoryTheory.SmallObject.Iteration

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 : { i // i ≤ j } ⥤ C ⥤ C equipped with the data which makes it the ith-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). We shall study morphisms in this category, showing first that there is at most one morphism between two morphisms (done), and secondly, 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:

@[reducible, inline]
noncomputable abbrev CategoryTheory.Functor.Iteration.mapSucc' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i j } C) [IsWellOrder J fun (x1 x2 : J) => x1 < x2] (i : J) (hi : i < j) :
F.obj i, F.obj wellOrderSucc i,

The map F.obj ⟨i, _⟩ ⟶ F.obj ⟨wellOrderSucc i, _⟩ when F : { i // i ≤ j } ⥤ C and i : J is such that i < j.

Equations
Instances For
    def CategoryTheory.Functor.Iteration.restrictionLT {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i j } C) {i : J} (hi : i j) :
    CategoryTheory.Functor { k : J // k < i } C

    The functor { k // k < i } ⥤ C obtained by "restriction" of F : { i // i ≤ j } ⥤ C when i ≤ j.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.Functor.Iteration.restrictionLT_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i j } C) {i : J} (hi : i j) (k : J) (hk : k < i) :
      (CategoryTheory.Functor.Iteration.restrictionLT F hi).obj k, hk = F.obj k,
      @[simp]
      theorem CategoryTheory.Functor.Iteration.restrictionLT_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i j } C) {i : J} (hi : i j) {k₁ : { k : J // k < i }} {k₂ : { k : J // k < i }} (φ : k₁ k₂) :
      @[simp]
      theorem CategoryTheory.Functor.Iteration.coconeOfLE_ι_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i j } C) {i : J} (hi : i j) :
      ∀ (x : { k : J // k < i }), (CategoryTheory.Functor.Iteration.coconeOfLE F hi).app x = match x with | k, hk => F.map (CategoryTheory.homOfLE )
      @[simp]
      theorem CategoryTheory.Functor.Iteration.coconeOfLE_pt {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i j } C) {i : J} (hi : i j) :

      Given F : { i // i ≤ j } ⥤ C, i : J such that hi : i ≤ j, this is the cocone consisting of all maps F.obj ⟨k, hk⟩ ⟶ F.obj ⟨i, hi⟩ for k : J such that k < i.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        structure CategoryTheory.Functor.Iteration {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} (ε : CategoryTheory.Functor.id C Φ) {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] (j : J) :
        Type (max (max u u_1) u_2)

        The category of jth 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.

        Instances For
          theorem CategoryTheory.Functor.Iteration.mapSucc'_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (self : CategoryTheory.Functor.Iteration ε j) (i : J) (hi : i < j) :
          CategoryTheory.Functor.Iteration.mapSucc' self.F i hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (self.F.obj i, ) ε) (self.isoSucc i hi).inv

          The natural map from an iteration to its successor is induced by ε.

          @[reducible, inline]
          noncomputable abbrev CategoryTheory.Functor.Iteration.mapSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (iter : CategoryTheory.Functor.Iteration ε j) (i : J) (hi : i < j) :
          iter.F.obj i, iter.F.obj wellOrderSucc i,

          For iter : Φ.Iteration.ε j, this is the map iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨wellOrderSucc i, _⟩ if i : J is such that i < j.

          Equations
          Instances For
            theorem CategoryTheory.Functor.Iteration.mapSucc_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (iter : CategoryTheory.Functor.Iteration ε j) (i : J) (hi : i < j) :
            iter.mapSucc i hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (iter.F.obj i, ) ε) (iter.isoSucc i hi).inv
            structure CategoryTheory.Functor.Iteration.Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (iter₁ : CategoryTheory.Functor.Iteration ε j) (iter₂ : CategoryTheory.Functor.Iteration ε j) :
            Type (max (max u u_1) u_2)

            A morphism between two objects iter₁ and iter₂ in the category Φ.Iteration ε j of jth 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.

            Instances For
              @[simp]
              theorem CategoryTheory.Functor.Iteration.Hom.natTrans_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} (self : iter₁.Hom iter₂) :
              self.natTrans.app , = CategoryTheory.CategoryStruct.comp iter₁.isoZero.hom iter₂.isoZero.inv
              theorem CategoryTheory.Functor.Iteration.Hom.natTrans_app_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} (self : iter₁.Hom iter₂) (i : J) (hi : i < j) :
              self.natTrans.app wellOrderSucc i, = CategoryTheory.CategoryStruct.comp (iter₁.isoSucc i hi).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (self.natTrans.app i, ) Φ) (iter₂.isoSucc i hi).inv)
              theorem CategoryTheory.Functor.Iteration.Hom.natTrans_app_zero_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} (self : iter₁.Hom iter₂) {Z : CategoryTheory.Functor C C} (h : iter₂.F.obj , Z) :
              CategoryTheory.CategoryStruct.comp (self.natTrans.app , ) h = CategoryTheory.CategoryStruct.comp iter₁.isoZero.hom (CategoryTheory.CategoryStruct.comp iter₂.isoZero.inv h)
              def CategoryTheory.Functor.Iteration.Hom.id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (iter₁ : CategoryTheory.Functor.Iteration ε j) :
              iter₁.Hom iter₁

              The identity morphism in the category Φ.Iteration ε j.

              Equations
              Instances For
                theorem CategoryTheory.Functor.Iteration.Hom.ext' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} {f : iter₁.Hom iter₂} {g : iter₁.Hom iter₂} (h : f.natTrans = g.natTrans) :
                f = g
                theorem CategoryTheory.Functor.Iteration.Hom.ext'_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} {f : iter₁.Hom iter₂} {g : iter₁.Hom iter₂} :
                f = g f.natTrans = g.natTrans
                @[simp]
                theorem CategoryTheory.Functor.Iteration.Hom.comp_natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} {iter₃ : CategoryTheory.Functor.Iteration ε j} (f : iter₁.Hom iter₂) (g : iter₂.Hom iter₃) :
                (f.comp g).natTrans = CategoryTheory.CategoryStruct.comp f.natTrans g.natTrans
                def CategoryTheory.Functor.Iteration.Hom.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} {iter₃ : CategoryTheory.Functor.Iteration ε j} (f : iter₁.Hom iter₂) (g : iter₂.Hom iter₃) :
                iter₁.Hom iter₃

                The composition of morphisms in the category Φ.Iteration ε j.

                Equations
                Instances For
                  Equations
                  • =