Commit 2023-03-07 13:26 dcdfad20

View on Github →

feat: port CategoryTheory.Limits.Shapes.ZeroObjects (#2594)

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.Functor.isZero

added theorem CategoryTheory.Functor.isZero_iff

added theorem CategoryTheory.Iso.isZero_iff

added theorem CategoryTheory.Limits.HasZeroObject.from_zero_ext

added theorem CategoryTheory.Limits.HasZeroObject.to_zero_ext

added def CategoryTheory.Limits.HasZeroObject.zeroIsInitial

added def CategoryTheory.Limits.HasZeroObject.zeroIsTerminal

added def CategoryTheory.Limits.HasZeroObject.zeroIsoInitial

added def CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial

added def CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal

added def CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal

added theorem CategoryTheory.Limits.IsZero.eq_from

added theorem CategoryTheory.Limits.IsZero.eq_of_src

added theorem CategoryTheory.Limits.IsZero.eq_of_tgt

added theorem CategoryTheory.Limits.IsZero.eq_to

added theorem CategoryTheory.Limits.IsZero.from_eq

added theorem CategoryTheory.Limits.IsZero.hasZeroObject

added def CategoryTheory.Limits.IsZero.iso

added def CategoryTheory.Limits.IsZero.isoIsInitial

added def CategoryTheory.Limits.IsZero.isoIsTerminal

added def CategoryTheory.Limits.IsZero.isoZero

added theorem CategoryTheory.Limits.IsZero.obj

added theorem CategoryTheory.Limits.IsZero.of_iso

added theorem CategoryTheory.Limits.IsZero.op

added theorem CategoryTheory.Limits.IsZero.to_eq

added theorem CategoryTheory.Limits.IsZero.unop

added structure CategoryTheory.Limits.IsZero

added theorem CategoryTheory.Limits.hasZeroObject_unop

added theorem CategoryTheory.Limits.isZero_zero