Commit 2023-06-13 00:47 b7cba33a

View on Github →

feat: change ConcreteCategory.hasCoeToFun to FunLike (#4693)

Estimated changes

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

added theorem CommRingCat.RingEquiv_coe_eq

deleted theorem CommSemiRing.coe_comp

deleted theorem CommSemiRing.coe_id

deleted theorem CommSemiRing.coe_of

deleted theorem CommSemiRing.ext

deleted theorem CommSemiRing.forget_map

deleted def CommSemiRing.of

deleted def CommSemiRing.ofHom

added theorem CommSemiRingCat.RingEquiv_coe_eq

added theorem CommSemiRingCat.coe_comp

added theorem CommSemiRingCat.coe_id

added theorem CommSemiRingCat.coe_of

added theorem CommSemiRingCat.ext

added theorem CommSemiRingCat.forget_map

added def CommSemiRingCat.of

added def CommSemiRingCat.ofHom

added theorem RingCat.RingEquiv_coe_eq

added theorem SemiRingCat.RingEquiv_coe_eq

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

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

Modified Mathlib/Algebra/Ring/Equiv.lean

modified theorem RingEquiv.toRingHom_eq_coe

Modified Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean

Modified Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

Modified Mathlib/AlgebraicGeometry/RingedSpace.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

Modified Mathlib/AlgebraicTopology/TopologicalSimplex.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

added def CategoryTheory.ConcreteCategory.funLike

deleted def CategoryTheory.ConcreteCategory.hasCoeToFun

added theorem CategoryTheory.comp_apply'

modified theorem CategoryTheory.comp_apply

added theorem CategoryTheory.forget_map_eq_coe

modified theorem CategoryTheory.id_apply

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/CategoryTheory/Elementwise.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

Modified Mathlib/CategoryTheory/MorphismProperty.lean

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Sites/Surjective.lean

Modified Mathlib/Order/Category/NonemptyFinLinOrdCat.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/Tactic/CategoryTheory/Elementwise.lean

Modified Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean

Modified Mathlib/Topology/Category/CompHaus/Projective.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

Modified Mathlib/Topology/Category/Profinite/Projective.lean

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

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

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

added theorem TopCat.pullbackFst_apply

added theorem TopCat.pullbackSnd_apply

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

Modified Mathlib/Topology/Sheaves/Presheaf.lean

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

Modified Mathlib/Topology/Sheaves/Sheafify.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean

added theorem TopCat.Presheaf.germ_res_apply