Commit 2023-03-31 10:28 de2321d0

View on Github →

feat: port CategoryTheory.Elements (#2815)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Elements.lean

added theorem CategoryTheory.CategoryOfElements.comp_val

added def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence

added theorem CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality

added theorem CategoryTheory.CategoryOfElements.ext

added def CategoryTheory.CategoryOfElements.fromCostructuredArrow

added theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_mk

added def CategoryTheory.CategoryOfElements.fromStructuredArrow

added theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_map

added theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_obj

added theorem CategoryTheory.CategoryOfElements.from_toCostructuredArrow_eq

added theorem CategoryTheory.CategoryOfElements.id_val

added def CategoryTheory.CategoryOfElements.map

added theorem CategoryTheory.CategoryOfElements.map_π

added def CategoryTheory.CategoryOfElements.structuredArrowEquivalence

added def CategoryTheory.CategoryOfElements.toCostructuredArrow

added def CategoryTheory.CategoryOfElements.toStructuredArrow

added theorem CategoryTheory.CategoryOfElements.toStructuredArrow_obj

added theorem CategoryTheory.CategoryOfElements.to_comma_map_right

added theorem CategoryTheory.CategoryOfElements.to_fromCostructuredArrow_eq

added def CategoryTheory.CategoryOfElements.π

added theorem CategoryTheory.Functor.Elements.ext

added def CategoryTheory.Functor.Elements

Modified Mathlib/CategoryTheory/StructuredArrow.lean

added theorem CategoryTheory.CostructuredArrow.eqToHom_left

added theorem CategoryTheory.CostructuredArrow.hom_ext

added theorem CategoryTheory.StructuredArrow.hom_ext