localization_localization_map_units

English

For any y in localizationLocalizationSubmodule M N, the image algebraMap_R_T y is a unit in T.

Русский

Для любого y из localizationLocalizationSubmodule M N образ algebraMap_R_T y является единицей в T.

LaTeX

$$$\text{IsUnit}(\mathrm{algebraMap}_{R\to T}(y))$$$

Lean4

theorem localization_localization_map_units [IsLocalization N T] (y : localizationLocalizationSubmodule M N) :
    IsUnit (algebraMap R T y) :=
  by
  obtain ⟨y', z, eq⟩ := mem_localizationLocalizationSubmodule.mp y.prop
  rw [IsScalarTower.algebraMap_apply R S T, eq, RingHom.map_mul, IsUnit.mul_iff]
  exact ⟨IsLocalization.map_units T y', (IsLocalization.map_units _ z).map (algebraMap S T)⟩

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