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.SmallObject.SuccStruct.ofCocone.obj {C : Type u_1} [Category.{v_1, 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 ofCocone.

Equations

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

def CategoryTheory.SmallObject.SuccStruct.ofCocone.objIso {C : Type u_1} [Category.{v_1, 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 ofCocone.

Equations

• CategoryTheory.SmallObject.SuccStruct.ofCocone.objIso c i hi = CategoryTheory.eqToIso ⋯

def CategoryTheory.SmallObject.SuccStruct.ofCocone.objIsoPt {C : Type u_1} [Category.{v_1, 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 ofCocone.

Equations

• CategoryTheory.SmallObject.SuccStruct.ofCocone.objIsoPt c = CategoryTheory.eqToIso ⋯

def CategoryTheory.SmallObject.SuccStruct.ofCocone.map {C : Type u_1} [Category.{v_1, 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 ofCocone.

Equations

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

theorem CategoryTheory.SmallObject.SuccStruct.ofCocone.map_id {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.ofCocone.map_comp {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.ofCocone {C : Type u_1} [Category.{v_1, 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.

theorem CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq {C : Type u_1} [Category.{v_1, 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⟩

def CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.ofCoconeObjIso c i hi = CategoryTheory.SmallObject.SuccStruct.ofCocone.objIso c (↑⟨i, ⋯⟩) hi

theorem CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq_pt {C : Type u_1} [Category.{v_1, 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

def CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIsoPt {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.ofCoconeObjIsoPt c = CategoryTheory.SmallObject.SuccStruct.ofCocone.objIsoPt c

theorem CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.ofCocone_map {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.ofCocone_map_assoc {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality_assoc {C : Type u_1} [Category.{v_1, 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.SmallObject.SuccStruct.restrictionLTOfCoconeIso {C : Type u_1} [Category.{v_1, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) : 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.SmallObject.SuccStruct.restrictionLTOfCoconeIso_inv_app {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_hom_app {C : Type u_1} [Category.{v_1, 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

def CategoryTheory.SmallObject.SuccStruct.isColimitCoconeOfLEOfCocone {C : Type u_1} [Category.{v_1, 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 (coconeOfLE (ofCocone c) ⋯)

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

Equations

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

theorem CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone {C : Type u_1} [Category.{v_1, u_1} C] {J : Type u} [LinearOrder J] {j : J} {F : Functor (↑(Set.Iio j)) C} (c : Limits.Cocone F) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j) : arrowMap (ofCocone c) i₁ i₂ h₁₂ ⋯ = Arrow.mk (F.map (homOfLE h₁₂))

theorem CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top {C : Type u_1} [Category.{v_1, 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) : arrowMap (ofCocone c) i j ⋯ ⋯ = Arrow.mk (c.ι.app ⟨i, hi⟩)