English
If L1 is a localization with W1 and L2 with W2, and W3 is inverted by L1 ⋙ L2 with suitable inequalities, then the composite L1 ⋙ L2 is a localization for W3.
Русский
Если L1 и L2 — локализации с W1, W2 соответственно, и W3 обращается по L1 ⋙ L2 с подходящими неравенствами, то составная локализация L1 ⋙ L2 локализует W3.
LaTeX
$$$\text{(L1 ∘ L2) isLocalization of } W3$ under hypotheses$$
Lean4
theorem comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] (W₃ : MorphismProperty C₁) (hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂))
(hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ ≤ W₃.map L₁) : (L₁ ⋙ L₂).IsLocalization W₃ := by
-- The proof proceeds by reducing to the case of the constructed
-- localized categories, which satisfy the strict universal property
-- of the localization. In order to do this, we introduce
-- an equivalence of categories `E₂ : C₂ ≅ W₁.Localization`. Via
-- this equivalence, we introduce `W₂' : MorphismProperty W₁.Localization`
-- which corresponds to `W₂` via the equivalence `E₂`.
-- Then, we have a localizer morphism `Φ : LocalizerMorphism W₂ W₂'` which
-- is a localized equivalence (because `E₂` is an equivalence).
let E₂ := Localization.uniq L₁ W₁.Q W₁
let W₂' := W₂.map E₂.functor
let Φ : LocalizerMorphism W₂ W₂' :=
{ functor := E₂.functor
map := by
have eq := W₂.isoClosure.inverseImage_map_eq_of_isEquivalence E₂.functor
rw [MorphismProperty.map_isoClosure] at eq
rw [eq]
apply W₂.le_isoClosure }
have :=
LocalizerMorphism.IsLocalizedEquivalence.of_equivalence Φ
(by rfl)
-- The fact that `Φ` is a localized equivalence allows to consider
-- the induced equivalence of categories `E₃ : C₃ ≅ W₂'.Localization`, and
-- the isomorphism `iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂`
let E₃ := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence
let iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ := by
calc
_ ≅ L₁ ⋙ E₂.functor ⋙ W₂'.Q ⋙ E₃.inverse :=
Functor.associator _ _ _ ≪≫ isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm _ ≪≫ Functor.associator _ _ _
_ ≅ L₁ ⋙ L₂ ⋙ E₃.functor ⋙ E₃.inverse :=
(isoWhiskerLeft _
((Functor.associator _ _ _).symm ≪≫
isoWhiskerRight (Φ.catCommSq L₂ W₂'.Q).iso E₃.inverse ≪≫ Functor.associator _ _ _))
_ ≅ L₁ ⋙ L₂ :=
isoWhiskerLeft _
(isoWhiskerLeft _ E₃.unitIso.symm ≪≫ L₂.rightUnitor)
-- In order to show `(W₁.Q ⋙ W₂'.Q).IsLocalization W₃`, we need
-- to check the assumptions of `StrictUniversalPropertyFixedTarget.comp`
have hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q) := by
simpa only [← MorphismProperty.IsInvertedBy.iff_comp _ _ E₃.inverse,
MorphismProperty.IsInvertedBy.iff_of_iso W₃ iso] using hW₃
have hW₂₃' : W₂' ≤ W₃.map W₁.Q :=
(MorphismProperty.monotone_map E₂.functor hW₂₃).trans
(by simpa only [W₃.map_map] using le_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁)))
have : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃ :=
by
refine IsLocalization.mk' _ _ ?_ ?_
all_goals
exact
(StrictUniversalPropertyFixedTarget.comp (strictUniversalPropertyFixedTargetQ W₁ _)
(strictUniversalPropertyFixedTargetQ W₂' _) W₃ hW₃' hW₁₃ hW₂₃')
-- Finally, the previous result can be transported via the equivalence `E₃`
exact IsLocalization.of_equivalence_target _ W₃ _ E₃.symm iso
