The functor from Set.Iic j deduced from a cocone

Given a functor F : Set.Iio j ⥤ C and c : Cocone F, we define an extension of F as a functor Set.Iic j ⥤ C for which the top element is mapped to c.pt.

def CategoryTheory.Functor.ofCocone.obj {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i : J) : C

Auxiliary definition for Functor.ofCocone.

Equations

• CategoryTheory.Functor.ofCocone.obj c i = if hi : i < j then F.obj ⟨i, hi⟩ else c.pt

def CategoryTheory.Functor.ofCocone.objIso {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i : J) (hi : i < j) : obj c i ≅ F.obj ⟨i, hi⟩

Auxiliary definition for Functor.ofCocone.

Equations

• CategoryTheory.Functor.ofCocone.objIso c i hi = CategoryTheory.eqToIso ⋯

def CategoryTheory.Functor.ofCocone.objIsoPt {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) : obj c j ≅ c.pt

Auxiliary definition for Functor.ofCocone.

Equations

• CategoryTheory.Functor.ofCocone.objIsoPt c = CategoryTheory.eqToIso ⋯

def CategoryTheory.Functor.ofCocone.map {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : obj c i₁ ⟶ obj c i₂

Auxiliary definition for Functor.ofCocone.

Equations

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

theorem CategoryTheory.Functor.ofCocone.map_id {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i : J) (hi : i ≤ j) : map c i i ⋯ hi = CategoryStruct.id (obj c i)

theorem CategoryTheory.Functor.ofCocone.map_comp {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (hi₃ : i₃ ≤ j) : map c i₁ i₃ ⋯ hi₃ = CategoryStruct.comp (map c i₁ i₂ hi ⋯) (map c i₂ i₃ hi' hi₃)

def CategoryTheory.Functor.ofCocone {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) : Functor (↑(Set.Iic j)) C

Given a functor F : Set.Iio j ⥤ C and a cocone c : Cocone F, where j : J and J is linearly ordered, this is the functor Set.Iic j ⥤ C which extends F and sends the top element to c.pt.

Equations

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

def CategoryTheory.Functor.ofCoconeObjIso {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i : J) (hi : i < j) : (ofCocone c).obj ⟨i, ⋯⟩ ≅ F.obj ⟨i, hi⟩

The isomorphism (ofCocone c).obj ⟨i, _⟩ ≅ F.obj ⟨i, _⟩ when i < j.

Equations

• CategoryTheory.Functor.ofCoconeObjIso c i hi = CategoryTheory.Functor.ofCocone.objIso c (↑⟨i, ⋯⟩) hi

def CategoryTheory.Functor.ofCoconeObjIsoPt {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) : (ofCocone c).obj ⟨j, ⋯⟩ ≅ c.pt

The isomorphism (ofCocone c).obj ⟨j, _⟩ ≅ c.pt.

Equations

• CategoryTheory.Functor.ofCoconeObjIsoPt c = CategoryTheory.Functor.ofCocone.objIsoPt c

theorem CategoryTheory.Functor.ofCocone_map_to_top {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i : J) (hi : i < j) : (ofCocone c).map (homOfLE ⋯) = CategoryStruct.comp (ofCoconeObjIso c i hi).hom (CategoryStruct.comp (c.ι.app ⟨i, hi⟩) (ofCoconeObjIsoPt c).inv)

theorem CategoryTheory.Functor.ofCocone_map {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) : (ofCocone c).map (homOfLE hi) = CategoryStruct.comp (ofCoconeObjIso c i₁ ⋯).hom (CategoryStruct.comp (F.map (homOfLE hi)) (ofCoconeObjIso c i₂ hi₂).inv)

theorem CategoryTheory.Functor.ofCocone_map_assoc {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) {Z : C} (h : (ofCocone c).obj ⟨i₂, ⋯⟩ ⟶ Z) : CategoryStruct.comp ((ofCocone c).map (homOfLE hi)) h = CategoryStruct.comp (ofCoconeObjIso c i₁ ⋯).hom (CategoryStruct.comp (F.map (homOfLE hi)) (CategoryStruct.comp (ofCoconeObjIso c i₂ hi₂).inv h))

theorem CategoryTheory.Functor.ofCoconeObjIso_hom_naturality {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) : CategoryStruct.comp ((ofCocone c).map (homOfLE hi)) (ofCoconeObjIso c i₂ hi₂).hom = CategoryStruct.comp (ofCoconeObjIso c i₁ ⋯).hom (F.map (homOfLE hi))

theorem CategoryTheory.Functor.ofCoconeObjIso_hom_naturality_assoc {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) {Z : C} (h : F.obj ⟨i₂, hi₂⟩ ⟶ Z) : CategoryStruct.comp ((ofCocone c).map (homOfLE hi)) (CategoryStruct.comp (ofCoconeObjIso c i₂ hi₂).hom h) = CategoryStruct.comp (ofCoconeObjIso c i₁ ⋯).hom (CategoryStruct.comp (F.map (homOfLE hi)) h)

def CategoryTheory.Functor.restrictionLTOfCoconeIso {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) : Iteration.restrictionLT (ofCocone c) ⋯ ≅ F

The isomorphism expressing that ofCocone c extends the functor F when c : Cocone F.

Equations

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

@[simp]

theorem CategoryTheory.Functor.restrictionLTOfCoconeIso_hom_app {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (X : ↑(Set.Iio j)) : (restrictionLTOfCoconeIso c).hom.app X = (ofCoconeObjIso c ↑X ⋯).hom

@[simp]

theorem CategoryTheory.Functor.restrictionLTOfCoconeIso_inv_app {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (X : ↑(Set.Iio j)) : (restrictionLTOfCoconeIso c).inv.app X = (ofCoconeObjIso c ↑X ⋯).inv

def CategoryTheory.Functor.isColimitCoconeOfLEOfCocone {C : Type u_1} [Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) : Limits.IsColimit (Iteration.coconeOfLE (ofCocone c) ⋯)

If c is a colimit cocone, then so is coconeOfLE (ofCocone c) (Preorder.le_refl j).

Equations

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