mk — Mathlib · SciLib

English

Under suitable hypotheses on a property P (notably stability under isomorphisms and a local check on generators), one can construct the localization-span structure for P from data on a generating set of the source ring.

Русский

При надлежащих предположениях на свойство P (особенно устойчивость к изоморфизмам и локальная проверка на генераторах) можно сконструировать структуру локализации для P из данных о наборе генераторов исходного кольца.

LaTeX

$$$\\forall P\\; (hP: RingHom.RespectsIso P)\\; (H:\\ \\forall \\{R,S\\}, [\\mathrm{CommRing}\\ R]\\ [\\mathrm{CommRing}\\ S]\\ [\\mathrm{Algebra}\\ R S](s:\\mathrm{Set}\\ R),\\; \\mathrm{span}\\ s=\\top\\rightarrow (\\forall r\\in s, P(\\text{algebraMap} (\\mathrm{Localization.Away}\\ r) (\\mathrm{Localization.Away}\\ r \\otimes_R S)))\\rightarrow P(\\mathrm{algebraMap}\\ R S))\\rightarrow \\RingHom.OfLocalizationSpan P$$$

Lean4

theorem mk (hP : RingHom.RespectsIso P)
    (H :
      ∀ {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (s : Set R),
        Ideal.span s = ⊤ →
          (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)) :
    OfLocalizationSpan P := by
  introv R hs hf
  algebraize [f]
  let _ := fun r : R => (Localization.awayMap (algebraMap R S) r).toAlgebra
  refine H s hs (fun r hr ↦ ?_)
  have :
    algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S) =
      ((IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm : _ →+* _).comp
        (algebraMap (Localization.Away r) (Localization.Away (algebraMap R S r))) :=
    by
    apply IsLocalization.ringHom_ext (Submonoid.powers r)
    ext
    simp [RingHom.algebraMap_toAlgebra, Localization.awayMap, IsLocalization.Away.map,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra]
  rw [this]
  exact hP.1 _ _ (hf ⟨r, hr⟩)

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