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} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i : J) (hi : i < j) : CategoryTheory.Functor.ofCocone.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} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor.ofCocone.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} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : CategoryTheory.Functor.ofCocone.obj c i₁ ⟶ CategoryTheory.Functor.ofCocone.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} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i : J) (hi : i ≤ j) : CategoryTheory.Functor.ofCocone.map c i i ⋯ hi = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.ofCocone.obj c i)

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

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

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

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

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

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

def CategoryTheory.Functor.restrictionLTOfCoconeIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor.Iteration.restrictionLT (CategoryTheory.Functor.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} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (X : ↑(Set.Iio j)) : (CategoryTheory.Functor.restrictionLTOfCoconeIso c).hom.app X = (CategoryTheory.Functor.ofCoconeObjIso c ↑X ⋯).hom

@[simp]

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

def CategoryTheory.Functor.isColimitCoconeOfLEOfCocone {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : CategoryTheory.Functor (↑(Set.Iio j)) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Functor.Iteration.coconeOfLE (CategoryTheory.Functor.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.