Preserving pullbacks

Constructions to relate the notions of preserving pullbacks and reflecting pullbacks to concrete pullback cones.

In particular, we show that pullbackComparison G f g is an isomorphism iff G preserves the pullback of f and g.

The dual is also given.

TODO

• Generalise to wide pullbacks

@[reducible, inline]

abbrev CategoryTheory.Limits.PullbackCone.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) (G : Functor C D) : PullbackCone (G.map f) (G.map g)

The image of a pullback cone by a functor.

def CategoryTheory.Limits.PullbackCone.isLimitMapConeEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) (G : Functor C D) : IsLimit (G.mapCone c) ≃ IsLimit (c.map G)

The map (as a cone) of a pullback cone is limit iff the map (as a pullback cone) is limit.

def CategoryTheory.Limits.isLimitMapConePullbackConeEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : CategoryStruct.comp h f = CategoryStruct.comp k g) : IsLimit (G.mapCone (PullbackCone.mk h k comm)) ≃ IsLimit (PullbackCone.mk (G.map h) (G.map k) ⋯)

The map of a pullback cone is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute PullbackCone.mk with Functor.mapCone.

def CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : CategoryStruct.comp h f = CategoryStruct.comp k g) [PreservesLimit (cospan f g) G] (l : IsLimit (PullbackCone.mk h k comm)) : have this := ⋯; IsLimit (PullbackCone.mk (G.map h) (G.map k) this)

The property of preserving pullbacks expressed in terms of binary fans.

def CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : CategoryStruct.comp h f = CategoryStruct.comp k g) [ReflectsLimit (cospan f g) G] (l : IsLimit (PullbackCone.mk (G.map h) (G.map k) ⋯)) : IsLimit (PullbackCone.mk h k comm)

The property of reflecting pullbacks expressed in terms of binary fans.

def CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] : have this := ⋯; IsLimit (PullbackCone.mk (G.map (pullback.fst f g)) (G.map (pullback.snd f g)) this)

If G preserves pullbacks and C has them, then the pullback cone constructed of the mapped morphisms of the pullback cone is a limit.

theorem CategoryTheory.Limits.preservesPullback_symmetry {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] : PreservesLimit (cospan g f) G

If F preserves the pullback of f, g, it also preserves the pullback of g, f.

theorem CategoryTheory.Limits.hasPullback_of_preservesPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] : HasPullback (G.map f) (G.map g)

def CategoryTheory.Limits.PreservesPullback.iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] : G.obj (pullback f g) ≅ pullback (G.map f) (G.map g)

If G preserves the pullback of (f,g), then the pullback comparison map for G at (f,g) is an isomorphism.

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] : (iso G f g).hom = pullbackComparison G f g

theorem CategoryTheory.Limits.PreservesPullback.iso_hom_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] : CategoryStruct.comp (iso G f g).hom (pullback.fst (G.map f) (G.map g)) = G.map (pullback.fst f g)

theorem CategoryTheory.Limits.PreservesPullback.iso_hom_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] {Z✝ : D} (h : G.obj X ⟶ Z✝) : CategoryStruct.comp (iso G f g).hom (CategoryStruct.comp (pullback.fst (G.map f) (G.map g)) h) = CategoryStruct.comp (G.map (pullback.fst f g)) h

theorem CategoryTheory.Limits.PreservesPullback.iso_hom_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] : CategoryStruct.comp (iso G f g).hom (pullback.snd (G.map f) (G.map g)) = G.map (pullback.snd f g)

theorem CategoryTheory.Limits.PreservesPullback.iso_hom_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] {Z✝ : D} (h : G.obj Y ⟶ Z✝) : CategoryStruct.comp (iso G f g).hom (CategoryStruct.comp (pullback.snd (G.map f) (G.map g)) h) = CategoryStruct.comp (G.map (pullback.snd f g)) h

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] : CategoryStruct.comp (iso G f g).inv (G.map (pullback.fst f g)) = pullback.fst (G.map f) (G.map g)

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] {Z✝ : D} (h : G.obj X ⟶ Z✝) : CategoryStruct.comp (iso G f g).inv (CategoryStruct.comp (G.map (pullback.fst f g)) h) = CategoryStruct.comp (pullback.fst (G.map f) (G.map g)) h

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] : CategoryStruct.comp (iso G f g).inv (G.map (pullback.snd f g)) = pullback.snd (G.map f) (G.map g)

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [PreservesLimit (cospan f g) G] [HasPullback f g] [HasPullback (G.map f) (G.map g)] {Z✝ : D} (h : G.obj Y ⟶ Z✝) : CategoryStruct.comp (iso G f g).inv (CategoryStruct.comp (G.map (pullback.snd f g)) h) = CategoryStruct.comp (pullback.snd (G.map f) (G.map g)) h

def CategoryTheory.Limits.PullbackCone.isLimitCoyonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (c : PullbackCone f g) : IsLimit c ≃ ((X_1 : Cᵒᵖ) → IsLimit (c.map (coyoneda.obj X_1)))

A pullback cone in C is a limit iff it is so after the application of coyoneda.obj X for all X : Cᵒᵖ.

@[reducible, inline]

abbrev CategoryTheory.Limits.PushoutCocone.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {W X Y : C} {f : W ⟶ X} {g : W ⟶ Y} (c : PushoutCocone f g) (G : Functor C D) : PushoutCocone (G.map f) (G.map g)

The image of a pullback cone by a functor.

