Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Pullbacks commute with connected limits #

source
noncomputable def CategoryTheory.Limits.isLimitOfIsPullbackOfIsConnected {I : Type u_1} {C : Type u_2} [Category.{v_1, u_1} I] [IsConnected I] [Category.{v_2, u_2} C] {F G : Functor I C} (α : F ⟶ G) (cF : Cone F) (cG : Cone G) (f : (Cone.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
    source
    noncomputable def CategoryTheory.Limits.isColimitOfIsPushoutOfIsConnected {I : Type u_1} {C : Type u_2} [Category.{v_1, u_1} I] [IsConnected I] [Category.{v_2, u_2} C] {F G : Functor I C} (α : F ⟶ G) (cF : Cocone F) (cG : Cocone G) (f : cF ⟶ (Cocone.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.
    Instances For