Degree-one elements of a symmetric algebra as prime elements

This file records the divisibility theory of the degree-one elements ι ℓ of a symmetric algebra Sym M. One degree-one element divides another exactly when the vectors are proportional: ι ℓ ∣ ι m ↔ m ∈ R ∙ ℓ, because a quotient of degree-one elements has degree zero. Over a field K, a nonzero ι ℓ is a prime element of Sym M, since ℓ extends to a basis and Sym M is then a polynomial ring in which ι ℓ is a variable. When M is finite-dimensional, Sym M is Noetherian and ι ℓ spans a prime ideal of height one.

For polynomial functions Sym(V*) on a vector space V, the prime ideal spanned by a nonzero linear form ℓ is the ideal of the hyperplane ker ℓ. These are the codimension-one primes along which the quotient map of a finite linear group can ramify.

Main results

• SymmetricAlgebra.ι_dvd_ι_iff: ι ℓ ∣ ι m exactly when m is a multiple of ℓ.
• SymmetricAlgebra.prime_ι: over a field, a nonzero degree-one element is prime.
• SymmetricAlgebra.height_span_singleton_ι: over a field and for finite-dimensional M, a nonzero degree-one element spans an ideal of height one.

@[simp]

theorem SymmetricAlgebra.ι_dvd_ι_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ℓ m : M} : (ι R M) ℓ ∣ (ι R M) m ↔ m ∈ R ∙ ℓ

A degree-one element ι ℓ of a symmetric algebra divides another one ι m exactly when m is a multiple of ℓ.

theorem SymmetricAlgebra.prime_ι {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] {ℓ : M} (hℓ : ℓ ≠ 0) : Prime ((ι K M) ℓ)

Over a field, a nonzero degree-one element of a symmetric algebra is a prime element: after extending ℓ to a basis, it is a variable of the polynomial ring Sym M.

theorem SymmetricAlgebra.isRelPrime_ι_of_ker_ne {K : Type u_1} [Field K] {V : Type u_3} [AddCommGroup V] [Module K V] {ℓ m : Module.Dual K V} (hℓ : ℓ ≠ 0) (hm : m ≠ 0) (hker : LinearMap.ker ℓ ≠ LinearMap.ker m) : IsRelPrime ((ι K (Module.Dual K V)) ℓ) ((ι K (Module.Dual K V)) m)

Nonzero linear forms cutting out different hyperplanes are relatively prime as elements of the algebra of polynomial functions.

theorem SymmetricAlgebra.height_span_singleton_ι {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] {ℓ : M} [Module.Finite K M] (hℓ : ℓ ≠ 0) : (Ideal.span {(ι K M) ℓ}).height = 1

Over a field, a nonzero degree-one element of the symmetric algebra of a finite-dimensional vector space spans a prime ideal of height one.