localizationAlgebraOfSubmonoidLe — Mathlib

English

Given submonoids M ≤ N of R, this is a canonical algebra structure of M^{-1}S acting on N^{-1}S, i.e., a lift of localization maps along the inclusion M ≤ N.

Русский

При задании M ≤ N внутри M локализация S действует на N локализацию S через естественную алгебраическую структуру.

LaTeX

$$localizationAlgebraOfSubmonoidLe (M N) (h : M ≤ N) [IsLocalization M S] [IsLocalization N T] : Algebra S T$$

Lean4

/-- Given submonoids `M ≤ N` of `R`, this is the canonical algebra structure
of `M⁻¹S` acting on `N⁻¹S`. -/
noncomputable abbrev localizationAlgebraOfSubmonoidLe (M N : Submonoid R) (h : M ≤ N) [IsLocalization M S]
    [IsLocalization N T] : Algebra S T :=
  (@IsLocalization.lift R _ M S _ _ T _ _ (algebraMap R T) (fun y => map_units T ⟨↑y, h y.prop⟩)).toAlgebra

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