Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-17 07:10 e83ba8f5

View on Github →

feat(category_theory/limits/shapes/diagonal): The diagonal object of a morphism. (#15711)

Estimated changes

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

added def category_theory.limits.diagonal_obj_pullback_fst_iso

added theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_fst_fst

added theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_fst_snd

added theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_snd

added theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_fst_fst

added theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_fst_snd

added theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_snd_fst

added theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_snd_snd

added theorem category_theory.limits.diagonal_pullback_fst

added def category_theory.limits.pullback.diagonal

added theorem category_theory.limits.pullback.diagonal_comp

added theorem category_theory.limits.pullback.diagonal_fst

added def category_theory.limits.pullback.diagonal_is_kernel_pair

added def category_theory.limits.pullback.diagonal_obj

added theorem category_theory.limits.pullback.diagonal_snd

added def category_theory.limits.pullback_diagonal_map_id_iso

added theorem category_theory.limits.pullback_diagonal_map_id_iso_hom_fst

added theorem category_theory.limits.pullback_diagonal_map_id_iso_hom_snd

added theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_fst

added theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_snd_fst

added theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_snd_snd

added def category_theory.limits.pullback_diagonal_map_iso

added theorem category_theory.limits.pullback_diagonal_map_iso_hom_fst

added theorem category_theory.limits.pullback_diagonal_map_iso_hom_snd

added theorem category_theory.limits.pullback_diagonal_map_iso_inv_fst

added theorem category_theory.limits.pullback_diagonal_map_iso_inv_snd_fst

added theorem category_theory.limits.pullback_diagonal_map_iso_inv_snd_snd

added theorem category_theory.limits.pullback_diagonal_map_snd_fst_fst

added theorem category_theory.limits.pullback_diagonal_map_snd_snd_fst

added def category_theory.limits.pullback_fst_fst_iso

added theorem category_theory.limits.pullback_fst_map_snd_is_pullback

added theorem category_theory.limits.pullback_lift_map_is_pullback

added theorem category_theory.limits.pullback_map_diagonal_is_pullback

added theorem category_theory.limits.pullback_map_eq_pullback_fst_fst_iso_inv

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

added def category_theory.is_kernel_pair.pullback