Constructors for combining (co)fans #
We provide constructors for combining (co)fans and show their (co)limit properties.
TODO #
- Combine (co)fans on sigma types
@[reducible, inline]
abbrev
CategoryTheory.Limits.Fan.combPairHoms
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{f₁ : ι₁ → C}
{f₂ : ι₂ → C}
(c₁ : CategoryTheory.Limits.Fan f₁)
(c₂ : CategoryTheory.Limits.Fan f₂)
(bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt)
(i : ι₁ ⊕ ι₂)
:
For fans on maps f₁ : ι₁ → C, f₂ : ι₂ → C and a binary fan on their
cone points, construct one family of morphisms indexed by ι₁ ⊕ ι₂
Equations
- c₁.combPairHoms c₂ bc (Sum.inl a) = CategoryTheory.CategoryStruct.comp bc.fst (c₁.proj a)
- c₁.combPairHoms c₂ bc (Sum.inr a) = CategoryTheory.CategoryStruct.comp bc.snd (c₂.proj a)
Instances For
def
CategoryTheory.Limits.Fan.combPairIsLimit
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{f₁ : ι₁ → C}
{f₂ : ι₂ → C}
{c₁ : CategoryTheory.Limits.Fan f₁}
{c₂ : CategoryTheory.Limits.Fan f₂}
{bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt}
(h₁ : CategoryTheory.Limits.IsLimit c₁)
(h₂ : CategoryTheory.Limits.IsLimit c₂)
(h : CategoryTheory.Limits.IsLimit bc)
:
CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk bc.pt (c₁.combPairHoms c₂ bc))
If c₁ and c₂ are limit fans and bc is a limit binary fan on their cone
points, then the fan constructed from combPairHoms is a limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Limits.Cofan.combPairHoms
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{f₁ : ι₁ → C}
{f₂ : ι₂ → C}
(c₁ : CategoryTheory.Limits.Cofan f₁)
(c₂ : CategoryTheory.Limits.Cofan f₂)
(bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt)
(i : ι₁ ⊕ ι₂)
:
For cofans on maps f₁ : ι₁ → C, f₂ : ι₂ → C and a binary cofan on their
cocone points, construct one family of morphisms indexed by ι₁ ⊕ ι₂
Equations
- c₁.combPairHoms c₂ bc (Sum.inl a) = CategoryTheory.CategoryStruct.comp (c₁.inj a) bc.inl
- c₁.combPairHoms c₂ bc (Sum.inr a) = CategoryTheory.CategoryStruct.comp (c₂.inj a) bc.inr
Instances For
def
CategoryTheory.Limits.Cofan.combPairIsColimit
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{f₁ : ι₁ → C}
{f₂ : ι₂ → C}
{c₁ : CategoryTheory.Limits.Cofan f₁}
{c₂ : CategoryTheory.Limits.Cofan f₂}
{bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt}
(h₁ : CategoryTheory.Limits.IsColimit c₁)
(h₂ : CategoryTheory.Limits.IsColimit c₂)
(h : CategoryTheory.Limits.IsColimit bc)
:
CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk bc.pt (c₁.combPairHoms c₂ bc))
If c₁ and c₂ are colimit cofans and bc is a colimit binary cofan on their cocone
points, then the cofan constructed from combPairHoms is a colimit cocone.
Equations
- One or more equations did not get rendered due to their size.