Jacobians in a symmetric algebra

The Jacobian of a family f : n → Sym M in a finite basis b : Basis n R M is the determinant of the matrix of partial derivatives ∂ (f i) / ∂ (b j), the derivatives SymmetricAlgebra.pderiv (b.coord j) (f i) along the coordinate forms of b. This file proves:

• a change of basis multiplies the Jacobian by the determinant of the change of basis, a unit;
• the chain rule: for an endomorphism g of M, the Jacobian of the family map g (f i) is det g times the image under map g of the Jacobian of f. Hence, if every f i is fixed by map g, the Jacobian is a relative invariant: det g • map g (jacobian b f) = jacobian b f;
• if every f i is homogeneous of degree d i, the Jacobian is homogeneous of degree ∑ i, (d i - 1);
• the Jacobian criterion: over a domain of characteristic zero, if every generator ι (b j) is algebraic over the subalgebra generated by the f i, then the Jacobian is nonzero. Otherwise a nonzero vector in the kernel of the Jacobian matrix gives a nonzero derivation killing every f i, which must then also kill every generator, since these are algebraic over the subalgebra they generate (Derivation.apply_eq_zero_of_isAlgebraic).

For a system of basic invariants of a finite group generated by reflections, these properties are the input to the classical identification of the Jacobian, up to a nonzero scalar, with the product of the linear forms of the reflecting hyperplanes.

Main definitions

• SymmetricAlgebra.jacobianMatrix: the matrix of partial derivatives of a family in Sym M, in the coordinates of a basis of M.
• SymmetricAlgebra.jacobian: its determinant.

Main results

• SymmetricAlgebra.jacobian_eq_algebraMap_det_mul: the Jacobian under a change of basis.
• SymmetricAlgebra.jacobian_map: the chain rule for Jacobians.
• SymmetricAlgebra.jacobian_mem_homogeneousSubmodule: the degree of the Jacobian.
• SymmetricAlgebra.jacobian_ne_zero: the Jacobian criterion in characteristic zero.

References

• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press (1990), Chapter 3 (the Jacobian criterion, and the Jacobian of a system of basic invariants).

noncomputable def SymmetricAlgebra.jacobianMatrix {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} (b : Module.Basis n R M) (f : n → SymmetricAlgebra R M) : Matrix n n (SymmetricAlgebra R M)

The Jacobian matrix of a family f in Sym M, in the coordinates of a basis b of M: its entry (i, j) is the partial derivative of f i in the variable b j.

@[simp]

theorem SymmetricAlgebra.jacobianMatrix_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} (b : Module.Basis n R M) (f : n → SymmetricAlgebra R M) (i j : n) : jacobianMatrix b f i j = (pderiv (b.coord j)) (f i)

The entries of the Jacobian matrix are the partial derivatives ∂ (f i) / ∂ (b j).

noncomputable def SymmetricAlgebra.jacobian {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) (f : n → SymmetricAlgebra R M) : SymmetricAlgebra R M

The Jacobian of a family f in Sym M, in the coordinates of a basis b of M: the determinant of the matrix of partial derivatives ∂ (f i) / ∂ (b j).

theorem SymmetricAlgebra.jacobian_def {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) (f : n → SymmetricAlgebra R M) : jacobian b f = (jacobianMatrix b f).det

The Jacobian is the determinant of the Jacobian matrix.

theorem SymmetricAlgebra.jacobian_eq_algebraMap_det_mul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (b b' : Module.Basis n R M) (f : n → SymmetricAlgebra R M) : jacobian b' f = (algebraMap R (SymmetricAlgebra R M)) (b'.det ⇑b) * jacobian b f

Change of basis. The Jacobians of a family in two bases b and b' differ by the determinant of b in the basis b', a unit.

theorem SymmetricAlgebra.jacobian_map {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) (g : M →ₗ[R] M) (f : n → SymmetricAlgebra R M) : (jacobian b fun (i : n) => (map R g) (f i)) = (algebraMap R (SymmetricAlgebra R M)) (LinearMap.det g) * (map R g) (jacobian b f)

The chain rule for Jacobians. For an endomorphism g of M, the Jacobian of the family map g (f i) is det g times the image under map g of the Jacobian of f.

theorem SymmetricAlgebra.algebraMap_det_mul_map_jacobian {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) {g : M →ₗ[R] M} {f : n → SymmetricAlgebra R M} (hf : ∀ (i : n), (map R g) (f i) = f i) : (algebraMap R (SymmetricAlgebra R M)) (LinearMap.det g) * (map R g) (jacobian b f) = jacobian b f

The Jacobian of invariants is a relative invariant. If every f i is fixed by the map induced by an endomorphism g of M, then the Jacobian of f satisfies det g • map g (jacobian b f) = jacobian b f; when det g is a unit, map g multiplies the Jacobian by (det g)⁻¹.

theorem SymmetricAlgebra.jacobian_mem_homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) {f : n → SymmetricAlgebra R M} (d : n → ℕ) (hf : ∀ (i : n), f i ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d i)) : jacobian b f ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (∑ i : n, (d i - 1))

The degree of the Jacobian. If every f i is homogeneous of degree d i, the Jacobian is homogeneous of degree ∑ i, (d i - 1).

theorem SymmetricAlgebra.jacobian_ne_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R M) [IsDomain R] [CharZero R] {f : n → SymmetricAlgebra R M} (hf : ∀ (j : n), IsAlgebraic (↥(Algebra.adjoin R (Set.range f))) ((ι R M) (b j))) : jacobian b f ≠ 0

The Jacobian criterion. Over a domain R of characteristic zero, if every generator ι (b j) is algebraic over the subalgebra generated by the family f, then the Jacobian of f is nonzero. This applies to a system of basic invariants of a finite group, over which the polynomial algebra is integral.