English
There is an induction principle for SymmetricAlgebra: to prove a property for all elements of SymmetricAlgebra, it suffices to prove it for algebra maps from R, for images of M under ι, and that it is preserved under multiplication and addition.
Русский
Существует индукционный принцип для SymmetricAlgebra: чтобы доказать свойство для всего элемента SymmetricAlgebra, достаточно доказать его для алгебраических отображений из R, для изображений M под ι и что оно сохраняется при умножении и сложении.
LaTeX
$$$\text{induction }(\text{motive}):\; (\forall r, motive( algebraMap R (SymmetricAlgebra R M) r)) \\ \; (\forall x, motive( ι R M x)) \\ \; (\forall a b, motive a \to motive b \to motive (a b)) \\ \; (\forall a b, motive a \to motive b \to motive (a + b)) \\ ; \forall a, motive(a)$$$
Lean4
/-- For any linear map `f : M →ₗ[R] A`, `SymmetricAlgebra.lift f` lifts the linear map to an
R-algebra homomorphism from `SymmetricAlgebra R M` to `A`. -/
def lift : (M →ₗ[R] A) ≃ (SymmetricAlgebra R M →ₐ[R] A) :=
by
let equiv :
(TensorAlgebra R M →ₐ[R] A) ≃
{ f : TensorAlgebra R M →ₐ[R] A // ∀ {x y}, (TensorAlgebra.SymRel R M) x y → f x = f y } :=
by
refine (Equiv.subtypeUnivEquiv fun h _ _ h' ↦ ?_).symm
induction h' with
| mul_comm x y => rw [map_mul, map_mul, mul_comm]
exact (TensorAlgebra.lift R).trans <| equiv.trans <| RingQuot.liftAlgHom R
