Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-10 16:44 477af65c

View on Github →

feat(category_theory/limits/shapes/wide_pullbacks): Adds some wrappers around the (co)limit api for wide pullbacks/pushouts (#7546) This PR adds some wrappers (mostly abbreviations) around the (co)limit api specifically for wide pullbacks and wide pushouts.

Estimated changes

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

added def category_theory.limits.has_wide_pullback

added def category_theory.limits.has_wide_pushout

added def category_theory.limits.wide_pullback.base

added theorem category_theory.limits.wide_pullback.eq_lift_of_comp_eq

added theorem category_theory.limits.wide_pullback.hom_eq_lift

added theorem category_theory.limits.wide_pullback.hom_ext

added def category_theory.limits.wide_pullback.lift

added theorem category_theory.limits.wide_pullback.lift_base

added theorem category_theory.limits.wide_pullback.lift_π

added def category_theory.limits.wide_pullback.π

added theorem category_theory.limits.wide_pullback.π_arrow

added def category_theory.limits.wide_pullback

added theorem category_theory.limits.wide_pushout.arrow_ι

added def category_theory.limits.wide_pushout.desc

added theorem category_theory.limits.wide_pushout.eq_desc_of_comp_eq

added def category_theory.limits.wide_pushout.head

added theorem category_theory.limits.wide_pushout.head_desc

added theorem category_theory.limits.wide_pushout.hom_eq_desc

added theorem category_theory.limits.wide_pushout.hom_ext

added def category_theory.limits.wide_pushout.ι

added theorem category_theory.limits.wide_pushout.ι_desc

added def category_theory.limits.wide_pushout