ofLocalizationSpan — Mathlib

English

The localization-span target principle yields a local-to-global principle for a map f: R→S via the span-target construction.

Русский

Принцип локализации по цели порождает принцип локального к глобальному переходу для отображения f: R→S через конструкцию span-target.

LaTeX

$$$\\text{OfLocalizationSpanTarget }P \\to \\text{IsLocalization map for }f$$$

Lean4

theorem ofLocalizationSpan (hP : RingHom.OfLocalizationSpanTarget @P)
    (hP' : RingHom.StableUnderCompositionWithLocalizationAwaySource @P) : RingHom.OfLocalizationSpan @P :=
  by
  introv R hs hs'
  apply_fun Ideal.map f at hs
  rw [Ideal.map_span, Ideal.map_top] at hs
  apply hP _ _ hs
  rintro ⟨_, r, hr, rfl⟩
  rw [← IsLocalization.map_comp (M := Submonoid.powers r) (S := Localization.Away r) (T := Submonoid.powers (f r))]
  · apply hP' _ r
    exact hs' ⟨r, hr⟩

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