English
If L1 and L2 are localizations with W1,W2, and W3 is a localization on C1 with W1 ≤ W3 and W2 = W3.map L1, then L2 is a localization of W2.
Русский
Если L1 и L2 — локализации с W1,W2, и W3 — локализация на C1 с W1 ≤ W3 и W2 = W3.map L1, то L2 является локализацией W2.
LaTeX
$$$L2 \text{IsLocalization } W2$ under the stated equalities$$
Lean4
theorem of_comp (W₃ : MorphismProperty C₁) [L₁.IsLocalization W₁] [(L₁ ⋙ L₂).IsLocalization W₃] (hW₁₃ : W₁ ≤ W₃)
(hW₂₃ : W₂ = W₃.map L₁) : L₂.IsLocalization W₂ :=
by
have : (L₁ ⋙ W₂.Q).IsLocalization W₃ :=
comp L₁ W₂.Q W₁ W₂ W₃
(fun X Y f hf => Localization.inverts W₂.Q W₂ _ (by simpa only [hW₂₃] using W₃.map_mem_map _ _ hf)) hW₁₃
(by rw [hW₂₃])
exact
IsLocalization.of_equivalence_target W₂.Q W₂ L₂ (Localization.uniq (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃)
(liftNatIso L₁ W₁ _ _ _ _
((Functor.associator _ _ _).symm ≪≫ Localization.compUniqFunctor (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃))
