Documentation

TauCeti.RepresentationTheory.Augmentation.Projection

A module splitting of augmentation #

Choosing an index splits the augmentation sequence as modules: subtract the coefficient sum at that index to project onto the sum-zero submodule. This projection is not generally equivariant, since the chosen index need not be fixed. It gives a split presentation of the augmentation module that remains exact after arbitrary extension of scalars. Over a commutative ring it also shows that every linear form on the augmentation module extends to R[X] (TauCeti.dualRestrict_augmentationSubrepresentation_surjective).

source
noncomputable def TauCeti.augmentationProjection (R : Type u_1) [Ring R] (G : Type u_2) (X : Type u_3) [Monoid G] [MulAction G X] (x₀ : X) :
MonoidAlgebra R X →ₗ[R] ↥(augmentationSubrepresentation R G X).toSubmodule

Project onto the sum-zero permutation module by subtracting the coefficient sum at x₀. This is a module map, not in general an equivariant map: the chosen index need not be fixed.

Instances For
    source
    @[simp]
    theorem TauCeti.coe_augmentationProjection (R : Type u_1) [Ring R] (G : Type u_2) (X : Type u_3) [Monoid G] [MulAction G X] (x₀ : X) (v : MonoidAlgebra R X) :
    ↑((augmentationProjection R G X x₀) v) = v - (MonoidAlgebra.basis X R).sumCoords v • MonoidAlgebra.single x₀ 1

    The projection subtracts the coefficient sum times the basis vector at the chosen index.

    source
    @[simp]
    theorem TauCeti.augmentationProjection_coe (R : Type u_1) [Ring R] (G : Type u_2) (X : Type u_3) [Monoid G] [MulAction G X] (x₀ : X) (v : ↥(augmentationSubrepresentation R G X).toSubmodule) :
    (augmentationProjection R G X x₀) ↑v = v

    The sum-zero projection is a retraction of the augmentation inclusion.

    source
    theorem TauCeti.exact_toSpanSingleton_augmentationProjection (R : Type u_1) [Ring R] (G : Type u_2) (X : Type u_3) [Monoid G] [MulAction G X] (x₀ : X) :
    Function.Exact ⇑(LinearMap.toSpanSingleton R (MonoidAlgebra R X) (MonoidAlgebra.single x₀ 1)) ⇑(augmentationProjection R G X x₀)

    The kernel of the sum-zero projection consists of the multiples of the chosen basis vector.

    source
    theorem TauCeti.augmentationProjection_surjective (R : Type u_1) [Ring R] (G : Type u_2) (X : Type u_3) [Monoid G] [MulAction G X] (x₀ : X) :
    Function.Surjective ⇑(augmentationProjection R G X x₀)

    Every sum-zero vector is in the image of the projection.

    source
    theorem TauCeti.dualRestrict_augmentationSubrepresentation_surjective {G : Type u_2} {X : Type u_3} [Monoid G] [MulAction G X] (R : Type u_4) [CommRing R] :
    Function.Surjective ⇑(augmentationSubrepresentation R G X).toSubmodule.dualRestrict

    Every linear form on the augmentation subrepresentation extends to R[X], over any commutative ring: compose it with the sum-zero projection at any index.