Documentation

Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Extension of a functor from Set.Iic j to Set.Iic (Order.succ j) #

Given a linearly ordered type J with SuccOrder J, j : J that is not maximal, we define the extension of a functor F : Set.Iic j ⥤ C as a functor Set.Iic (Order.succ j) ⥤ C when an object X : C and a morphism τ : F.obj ⟨j, _⟩ ⟶ X is given.

def CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (F : Functor (↑(Set.Iic j)) C) (X : C) (i : (Set.Iic (Order.succ j))) :
C

extendToSucc, on objects: it coincides with F.obj for i ≤ j, and it sends Order.succ j to the given object X.

Equations
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_eq {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (F : Functor (↑(Set.Iic j)) C) (X : C) (i : (Set.Iic j)) :
obj F X i, = F.obj i
def CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (F : Functor (↑(Set.Iic j)) C) (X : C) (i : (Set.Iic j)) :
obj F X i, F.obj i

The isomorphism obj F X ⟨i, _⟩ ≅ F.obj i when i : Set.Iic j.

Equations
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_succ_eq {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) (X : C) :
obj F X Order.succ j, = X
def CategoryTheory.SmallObject.SuccStruct.extendToSucc.objSuccIso {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) (X : C) :
obj F X Order.succ j, X

The isomorphism obj F X ⟨Order.succ j, _⟩ ≅ X.

Equations
def CategoryTheory.SmallObject.SuccStruct.extendToSucc.map {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i₁ i₂ : J) (hi : i₁ i₂) (hi₂ : i₂ Order.succ j) :
obj F X i₁, obj F X i₂, hi₂

extendToSucc, on morphisms.

Equations
  • One or more equations did not get rendered due to their size.
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_eq {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i₁ i₂ : J) (hi : i₁ i₂) (hi₂ : i₂ j) :
map hj F τ i₁ i₂ hi = CategoryStruct.comp (objIso F X i₁, ).hom (CategoryStruct.comp (F.map (homOfLE hi)) (objIso F X i₂, hi₂).inv)
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_self_succ {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) :
map hj F τ j (Order.succ j) = CategoryStruct.comp (objIso F X j, ).hom (CategoryStruct.comp τ (objSuccIso hj F X).inv)
@[simp]
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_id {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i : J) (hi : i Order.succ j) :
map hj F τ i i hi = CategoryStruct.id (obj F X i, )
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_comp {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i₁ i₂ i₃ : J) (h₁₂ : i₁ i₂) (h₂₃ : i₂ i₃) (h : i₃ Order.succ j) :
map hj F τ i₁ i₃ h = CategoryStruct.comp (map hj F τ i₁ i₂ h₁₂ ) (map hj F τ i₂ i₃ h₂₃ h)
def CategoryTheory.SmallObject.SuccStruct.extendToSucc {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) :

The extension to Set.Iic (Order.succ j) ⥤ C of a functor F : Set.Iic j ⥤ C, when we specify a morphism F.obj ⟨j, _⟩ ⟶ X.

Equations
  • One or more equations did not get rendered due to their size.
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i : J) (hi : i j) :
(extendToSucc hj F τ).obj i, = F.obj i, hi
def CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i : J) (hi : i j) :
(extendToSucc hj F τ).obj i, F.obj i, hi

The isomorphism (extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i when i ≤ j

Equations
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_succ_eq {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) :
(extendToSucc hj F τ).obj Order.succ j, = X
def CategoryTheory.SmallObject.SuccStruct.extendToSuccObjSuccIso {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) :

The isomorphism (extendToSucc hj F τ).obj ⟨Order.succ j, _⟩ ≅ X.

Equations
theorem CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i₁ i₂ : J) (hi : i₁ i₂) (hi₂ : i₂ j) :
CategoryStruct.comp ((extendToSucc hj F τ).map (homOfLE hi)) (extendToSuccObjIso hj F τ i₂ hi₂).hom = CategoryStruct.comp (extendToSuccObjIso hj F τ i₁ ).hom (F.map (homOfLE hi))
theorem CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality_assoc {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i₁ i₂ : J) (hi : i₁ i₂) (hi₂ : i₂ j) {Z : C} (h : F.obj i₂, hi₂ Z) :
def CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) :

The isomorphism expressing that extendToSucc hj F τ extends F.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_hom_app {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (X✝ : (Set.Iic j)) :
(extendToSuccRestrictionLEIso hj F τ).hom.app X✝ = (extendToSuccObjIso hj F τ X✝ ).hom
@[simp]
theorem CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_inv_app {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (X✝ : (Set.Iic j)) :
(extendToSuccRestrictionLEIso hj F τ).inv.app X✝ = (extendToSuccObjIso hj F τ X✝ ).inv
theorem CategoryTheory.SmallObject.SuccStruct.extendToSucc_map {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i₁ i₂ : J) (hi : i₁ i₂) (hi₂ : i₂ j) :
(extendToSucc hj F τ).map (homOfLE hi) = CategoryStruct.comp (extendToSuccObjIso hj F τ i₁ ).hom (CategoryStruct.comp (F.map (homOfLE hi)) (extendToSuccObjIso hj F τ i₂ hi₂).inv)
theorem CategoryTheory.SmallObject.SuccStruct.arrowMap_extendToSucc {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) (i₁ i₂ : J) (hi : i₁ i₂) (hi₂ : i₂ j) :
arrowMap (extendToSucc hj F τ) i₁ i₂ hi = arrowMap F i₁ i₂ hi hi₂
theorem CategoryTheory.SmallObject.SuccStruct.arrowSucc_extendToSucc {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Functor (↑(Set.Iic j)) C) {X : C} (τ : F.obj j, X) :
arrowSucc (extendToSucc hj F τ) j = Arrow.mk τ