Commit 2025-12-11 07:09 118bff18

View on Github →

feat(CategoryTheory): right Bousfield localization (#32469) This PR dualises definitions and basic results about ObjectProperty.isLocal and MorphismProperty.isLocal. The dual definitions are named ObjectProperty.isColocal and MorphismProperty.isColocal.

Estimated changes

Modified Mathlib/CategoryTheory/Localization/Adjunction.lean

added theorem CategoryTheory.Adjunction.isLocalization'

Modified Mathlib/CategoryTheory/Localization/Bousfield.lean

added theorem CategoryTheory.MorphismProperty.le_isColocal_isColocal

added theorem CategoryTheory.ObjectProperty.galoisConnection_isColocal

added def CategoryTheory.ObjectProperty.isColocal

added theorem CategoryTheory.ObjectProperty.isColocal_adj_counit_app

added theorem CategoryTheory.ObjectProperty.isColocal_eq_inverseImage_isomorphisms

added theorem CategoryTheory.ObjectProperty.isColocal_iff_isIso

added theorem CategoryTheory.ObjectProperty.isColocal_iff_isIso_map

added theorem CategoryTheory.ObjectProperty.isColocal_of_isIso

added theorem CategoryTheory.ObjectProperty.isLocalization_isColocal

added theorem CategoryTheory.ObjectProperty.isoClosure_isColocal

added theorem CategoryTheory.ObjectProperty.le_isColocal_iff

added theorem CategoryTheory.ObjectProperty.le_isColocal_isColocal

Modified Mathlib/CategoryTheory/Localization/Opposite.lean

added theorem CategoryTheory.Functor.IsLocalization.op_iff

deleted theorem CategoryTheory.Functor.op_iff

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

added theorem CategoryTheory.MorphismProperty.op_inverseImage

added theorem CategoryTheory.MorphismProperty.op_isomorphisms

Modified Mathlib/CategoryTheory/ObjectProperty/Local.lean

added def CategoryTheory.MorphismProperty.isColocal

added theorem CategoryTheory.MorphismProperty.isColocal_iff

Modified Mathlib/CategoryTheory/Triangulated/Orthogonal.lean

added theorem CategoryTheory.ObjectProperty.isColocal_trW

added theorem CategoryTheory.ObjectProperty.leftOrthogonal.map_bijective_of_isTriangulated