category_theory.limits.preserves.shapes.pullbacks

source

def category_theory.limits.is_limit_map_cone_pullback_cone_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : h ≫ f = k ≫ g) :

category_theory.limits.is_limit (G.map_cone (category_theory.limits.pullback_cone.mk h k comm)) ≃ category_theory.limits.is_limit (category_theory.limits.pullback_cone.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 pullback_cone.mk with functor.map_cone.

Equations

source

def category_theory.limits.is_limit_pullback_cone_map_of_is_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : h ≫ f = k ≫ g) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] (l : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk h k comm)) :

category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk (G.map h) (G.map k) _)

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

Equations

category_theory.limits.is_limit_pullback_cone_map_of_is_limit G comm l = ⇑(category_theory.limits.is_limit_map_cone_pullback_cone_equiv G comm) (category_theory.limits.preserves_limit.preserves l)

source

def category_theory.limits.is_limit_of_is_limit_pullback_cone_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : h ≫ f = k ≫ g) [category_theory.limits.reflects_limit (category_theory.limits.cospan f g) G] (l : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk (G.map h) (G.map k) _)) :

category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk h k comm)

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

Equations

category_theory.limits.is_limit_of_is_limit_pullback_cone_map G comm l = category_theory.limits.reflects_limit.reflects (⇑((category_theory.limits.is_limit_map_cone_pullback_cone_equiv G comm).symm) l)

source

noncomputable def category_theory.limits.is_limit_of_has_pullback_of_preserves_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] :

category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk (G.map category_theory.limits.pullback.fst) (G.map category_theory.limits.pullback.snd) _)

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

Equations

category_theory.limits.is_limit_of_has_pullback_of_preserves_limit G f g = category_theory.limits.is_limit_pullback_cone_map_of_is_limit G category_theory.limits.pullback.condition (category_theory.limits.pullback_is_pullback f g)

source

def category_theory.limits.preserves_pullback_symmetry {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] :

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) G

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

Equations

category_theory.limits.preserves_pullback_symmetry G f g = {preserves := λ (c : category_theory.limits.cone (category_theory.limits.cospan g f)) (hc : category_theory.limits.is_limit c), (category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.diagram_iso_cospan (category_theory.limits.cospan g f ⋙ G)) (G.map_cone c)).to_fun ((category_theory.limits.pullback_cone.flip_is_limit ((category_theory.limits.is_limit_map_cone_pullback_cone_equiv G _).to_fun (category_theory.limits.preserves_limit.preserves (category_theory.limits.pullback_cone.flip_is_limit (((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.diagram_iso_cospan (category_theory.limits.cospan g f)) c).inv_fun hc).of_iso_limit (category_theory.limits.pullback_cone.iso_mk c)))))).of_iso_limit (category_theory.limits.pullback_cone.iso_mk (G.map_cone c)).symm)}

source

theorem category_theory.limits.has_pullback_of_preserves_pullback {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] :

category_theory.limits.has_pullback (G.map f) (G.map g)

source

noncomputable def category_theory.limits.preserves_pullback.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] :

G.obj (category_theory.limits.pullback f g) ≅ category_theory.limits.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.

Equations

category_theory.limits.preserves_pullback.iso G f g = (category_theory.limits.is_limit_of_has_pullback_of_preserves_limit G f g).cone_point_unique_up_to_iso (category_theory.limits.limit.is_limit (category_theory.limits.cospan (G.map f) (G.map g)))

source

theorem category_theory.limits.preserves_pullback.iso_hom_fst {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] :

(category_theory.limits.preserves_pullback.iso G f g).hom ≫ category_theory.limits.pullback.fst = G.map category_theory.limits.pullback.fst

source

