of_isLocalization — Mathlib

English

If S is a localization of R for a multiplicative set M, then EssFiniteType R S holds.

Русский

Если S является локализацией кольца R по множеству мультипликаторов M, то EssFiniteType R S выполняется.

LaTeX

$$$EssFiniteType R S$ given IsLocalization M S$$

Lean4

theorem of_isLocalization (M : Submonoid R) [IsLocalization M S] : EssFiniteType R S :=
  by
  rw [essFiniteType_iff]
  use ∅
  simp only [Finset.coe_empty, Algebra.adjoin_empty, Algebra.mem_bot, Set.mem_range, exists_exists_eq_and]
  intro s
  obtain ⟨⟨x, t⟩, e⟩ := IsLocalization.surj M s
  exact ⟨_, IsLocalization.map_units S t, x, e.symm⟩

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