isIntegral_localization' — Mathlib

English

A restatement of integrality for a localized map under stronger hypotheses.

Русский

Переформулировка интегральности для локализованного отображения с дополнительными предпосылками.

LaTeX

$$$\text{isIntegral_localization'}$$$

Lean4

theorem isIntegral_localization' {R S : Type*} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IsIntegral)
    (M : Submonoid R) :
    (map (Localization (M.map (f : R →* S))) f (M.le_comap_map : _ ≤ Submonoid.comap (f : R →* S) _) :
        Localization M →+* _).IsIntegral :=
  let _ := f.toAlgebra
  have : Algebra.IsIntegral R S := ⟨hf⟩
  have : IsLocalization (Algebra.algebraMapSubmonoid S M) (Localization (Submonoid.map (f : R →* S) M)) :=
    Localization.isLocalization
  isIntegral_localization

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