Derivations of the symmetric algebra

In this file we prove that a derivation of SymmetricAlgebra R M is determined by its values on the generators. We also provide a constructor SymmetricAlgebra.mkDerivation that builds a derivation from its values on the generators and a linear equivalence SymmetricAlgebra.mkDerivationEquiv between M →ₗ[R] N and Derivation R (SymmetricAlgebra R M) N, the siblings of MvPolynomial.mkDerivation and MvPolynomial.mkDerivationEquiv. [UPSTREAM]

Implementation notes

mkDerivation f is the second component of the algebra homomorphism into the trivial square-zero extension TrivSqZeroExt (SymmetricAlgebra R M) N that lifts x ↦ (ι R M x, f x): a map a ↦ (a, D a) into the extension is multiplicative exactly when D satisfies the Leibniz rule.

theorem SymmetricAlgebra.derivation_ext {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] {D₁ D₂ : Derivation R (SymmetricAlgebra R M) N} (h : ∀ (x : M), D₁ ((ι R M) x) = D₂ ((ι R M) x)) : D₁ = D₂

theorem SymmetricAlgebra.derivation_ext_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] {D₁ D₂ : Derivation R (SymmetricAlgebra R M) N} : D₁ = D₂ ↔ ∀ (x : M), D₁ ((ι R M) x) = D₂ ((ι R M) x)

@[instance_reducible]

def SymmetricAlgebra.instModuleMulOpposite_linglib {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module (SymmetricAlgebra R M) N] : Module (SymmetricAlgebra R M)ᵐᵒᵖ N

The right action of the commutative algebra SymmetricAlgebra R M on N needed by TrivSqZeroExt; it agrees with the left action.

Equations

• SymmetricAlgebra.instModuleMulOpposite_linglib = Module.compHom N ((RingHom.id (SymmetricAlgebra R M)).fromOpposite ⋯)

theorem SymmetricAlgebra.instIsCentralScalar_linglib {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module (SymmetricAlgebra R M) N] : IsCentralScalar (SymmetricAlgebra R M) N

def SymmetricAlgebra.liftTrivSqZeroExt {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] [IsScalarTower R (SymmetricAlgebra R M) N] (f : M →ₗ[R] N) : SymmetricAlgebra R M →ₐ[R] TrivSqZeroExt (SymmetricAlgebra R M) N

The algebra homomorphism into the trivial square-zero extension lifting x ↦ (ι R M x, f x). Its first component is the identity and its second component is mkDerivation f; use SymmetricAlgebra.mkDerivation instead.

Equations

• One or more equations did not get rendered due to their size.

theorem SymmetricAlgebra.fst_liftTrivSqZeroExt {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] [IsScalarTower R (SymmetricAlgebra R M) N] (f : M →ₗ[R] N) (a : SymmetricAlgebra R M) : ((liftTrivSqZeroExt f) a).fst = a

def SymmetricAlgebra.mkDerivation {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] [IsScalarTower R (SymmetricAlgebra R M) N] (f : M →ₗ[R] N) : Derivation R (SymmetricAlgebra R M) N

The derivation on SymmetricAlgebra R M that takes the value f x on ι R M x.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SymmetricAlgebra.mkDerivation_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] [IsScalarTower R (SymmetricAlgebra R M) N] (f : M →ₗ[R] N) (x : M) : (mkDerivation f) ((ι R M) x) = f x

def SymmetricAlgebra.mkDerivationEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] [IsScalarTower R (SymmetricAlgebra R M) N] : (M →ₗ[R] N) ≃ₗ[R] Derivation R (SymmetricAlgebra R M) N

SymmetricAlgebra.mkDerivation as a linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SymmetricAlgebra.mkDerivationEquiv_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] [IsScalarTower R (SymmetricAlgebra R M) N] (f : M →ₗ[R] N) : mkDerivationEquiv f = mkDerivation f

@[simp]

theorem SymmetricAlgebra.mkDerivationEquiv_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (SymmetricAlgebra R M) N] [IsScalarTower R (SymmetricAlgebra R M) N] (D : Derivation R (SymmetricAlgebra R M) N) : mkDerivationEquiv.symm D = ↑D ∘ₗ ι R M