English
If there exists an injective map R/p → S/P making the natural square commute, then comap(algebraMap R S) P = p.
Русский
Если существует инъективное отображение R/p → S/P и диаграмма скаляров commute, то comap(algebraMap R S) P = p.
LaTeX
$$$\\operatorname{comap}(\\text{algebraMap } R S) P = p$$$
Lean4
/-- If there is an injective map `R/p → S/P` such that following diagram commutes:
```
R → S
↓ ↓
R/p → S/P
```
then `P` lies over `p`.
-/
theorem comap_eq_of_scalar_tower_quotient [Algebra R S] [Algebra (R ⧸ p) (S ⧸ P)] [IsScalarTower R (R ⧸ p) (S ⧸ P)]
(h : Function.Injective (algebraMap (R ⧸ p) (S ⧸ P))) : comap (algebraMap R S) P = p :=
by
ext x
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← Quotient.eq_zero_iff_mem, Quotient.mk_algebraMap,
IsScalarTower.algebraMap_apply R (R ⧸ p) (S ⧸ P), Quotient.algebraMap_eq]
constructor
· intro hx
exact (injective_iff_map_eq_zero (algebraMap (R ⧸ p) (S ⧸ P))).mp h _ hx
· intro hx
rw [hx, RingHom.map_zero]
