algebraMap_apply_eq_map_map_submonoid

English

The bottom localization map equals the composition of maps as dictated by the map_submonoid construction.

Русский

Нижняя локализационная карта равна композиции отображений, заданной конструкцией map_submonoid.

LaTeX

$$$\text{algebraMap } R_m S_m = \text{map } S_m (\text{algebraMap } R S) (\text{show } _ \leq (\text{Algebra.algebraMapSubmonoid } S M).comap _ \text{ from } M.le_comap_map) $$$

Lean4

/-- If the square below commutes, the bottom map is uniquely specified:
```
R  →  S
↓     ↓
Rₘ → Sₘ
```
-/
theorem algebraMap_apply_eq_map_map_submonoid (x) :
    algebraMap Rₘ Sₘ x =
      map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) x :=
  DFunLike.congr_fun (IsLocalization.algebraMap_eq_map_map_submonoid _ _ _ _) x

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