Commit 2025-11-24 11:02 0f04bd1f

View on Github →

chore(CategoryTheory): rename LeftBousfield.W as ObjectProperty.isLocal (#31842) This is more consistent with the dual construction MorphismProperty.isLocal.

Estimated changes

Modified Mathlib/CategoryTheory/Abelian/SerreClass/Bousfield.lean

added theorem CategoryTheory.Abelian.isoModSerre_kernel_eq_isLocal_of_rightAdjoint

deleted theorem CategoryTheory.Abelian.isoModSerre_kernel_eq_leftBousfield_W_of_rightAdjoint

Modified Mathlib/CategoryTheory/Localization/Bousfield.lean

deleted def CategoryTheory.Localization.LeftBousfield.W

deleted theorem CategoryTheory.Localization.LeftBousfield.W_adj_unit_app

deleted theorem CategoryTheory.Localization.LeftBousfield.W_eq_inverseImage_isomorphisms

deleted theorem CategoryTheory.Localization.LeftBousfield.W_iff_isIso

deleted theorem CategoryTheory.Localization.LeftBousfield.W_iff_isIso_map

deleted theorem CategoryTheory.Localization.LeftBousfield.W_isoClosure

deleted theorem CategoryTheory.Localization.LeftBousfield.W_of_isIso

deleted theorem CategoryTheory.Localization.LeftBousfield.galoisConnection

deleted theorem CategoryTheory.Localization.LeftBousfield.isLocalization

deleted theorem CategoryTheory.Localization.LeftBousfield.le_W_iff

added theorem CategoryTheory.MorphismProperty.le_isLocal_isLocal

deleted theorem CategoryTheory.MorphismProperty.le_leftBousfieldW_isLocal

added theorem CategoryTheory.ObjectProperty.galoisConnection_isLocal

added def CategoryTheory.ObjectProperty.isLocal

added theorem CategoryTheory.ObjectProperty.isLocal_adj_unit_app

added theorem CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms

added theorem CategoryTheory.ObjectProperty.isLocal_iff_isIso

added theorem CategoryTheory.ObjectProperty.isLocal_iff_isIso_map

added theorem CategoryTheory.ObjectProperty.isLocal_of_isIso

added theorem CategoryTheory.ObjectProperty.isLocalization_isLocal

added theorem CategoryTheory.ObjectProperty.isoClosure_isLocal

deleted theorem CategoryTheory.ObjectProperty.le_isLocal_W

added theorem CategoryTheory.ObjectProperty.le_isLocal_iff

added theorem CategoryTheory.ObjectProperty.le_isLocal_isLocal

Modified Mathlib/CategoryTheory/Localization/BousfieldTransfiniteComposition.lean

Modified Mathlib/CategoryTheory/ObjectProperty/Local.lean

Modified Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

added theorem CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc

deleted theorem CategoryTheory.OrthogonalReflection.leftBousfieldW_isLocal_toSucc

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

Modified Mathlib/CategoryTheory/Sites/Localization.lean

deleted theorem CategoryTheory.GrothendieckTopology.W_eq_W_range_sheafToPresheaf_obj

added theorem CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj

Modified Mathlib/CategoryTheory/Sites/PreservesSheafification.lean