Commit 2026-02-06 21:24 045ac404

View on Github →

refactor(CategoryTheory): remove HasForget (#34741)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/AlgCat/Basic.lean

Modified Mathlib/Algebra/Category/BialgCat/Basic.lean

Modified Mathlib/Algebra/Category/CommAlgCat/Basic.lean

modified theorem CommAlgCat.forget_map

Modified Mathlib/Algebra/Category/CommBialgCat.lean

modified theorem CommBialgCat.forget_map

Modified Mathlib/Algebra/Category/GrpWithZero.lean

modified theorem GrpWithZero.forget_map

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Modified Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean

Modified Mathlib/Algebra/Category/ModuleCat/Semi.lean

Modified Mathlib/Algebra/Category/ModuleCat/Subobject.lean

Modified Mathlib/Algebra/Category/ModuleCat/Ulift.lean

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

Modified Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

Modified Mathlib/Algebra/Category/MonCat/Limits.lean

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

Modified Mathlib/Algebra/Category/Ring/FilteredColimits.lean

Modified Mathlib/Algebra/Category/Semigrp/Basic.lean

Modified Mathlib/Algebra/Homology/ImageToKernel.lean

Modified Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/AlgebraicGeometry/Sites/Representability.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

Modified Mathlib/CategoryTheory/Action/Basic.lean

Modified Mathlib/CategoryTheory/Action/Continuous.lean

modified def CategoryTheory.Functor.mapContActionComp

Modified Mathlib/CategoryTheory/Action/Limits.lean

Modified Mathlib/CategoryTheory/Category/Pointed.lean

Modified Mathlib/CategoryTheory/Category/TwoP.lean

Modified Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

added theorem CategoryTheory.ConcreteCategory.coe_comp

added theorem CategoryTheory.ConcreteCategory.coe_id

modified theorem CategoryTheory.ConcreteCategory.congr_arg

modified theorem CategoryTheory.ConcreteCategory.congr_hom

deleted theorem CategoryTheory.ConcreteCategory.forget_map_eq_coe

deleted theorem CategoryTheory.ConcreteCategory.forget₂_comp_apply

deleted theorem CategoryTheory.ConcreteCategory.hasCoeToFun_Type

modified theorem CategoryTheory.ConcreteCategory.hom_ext

deleted def CategoryTheory.HasForget.hasCoeToSort

deleted def CategoryTheory.HasForget₂.mk'

deleted def CategoryTheory.HasForget₂.trans

deleted theorem CategoryTheory.NatTrans.naturality_apply

deleted theorem CategoryTheory.coe_comp

deleted theorem CategoryTheory.coe_id

deleted theorem CategoryTheory.coe_toHasForget_instFunLike

deleted theorem CategoryTheory.comp_apply'

modified theorem CategoryTheory.comp_apply

deleted theorem CategoryTheory.congr_hom

deleted theorem CategoryTheory.forget_eq_ConcreteCategory_hom

deleted theorem CategoryTheory.forget_map_eq_coe

deleted theorem CategoryTheory.forget_obj

deleted theorem CategoryTheory.forget₂_comp_apply

deleted def CategoryTheory.hasForgetToType

modified theorem CategoryTheory.hom_comp

modified theorem CategoryTheory.hom_id

modified theorem CategoryTheory.id_apply

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

deleted def CategoryTheory.BundledHom.map

deleted def CategoryTheory.BundledHom.mkHasForget₂

deleted structure CategoryTheory.BundledHom

Modified Mathlib/CategoryTheory/ConcreteCategory/Elementwise.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean

Created Mathlib/CategoryTheory/ConcreteCategory/Forget.lean

added theorem CategoryTheory.ConcreteCategory.forget_map_eq_coe

added theorem CategoryTheory.ConcreteCategory.forget₂_comp_apply

added def CategoryTheory.HasForget₂.mk'

added def CategoryTheory.HasForget₂.trans

added theorem CategoryTheory.NatTrans.naturality_apply

added theorem CategoryTheory.Types.hom_eq_coe

added def CategoryTheory.forget

added theorem CategoryTheory.forget_obj

added theorem CategoryTheory.forget₂_comp_apply

Modified Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/UnbundledHom.lean

deleted def CategoryTheory.UnbundledHom.mkHasForget₂

Modified Mathlib/CategoryTheory/DifferentialObject.lean

Modified Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean

Modified Mathlib/CategoryTheory/FintypeCat.lean

Modified Mathlib/CategoryTheory/Functor/Flat.lean

Modified Mathlib/CategoryTheory/Galois/Examples.lean

Modified Mathlib/CategoryTheory/GradedObject.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/MonoCoprod.lean

Modified Mathlib/CategoryTheory/Limits/Types/Products.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Concrete.lean

Modified Mathlib/CategoryTheory/Sites/Adjunction.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean

Modified Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

Modified Mathlib/CategoryTheory/Sites/LeftExact.lean

Modified Mathlib/CategoryTheory/Sites/LocallyBijective.lean

Modified Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean

Modified Mathlib/CategoryTheory/Sites/LocallyInjective.lean

Modified Mathlib/CategoryTheory/Sites/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/PreservesSheafification.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Subfunctor/Basic.lean

Modified Mathlib/Condensed/Basic.lean

Modified Mathlib/Condensed/CartesianClosed.lean

Modified Mathlib/Condensed/Discrete/Basic.lean

Modified Mathlib/Condensed/Discrete/Characterization.lean

Modified Mathlib/Condensed/Discrete/LocallyConstant.lean

Modified Mathlib/Condensed/Discrete/Module.lean

Modified Mathlib/Condensed/Epi.lean

Modified Mathlib/Condensed/Explicit.lean

Modified Mathlib/Condensed/Light/Basic.lean

Modified Mathlib/Condensed/Light/Epi.lean

Modified Mathlib/Condensed/Light/Explicit.lean

Modified Mathlib/Condensed/Light/TopCatAdjunction.lean

Modified Mathlib/Condensed/TopCatAdjunction.lean

Modified Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

Modified Mathlib/Geometry/RingedSpace/Basic.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Order/Category/BddDistLat.lean

Modified Mathlib/Order/Category/BddOrd.lean

Modified Mathlib/Order/Category/BoolAlg.lean

Modified Mathlib/Order/Category/DistLat.lean

Modified Mathlib/Order/Category/FinBddDistLat.lean

Modified Mathlib/Order/Category/Frm.lean

Modified Mathlib/Order/Category/HeytAlg.lean

Modified Mathlib/Order/Category/Lat.lean

Modified Mathlib/Order/Category/LinOrd.lean

Modified Mathlib/Order/Category/PartOrd.lean

Modified Mathlib/Order/Category/PartOrdEmb.lean

Modified Mathlib/Order/Category/Preord.lean

Modified Mathlib/RepresentationTheory/FDRep.lean

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean

Modified Mathlib/RepresentationTheory/Tannaka.lean

Modified Mathlib/RingTheory/Invariant/Profinite.lean

Modified Mathlib/Tactic/CategoryTheory/Elementwise.lean

modified theorem Tactic.Elementwise.hom_elementwise

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

Modified Mathlib/Topology/Category/CompHausLike/Limits.lean

Modified Mathlib/Topology/Category/TopCat/Yoneda.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean

Modified Mathlib/Topology/Sheaves/MayerVietoris.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean

Modified Mathlib/Topology/Sheaves/Sheafify.lean

Modified MathlibTest/CategoryTheory/Elementwise.lean

modified theorem ElementwiseTest.HasForget.ex1

Modified MathlibTest/CategoryTheory/Sites/ConcreteSheafification.lean

Modified MathlibTest/CategoryTheory/Sites/PreservesSheafification.lean