Commit 2026-09-13 10:05 2cf4ee53

View on Github →

chore(CategoryTheory/Limits/Shapes/Zero): use to_dual (#43554) This PR uses to_dual on zero objects and zero morphisms in category theory. Some more tagging can be done once products and binary products have been tagged with to_dual.

Estimated changes

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts/BinaryFan.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

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

deleted theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_hom

deleted theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv

deleted theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom

deleted theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv

deleted theorem CategoryTheory.Limits.IsColimit.isZero_pt

deleted def CategoryTheory.Limits.IsColimit.ofIsZero

deleted theorem CategoryTheory.Limits.IsTerminal.isZero

deleted theorem CategoryTheory.Limits.IsZero.eq_zero_of_tgt

deleted theorem CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero

deleted theorem CategoryTheory.Limits.IsZero.of_mono

deleted theorem CategoryTheory.Limits.IsZero.of_mono_eq_zero

deleted theorem CategoryTheory.Limits.IsZero.of_mono_zero

deleted theorem CategoryTheory.Limits.Sigma.ι_π_eq_id

deleted def CategoryTheory.Limits.Sigma.π

deleted theorem CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object

deleted theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom

deleted theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv

deleted def CategoryTheory.Limits.isoZeroOfMonoEqZero

deleted def CategoryTheory.Limits.isoZeroOfMonoZero

deleted theorem CategoryTheory.Limits.mono_of_source_iso_zero

modified theorem CategoryTheory.Limits.op_zero

modified theorem CategoryTheory.Limits.unop_zero

deleted theorem CategoryTheory.Limits.zero_comp

deleted theorem CategoryTheory.Limits.zero_of_comp_mono

deleted theorem CategoryTheory.Limits.zero_of_from_zero

deleted theorem CategoryTheory.Limits.zero_of_source_iso_zero

deleted theorem CategoryTheory.Limits.zero_of_target_iso_zero'

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

deleted theorem CategoryTheory.Limits.HasZeroObject.from_zero_ext

deleted def CategoryTheory.Limits.HasZeroObject.zeroIsTerminal

deleted def CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal

deleted def CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal

deleted theorem CategoryTheory.Limits.IsZero.eq_from

deleted theorem CategoryTheory.Limits.IsZero.eq_of_tgt

deleted theorem CategoryTheory.Limits.IsZero.from_eq

deleted def CategoryTheory.Limits.IsZero.isoIsTerminal

deleted theorem CategoryTheory.Limits.IsZero.mono

Modified Mathlib/CategoryTheory/Monoidal/Limits/Cokernels.lean