isScalarTower_of_section_of_ker_sqZero

English

From a section g: S → P with suitable square-zero hypotheses, one gets an IsScalarTower P S ker(algebraMap P S).

Русский

Из секции g: S → P при заданных гипотезах квадратно-нулевого ядра получаем IsScalarTower P S ker(algebraMap P S).

LaTeX

$$IsScalarTower P S (RingHom.ker (algebraMap P S))$$

Lean4

theorem isScalarTower_of_section_of_ker_sqZero :
    letI := g.toRingHom.toAlgebra;
    IsScalarTower P S (RingHom.ker (algebraMap P S)) :=
  by
  letI := g.toRingHom.toAlgebra
  constructor
  intro p s m
  ext
  change g (p • s) * m = p * (g s * m)
  simp only [Algebra.smul_def, map_mul, mul_assoc, mul_left_comm _ (g s)]
  congr 1
  rw [← sub_eq_zero, ← Ideal.mem_bot, ← hf', pow_two, ← sub_mul]
  refine Ideal.mul_mem_mul ?_ m.2
  simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg (algebraMap P S p)

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