algebraMap_isLocalizationAway — Mathlib

English

The algebra map to a localization away r is standard-smooth of relative dimension 0.

Русский

Алгебраическая карта в локализацию удаленного элемента r имеет стандартную гладкость относительной размерности 0.

LaTeX

$$$$ \operatorname{IsStandardSmoothOfRelativeDimension}(0, \operatorname{algebraMap} R R^{\mathrm{Away}}_r). $$$$

Lean4

theorem algebraMap_isLocalizationAway {Rᵣ : Type*} [CommRing Rᵣ] [Algebra R Rᵣ] (r : R) [IsLocalization.Away r Rᵣ] :
    IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ) :=
  by
  have : (algebraMap R Rᵣ).toAlgebra = ‹Algebra R Rᵣ› := by
    ext
    rw [Algebra.smul_def]
    rfl
  rw [IsStandardSmoothOfRelativeDimension, this]
  exact Algebra.IsStandardSmoothOfRelativeDimension.localization_away r

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