Commit 2026-09-03 15:14 b6f78cf9

View on Github →

refactor(CategoryTheory): cleaning up Functor.Elements (#43228) The objects and morphisms of Functor.Elements are redefined using structures. The definition which were in the CategoryOfElements namespace are moved to Functor.Elements.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

Modified Mathlib/CategoryTheory/Action.lean

deleted theorem CategoryTheory.ActionCategory.homOfPair.val

modified def CategoryTheory.ActionCategory.homOfPair

added theorem CategoryTheory.ActionCategory.homOfPair_hom

deleted theorem CategoryTheory.ActionCategory.hom_as_subtype

modified def CategoryTheory.ActionCategory.stabilizerIsoEnd

modified theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply

modified theorem CategoryTheory.ActionCategory.π_map

Modified Mathlib/CategoryTheory/Elements.lean

deleted theorem CategoryTheory.CategoryOfElements.comp_val

deleted def CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence

deleted def CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso

deleted def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence

deleted def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj

deleted def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ

deleted theorem CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality

deleted theorem CategoryTheory.CategoryOfElements.ext

deleted def CategoryTheory.CategoryOfElements.fromCostructuredArrow

deleted theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_mk

deleted def CategoryTheory.CategoryOfElements.fromStructuredArrow

deleted theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_map

deleted theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_obj

deleted def CategoryTheory.CategoryOfElements.homMk

deleted theorem CategoryTheory.CategoryOfElements.id_val

deleted def CategoryTheory.CategoryOfElements.isoMk

deleted def CategoryTheory.CategoryOfElements.map

deleted theorem CategoryTheory.CategoryOfElements.map_snd

deleted theorem CategoryTheory.CategoryOfElements.map_π

deleted def CategoryTheory.CategoryOfElements.structuredArrowEquivalence

deleted def CategoryTheory.CategoryOfElements.toCostructuredArrow

deleted def CategoryTheory.CategoryOfElements.toStructuredArrow

deleted theorem CategoryTheory.CategoryOfElements.toStructuredArrow_obj

modified theorem CategoryTheory.CategoryOfElements.to_comma_map_right

deleted def CategoryTheory.CategoryOfElements.π

added structure CategoryTheory.Functor.Elements.Hom

added def CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence

added def CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso

added def CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalence

added def CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceFunctorProj

added def CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceInverseπ

modified theorem CategoryTheory.Functor.Elements.ext

added def CategoryTheory.Functor.Elements.fromCostructuredArrow

added theorem CategoryTheory.Functor.Elements.fromCostructuredArrow_obj_mk

added def CategoryTheory.Functor.Elements.fromStructuredArrow

added theorem CategoryTheory.Functor.Elements.hom_ext

deleted def CategoryTheory.Functor.Elements.initial

deleted def CategoryTheory.Functor.Elements.initialOfCorepresentableBy

deleted def CategoryTheory.Functor.Elements.initialOfRepresentableBy

deleted def CategoryTheory.Functor.Elements.isInitial

modified def CategoryTheory.Functor.Elements.isInitialOfCorepresentableBy

modified def CategoryTheory.Functor.Elements.isInitialOfRepresentableBy

added def CategoryTheory.Functor.Elements.isInitialYonedaObj

added def CategoryTheory.Functor.Elements.isoMk

modified def CategoryTheory.Functor.Elements.precomp

added def CategoryTheory.Functor.Elements.structuredArrowEquivalence

added def CategoryTheory.Functor.Elements.toCostructuredArrow

added def CategoryTheory.Functor.Elements.toStructuredArrow

added def CategoryTheory.Functor.Elements.π

added structure CategoryTheory.Functor.Elements

deleted def CategoryTheory.Functor.Elements

modified def CategoryTheory.NatTrans.mapElements

added def CategoryTheory.NatTrans.mapElementsCompπIso

added def CategoryTheory.NatTrans.mapElementsOpCompToCostructuredArrowIso

added theorem CategoryTheory.NatTrans.mapElements_comp_π

added theorem CategoryTheory.NatTrans.mapElements_op_comp_toCostructuredArrow

Modified Mathlib/CategoryTheory/Functor/Flat.lean

Modified Mathlib/CategoryTheory/Functor/TypeValuedFlat.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

Modified Mathlib/CategoryTheory/Limits/Elements.lean

deleted theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone

deleted theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement

deleted theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.π_liftedConeElement'

added theorem CategoryTheory.Functor.Elements.CreatesLimitsAux.map_lift_mapCone

added theorem CategoryTheory.Functor.Elements.CreatesLimitsAux.map_π_liftedConeElement

added theorem CategoryTheory.Functor.Elements.CreatesLimitsAux.π_liftedConeElement'

Modified Mathlib/CategoryTheory/Limits/Preserves/Presheaf.lean

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

Modified Mathlib/CategoryTheory/Limits/Weighted/HasWeightedLimit.lean

Modified Mathlib/CategoryTheory/Sites/Point/Basic.lean

Modified Mathlib/CategoryTheory/Sites/Point/Map.lean

Modified Mathlib/CategoryTheory/Sites/Point/OfIsCofiltered.lean

Modified Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Subfunctor/Basic.lean

Modified Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean

Modified Mathlib/Topology/Sheaves/Flasque.lean

Modified Mathlib/Topology/Sheaves/Points.lean