Commit 2025-02-03 05:29 b76b14cf

View on Github →

feat(CategoryTheory): the class of morphisms given by a family of maps (#21354) Given a family of morphisms f i : X i ⟶ Y i in a category C, this PR introduces that the class of morphisms ofHoms f : MorphismProperty C consisting of these morphisms f i.

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Arrow.lean

added theorem CategoryTheory.Arrow.arrow_mk_comp_eqToHom

added theorem CategoryTheory.Arrow.arrow_mk_eqToHom_comp

modified theorem CategoryTheory.Arrow.ext

added theorem CategoryTheory.Arrow.functor_ext

modified def CategoryTheory.Arrow.isoOfNatIso

added theorem CategoryTheory.Arrow.mk_eq_mk_iff

Modified Mathlib/CategoryTheory/Comma/CardinalArrow.lean

Modified Mathlib/CategoryTheory/Localization/Triangulated.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

added theorem CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff

added def CategoryTheory.MorphismProperty.homFamily

added theorem CategoryTheory.MorphismProperty.homFamily_apply

added theorem CategoryTheory.MorphismProperty.homFamily_arrow_mk

added inductive CategoryTheory.MorphismProperty.ofHoms

added theorem CategoryTheory.MorphismProperty.ofHoms_homFamily

added theorem CategoryTheory.MorphismProperty.ofHoms_iff

modified theorem CategoryTheory.MorphismProperty.of_eq

added def CategoryTheory.MorphismProperty.toSet