Commit 2023-03-13 13:03 8a946eea

View on Github →

feat: port CategoryTheory.Limits.Constructions.ZeroObjects (#2823)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean

added def CategoryTheory.Limits.binaryCofanZeroLeft

added def CategoryTheory.Limits.binaryCofanZeroLeftIsColimit

added def CategoryTheory.Limits.binaryCofanZeroRight

added def CategoryTheory.Limits.binaryCofanZeroRightIsColimit

added def CategoryTheory.Limits.binaryFanZeroLeft

added def CategoryTheory.Limits.binaryFanZeroLeftIsLimit

added def CategoryTheory.Limits.binaryFanZeroRight

added def CategoryTheory.Limits.binaryFanZeroRightIsLimit

added def CategoryTheory.Limits.coprodZeroIso

added theorem CategoryTheory.Limits.coprodZeroIso_inv

added theorem CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom

added theorem CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv

added theorem CategoryTheory.Limits.inr_coprod_zeroiso_hom

added theorem CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom

added theorem CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv

added theorem CategoryTheory.Limits.inr_zeroCoprodIso_hom

added def CategoryTheory.Limits.prodZeroIso

added theorem CategoryTheory.Limits.prodZeroIso_hom

added theorem CategoryTheory.Limits.prodZeroIso_iso_inv_snd

added def CategoryTheory.Limits.pullbackZeroZeroIso

added theorem CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst

added theorem CategoryTheory.Limits.pullbackZeroZeroIso_hom_snd

added theorem CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst

added theorem CategoryTheory.Limits.pullbackZeroZeroIso_inv_snd

added def CategoryTheory.Limits.pushoutZeroZeroIso

added def CategoryTheory.Limits.zeroCoprodIso

added theorem CategoryTheory.Limits.zeroCoprodIso_inv

added def CategoryTheory.Limits.zeroProdIso

added theorem CategoryTheory.Limits.zeroProdIso_hom

added theorem CategoryTheory.Limits.zeroProdIso_inv_snd