Commit 2022-05-24 12:33 9d193c59

feat(category_theory/comm_sq): functors mapping pullback/pushout squares (#14351)

lemma map_is_pullback [preserves_limit (cospan h i) F] (s : is_pullback f g h i) :
  is_pullback (F.map f) (F.map g) (F.map h) (F.map i) := ...

Estimated changes

Modified src/category_theory/limits/shapes/comm_sq.lean

added def category_theory.comm_sq.cocone

added def category_theory.comm_sq.cone

added theorem category_theory.comm_sq.flip

added theorem category_theory.comm_sq.of_arrow

added structure category_theory.comm_sq

added theorem category_theory.functor.map_comm_sq

added theorem category_theory.functor.map_is_pullback

added theorem category_theory.functor.map_is_pushout

added def category_theory.is_pullback.cone

added theorem category_theory.is_pullback.flip

added def category_theory.is_pullback.iso_pullback

added theorem category_theory.is_pullback.iso_pullback_hom_fst

added theorem category_theory.is_pullback.iso_pullback_hom_snd

added theorem category_theory.is_pullback.iso_pullback_inv_fst

added theorem category_theory.is_pullback.iso_pullback_inv_snd

added theorem category_theory.is_pullback.of_bot

added theorem category_theory.is_pullback.of_has_pullback

added theorem category_theory.is_pullback.of_is_limit'

added theorem category_theory.is_pullback.of_is_limit

added theorem category_theory.is_pullback.of_iso_pullback

added theorem category_theory.is_pullback.of_right

added theorem category_theory.is_pullback.paste_horiz

added theorem category_theory.is_pullback.paste_vert

added theorem category_theory.is_pullback.zero_left

added theorem category_theory.is_pullback.zero_top

added structure category_theory.is_pullback

added def category_theory.is_pushout.cocone

added theorem category_theory.is_pushout.flip

added theorem category_theory.is_pushout.inl_iso_pushout_hom

added theorem category_theory.is_pushout.inl_iso_pushout_inv

added theorem category_theory.is_pushout.inr_iso_pushout_hom

added theorem category_theory.is_pushout.inr_iso_pushout_inv

added def category_theory.is_pushout.iso_pushout

added theorem category_theory.is_pushout.of_bot

added theorem category_theory.is_pushout.of_has_pushout

added theorem category_theory.is_pushout.of_is_colimit'

added theorem category_theory.is_pushout.of_is_colimit

added theorem category_theory.is_pushout.of_iso_pushout

added theorem category_theory.is_pushout.of_right

added theorem category_theory.is_pushout.paste_horiz

added theorem category_theory.is_pushout.paste_vert

added theorem category_theory.is_pushout.zero_bot

added theorem category_theory.is_pushout.zero_right

added structure category_theory.is_pushout

deleted theorem category_theory.limits.comm_sq.flip

deleted theorem category_theory.limits.comm_sq.of_arrow

deleted structure category_theory.limits.comm_sq

deleted def category_theory.limits.is_pullback.cone

deleted theorem category_theory.limits.is_pullback.flip

deleted theorem category_theory.limits.is_pullback.of_bot

deleted theorem category_theory.limits.is_pullback.of_has_pullback

deleted theorem category_theory.limits.is_pullback.of_is_limit

deleted theorem category_theory.limits.is_pullback.of_right

deleted theorem category_theory.limits.is_pullback.paste_horiz

deleted theorem category_theory.limits.is_pullback.paste_vert

deleted theorem category_theory.limits.is_pullback.zero_left

deleted theorem category_theory.limits.is_pullback.zero_top

deleted structure category_theory.limits.is_pullback

deleted def category_theory.limits.is_pushout.cocone

deleted theorem category_theory.limits.is_pushout.flip

deleted theorem category_theory.limits.is_pushout.of_bot

deleted theorem category_theory.limits.is_pushout.of_has_pushout

deleted theorem category_theory.limits.is_pushout.of_is_colimit

deleted theorem category_theory.limits.is_pushout.of_right

deleted theorem category_theory.limits.is_pushout.paste_horiz

deleted theorem category_theory.limits.is_pushout.paste_vert

deleted theorem category_theory.limits.is_pushout.zero_bot

deleted theorem category_theory.limits.is_pushout.zero_right

deleted structure category_theory.limits.is_pushout

Modified src/category_theory/limits/shapes/pullbacks.lean

added def category_theory.limits.walking_cospan.ext

added def category_theory.limits.walking_span.ext