refactor(Algebra/DualNumber): generalize the universal property to no…

…n-commutative rings (#7934)

The current universal properties of `TrivSqZeroExt` and `DualNumber` work only when the underlying ring is commutative.
This is not the case for things like the dual quaternions.

This generalizes both sets of results to the non-commutative case.
Unfortunately the new `TrivSqZeroExt` version is rather involved, so this keeps the old statement as a special case.

The new `DualNumber` version is less bad, so I just discarded the commutative special case.

For dual numbers, the generalization is from `R[ε] →ₐ[R] B` to `A[ε] →ₐ[R] B`, where `R` is commutative but `A` may not be.
Some variable names had to be shuffled to make the new statement look nice.

Mathlib/Algebra/DualNumber.lean

@@ -11,8 +11,8 @@ import Mathlib.Algebra.TrivSqZeroExt
 # Dual numbers
 
 The dual numbers over `R` are of the form `a + bε`, where `a` and `b` are typically elements of a
-commutative ring `R`, and `ε` is a symbol satisfying `ε^2 = 0`. They are a special case of
-`TrivSqZeroExt R M` with `M = R`.
+commutative ring `R`, and `ε` is a symbol satisfying `ε^2 = 0` that commutes with every other
+element. They are a special case of `TrivSqZeroExt R M` with `M = R`.
 
 ## Notation
 
@@ -37,7 +37,7 @@ Rather than duplicating the API of `TrivSqZeroExt`, this file reuses the functio
 -/
 
 
-variable {R : Type*}
+variable {R A B : Type*}
 
 /-- The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.
 `R[ε]` is notation for `DualNumber R`. -/
@@ -95,40 +95,94 @@ theorem commute_eps_left [Semiring R] (x : DualNumber R) : Commute ε x := by
 /-- `ε` commutes with every element of the algebra. -/
 theorem commute_eps_right [Semiring R] (x : DualNumber R) : Commute x ε := (commute_eps_left x).symm
 
-/-- For two algebra morphisms out of `R[ε]` to agree, it suffices for them to agree on `ε`. -/
-@[ext]
-theorem algHom_ext {A} [CommSemiring R] [Semiring A] [Algebra R A] ⦃f g : R[ε] →ₐ[R] A⦄
-    (h : f ε = g ε) : f = g :=
-  algHom_ext' <| LinearMap.ext_ring <| h
+variable {A : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
+
+/-- For two `R`-algebra morphisms out of `A[ε]` to agree, it suffices for them to agree on the
+elements of `A` and the `A`-multiples of `ε`. -/
+@[ext 1100]
+nonrec theorem algHom_ext' ⦃f g : A[ε] →ₐ[R] B⦄
+    (hinl : f.comp (inlAlgHom _ _ _) = g.comp (inlAlgHom _ _ _))
+    (hinr : f.toLinearMap ∘ₗ (LinearMap.toSpanSingleton A A[ε] ε).restrictScalars R =
+        g.toLinearMap ∘ₗ (LinearMap.toSpanSingleton A A[ε] ε).restrictScalars R) :
+      f = g :=
+  algHom_ext' hinl (by
+    ext a
+    show f (inr a) = g (inr a)
+    simpa only [inr_eq_smul_eps] using FunLike.congr_fun hinr a)
+
+/-- For two `R`-algebra morphisms out of `R[ε]` to agree, it suffices for them to agree on `ε`. -/
+@[ext 1200]
+nonrec theorem algHom_ext ⦃f g : R[ε] →ₐ[R] A⦄ (hε : f ε = g ε) : f = g := by
+  ext
+  dsimp
+  simp only [one_smul, hε]
 #align dual_number.alg_hom_ext DualNumber.algHom_ext
 
-variable {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
-
-/-- A universal property of the dual numbers, providing a unique `R[ε] →ₐ[R] A` for every element
-of `A` which squares to `0`.
-
-This isomorphism is named to match the very similar `Complex.lift`. -/
-@[simps!]
-def lift : { e : A // e * e = 0 } ≃ (R[ε] →ₐ[R] A) :=
-  Equiv.trans
-    (show { e : A // e * e = 0 } ≃ { f : R →ₗ[R] A // ∀ x y, f x * f y = 0 } from
-      (LinearMap.ringLmapEquivSelf R ℕ A).symm.toEquiv.subtypeEquiv fun a => by
-        dsimp
-        simp_rw [smul_mul_smul]
-        refine' ⟨fun h x y => h.symm ▸ smul_zero _, fun h => by simpa using h 1 1⟩)
-    TrivSqZeroExt.lift
+/-- A universal property of the dual numbers, providing a unique `A[ε] →ₐ[R] B` for every map
+`f : A →ₐ[R] B` and a choice of element `e : B` which squares to `0` and commutes with the range of
+`f`.
+
+This isomorphism is named to match the similar `Complex.lift`.
+Note that when `f : R →ₐ[R] B := Algebra.ofId R B`, the commutativity assumption is automatic, and
+we are free to choose any element `e : B`. -/
+def lift :
+    {fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ a, Commute fe.2 (fe.1 a)} ≃ (A[ε] →ₐ[R] B) := by
+  refine Equiv.trans ?_ TrivSqZeroExt.liftEquiv
+  exact {
+    toFun := fun fe => ⟨
+      (fe.val.1, MulOpposite.op fe.val.2 • fe.val.1.toLinearMap),
+      fun x y => show (fe.val.1 x * fe.val.2) * (fe.val.1 y * fe.val.2) = 0 by
+        rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero],
+      fun r x => show fe.val.1 (r * x) * fe.val.2 = fe.val.1 r * (fe.val.1 x * fe.val.2) by
+        rw [map_mul, mul_assoc],
+      fun r x => show fe.val.1 (x * r) * fe.val.2 = (fe.val.1 x * fe.val.2) * fe.val.1 r by
+        rw [map_mul, (fe.prop.2 _).right_comm]⟩
+    invFun := fun fg => ⟨
+      (fg.val.1, fg.val.2 1),
+      fg.prop.1 _ _,
+      fun a => show fg.val.2 1 * fg.val.1 a = fg.val.1 a * fg.val.2 1 by
+        rw [←fg.prop.2.1, ←fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]⟩
+    left_inv := fun fe => Subtype.ext <| Prod.ext rfl <|
+      show fe.val.1 1 * fe.val.2 = fe.val.2 by
+        rw [map_one, one_mul]
+    right_inv := fun fg => Subtype.ext <| Prod.ext rfl <| LinearMap.ext fun x =>
+      show fg.val.1 x * fg.val.2 1 = fg.val.2 x by
+        rw [← fg.prop.2.1, smul_eq_mul, mul_one] }
 #align dual_number.lift DualNumber.lift
 
-/-- When applied to `ε`, `DualNumber.lift` produces the element of `A` that squares to 0. -/
--- @[simp] -- Porting note: simp can prove this
-theorem lift_apply_eps (e : { e : A // e * e = 0 }) : @lift R _ _ _ _ e (ε : R[ε]) = e := by
-  simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, one_smul, zero_add]
+theorem lift_apply_apply (fe : {_fe : (A →ₐ[R] B) × B // _}) (a : A[ε]) :
+    lift fe a = fe.val.1 a.fst + fe.val.1 a.snd * fe.val.2 := rfl
+
+@[simp] theorem coe_lift_symm_apply (F : A[ε] →ₐ[R] B) :
+    (lift.symm F).val = (F.comp (inlAlgHom _ _ _), F ε) := rfl
+
+/-- When applied to `inl`, `DualNumber.lift` applies the map `f : A →ₐ[R] B`. -/
+@[simp] theorem lift_apply_inl (fe : {fe : (A →ₐ[R] B) × B // _}) (a : A) :
+    lift fe (inl a : A[ε]) = fe.val.1 a := by
+  rw [lift_apply_apply, fst_inl, snd_inl, map_zero, zero_mul, add_zero]
+
+/-- Scaling on the left is sent by `DualNumber.lift` to multiplication on the left -/
+@[simp] theorem lift_smul (fe : {fe : (A →ₐ[R] B) × B // _}) (a : A) (ad : A[ε]) :
+    lift fe (a • ad) = fe.val.1 a * lift fe ad := by
+  rw [←inl_mul_eq_smul, map_mul, lift_apply_inl]
+
+/-- Scaling on the right is sent by `DualNumber.lift` to multiplication on the right -/
+@[simp] theorem lift_op_smul (fe : {fe : (A →ₐ[R] B) × B // _}) (a : A) (ad : A[ε]) :
+    lift fe (MulOpposite.op a • ad) = lift fe ad * fe.val.1 a := by
+  rw [←mul_inl_eq_op_smul, map_mul, lift_apply_inl]
+
+/-- When applied to `ε`, `DualNumber.lift` produces the element of `B` that squares to 0. -/
+@[simp] theorem lift_apply_eps
+    (fe : {fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ a, Commute fe.2 (fe.1 a)}) :
+    lift fe (ε : A[ε]) = fe.val.2 := by
+  simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, map_one, one_mul, zero_add]
 #align dual_number.lift_apply_eps DualNumber.lift_apply_eps
 
 /-- Lifting `DualNumber.eps` itself gives the identity. -/
 @[simp]
-theorem lift_eps : lift ⟨ε, eps_mul_eps⟩ = AlgHom.id R R[ε] :=
-  algHom_ext <| lift_apply_eps _
-#align dual_number.lift_eps DualNumber.lift_eps
+theorem lift_inlAlgHom_eps :
+    lift ⟨(inlAlgHom _ _ _, ε), eps_mul_eps, fun _ => commute_eps_left _⟩ = AlgHom.id R A[ε] :=
+  lift.apply_symm_apply <| AlgHom.id R A[ε]
+#align dual_number.lift_eps DualNumber.lift_inlAlgHom_epsₓ
 
 end DualNumber

Mathlib/Algebra/TrivSqZeroExt.lean

@@ -40,13 +40,18 @@ Many of the later results in this file are only stated for the commutative `R'`
 * `TrivSqZeroExt.fst`, `TrivSqZeroExt.snd`: the canonical projections from
   `TrivSqZeroExt R M`.
 * `triv_sq_zero_ext.algebra`: the associated `R`-algebra structure.
+* `TrivSqZeroExt.lift`: the universal property of the trivial square-zero extension; algebra
+  morphisms `TrivSqZeroExt R M →ₐ[S] A` are uniquely defined by an algebra morphism `f : R →ₐ[S] A`
+  on `R` and a linear map `g : M →ₗ[S] A` on `M` such that:
+  * `g x * g y = 0`: the elements of `M` continue to square to zero.
+  * `g (r • x) = f r * g x` and `g (op r • x) = g x * f r`: left and right actions are preserved by
+    `g`.
 * `TrivSqZeroExt.lift`: the universal property of the trivial square-zero extension; algebra
   morphisms `TrivSqZeroExt R M →ₐ[R] A` are uniquely defined by linear maps `M →ₗ[R] A` for
   which the product of any two elements in the range is zero.
 
 -/
 
-
 universe u v w
 
 /-- "Trivial Square-Zero Extension".
@@ -500,6 +505,16 @@ theorem inr_mul_inl [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒ
     show (0 : R) • (0 : M) + op r • m = op r • m by rw [smul_zero, zero_add]
 #align triv_sq_zero_ext.inr_mul_inl TrivSqZeroExt.inr_mul_inl
 
+theorem inl_mul_eq_smul [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
+    (r : R) (x : tsze R M) :
+    inl r * x = r • x :=
+  ext rfl (by dsimp; rw [smul_zero, add_zero])
+
+theorem mul_inl_eq_op_smul [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
+    (x : tsze R M) (r : R) :
+    x * inl r = op r • x :=
+  ext rfl (by dsimp; rw [smul_zero, zero_add])
+
 instance mulOneClass [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] :
     MulOneClass (tsze R M) :=
   { TrivSqZeroExt.one, TrivSqZeroExt.mul with
@@ -769,7 +784,7 @@ theorem algebraMap_eq_inl' (s : S) : algebraMap S (tsze R M) s = inl (algebraMap
   rfl
 #align triv_sq_zero_ext.algebra_map_eq_inl' TrivSqZeroExt.algebraMap_eq_inl'
 
-/-- The canonical `R`-algebra projection `TrivSqZeroExt R M → R`. -/
+/-- The canonical `S`-algebra projection `TrivSqZeroExt R M → R`. -/
 @[simps]
 def fstHom : tsze R M →ₐ[S] R where
   toFun := fst
@@ -780,6 +795,16 @@ def fstHom : tsze R M →ₐ[S] R where
   commutes' _r := fst_inl M _
 #align triv_sq_zero_ext.fst_hom TrivSqZeroExt.fstHom
 
+/-- The canonical `S`-algebra inclusion `R → TrivSqZeroExt R M`. -/
+@[simps]
+def inlAlgHom : R →ₐ[S] tsze R M where
+  toFun := inl
+  map_one' := inl_one _
+  map_mul' := inl_mul _
+  map_zero' := inl_zero (M := M)
+  map_add' := inl_add _
+  commutes' _r := (algebraMap_eq_inl' _ _ _ _).symm
+
 variable {R R' S M}
 
 theorem algHom_ext {A} [Semiring A] [Algebra R' A] ⦃f g : tsze R' M →ₐ[R'] A⦄
@@ -789,64 +814,127 @@ theorem algHom_ext {A} [Semiring A] [Algebra R' A] ⦃f g : tsze R' M →ₐ[R']
 #align triv_sq_zero_ext.alg_hom_ext TrivSqZeroExt.algHom_ext
 
 @[ext]
-theorem algHom_ext' {A} [Semiring A] [Algebra R' A] ⦃f g : tsze R' M →ₐ[R'] A⦄
-    (h : f.toLinearMap.comp (inrHom R' M) = g.toLinearMap.comp (inrHom R' M)) : f = g :=
-  algHom_ext <| LinearMap.congr_fun h
+theorem algHom_ext' {A} [Semiring A] [Algebra S A] ⦃f g : tsze R M →ₐ[S] A⦄
+    (hinl : f.comp (inlAlgHom S R M) = g.comp (inlAlgHom S R M))
+    (hinr : f.toLinearMap.comp (inrHom R M |>.restrictScalars S) =
+      g.toLinearMap.comp (inrHom R M |>.restrictScalars S)) : f = g :=
+  AlgHom.toLinearMap_injective <|
+    linearMap_ext (AlgHom.congr_fun hinl) (LinearMap.congr_fun hinr)
 #align triv_sq_zero_ext.alg_hom_ext' TrivSqZeroExt.algHom_ext'
 
-variable {A : Type*} [Semiring A] [Algebra R' A]
+variable {A : Type*} [Semiring A] [Algebra S A] [Algebra R' A]
+
+/--
+Assemble an algebra morphism `TrivSqZeroExt R M →ₐ[S] A` from separate morphisms on `R` and `M`.
+
+Namely, we require that for an algebra morphism `f : R →ₐ[S] A` and a linear map `g : M →ₗ[S] A`,
+we have:
 
-/-- There is an alg_hom from the trivial square zero extension to any `R`-algebra with a submodule
-whose products are all zero.
+* `g x * g y = 0`: the elements of `M` continue to square to zero.
+* `g (r • x) = f r * g x` and `g (op r • x) = g x * f r`: scalar multiplication on the left and
+  right is sent to left- and right- multiplication by the image under `f`.
 
-See `TrivSqZeroExt.lift` for this as an equiv. -/
-def liftAux (f : M →ₗ[R'] A) (hf : ∀ x y, f x * f y = 0) : tsze R' M →ₐ[R'] A :=
+See `TrivSqZeroExt.liftEquiv` for this as an equiv; namely that any such algebra morphism can be
+factored in this way.
+
+When `R` is commutative, this can be invoked with `f = Algebra.ofId R A`, which satisfies `hfg` and
+`hgf`. This version is captured as an equiv by `TrivSqZeroExt.liftEquivOfComm`. -/
+def lift (f : R →ₐ[S] A) (g : M →ₗ[S] A)
+    (hg : ∀ x y, g x * g y = 0)
+    (hfg : ∀ r x, g (r • x) = f r * g x)
+    (hgf : ∀ r x, g (op r • x) = g x * f r) : tsze R M →ₐ[S] A :=
   AlgHom.ofLinearMap
-    ((Algebra.linearMap R' A).comp (fstHom R' R' M).toLinearMap + f.comp (sndHom R' M))
-    (show algebraMap R' A 1 + f (0 : M) = 1 by rw [map_zero, map_one, add_zero])
+    ((f.comp <| fstHom S R M).toLinearMap + g ∘ₗ (sndHom R M |>.restrictScalars S))
+    (show f 1 + g (0 : M) = 1 by rw [map_zero, map_one, add_zero])
     (TrivSqZeroExt.ind fun r₁ m₁ =>
       TrivSqZeroExt.ind fun r₂ m₂ => by
         dsimp
-        simp only [add_zero, zero_add, add_mul, mul_add, smul_mul_smul, hf, smul_zero,
+        simp only [add_zero, zero_add, add_mul, mul_add, smul_mul_smul, hg, smul_zero,
           op_smul_eq_smul]
-        rw [← RingHom.map_mul, LinearMap.map_add, ← Algebra.commutes _ (f _), ← Algebra.smul_def, ←
-          Algebra.smul_def, add_right_comm, add_assoc, LinearMap.map_smul, LinearMap.map_smul])
-#align triv_sq_zero_ext.lift_aux TrivSqZeroExt.liftAux
-
-@[simp]
-theorem liftAux_apply_inr (f : M →ₗ[R'] A) (hf : ∀ x y, f x * f y = 0) (m : M) :
-    liftAux f hf (inr m) = f m :=
-  show algebraMap R' A 0 + f m = f m by rw [RingHom.map_zero, zero_add]
-#align triv_sq_zero_ext.lift_aux_apply_inr TrivSqZeroExt.liftAux_apply_inr
-
-@[simp]
-theorem liftAux_comp_inrHom (f : M →ₗ[R'] A) (hf : ∀ x y, f x * f y = 0) :
-    (liftAux f hf).toLinearMap.comp (inrHom R' M) = f :=
-  LinearMap.ext <| liftAux_apply_inr f hf
-#align triv_sq_zero_ext.lift_aux_comp_inr_hom TrivSqZeroExt.liftAux_comp_inrHom
-
-/-- When applied to `inr` itself, `liftAux` is the identity. -/
-@[simp]
-theorem liftAux_inrHom : liftAux (inrHom R' M) (inr_mul_inr R') = AlgHom.id R' (tsze R' M) :=
-  algHom_ext' <| liftAux_comp_inrHom _ _
-#align triv_sq_zero_ext.lift_aux_inr_hom TrivSqZeroExt.liftAux_inrHom
+        rw [← AlgHom.map_mul, LinearMap.map_add, add_comm (g _), add_assoc, hfg, hgf])
+#align triv_sq_zero_ext.lift_aux TrivSqZeroExt.lift
+
+@[simp]
+theorem lift_apply_inl (f : R →ₐ[S] A) (g : M →ₗ[S] A)
+    (hg : ∀ x y, g x * g y = 0)
+    (hfg : ∀ r x, g (r • x) = f r * g x)
+    (hgf : ∀ r x, g (op r • x) = g x * f r)
+    (r : R) :
+    lift f g hg hfg hgf (inl r) = f r :=
+  show f r + g 0 = f r by rw [map_zero, add_zero]
+
+@[simp]
+theorem lift_apply_inr (f : R →ₐ[S] A) (g : M →ₗ[S] A)
+    (hg : ∀ x y, g x * g y = 0)
+    (hfg : ∀ r x, g (r • x) = f r * g x)
+    (hgf : ∀ r x, g (op r • x) = g x * f r)
+    (m : M) :
+    lift f g hg hfg hgf (inr m) = g m :=
+  show f 0 + g m = g m by rw [map_zero, zero_add]
+#align triv_sq_zero_ext.lift_aux_apply_inr TrivSqZeroExt.lift_apply_inr
+
+@[simp]
+theorem lift_comp_inlHom (f : R →ₐ[S] A) (g : M →ₗ[S] A)
+    (hg : ∀ x y, g x * g y = 0)
+    (hfg : ∀ r x, g (r • x) = f r * g x)
+    (hgf : ∀ r x, g (op r • x) = g x * f r) :
+    (lift f g hg hfg hgf).comp (inlAlgHom S R M) = f :=
+  AlgHom.ext <| lift_apply_inl f g hg hfg hgf
+
+@[simp]
+theorem lift_comp_inrHom (f : R →ₐ[S] A) (g : M →ₗ[S] A)
+    (hg : ∀ x y, g x * g y = 0)
+    (hfg : ∀ r x, g (r • x) = f r * g x)
+    (hgf : ∀ r x, g (op r • x) = g x * f r) :
+    (lift f g hg hfg hgf).toLinearMap.comp (inrHom R M |>.restrictScalars S) = g :=
+  LinearMap.ext <| lift_apply_inr f g hg hfg hgf
+#align triv_sq_zero_ext.lift_aux_comp_inr_hom TrivSqZeroExt.lift_comp_inrHom
+
+/-- When applied to `inr` and `inl` themselves, `lift` is the identity. -/
+@[simp]
+theorem lift_inlAlgHom_inrHom :
+    lift (inlAlgHom _ _ _) (inrHom R M |>.restrictScalars S)
+      (inr_mul_inr R) (fun _ _ => (inl_mul_inr _ _).symm) (fun _ _ => (inr_mul_inl _ _).symm) =
+    AlgHom.id S (tsze R M) :=
+  algHom_ext' (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)
+#align triv_sq_zero_ext.lift_aux_inr_hom TrivSqZeroExt.lift_inlAlgHom_inrHomₓ
 
 /-- A universal property of the trivial square-zero extension, providing a unique
-`TrivSqZeroExt R M →ₐ[R] A` for every linear map `M →ₗ[R] A` whose range has no non-zero
-products.
+`TrivSqZeroExt R M →ₐ[R] A` for every pair of maps `f : R →ₐ[S] A` and `g : M →ₗ[S] A`,
+where the range of `g` has no non-zero products, and scaling the input to `g` on the left or right
+amounts to a corresponding multiplication by `f` in the output.
 
 This isomorphism is named to match the very similar `Complex.lift`. -/
-@[simps]
-def lift : { f : M →ₗ[R'] A // ∀ x y, f x * f y = 0 } ≃ (tsze R' M →ₐ[R'] A) where
-  toFun f := liftAux f f.prop
+@[simps!]
+def liftEquiv :
+    {fg : (R →ₐ[S] A) × (M →ₗ[S] A) //
+      (∀ x y, fg.2 x * fg.2 y = 0) ∧
+      (∀ r x, fg.2 (r • x) = fg.1 r * fg.2 x) ∧
+      (∀ r x, fg.2 (op r • x) = fg.2 x * fg.1 r)} ≃ (tsze R M →ₐ[S] A) where
+  toFun fg := lift fg.val.1 fg.val.2 fg.prop.1 fg.prop.2.1 fg.prop.2.2
   invFun F :=
-    ⟨F.toLinearMap.comp (inrHom R' M), fun _x _y =>
-      (F.map_mul _ _).symm.trans <| (F.congr_arg <| inr_mul_inr _ _ _).trans F.map_zero⟩
-  left_inv f := Subtype.ext <| liftAux_comp_inrHom _ f.prop
-  right_inv _F := algHom_ext' <| liftAux_comp_inrHom _ _
-#align triv_sq_zero_ext.lift TrivSqZeroExt.lift
-
-attribute [nolint simpNF] lift_symm_apply_coe
+    ⟨(F.comp (inlAlgHom _ _ _), F.toLinearMap ∘ₗ (inrHom _ _ |>.restrictScalars _)),
+      (fun _x _y =>
+        (F.map_mul _ _).symm.trans <| (F.congr_arg <| inr_mul_inr _ _ _).trans F.map_zero),
+      (fun _r _x => (F.congr_arg (inl_mul_inr _ _).symm).trans (F.map_mul _ _)),
+      (fun _r _x => (F.congr_arg (inr_mul_inl _ _).symm).trans (F.map_mul _ _))⟩
+  left_inv _f := Subtype.ext <| Prod.ext (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)
+  right_inv _F := algHom_ext' (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)
+
+/-- A simplified version of `TrivSqZeroExt.liftEquiv` for the commutative case. -/
+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⟩
+    left_inv := fun f => rfl
+    right_inv := fun fg => Subtype.ext <|
+      Prod.ext (AlgHom.toLinearMap_injective <| LinearMap.ext_ring <| by simp)
+      rfl }
+#align triv_sq_zero_ext.lift TrivSqZeroExt.liftEquiv
 
 end Algebra