Commit 2022-11-03 01:01 f6bab678

View on Github →

feat(category_theory/limits/shapes/*): More API around kernel pairs. (#17301) is_kernel_pair is also redefined to be a Prop using the new is_pullback api.

Estimated changes

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

added theorem category_theory.comm_sq.cocone_inl

added theorem category_theory.comm_sq.cocone_inr

added theorem category_theory.comm_sq.cone_fst

added theorem category_theory.comm_sq.cone_snd

modified theorem category_theory.functor.map_is_pullback

modified theorem category_theory.functor.map_is_pushout

added theorem category_theory.is_pullback.cone_fst

added theorem category_theory.is_pullback.cone_snd

added theorem category_theory.is_pullback.flip_iff

added theorem category_theory.is_pullback.map_iff

added theorem category_theory.is_pullback.of_map

added theorem category_theory.is_pullback.of_map_of_faithful

added theorem category_theory.is_pullback.paste_horiz_iff

added theorem category_theory.is_pullback.paste_vert_iff

added theorem category_theory.is_pushout.cocone_inl

added theorem category_theory.is_pushout.cocone_inr

added theorem category_theory.is_pushout.flip_iff

added theorem category_theory.is_pushout.map_iff

added theorem category_theory.is_pushout.of_map

added theorem category_theory.is_pushout.of_map_of_faithful

added theorem category_theory.is_pushout.paste_horiz_iff

added theorem category_theory.is_pushout.paste_vert_iff

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

added theorem category_theory.limits.pullback.diagonal_is_kernel_pair

deleted def category_theory.limits.pullback.diagonal_is_kernel_pair

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

added theorem category_theory.is_kernel_pair.cancel_right

deleted def category_theory.is_kernel_pair.cancel_right

added theorem category_theory.is_kernel_pair.cancel_right_of_mono

deleted def category_theory.is_kernel_pair.cancel_right_of_mono

added theorem category_theory.is_kernel_pair.comp_of_mono

deleted def category_theory.is_kernel_pair.comp_of_mono

added theorem category_theory.is_kernel_pair.id_of_mono

deleted def category_theory.is_kernel_pair.id_of_mono

added theorem category_theory.is_kernel_pair.is_iso_of_mono

added theorem category_theory.is_kernel_pair.mono_of_is_iso_fst

added theorem category_theory.is_kernel_pair.of_is_iso_of_mono

added theorem category_theory.is_kernel_pair.pullback

deleted def category_theory.is_kernel_pair.pullback

added def category_theory.is_kernel_pair

deleted structure category_theory.is_kernel_pair