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}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(F : CategoryTheory.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
Instances For
def
CategoryTheory.Functor.extendToSucc.objIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
(X : C)
(i : ↑(Set.Iic j))
:
CategoryTheory.Functor.extendToSucc.obj F X ⟨↑i, ⋯⟩ ≅ F.obj i
The isomorphism obj F X ⟨i, _⟩ ≅ F.obj i when i : Set.Iic j.
Equations
Instances For
def
CategoryTheory.Functor.extendToSucc.objSuccIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
(X : C)
:
CategoryTheory.Functor.extendToSucc.obj F X ⟨Order.succ j, ⋯⟩ ≅ X
The isomorphism obj F X ⟨Order.succ j, _⟩ ≅ X.
Equations
Instances For
def
CategoryTheory.Functor.extendToSucc.map
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
(i₁ i₂ : J)
(hi : i₁ ≤ i₂)
(hi₂ : i₂ ≤ Order.succ j)
:
CategoryTheory.Functor.extendToSucc.obj F X ⟨i₁, ⋯⟩ ⟶ CategoryTheory.Functor.extendToSucc.obj F X ⟨i₂, hi₂⟩
extendToSucc, on morphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.extendToSucc.map_eq
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
(i₁ i₂ : J)
(hi : i₁ ≤ i₂)
(hi₂ : i₂ ≤ j)
:
CategoryTheory.Functor.extendToSucc.map hj F τ i₁ i₂ hi ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi))
(CategoryTheory.Functor.extendToSucc.objIso F X ⟨i₂, hi₂⟩).inv)
theorem
CategoryTheory.Functor.extendToSucc.map_self_succ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
:
CategoryTheory.Functor.extendToSucc.map hj F τ j (Order.succ j) ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.extendToSucc.objIso F X ⟨j, ⋯⟩).hom
(CategoryTheory.CategoryStruct.comp τ (CategoryTheory.Functor.extendToSucc.objSuccIso hj F X).inv)
@[simp]
theorem
CategoryTheory.Functor.extendToSucc.map_id
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
(i : J)
(hi : i ≤ Order.succ j)
:
CategoryTheory.Functor.extendToSucc.map hj F τ i i ⋯ hi = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.extendToSucc.obj F X ⟨i, ⋯⟩)
theorem
CategoryTheory.Functor.extendToSucc.map_comp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.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)
:
CategoryTheory.Functor.extendToSucc.map hj F τ i₁ i₃ ⋯ h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.extendToSucc.map hj F τ i₁ i₂ h₁₂ ⋯)
(CategoryTheory.Functor.extendToSucc.map hj F τ i₂ i₃ h₂₃ h)
def
CategoryTheory.Functor.extendToSucc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
:
CategoryTheory.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.
Instances For
def
CategoryTheory.Functor.extendToSuccObjIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
(i : ↑(Set.Iic j))
:
(CategoryTheory.Functor.extendToSucc hj F τ).obj ⟨↑i, ⋯⟩ ≅ F.obj i
The isomorphism (extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i when i : Set.Iic j
Equations
Instances For
def
CategoryTheory.Functor.extendToSuccObjSuccIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
:
(CategoryTheory.Functor.extendToSucc hj F τ).obj ⟨Order.succ j, ⋯⟩ ≅ X
The isomorphism (extendToSucc hj F τ).obj ⟨Order.succ j, _⟩ ≅ X.
Equations
Instances For
theorem
CategoryTheory.Functor.extendToSuccObjIso_hom_naturality
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
(i₁ i₂ : J)
(hi : i₁ ≤ i₂)
(hi₂ : i₂ ≤ j)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.extendToSucc hj F τ).map (CategoryTheory.homOfLE hi))
(CategoryTheory.Functor.extendToSuccObjIso hj F τ ⟨i₂, hi₂⟩).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.extendToSuccObjIso hj F τ ⟨i₁, ⋯⟩).hom
(F.map (CategoryTheory.homOfLE hi))
theorem
CategoryTheory.Functor.extendToSuccObjIso_hom_naturality_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.extendToSucc hj F τ).map (CategoryTheory.homOfLE hi))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.extendToSuccObjIso hj F τ ⟨i₂, hi₂⟩).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.extendToSuccObjIso hj F τ ⟨i₁, ⋯⟩).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi)) h)
def
CategoryTheory.Functor.extendToSuccRestrictionLEIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
:
The isomorphism expressing that extendToSucc hj F τ extends F.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.extendToSuccRestrictionLEIso_hom_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
(X✝ : ↑(Set.Iic j))
:
(CategoryTheory.Functor.extendToSuccRestrictionLEIso hj F τ).hom.app X✝ = (CategoryTheory.Functor.extendToSuccObjIso hj F τ X✝).hom
@[simp]
theorem
CategoryTheory.Functor.extendToSuccRestrictionLEIso_inv_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
(X✝ : ↑(Set.Iic j))
:
(CategoryTheory.Functor.extendToSuccRestrictionLEIso hj F τ).inv.app X✝ = (CategoryTheory.Functor.extendToSuccObjIso hj F τ X✝).inv
theorem
CategoryTheory.Functor.extentToSucc_map
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
(i₁ i₂ : J)
(hi : i₁ ≤ i₂)
(hi₂ : i₂ ≤ j)
:
(CategoryTheory.Functor.extendToSucc hj F τ).map (CategoryTheory.homOfLE hi) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.extendToSuccObjIso hj F τ ⟨i₁, ⋯⟩).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi))
(CategoryTheory.Functor.extendToSuccObjIso hj F τ ⟨i₂, hi₂⟩).inv)
theorem
CategoryTheory.Functor.extendToSucc_map_le_succ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{J : Type u}
[LinearOrder J]
[SuccOrder J]
{j : J}
(hj : ¬IsMax j)
(F : CategoryTheory.Functor (↑(Set.Iic j)) C)
{X : C}
(τ : F.obj ⟨j, ⋯⟩ ⟶ X)
:
(CategoryTheory.Functor.extendToSucc hj F τ).map (CategoryTheory.homOfLE ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.extendToSuccObjIso hj F τ ⟨j, ⋯⟩).hom
(CategoryTheory.CategoryStruct.comp τ (CategoryTheory.Functor.extendToSuccObjSuccIso hj F τ).inv)