The augmentation ideal of a symmetric algebra

The augmentation ideal of SymmetricAlgebra R M is the ideal generated by the canonical degree-one elements SymmetricAlgebra.ι R M m. This description is basis-free and applies to an arbitrary module over an arbitrary commutative ring. In rank one it identifies the augmentation ideal with the principal ideal generated by SymmetricAlgebra.ι R R 1.

The calculation links the generic augmentation Hopf ideal with the coordinate ideals used for additive groups and vector groups. In rank one, it supplies the coordinate-ideal input for identifying the explicit αₚ quotient with the scheme-theoretic kernel of Frobenius on 𝔾ₐ.

Main declarations

• TauCeti.SymmetricAlgebra.augmentation_toIdeal_eq_span_range_ι: the augmentation ideal is generated by the degree-one generators.
• TauCeti.SymmetricAlgebra.augmentation_toIdeal_eq_span_singleton_ι_one: in rank one, the augmentation ideal is principal, generated by ι 1.

@[simp]

theorem TauCeti.SymmetricAlgebra.augmentation_toIdeal_eq_span_range_ι (R : Type u) [CommRing R] (M : Type v) [AddCommMonoid M] [Module R M] : (HopfIdeal.augmentation R (SymmetricAlgebra R M)).toIdeal = Ideal.span (Set.range ⇑(SymmetricAlgebra.ι R M))

The underlying ideal of the augmentation Hopf ideal of a symmetric algebra is generated by the canonical degree-one generators. This description is basis-free and applies to every module over an arbitrary commutative ring.

@[simp]

theorem TauCeti.SymmetricAlgebra.augmentation_toIdeal_eq_span_singleton_ι_one (R : Type u) [CommRing R] : (HopfIdeal.augmentation R (SymmetricAlgebra R R)).toIdeal = Ideal.span {(SymmetricAlgebra.ι R R) 1}

For the rank-one symmetric algebra SymmetricAlgebra R R, the augmentation ideal is the principal ideal generated by the degree-one coordinate ι R R 1.