Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 06:53 b5128b8a

View on Github →

feat(category_theory/limits): pullback squares (#14220) Per zulip.

Estimated changes

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

added theorem category_theory.limits.comm_sq.flip

added theorem category_theory.limits.comm_sq.of_arrow

added structure category_theory.limits.comm_sq

added def category_theory.limits.is_pullback.cone

added theorem category_theory.limits.is_pullback.flip

added theorem category_theory.limits.is_pullback.of_bot

added theorem category_theory.limits.is_pullback.of_has_pullback

added theorem category_theory.limits.is_pullback.of_is_limit

added theorem category_theory.limits.is_pullback.of_right

added theorem category_theory.limits.is_pullback.paste_horiz

added theorem category_theory.limits.is_pullback.paste_vert

added theorem category_theory.limits.is_pullback.zero_left

added theorem category_theory.limits.is_pullback.zero_top

added structure category_theory.limits.is_pullback

added def category_theory.limits.is_pushout.cocone

added theorem category_theory.limits.is_pushout.flip

added theorem category_theory.limits.is_pushout.of_bot

added theorem category_theory.limits.is_pushout.of_has_pushout

added theorem category_theory.limits.is_pushout.of_is_colimit

added theorem category_theory.limits.is_pushout.of_right

added theorem category_theory.limits.is_pushout.paste_horiz

added theorem category_theory.limits.is_pushout.paste_vert

added theorem category_theory.limits.is_pushout.zero_bot

added theorem category_theory.limits.is_pushout.zero_right

added structure category_theory.limits.is_pushout

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

added theorem category_theory.limits.pullback_cone.condition_one

added def category_theory.limits.pullback_cone.ext

added theorem category_theory.limits.pushout_cocone.condition_zero

added def category_theory.limits.pushout_cocone.ext