Commit 2022-10-05 06:38 52a270e2

feat(category_theory/limits): bicartesian squares (#14375)

 X ⊞ Y --fst--> X
   |            |
  snd           0
   |            |
   v            v
   Y

Estimated changes

Created src/category_theory/limits/constructions/zero_objects.lean

added def category_theory.limits.binary_cofan_zero_left

added def category_theory.limits.binary_cofan_zero_left_is_colimit

added def category_theory.limits.binary_cofan_zero_right

added def category_theory.limits.binary_cofan_zero_right_is_colimit

added def category_theory.limits.binary_fan_zero_left

added def category_theory.limits.binary_fan_zero_left_is_limit

added def category_theory.limits.binary_fan_zero_right

added def category_theory.limits.binary_fan_zero_right_is_limit

added def category_theory.limits.coprod_zero_iso

added theorem category_theory.limits.coprod_zero_iso_inv

added theorem category_theory.limits.inl_pushout_zero_zero_iso_hom

added theorem category_theory.limits.inl_pushout_zero_zero_iso_inv

added theorem category_theory.limits.inr_coprod_zeroiso_hom

added theorem category_theory.limits.inr_pushout_zero_zero_iso_hom

added theorem category_theory.limits.inr_pushout_zero_zero_iso_inv

added theorem category_theory.limits.inr_zero_coprod_iso_hom

added def category_theory.limits.prod_zero_iso

added theorem category_theory.limits.prod_zero_iso_hom

added theorem category_theory.limits.prod_zero_iso_iso_inv_snd

added def category_theory.limits.pullback_zero_zero_iso

added theorem category_theory.limits.pullback_zero_zero_iso_hom_fst

added theorem category_theory.limits.pullback_zero_zero_iso_hom_snd

added theorem category_theory.limits.pullback_zero_zero_iso_inv_fst

added theorem category_theory.limits.pullback_zero_zero_iso_inv_snd

added def category_theory.limits.pushout_zero_zero_iso

added def category_theory.limits.zero_coprod_iso

added theorem category_theory.limits.zero_coprod_iso_inv

added def category_theory.limits.zero_prod_iso

added theorem category_theory.limits.zero_prod_iso_hom

added theorem category_theory.limits.zero_prod_iso_inv_snd

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

added def category_theory.limits.binary_cofan.is_colimit_mk

added def category_theory.limits.binary_fan.is_limit_mk

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

added theorem category_theory.bicartesian_sq.flip

added theorem category_theory.bicartesian_sq.of_has_biproduct₁

added theorem category_theory.bicartesian_sq.of_has_biproduct₂

added theorem category_theory.bicartesian_sq.of_is_biproduct₁

added theorem category_theory.bicartesian_sq.of_is_biproduct₂

added theorem category_theory.bicartesian_sq.of_is_pullback_is_pushout

added structure category_theory.bicartesian_sq

added theorem category_theory.is_pullback.inl_snd'

added theorem category_theory.is_pullback.inl_snd

added theorem category_theory.is_pullback.inr_fst'

added theorem category_theory.is_pullback.inr_fst

added theorem category_theory.is_pullback.of_has_binary_biproduct

added theorem category_theory.is_pullback.of_has_biproduct

added theorem category_theory.is_pullback.of_is_bilimit'

added theorem category_theory.is_pullback.of_is_bilimit

added theorem category_theory.is_pullback.of_is_product'

added def category_theory.is_pullback.pullback_biprod_inl_biprod_inr

added theorem category_theory.is_pullback.zero_bot

modified theorem category_theory.is_pullback.zero_left

added theorem category_theory.is_pullback.zero_right

modified theorem category_theory.is_pullback.zero_top

modified structure category_theory.is_pullback

added theorem category_theory.is_pushout.inl_snd'

added theorem category_theory.is_pushout.inl_snd

added theorem category_theory.is_pushout.inr_fst'

added theorem category_theory.is_pushout.inr_fst

added theorem category_theory.is_pushout.of_has_binary_biproduct

added theorem category_theory.is_pushout.of_has_biproduct

added theorem category_theory.is_pushout.of_is_bilimit'

added theorem category_theory.is_pushout.of_is_bilimit

added theorem category_theory.is_pushout.of_is_coproduct'

added def category_theory.is_pushout.pushout_biprod_fst_biprod_snd

modified theorem category_theory.is_pushout.zero_bot

added theorem category_theory.is_pushout.zero_left

modified theorem category_theory.is_pushout.zero_right

added theorem category_theory.is_pushout.zero_top

modified structure category_theory.is_pushout