English
The infinitesimal extension associated to an R-S extension P is defined by quotienting the base ring by the square of the kernel and adjusting σ accordingly.
Русский
Инфинитезимальное расширение связано с исходным R-S расширением через факторизацию по квадрату ядра и соответствующую корректировку σ.
LaTeX
$$$\\text{infinitesimal}(P):= \\text{Extension } R S\\text{ with Ring } P.Ring/\\ker(P)^2, \\; σ=\\text{quotient}(P.σ)$$$
Lean4
/-- Given an `R`-algebra extension `0 → I → P → S → 0` of `S`,
the infinitesimal extension associated to it is `0 → I/I² → P/I² → S → 0`. -/
noncomputable def infinitesimal (P : Extension R S) : Extension R S
where
Ring := P.Ring ⧸ P.ker ^ 2
σ := Ideal.Quotient.mk _ ∘ P.σ
algebraMap_σ x := by dsimp; exact P.algebraMap_σ x
