English
If S is the localization of R away from r, there is a canonical Generators object localizationAway R S Unit whose val maps to invSelf r and σ' encodes the unit generator.
Русский
Если S — локализация R away от r, существует канонический объект Generators localizationAway R S Unit, где val отображает обратное r, а σ' кодирует единичный генератор.
LaTeX
$$localizationAway : Generators R S Unit$$
Lean4
/-- If `S` is the localization of `R` away from `r`, we obtain a canonical generator mapping
to the inverse of `r`. -/
@[simps val, simps -isSimp σ]
noncomputable def localizationAway : Generators R S Unit
where
val _ := IsLocalization.Away.invSelf r
σ'
s :=
letI a : R := (IsLocalization.Away.sec r s).1
letI n : ℕ := (IsLocalization.Away.sec r s).2
C a * X () ^ n
aeval_val_σ'
s := by
rw [map_mul, algHom_C, map_pow, aeval_X]
simp only [← IsLocalization.Away.sec_spec, map_pow, IsLocalization.Away.invSelf]
rw [← IsLocalization.mk'_pow, one_pow, ← IsLocalization.mk'_one (M := Submonoid.powers r) S r]
rw [← IsLocalization.mk'_pow, one_pow, mul_assoc, ← IsLocalization.mk'_mul]
rw [mul_one, one_mul, IsLocalization.mk'_pow]
simp
