Pullbacks commute with connected limits #
noncomputable def
CategoryTheory.Limits.isLimitOfIsPullbackOfIsConnected
{I : Type u_1}
{C : Type u_2}
[Category.{u_3, u_1} I]
[IsConnected I]
[Category.{u_4, u_2} C]
{F G : Functor I C}
(α : F ⟶ G)
(cF : Cone F)
(cG : Cone G)
(f : (Cones.postcompose α).obj cF ⟶ cG)
(hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i))
(hcG : IsLimit cG)
:
IsLimit cF
Let F and G be two diagrams indexed by a connected I, and X and Y be two cones over
F and G respectively, with maps α : F ⟶ G and f : X ⟶ Y that commutes with the cone maps.
Suppose X = Y x[G i] F i for all i and Y = lim G, then X = lim F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.isColimitOfIsPushoutOfIsConnected
{I : Type u_1}
{C : Type u_2}
[Category.{u_3, u_1} I]
[IsConnected I]
[Category.{u_4, u_2} C]
{F G : Functor I C}
(α : F ⟶ G)
(cF : Cocone F)
(cG : Cocone G)
(f : cF ⟶ (Cocones.precompose α).obj cG)
(hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i))
(hcF : IsColimit cF)
:
IsColimit cG
Let F and G be two diagrams indexed by a connected I, and X and Y be two cocones over
F and G respectively, with maps α : F ⟶ G and f : X ⟶ Y that commutes with the cocone maps.
Suppose Y = X ⨿[F i] G i for all i and Y = colim G, then X = colim F.
Equations
- One or more equations did not get rendered due to their size.