Commit 2026-05-01 00:39 49f10344

View on Github →

chore(Topology/Category): replace TopCat by TopCat.{u} (#38779) TopCat has by design a free universe parameter. If we don't explicitly specify TopCat to be TopCat.{u}, universe unification can accidentally make lemmas less general. An example for this is TopCat.range_pullback_to_prod, which is currently unnecessarily specialized to TopCat.{0}.

Estimated changes

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

modified theorem TopModuleCat.freeMap_map

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

modified theorem AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

modified theorem FundamentalGroupoid.map_eq

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

modified theorem ContinuousMap.Homotopy.hcast_def

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

modified def AlgebraicGeometry.LocallyRingedSpace.ofRestrict

modified def AlgebraicGeometry.LocallyRingedSpace.restrict

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

modified theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp

modified theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp

modified theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp

Modified Mathlib/Geometry/RingedSpace/Stalks.lean

modified def AlgebraicGeometry.PresheafedSpace.restrictStalkIso

modified theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ

modified theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ

modified theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict

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

modified theorem TopCat.ext

modified theorem TopCat.hom_ext

modified theorem TopCat.hom_inv_id_apply

modified theorem TopCat.inv_hom_id_apply

modified theorem TopCat.isOpenEmbedding_iff_comp_isIso'

modified theorem TopCat.isOpenEmbedding_iff_comp_isIso

modified theorem TopCat.isOpenEmbedding_iff_isIso_comp'

modified theorem TopCat.isOpenEmbedding_iff_isIso_comp

modified theorem TopCat.ofHom_hom

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

modified theorem TopCat.exists_mem_zeroHypercover_range

modified theorem TopCat.isOpenEmbedding_f_zeroHypercover

modified theorem TopCat.isOpenEmbedding_iff

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

modified theorem TopCat.binaryCofan_isColimit_iff

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

modified theorem TopCat.fst_isEmbedding_of_right

modified theorem TopCat.fst_isOpenEmbedding_of_right

modified theorem TopCat.fst_iso_of_right_embedding_range_subset

modified theorem TopCat.isEmbedding_of_pullback

modified theorem TopCat.isOpenEmbedding_of_pullback

modified theorem TopCat.pullback_fst_range

modified theorem TopCat.pullback_snd_range

modified theorem TopCat.range_pullback_map

modified theorem TopCat.range_pullback_to_prod

modified theorem TopCat.snd_isEmbedding_of_left

modified theorem TopCat.snd_isOpenEmbedding_of_left

modified theorem TopCat.snd_iso_of_left_embedding_range_subset

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

modified def IsOpenMap.adjunction

modified def IsOpenMap.functor

modified theorem TopologicalSpace.Opens.adjunction_counit_app_self

modified theorem TopologicalSpace.Opens.adjunction_counit_map_functor

modified theorem TopologicalSpace.Opens.coe_inclusion'

modified theorem TopologicalSpace.Opens.functor_map_eq_inf

modified theorem TopologicalSpace.Opens.functor_obj_map_obj

modified theorem TopologicalSpace.Opens.inclusion'_map_eq_top

modified theorem TopologicalSpace.Opens.isOpenEmbedding_obj_top

modified theorem TopologicalSpace.Opens.mapMapIso_counitIso

modified theorem TopologicalSpace.Opens.mapMapIso_functor

modified theorem TopologicalSpace.Opens.mapMapIso_inverse

modified theorem TopologicalSpace.Opens.mapMapIso_unitIso

modified theorem TopologicalSpace.Opens.map_functor_eq'

modified theorem TopologicalSpace.Opens.map_functor_eq

modified theorem TopologicalSpace.Opens.set_range_inclusion'

modified def Topology.IsInducing.adjunction

modified def Topology.IsInducing.functor

modified def Topology.IsInducing.functorObj

modified theorem Topology.IsInducing.le_functorObj_iff

modified theorem Topology.IsInducing.map_functorObj

modified theorem Topology.IsInducing.mem_functorObj_iff

modified def Topology.IsInducing.opensGI

modified theorem Topology.IsOpenEmbedding.functor_obj_injective

Modified Mathlib/Topology/Sheaves/CommRingCat.lean

modified theorem TopCat.Presheaf.restrictOpenCommRingCat_apply

modified theorem TopCat.Presheaf.stalk_open_algebraMap

modified def TopCat.Sheaf.objSupIsoProdEqLocus

modified theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst

modified theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd

modified theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst

modified theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd

Modified Mathlib/Topology/Sheaves/Limits.lean

modified theorem TopCat.isSheaf_of_isLimit

modified theorem TopCat.limit_isSheaf

Modified Mathlib/Topology/Sheaves/Presheaf.lean

modified theorem TopCat.Presheaf.comp_app

modified theorem TopCat.Presheaf.ext

modified def TopCat.Presheaf.presheafEquivOfIso

modified def TopCat.Presheaf.pushforwardToOfIso

modified theorem TopCat.Presheaf.pushforwardToOfIso_app

modified def TopCat.Presheaf.toPushforwardOfIso

modified theorem TopCat.Presheaf.toPushforwardOfIso_app

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

Modified Mathlib/Topology/Sheaves/Stalks.lean

modified def TopCat.Presheaf.stalkCongr

modified theorem TopCat.Presheaf.stalkSpecializes_comp

modified theorem TopCat.Presheaf.stalkSpecializes_refl