Documentation

TauCeti.Algebra.Algebra.Frobenius.AdjoinRoot

R[X]/(g) is a symmetric Frobenius algebra #

Let g be a monic polynomial of degree d over a commutative ring R. When d > 0, the quotient AdjoinRoot g = R[X]/(g) is free over R with power basis 1, x, …, x ^ (d - 1), where x is the class of X. This file shows that the last coordinate in that basis, the coefficient of x ^ (d - 1), is a symmetric Frobenius functional on R[X]/(g). When d = 0, the quotient and functional are zero. No hypothesis on R (such as being a field, or its characteristic) is needed.

The main example is the truncated polynomial algebra k[x]/(x ^ n), where for n > 0 the functional is the coefficient of x ^ (n - 1). Over a field it is the basic example of a symmetric Frobenius algebra that is not semisimple (for n ≥ 2), and so, being self-injective, the basic example of an algebra whose finite-dimensional modules form a Frobenius exact category with a nontrivial stable category.

Main definitions #

Main results #

References #

source
noncomputable def AdjoinRoot.lastCoeff {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
AdjoinRoot g →ₗ[R] R

For a monic polynomial g of positive degree d, the coefficient of x ^ (d - 1) in the power basis 1, x, …, x ^ (d - 1) of R[X]/(g), where x = AdjoinRoot.root g: it sends the class of p to the coefficient of X ^ (d - 1) in the remainder p %ₘ g. For d = 0, the quotient and functional are zero.

Equations
Instances For
    source
    @[simp]
    theorem AdjoinRoot.lastCoeff_mk {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (p : Polynomial R) :
    (lastCoeff hg) ((mk g) p) = (p %ₘ g).coeff (g.natDegree - 1)

    The value of AdjoinRoot.lastCoeff on the class of a polynomial p.

    source
    @[simp]
    theorem AdjoinRoot.lastCoeff_root_pow {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) {i : ℕ} (hi : i < g.natDegree) :
    (lastCoeff hg) (root g ^ i) = if i + 1 = g.natDegree then 1 else 0

    On the basis vectors x ^ i with i < d, AdjoinRoot.lastCoeff is 1 at x ^ (d - 1) and 0 elsewhere.

    source
    theorem AdjoinRoot.lastCoeff_eq_repr {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (hd : 0 < g.natDegree) (a : AdjoinRoot g) :
    (lastCoeff hg) a = ((powerBasis' hg).basis.repr a) ⟨g.natDegree - 1, ⋯⟩

    AdjoinRoot.lastCoeff is the last coordinate in the power basis AdjoinRoot.powerBasis'.

    source
    theorem AdjoinRoot.isSymmetricFrobeniusFunctional_lastCoeff {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
    (lastCoeff hg).IsSymmetricFrobeniusFunctional

    For a monic polynomial g of positive degree d over a commutative ring, the coefficient of x ^ (d - 1) in the power basis is a symmetric Frobenius functional on R[X]/(g). For d = 0, the quotient and functional are zero.

    The truncated polynomial algebra R[X]/(X ^ n) #

    source
    @[simp]
    theorem AdjoinRoot.lastCoeff_X_pow_root_pow {R : Type u_1} [CommRing R] (n i : ℕ) :
    (lastCoeff ⋯) (root (Polynomial.X ^ n) ^ i) = if i + 1 = n then 1 else 0

    On R[X]/(X ^ n) for n > 0, AdjoinRoot.lastCoeff extracts the coefficient of x ^ (n - 1): it is 1 on x ^ (n - 1) and 0 on every other power of x. For n = 0, the quotient and functional are zero.

    source
    theorem AdjoinRoot.lastCoeff_X_pow_mk {R : Type u_1} [CommRing R] {n : ℕ} (hn : 0 < n) (p : Polynomial R) :
    (lastCoeff ⋯) ((mk (Polynomial.X ^ n)) p) = p.coeff (n - 1)

    On R[X]/(X ^ n) for n > 0, AdjoinRoot.lastCoeff sends the class of p to the coefficient of X ^ (n - 1) in p.

    source
    theorem AdjoinRoot.isSymmetricFrobeniusFunctional_lastCoeff_X_pow {R : Type u_1} [CommRing R] (n : ℕ) :
    (lastCoeff ⋯).IsSymmetricFrobeniusFunctional

    The truncated polynomial algebra R[X]/(X ^ n) is a symmetric Frobenius algebra: for n > 0, the coefficient of x ^ (n - 1) is a symmetric Frobenius functional on it, over any commutative ring R. For n = 0, the quotient and functional are zero.