algebraMap_eq_map_map_submonoid — Mathlib

English

There is a unique algebra map compatible with the localization generators, matching mk' rules on both sides.

Русский

Существует уникальная алгебраическая карта, совместимая с генераторами локализации, соответствующая правилам mk'.

LaTeX

$$$\text{IsLocalization.algEquiv } M S\; (\text{mk'}\; R_m x y) = \text{mk'}\; S x y$$$

Lean4

/-- If the square below commutes, the bottom map is uniquely specified:
```
R  →  S
↓     ↓
Rₘ → Sₘ
```
-/
theorem algebraMap_eq_map_map_submonoid :
    algebraMap Rₘ Sₘ =
      map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :=
  Eq.symm <|
    IsLocalization.map_unique _ (algebraMap Rₘ Sₘ) fun x => by
      rw [← IsScalarTower.algebraMap_apply R S Sₘ, ← IsScalarTower.algebraMap_apply R Rₘ Sₘ]

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