of_iso — Mathlib

English

If L1 ≅ L2 and L1 is a localization for W, then L2 is also a localization for W.

Русский

Если L1 изоморфно L2 и L1 является локализацией для W, то и L2 является локализацией для W.

LaTeX

$$$(L_1 \\cong L_2) \\;[L_1:\\text{IsLocalization } W] \\Rightarrow L_2\\text{ IsLocalization } W$$$

Lean4

theorem of_iso {L₁ L₂ : C ⥤ D} (e : L₁ ≅ L₂) [L₁.IsLocalization W] : L₂.IsLocalization W :=
  by
  have h := Localization.inverts L₁ W
  rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at h
  let F₁ := Localization.Construction.lift L₁ (Localization.inverts L₁ W)
  let F₂ := Localization.Construction.lift L₂ h
  exact
    { inverts := h
      isEquivalence := Functor.isEquivalence_of_iso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) }

Похожие утверждения