English
Applying lift to an element of M yields g m.
Русский
Применение lift к элементу m даёт g m.
LaTeX
$$$ lift(f,g,hg,hfg,hgf)(inr\\, m) = g(m) $$$
Lean4
/-- 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:
* `g x * g y = 0`: the elements of `M` continue to square to zero.
* `g (r •> x) = f r * g x` and `g (x <• r) = 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.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 (x <• r) = g x * f r) : tsze R M →ₐ[S] A :=
AlgHom.ofLinearMap ((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, hg]
rw [← map_mul, LinearMap.map_add, add_comm (g _), add_assoc, hfg, hgf])
