English
As above, the canonical difference map evaluates to the difference of the two lifts on x.
Русский
Как выше, каноническая разностная карта оценивает разности двух лифтов на x.
LaTeX
$$$((diffToIdealOfQuotientCompEq I f1 f2 e) x) = f1 x - f2 x$$$
Lean4
/-- Given a tower of algebras `R → A → B`, and a square-zero `I : Ideal B`, each lift `A →ₐ[R] B`
of the canonical map `A →ₐ[R] B ⧸ I` corresponds to an `R`-derivation from `A` to `I`. -/
def derivationToSquareZeroOfLift [IsScalarTower R A B] (hI : I ^ 2 = ⊥) (f : A →ₐ[R] B)
(e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)) : Derivation R A I :=
by
refine
{
diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
?_ with
map_one_eq_zero' := ?_
leibniz' := ?_ }
· rw [e]; ext; rfl
· ext; simp
· intro x y
let F := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) (by rw [e]; ext; rfl)
have : (f x - algebraMap A B x) * (f y - algebraMap A B y) = 0 :=
by
rw [← Ideal.mem_bot, ← hI, pow_two]
convert Ideal.mul_mem_mul (F x).2 (F y).2 using 1
ext
dsimp only [Submodule.coe_add, Submodule.coe_mk, LinearMap.coe_mk, diffToIdealOfQuotientCompEq_apply,
Submodule.coe_smul_of_tower, IsScalarTower.coe_toAlgHom', LinearMap.toFun_eq_coe]
simp only [map_mul, sub_mul, mul_sub, Algebra.smul_def] at this ⊢
rw [sub_eq_iff_eq_add, sub_eq_iff_eq_add] at this
simp only [this]
ring
