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.Functor.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

• CategoryTheory.Functor.extendToSucc.obj F X i = if hij : ↑i ≤ j then F.obj ⟨↑i, hij⟩ else X

def CategoryTheory.Functor.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

• CategoryTheory.Functor.extendToSucc.objIso F X i = CategoryTheory.eqToIso ⋯

def CategoryTheory.Functor.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

• CategoryTheory.Functor.extendToSucc.objSuccIso hj F X = CategoryTheory.eqToIso ⋯

def CategoryTheory.Functor.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.Functor.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.Functor.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.Functor.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.Functor.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.Functor.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) : Functor (↑(Set.Iic (Order.succ j))) C

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.

def CategoryTheory.Functor.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 : ↑(Set.Iic j)) : (extendToSucc hj F τ).obj ⟨↑i, ⋯⟩ ≅ F.obj i

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

Equations

• CategoryTheory.Functor.extendToSuccObjIso hj F τ i = CategoryTheory.Functor.extendToSucc.objIso F X i

def CategoryTheory.Functor.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) : (extendToSucc hj F τ).obj ⟨Order.succ j, ⋯⟩ ≅ X

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

Equations

• CategoryTheory.Functor.extendToSuccObjSuccIso hj F τ = CategoryTheory.Functor.extendToSucc.objSuccIso hj F X

theorem CategoryTheory.Functor.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.Functor.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) : CategoryStruct.comp ((extendToSucc hj F τ).map (homOfLE hi)) (CategoryStruct.comp (extendToSuccObjIso hj F τ ⟨i₂, hi₂⟩).hom h) = CategoryStruct.comp (extendToSuccObjIso hj F τ ⟨i₁, ⋯⟩).hom (CategoryStruct.comp (F.map (homOfLE hi)) h)

def CategoryTheory.Functor.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) : Iteration.restrictionLE (extendToSucc hj F τ) ⋯ ≅ F

The isomorphism expressing that extendToSucc hj F τ extends F.

Equations

• CategoryTheory.Functor.extendToSuccRestrictionLEIso hj F τ = CategoryTheory.NatIso.ofComponents (CategoryTheory.Functor.extendToSuccObjIso hj F τ) ⋯

@[simp]

theorem CategoryTheory.Functor.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.Functor.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.Functor.extentToSucc_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.Functor.extendToSucc_map_le_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) : (extendToSucc hj F τ).map (homOfLE ⋯) = CategoryStruct.comp (extendToSuccObjIso hj F τ ⟨j, ⋯⟩).hom (CategoryStruct.comp τ (extendToSuccObjSuccIso hj F τ).inv)