English
Let R → S be a tower of rings with S NoZeroDivisors and S algebraic over R, and A an R-algebra with an S-algebra structure such that the scalar tower is compatible. If the map R → A is injective, then the map S → A is also injective.
Русский
Пусть R ⊆ S ⊆ A образуют башню колец, S без нулевых делителей и S алгебраический над R, а A имеет структуры алгебры над R и над S так, что тензорная башня совместима. Если отображение R → A инъективно, то отображение S → A тоже инъективно.
LaTeX
$$$\\text{Injective}(\\operatorname{algebraMap} \\; R \\; A) \\;\Longrightarrow\\; \\text{Injective}(\\operatorname{algebraMap} \\; S \\; A)$$$
Lean4
theorem injective_tower_top (inj : Injective (algebraMap R A)) : Injective (algebraMap S A) :=
by
refine (injective_iff_map_eq_zero _).mpr fun s eq ↦ of_not_not fun ne ↦ ?_
have ⟨r, ne, dvd⟩ := (alg.1 s).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero ne)
refine ne (inj <| map_zero (algebraMap R A) ▸ zero_dvd_iff.mp ?_)
simp_rw [← eq, IsScalarTower.algebraMap_apply R S A, map_dvd (algebraMap S A) dvd]
