ofIsLocalization' — Mathlib

English

A variant where the localized data uses the Away map construction, yielding P for the localized map.

Русский

Вариант, где локализованные данные используют отображение Away, давая P для локализованного отображения.

LaTeX

$$$\\text{OfLocalizationSpanTarget}'P \\Rightarrow P(f)$$$

Lean4

/-- Variant of `RingHom.OfLocalizationSpan.ofIsLocalization` where
`fᵣ = IsLocalization.Away.map`. -/
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ᵣ), P (IsLocalization.Away.map Rᵣ Sᵣ f r)) :
    P f := by
  apply hP.ofIsLocalization hPi _ s hs
  intro r
  obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, hf⟩ := hT r
  exact
    ⟨Rᵣ, Sᵣ, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
      IsLocalization.Away.map Rᵣ Sᵣ f r, IsLocalization.map_comp _, hf⟩

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