Documentation

TauCeti.GroupTheory.GroupAction.Norm

The norm of a finite group action #

The norm TauCeti.groupNorm G M sums the scalar translates of an element of an additive commutative monoid. Its definition needs only distributive scalar multiplication by the finite scalar type. For a finite normal subgroup of a group acting on M, the norm commutes with the ambient action and is bundled as the equivariant additive map TauCeti.groupNormHom.

For a finite cyclic group generated by g, TauCeti.groupNorm_eq_sum_range expresses the norm as the sum over 1, g, …, gⁿ⁻¹, where n = orderOf g. This formula applies without a ring of scalars or a representation.

source
def TauCeti.groupNorm (G : Type u_1) (M : Type u_2) [Fintype G] [AddCommMonoid M] [DistribSMul G M] :
M →+ M

The group norm, m ↦ ∑ x, x • m, as an additive homomorphism. It needs only a finite scalar type and distributive scalar multiplication on an additive commutative monoid.

Instances For
    source
    @[simp]
    theorem TauCeti.groupNorm_apply (G : Type u_1) (M : Type u_2) [Fintype G] [AddCommMonoid M] [DistribSMul G M] (m : M) :
    (groupNorm G M) m = ∑ x : G, x • m

    Applying the group norm sums the scalar translates of the argument.

    source
    theorem TauCeti.groupNorm_smul {G : Type u_1} {M : Type u_2} [Group G] [AddCommMonoid M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] [Fintype ↥N] (g : G) (m : M) :
    (groupNorm (↥N) M) (g • m) = g • (groupNorm (↥N) M) m

    The norm of a finite normal subgroup N of G commutes with the action of G: conjugation by g permutes N.

    source
    def TauCeti.groupNormHom {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [Fintype ↥N] (M : Type u_2) [AddCommMonoid M] [DistribMulAction G M] :
    M →+[G] M

    The norm of a finite normal subgroup N of G, as a G-equivariant additive endomorphism of M (TauCeti.groupNorm_smul).

    Instances For
      source
      @[simp]
      theorem TauCeti.groupNormHom_apply {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [Fintype ↥N] (M : Type u_2) [AddCommMonoid M] [DistribMulAction G M] (m : M) :
      (groupNormHom N M) m = (groupNorm (↥N) M) m

      The equivariant norm groupNormHom N M is the group norm of N.

      source
      theorem TauCeti.groupNorm_eq_sum_range {G : Type u_1} {M : Type u_2} [Group G] [Fintype G] [AddCommMonoid M] [DistribSMul G M] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (m : M) :
      (groupNorm G M) m = ∑ i ∈ Finset.range (orderOf g), g ^ i • m

      The norm of a finite cyclic group is the sum of the translates by powers of a generator. Only distributive scalar multiplication on an additive commutative monoid is required.