localizationAway — Mathlib

English

The kernel of localizationAway S r equals the ideal generated by {C r · X() − 1}.

Русский

Ядро локализации Away равно идеалу, порождённому элементом {C r · X() − 1}.

LaTeX

$$$\\mathrm{Generators.localizationAway}\\; S\\; r\\; .\\ker = \\operatorname{span}\\{ C r \\cdot X() - 1 \\}$$$

Lean4

/-- If `S` is the localization of `R` away from `r`, we can construct a natural
presentation of `S` as `R`-algebra with a single generator `X` and the relation `r * X - 1 = 0`. -/
@[simps relation]
noncomputable def localizationAway : Presentation R S Unit Unit
    where
  toGenerators := Generators.localizationAway S r
  relation _ := C r * X () - 1
  span_range_relation_eq_ker := by
    simp only [Set.range_const]
    exact (Generators.ker_localizationAway r).symm

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