theorem category_theory.limits.preserves_pullback.iso_hom_fst_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] {X' : D} (f' : G.obj X ⟶ X') :

(category_theory.limits.preserves_pullback.iso G f g).hom ≫ category_theory.limits.pullback.fst ≫ f' = G.map category_theory.limits.pullback.fst ≫ f'

source

theorem category_theory.limits.preserves_pullback.iso_hom_snd_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] {X' : D} (f' : G.obj Y ⟶ X') :

(category_theory.limits.preserves_pullback.iso G f g).hom ≫ category_theory.limits.pullback.snd ≫ f' = G.map category_theory.limits.pullback.snd ≫ f'

source

theorem category_theory.limits.preserves_pullback.iso_hom_snd {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] :

(category_theory.limits.preserves_pullback.iso G f g).hom ≫ category_theory.limits.pullback.snd = G.map category_theory.limits.pullback.snd

source

@[simp]

theorem category_theory.limits.preserves_pullback.iso_inv_fst_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] {X' : D} (f' : G.obj X ⟶ X') :

(category_theory.limits.preserves_pullback.iso G f g).inv ≫ G.map category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ f'

source

@[simp]

theorem category_theory.limits.preserves_pullback.iso_inv_fst {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] :

(category_theory.limits.preserves_pullback.iso G f g).inv ≫ G.map category_theory.limits.pullback.fst = category_theory.limits.pullback.fst

source

@[simp]

theorem category_theory.limits.preserves_pullback.iso_inv_snd_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] {X' : D} (f' : G.obj Y ⟶ X') :

(category_theory.limits.preserves_pullback.iso G f g).inv ≫ G.map category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.snd ≫ f'

source

@[simp]

theorem category_theory.limits.preserves_pullback.iso_inv_snd {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] :

(category_theory.limits.preserves_pullback.iso G f g).inv ≫ G.map category_theory.limits.pullback.snd = category_theory.limits.pullback.snd

source

def category_theory.limits.is_colimit_map_cocone_pushout_cocone_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : f ≫ h = g ≫ k) :

category_theory.limits.is_colimit (G.map_cocone (category_theory.limits.pushout_cocone.mk h k comm)) ≃ category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.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 pushout_cocone.mk with functor.map_cocone.

Equations

source

def category_theory.limits.is_colimit_pushout_cocone_map_of_is_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : f ≫ h = g ≫ k) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] (l : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk h k comm)) :

category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (G.map h) (G.map k) _)

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

Equations

category_theory.limits.is_colimit_pushout_cocone_map_of_is_colimit G comm l = ⇑(category_theory.limits.is_colimit_map_cocone_pushout_cocone_equiv G comm) (category_theory.limits.preserves_colimit.preserves l)

source

def category_theory.limits.is_colimit_of_is_colimit_pushout_cocone_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : f ≫ h = g ≫ k) [category_theory.limits.reflects_colimit (category_theory.limits.span f g) G] (l : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (G.map h) (G.map k) _)) :

category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk h k comm)

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

Equations

category_theory.limits.is_colimit_of_is_colimit_pushout_cocone_map G comm l = category_theory.limits.reflects_colimit.reflects (⇑((category_theory.limits.is_colimit_map_cocone_pushout_cocone_equiv G comm).symm) l)

source

noncomputable def category_theory.limits.is_colimit_of_has_pushout_of_preserves_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] :

category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (G.map category_theory.limits.pushout.inl) (G.map category_theory.limits.pushout.inr) _)

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

Equations

category_theory.limits.is_colimit_of_has_pushout_of_preserves_colimit G f g = category_theory.limits.is_colimit_pushout_cocone_map_of_is_colimit G category_theory.limits.pushout.condition (category_theory.limits.pushout_is_pushout f g)

source

def category_theory.limits.preserves_pushout_symmetry {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] :

category_theory.limits.preserves_colimit (category_theory.limits.span g f) G

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

Equations

category_theory.limits.preserves_pushout_symmetry G f g = {preserves := λ (c : category_theory.limits.cocone (category_theory.limits.span g f)) (hc : category_theory.limits.is_colimit c), (category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.limits.diagram_iso_span (category_theory.limits.span g f ⋙ G)).symm (G.map_cocone c)).to_fun ((category_theory.limits.pushout_cocone.flip_is_colimit ((category_theory.limits.is_colimit_map_cocone_pushout_cocone_equiv G _).to_fun (category_theory.limits.preserves_colimit.preserves (category_theory.limits.pushout_cocone.flip_is_colimit (((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.limits.diagram_iso_span (category_theory.limits.span ((category_theory.limits.span g f).map category_theory.limits.walking_span.hom.fst) ((category_theory.limits.span g f).map category_theory.limits.walking_span.hom.snd))) c).inv_fun hc).of_iso_colimit (category_theory.limits.pushout_cocone.iso_mk c)))))).of_iso_colimit (category_theory.limits.pushout_cocone.iso_mk (G.map_cocone c)).symm)}

source

theorem category_theory.limits.has_pushout_of_preserves_pushout {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] :

category_theory.limits.has_pushout (G.map f) (G.map g)

source

noncomputable def category_theory.limits.preserves_pushout.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] :

category_theory.limits.pushout (G.map f) (G.map g) ≅ G.obj (category_theory.limits.pushout f g)

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

Equations

category_theory.limits.preserves_pushout.iso G f g = (category_theory.limits.colimit.is_colimit (category_theory.limits.span (G.map f) (G.map g))).cocone_point_unique_up_to_iso (category_theory.limits.is_colimit_of_has_pushout_of_preserves_colimit G f g)

source

