ofIsLocalization — Mathlib

English

If there exists a compatible set of localizations making the target ring is localized with respect to f, then P(f) follows from local data.

Русский

Если существует совместимый набор локализаций, делающих целевое кольцо локализованным по отношению к f, тогда P(f) следует из локальных данных.

LaTeX

$$$\\exists T, IsLocalization(\\text{map}) \\Rightarrow P(f)$$$

Lean4

theorem ofIsLocalization (hP : RingHom.OfLocalizationSpan P) (hPi : RingHom.RespectsIso P) {R S : Type u} [CommRing R]
    [CommRing S] (f : R →+* S) (s : Set R) (hs : Ideal.span s = ⊤)
    (hT :
      ∀ r : s,
        ∃ (Rᵣ Sᵣ : Type u) (_ : CommRing Rᵣ) (_ : CommRing Sᵣ) (_ : Algebra R Rᵣ) (_ : Algebra S Sᵣ) (_ :
          IsLocalization.Away r.val Rᵣ) (_ : IsLocalization.Away (f r.val) Sᵣ) (fᵣ : Rᵣ →+* Sᵣ) (_ :
          fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ) :
    P f := by
  apply hP _ s hs
  intro r
  obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, fᵣ, hfᵣ, hf⟩ := hT r
  let e₁ := (Localization.algEquiv (.powers r.val) Rᵣ).toRingEquiv
  let e₂ := (IsLocalization.algEquiv (.powers (f r.val)) (Localization (.powers (f r.val))) Sᵣ).symm.toRingEquiv
  have : Localization.awayMap f r.val = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom :=
    by
    apply IsLocalization.ringHom_ext (.powers r.val)
    ext x
    have : fᵣ ((algebraMap R Rᵣ) x) = algebraMap S Sᵣ (f x) := by rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]
    simp [-AlgEquiv.symm_toRingEquiv, e₂, e₁, Localization.awayMap, IsLocalization.Away.map, this]
  rw [this]
  apply hPi.right
  apply hPi.left
  exact hf

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