def CategoryTheory.Limits.PushoutCocone.isColimitMapCoconeEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {W X Y : C} {f : W ⟶ X} {g : W ⟶ Y} (c : PushoutCocone f g) (G : Functor C D) : IsColimit (G.mapCocone c) ≃ IsColimit (c.map G)

The map (as a cocone) of a pushout cocone is colimit iff the map (as a pushout cocone) is limit.

def CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) : IsColimit (G.mapCocone (PushoutCocone.mk h k comm)) ≃ IsColimit (PushoutCocone.mk (G.map h) (G.map k) ⋯)

The map of a pushout cocone is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute PushoutCocone.mk with Functor.mapCocone.

def CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) [PreservesColimit (span f g) G] (l : IsColimit (PushoutCocone.mk h k comm)) : IsColimit (PushoutCocone.mk (G.map h) (G.map k) ⋯)

The property of preserving pushouts expressed in terms of binary cofans.

def CategoryTheory.Limits.isColimitOfIsColimitPushoutCoconeMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : CategoryStruct.comp f h = CategoryStruct.comp g k) [ReflectsColimit (span f g) G] (l : IsColimit (PushoutCocone.mk (G.map h) (G.map k) ⋯)) : IsColimit (PushoutCocone.mk h k comm)

The property of reflecting pushouts expressed in terms of binary cofans.

def CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [i : HasPushout f g] : IsColimit (PushoutCocone.mk (G.map (pushout.inl f g)) (G.map (pushout.inr f g)) ⋯)

If G preserves pushouts and C has them, then the pushout cocone constructed of the mapped morphisms of the pushout cocone is a colimit.

theorem CategoryTheory.Limits.preservesPushout_symmetry {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] : PreservesColimit (span g f) G

If F preserves the pushout of f, g, it also preserves the pushout of g, f.

theorem CategoryTheory.Limits.hasPushout_of_preservesPushout {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] : HasPushout (G.map f) (G.map g)

def CategoryTheory.Limits.PreservesPushout.iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] : pushout (G.map f) (G.map g) ≅ G.obj (pushout f g)

If G preserves the pushout of (f,g), then the pushout comparison map for G at (f,g) is an isomorphism.

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] : (iso G f g).hom = pushoutComparison G f g

theorem CategoryTheory.Limits.PreservesPushout.inl_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] : CategoryStruct.comp (pushout.inl (G.map f) (G.map g)) (iso G f g).hom = G.map (pushout.inl f g)

theorem CategoryTheory.Limits.PreservesPushout.inl_iso_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] {Z : D} (h : G.obj (pushout f g) ⟶ Z) : CategoryStruct.comp (pushout.inl (G.map f) (G.map g)) (CategoryStruct.comp (iso G f g).hom h) = CategoryStruct.comp (G.map (pushout.inl f g)) h

theorem CategoryTheory.Limits.PreservesPushout.inr_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] : CategoryStruct.comp (pushout.inr (G.map f) (G.map g)) (iso G f g).hom = G.map (pushout.inr f g)

theorem CategoryTheory.Limits.PreservesPushout.inr_iso_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] {Z : D} (h : G.obj (pushout f g) ⟶ Z) : CategoryStruct.comp (pushout.inr (G.map f) (G.map g)) (CategoryStruct.comp (iso G f g).hom h) = CategoryStruct.comp (G.map (pushout.inr f g)) h

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.inl_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] : CategoryStruct.comp (G.map (pushout.inl f g)) (iso G f g).inv = pushout.inl (G.map f) (G.map g)

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.inl_iso_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] {Z : D} (h : pushout (G.map f) (G.map g) ⟶ Z) : CategoryStruct.comp (G.map (pushout.inl f g)) (CategoryStruct.comp (iso G f g).inv h) = CategoryStruct.comp (pushout.inl (G.map f) (G.map g)) h

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.inr_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] : CategoryStruct.comp (G.map (pushout.inr f g)) (iso G f g).inv = pushout.inr (G.map f) (G.map g)

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.inr_iso_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [PreservesColimit (span f g) G] [HasPushout f g] [HasPushout (G.map f) (G.map g)] {Z : D} (h : pushout (G.map f) (G.map g) ⟶ Z) : CategoryStruct.comp (G.map (pushout.inr f g)) (CategoryStruct.comp (iso G f g).inv h) = CategoryStruct.comp (pushout.inr (G.map f) (G.map g)) h

theorem CategoryTheory.Limits.PreservesPullback.of_iso_comparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] [HasPullback (G.map f) (G.map g)] [i : IsIso (pullbackComparison G f g)] : PreservesLimit (cospan f g) G

If the pullback comparison map for G at (f,g) is an isomorphism, then G preserves the pullback of (f,g).

instance CategoryTheory.Limits.instIsIsoPullbackComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] [HasPullback (G.map f) (G.map g)] [PreservesLimit (cospan f g) G] : IsIso (pullbackComparison G f g)

theorem CategoryTheory.Limits.PreservesPushout.of_iso_comparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] [HasPushout (G.map f) (G.map g)] [i : IsIso (pushoutComparison G f g)] : PreservesColimit (span f g) G

If the pushout comparison map for G at (f,g) is an isomorphism, then G preserves the pushout of (f,g).

instance CategoryTheory.Limits.instIsIsoPushoutComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] [HasPushout (G.map f) (G.map g)] [PreservesColimit (span f g) G] : IsIso (pushoutComparison G f g)

def CategoryTheory.Limits.PushoutCocone.isColimitYonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : IsColimit c ≃ ((X_1 : C) → IsLimit (c.op.map (yoneda.obj X_1)))

A pushout cocone in C is colimit iff it becomes limit after the application of yoneda.obj X for all X : C.