Commit 2024-05-26 15:17 2549439e

View on Github →

feat(CategoryTheory/Localization): left resolutions for localizer morphisms (#12631) The left resolutions of a localizer morphism are defined, and it is shown that this is the dual notion to that of right resolutions for the opposite localizer morphism.

Estimated changes

Modified Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

added def CategoryTheory.LocalizerMorphism.op

Modified Mathlib/CategoryTheory/Localization/Resolution.lean

added def CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comp

added def CategoryTheory.LocalizerMorphism.LeftResolution.Hom.id

added structure CategoryTheory.LocalizerMorphism.LeftResolution.Hom

added theorem CategoryTheory.LocalizerMorphism.LeftResolution.comp_f

added theorem CategoryTheory.LocalizerMorphism.LeftResolution.hom_ext

added theorem CategoryTheory.LocalizerMorphism.LeftResolution.id_f

added theorem CategoryTheory.LocalizerMorphism.LeftResolution.mk_surjective

added def CategoryTheory.LocalizerMorphism.LeftResolution.op

added def CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence

added def CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor

added def CategoryTheory.LocalizerMorphism.LeftResolution.unop

added structure CategoryTheory.LocalizerMorphism.LeftResolution

added def CategoryTheory.LocalizerMorphism.RightResolution.op

added def CategoryTheory.LocalizerMorphism.RightResolution.unop

added def CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor

added theorem CategoryTheory.LocalizerMorphism.essSurj_of_hasLeftResolutions

modified theorem CategoryTheory.LocalizerMorphism.essSurj_of_hasRightResolutions

added theorem CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_op

added theorem CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_op

added theorem CategoryTheory.LocalizerMorphism.isIso_iff_of_hasLeftResolutions

modified theorem CategoryTheory.LocalizerMorphism.isIso_iff_of_hasRightResolutions

added theorem CategoryTheory.LocalizerMorphism.nonempty_leftResolution_iff_op

added theorem CategoryTheory.LocalizerMorphism.nonempty_rightResolution_iff_op