localization_isScalarTower_of_submonoid_le

English

If M ≤ N are submonoids of R, then the natural map M^{-1}S →+* N^{-1}S commutes with localization maps, giving a scalar tower R S T.

Русский

Если M ≤ N — подмоноиды R, то естественная карта M^{-1}S → N^{-1}S коммутирует с локализациями и задаёт скалярную башню.

LaTeX

$$IsScalarTower R S T$$

Lean4

/-- If `M ≤ N` are submonoids of `R`, then the natural map `M⁻¹S →+* N⁻¹S` commutes with the
localization maps -/
theorem localization_isScalarTower_of_submonoid_le (M N : Submonoid R) (h : M ≤ N) [IsLocalization M S]
    [IsLocalization N T] : @IsScalarTower R S T _ (localizationAlgebraOfSubmonoidLe S T M N h).toSMul _ :=
  letI := localizationAlgebraOfSubmonoidLe S T M N h
  IsScalarTower.of_algebraMap_eq' (IsLocalization.lift_comp _).symm

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