English
In the commutative setting, there is a simplified version of the lift equivalence: maps f from M to A that are linear over R' and pair with the trivial extension give an algebra homomorphism from tsze R' M to A, with a straightforward construction.
Русский
В коммутативном случае существует упрощённая версия эквивалентности лифта: линейные карты f с M в A образуют алгебра-гомоморфизм из тривиального квадратно-нульевого расширения в A; утверждается простая конструкция обратного перехода.
LaTeX
$$$\\text{liftEquivOfComm} : { f : M \\to_l[R'] A // ∀ x,y, f x f y = 0 } \\simeq (tsze\\ R' M \\to_A[R'] A)$$$
Lean4
/-- A simplified version of `TrivSqZeroExt.liftEquiv` for the commutative case. -/
@[simps! apply symm_apply_coe]
def liftEquivOfComm : { f : M →ₗ[R'] A // ∀ x y, f x * f y = 0 } ≃ (tsze R' M →ₐ[R'] A) :=
by
refine Equiv.trans ?_ liftEquiv
exact
{ toFun := fun f =>
⟨(Algebra.ofId _ _, f.val), f.prop, fun r x => by simp [Algebra.smul_def, Algebra.ofId_apply], fun r x => by
simp [Algebra.smul_def, Algebra.ofId_apply, Algebra.commutes]⟩
invFun := fun fg => ⟨fg.val.2, fg.prop.1⟩ }
