English
There is a correspondence between R-derivations A → I and lifts A → B of the canonical map A → B/I, given by a construction derivationToSquareZeroOfLift. Specifically, from a lift f of A → B modulo I one obtains a derivation der: A → I, and conversely.
Русский
Существуют взаимнооднозначные соответствия между R-производными A → I и лифтом A → B над каноническим отображением A → B/I, задаваемые конструкцией derivationToSquareZeroOfLift.
LaTeX
$$$\text{There is a bijection } \mathrm{Derivation}(R,A,I) \cong \{ f: A \to_{R} B \mid (\Ideal.Quotient.mk_{R} I) \circ f = IsScalarTower.toAlgHom R A (B/I) \}$$$
Lean4
theorem derivationToSquareZeroOfLift_apply [IsScalarTower R A B] (f : A →ₐ[R] B)
(e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)) (x : A) :
(derivationToSquareZeroOfLift I hI f e x : B) = f x - algebraMap A B x :=
rfl
