Commit 2025-03-03 19:22 692313ef

View on Github →

feat(CategoryTheory): inclusion morphism into products in categories with 0-morphisms (#22504) Fixes TwoFx/cats#26

Estimated changes

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

added def CategoryTheory.Limits.Pi.ι

added theorem CategoryTheory.Limits.Pi.ι_π

added theorem CategoryTheory.Limits.Pi.ι_π_eq_id

added theorem CategoryTheory.Limits.Pi.ι_π_of_ne

added theorem CategoryTheory.Limits.Sigma.ι_π

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

added theorem CategoryTheory.Limits.Sigma.ι_π_of_ne

added def CategoryTheory.Limits.Sigma.π

added def CategoryTheory.Limits.coprod.fst

added theorem CategoryTheory.Limits.coprod.inl_fst

added theorem CategoryTheory.Limits.coprod.inl_snd

added theorem CategoryTheory.Limits.coprod.inr_fst

added theorem CategoryTheory.Limits.coprod.inr_snd

added def CategoryTheory.Limits.coprod.snd

added def CategoryTheory.Limits.prod.inl

added theorem CategoryTheory.Limits.prod.inl_fst

added theorem CategoryTheory.Limits.prod.inl_snd

added def CategoryTheory.Limits.prod.inr

added theorem CategoryTheory.Limits.prod.inr_fst

added theorem CategoryTheory.Limits.prod.inr_snd