Commit 2023-03-08 07:00 fa930011

View on Github →

feat: port CategoryTheory.Limits.Shapes.ZeroMorphisms (#2621)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

added theorem CategoryTheory.Functor.zero_obj

added theorem CategoryTheory.Limits.HasZeroMorphisms.ext

added theorem CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom

added theorem CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_inv

added theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_hom

added theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_inv

added theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_hom

added theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv

added theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom

added theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv

added def CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject

added theorem CategoryTheory.Limits.IsZero.eq_zero_of_src

added theorem CategoryTheory.Limits.IsZero.eq_zero_of_tgt

added def CategoryTheory.Limits.IsZero.hasZeroMorphisms

added theorem CategoryTheory.Limits.IsZero.iff_id_eq_zero

added theorem CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero

added theorem CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero

added theorem CategoryTheory.Limits.IsZero.map

added theorem CategoryTheory.Limits.IsZero.of_epi

added theorem CategoryTheory.Limits.IsZero.of_epi_eq_zero

added theorem CategoryTheory.Limits.IsZero.of_epi_zero

added theorem CategoryTheory.Limits.IsZero.of_mono

added theorem CategoryTheory.Limits.IsZero.of_mono_eq_zero

added theorem CategoryTheory.Limits.IsZero.of_mono_zero

added theorem CategoryTheory.Limits.comp_factorThruImage_eq_zero

added theorem CategoryTheory.Limits.comp_zero

added theorem CategoryTheory.Limits.epi_of_target_iso_zero

added theorem CategoryTheory.Limits.eq_zero_of_image_eq_zero

added theorem CategoryTheory.Limits.hasZeroObject_of_hasInitial_object

added theorem CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object

added def CategoryTheory.Limits.idZeroEquivIsoZero

added theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom

added theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv

added theorem CategoryTheory.Limits.id_zero

added theorem CategoryTheory.Limits.image.ι_zero'

added theorem CategoryTheory.Limits.image.ι_zero

added def CategoryTheory.Limits.imageFactorisationZero

added def CategoryTheory.Limits.imageZero'

added def CategoryTheory.Limits.imageZero

added theorem CategoryTheory.Limits.image_ι_comp_eq_zero

added def CategoryTheory.Limits.isIsoZeroEquiv

added def CategoryTheory.Limits.isIsoZeroEquivIsoZero

added def CategoryTheory.Limits.isIsoZeroSelfEquiv

added def CategoryTheory.Limits.isIsoZeroSelfEquivIsoZero

added theorem CategoryTheory.Limits.isIso_of_source_target_iso_zero

added def CategoryTheory.Limits.isoOfIsIsomorphicZero

added def CategoryTheory.Limits.isoZeroOfEpiEqZero

added def CategoryTheory.Limits.isoZeroOfEpiZero

added def CategoryTheory.Limits.isoZeroOfMonoEqZero

added def CategoryTheory.Limits.isoZeroOfMonoZero

added def CategoryTheory.Limits.monoFactorisationZero

added theorem CategoryTheory.Limits.mono_of_source_iso_zero

added theorem CategoryTheory.Limits.nonzero_image_of_nonzero

added theorem CategoryTheory.Limits.zero_app

added theorem CategoryTheory.Limits.zero_comp

added theorem CategoryTheory.Limits.zero_of_comp_mono

added theorem CategoryTheory.Limits.zero_of_epi_comp

added theorem CategoryTheory.Limits.zero_of_from_zero

added theorem CategoryTheory.Limits.zero_of_source_iso_zero'

added theorem CategoryTheory.Limits.zero_of_source_iso_zero

added theorem CategoryTheory.Limits.zero_of_target_iso_zero'

added theorem CategoryTheory.Limits.zero_of_target_iso_zero

added theorem CategoryTheory.Limits.zero_of_to_zero

added theorem CategoryTheory.zero_map