theorem category_theory.limits.preserves_pushout.inl_iso_hom_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] {X' : D} (f' : G.obj (category_theory.limits.pushout f g) ⟶ X') :

category_theory.limits.pushout.inl ≫ (category_theory.limits.preserves_pushout.iso G f g).hom ≫ f' = G.map category_theory.limits.pushout.inl ≫ f'

source

theorem category_theory.limits.preserves_pushout.inl_iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] :

category_theory.limits.pushout.inl ≫ (category_theory.limits.preserves_pushout.iso G f g).hom = G.map category_theory.limits.pushout.inl

source

theorem category_theory.limits.preserves_pushout.inr_iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] :

category_theory.limits.pushout.inr ≫ (category_theory.limits.preserves_pushout.iso G f g).hom = G.map category_theory.limits.pushout.inr

source

theorem category_theory.limits.preserves_pushout.inr_iso_hom_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] {X' : D} (f' : G.obj (category_theory.limits.pushout f g) ⟶ X') :

category_theory.limits.pushout.inr ≫ (category_theory.limits.preserves_pushout.iso G f g).hom ≫ f' = G.map category_theory.limits.pushout.inr ≫ f'

source

@[simp]

theorem category_theory.limits.preserves_pushout.inl_iso_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] :

G.map category_theory.limits.pushout.inl ≫ (category_theory.limits.preserves_pushout.iso G f g).inv = category_theory.limits.pushout.inl

source

@[simp]

theorem category_theory.limits.preserves_pushout.inl_iso_inv_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] {X' : D} (f' : category_theory.limits.pushout (G.map f) (G.map g) ⟶ X') :

G.map category_theory.limits.pushout.inl ≫ (category_theory.limits.preserves_pushout.iso G f g).inv ≫ f' = category_theory.limits.pushout.inl ≫ f'

source

@[simp]

theorem category_theory.limits.preserves_pushout.inr_iso_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] :

G.map category_theory.limits.pushout.inr ≫ (category_theory.limits.preserves_pushout.iso G f g).inv = category_theory.limits.pushout.inr

source

@[simp]

theorem category_theory.limits.preserves_pushout.inr_iso_inv_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] {X' : D} (f' : category_theory.limits.pushout (G.map f) (G.map g) ⟶ X') :

G.map category_theory.limits.pushout.inr ≫ (category_theory.limits.preserves_pushout.iso G f g).inv ≫ f' = category_theory.limits.pushout.inr ≫ f'

source

noncomputable def category_theory.limits.preserves_pullback.of_iso_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] [i : category_theory.is_iso (category_theory.limits.pullback_comparison G f g)] :

category_theory.limits.preserves_limit (category_theory.limits.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).

Equations

category_theory.limits.preserves_pullback.of_iso_comparison G = category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.pullback_is_pullback f g) (⇑((category_theory.limits.is_limit_map_cone_pullback_cone_equiv G category_theory.limits.pullback.condition).symm) (category_theory.limits.limit.is_limit (category_theory.limits.cospan (G.map f) (G.map g))).of_point_iso)

source

@[simp]

theorem category_theory.limits.preserves_pullback.iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] :

(category_theory.limits.preserves_pullback.iso G f g).hom = category_theory.limits.pullback_comparison G f g

source

@[protected, instance]

def category_theory.limits.pullback_comparison.category_theory.is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (G.map f) (G.map g)] [category_theory.limits.preserves_limit (category_theory.limits.cospan f g) G] :

category_theory.is_iso (category_theory.limits.pullback_comparison G f g)

source

noncomputable def category_theory.limits.preserves_pushout.of_iso_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] [i : category_theory.is_iso (category_theory.limits.pushout_comparison G f g)] :

category_theory.limits.preserves_colimit (category_theory.limits.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).

Equations

category_theory.limits.preserves_pushout.of_iso_comparison G = category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.limits.pushout_is_pushout f g) (⇑((category_theory.limits.is_colimit_map_cocone_pushout_cocone_equiv G category_theory.limits.pushout.condition).symm) (category_theory.limits.colimit.is_colimit (category_theory.limits.span (G.map f) (G.map g))).of_point_iso)

source

@[simp]

theorem category_theory.limits.preserves_pushout.iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] :

(category_theory.limits.preserves_pushout.iso G f g).hom = category_theory.limits.pushout_comparison G f g

source

@[protected, instance]

def category_theory.limits.pushout_comparison.category_theory.is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] [category_theory.limits.preserves_colimit (category_theory.limits.span f g) G] :

category_theory.is_iso (category_theory.limits.pushout_comparison G f g)

mathlib3 documentation

Preserving pullbacks #

TODO #