Documentation

TauCeti.RepresentationTheory.InvariantForm.SumOfConjugates

Summing a bilinear form over the conjugates of a representation #

Summing a bilinear form over the orbit of a representation of a finite group, ∑_g B (σ g ·) (σ g ·), makes it invariant: this is the standard construction that produces invariant forms out of arbitrary ones. No division by |G| is performed -- as in Mathlib's MonoidAlgebra.sumOfConjugates for a linear map, the undivided sum is the construction, and it needs no invertibility of the group order. The sum over the conjugates of a symmetric form is symmetric.

Over an ordered field the construction also produces a nonzero invariant symmetric form on any nontrivial finite-dimensional representation: sum the coordinate dot product read in a basis. Positivity is what makes the sum nonzero -- the sum of the nonnegative numbers B₀ (σ g x) (σ g x) is at least its term at g = 1, which is positive -- so it is the ordering of the field, not a division by |G|, that does the work.

Main definitions #

Main results #

References #

Summing a bilinear form over a finite group #

source
def Representation.sumOfConjugatesForm {k : Type u_1} {G : Type u_2} {W : Type u_3} [CommSemiring k] [Monoid G] [Fintype G] [AddCommMonoid W] [Module k W] (σ : Representation k G W) (B : LinearMap.BilinForm k W) :
LinearMap.BilinForm k W

The sum of a bilinear form over the conjugates of a representation of a finite monoid, ∑_g B (σ g ·) (σ g ·). No division by |G| is performed, so no invertibility of the monoid order is needed; when G is a group the plain sum is already invariant (Representation.isInvariantForm_sumOfConjugatesForm), being the Representation.norm of B for the conjugation action of G on bilinear forms. The name follows Mathlib's MonoidAlgebra.sumOfConjugates, the same undivided sum for a linear map.

Instances For
    source
    @[simp]
    theorem Representation.sumOfConjugatesForm_apply {k : Type u_1} {G : Type u_2} {W : Type u_3} [CommSemiring k] [Monoid G] [Fintype G] [AddCommMonoid W] [Module k W] (σ : Representation k G W) (B : LinearMap.BilinForm k W) (x y : W) :
    ((σ.sumOfConjugatesForm B) x) y = ∑ g : G, (B ((σ g) x)) ((σ g) y)
    source
    theorem Representation.isSymm_sumOfConjugatesForm {k : Type u_1} {G : Type u_2} {W : Type u_3} [CommSemiring k] [Monoid G] [Fintype G] [AddCommMonoid W] [Module k W] {σ : Representation k G W} {B : LinearMap.BilinForm k W} (hB : B.IsSymm) :
    (σ.sumOfConjugatesForm B).IsSymm

    The sum over the conjugates of a symmetric bilinear form is symmetric.

    Positivity of the sum over the conjugates #

    source
    theorem Representation.le_sumOfConjugatesForm_apply_self {k : Type u_1} {G : Type u_2} {W : Type u_3} [CommSemiring k] [PartialOrder k] [IsOrderedAddMonoid k] [Monoid G] [Fintype G] [AddCommMonoid W] [Module k W] {σ : Representation k G W} {B : LinearMap.BilinForm k W} (hB : ∀ (y : W), 0 ≤ (B y) y) (x : W) :
    (B x) x ≤ ((σ.sumOfConjugatesForm B) x) x

    The sum over the conjugates of a form with nonnegative diagonal dominates its term at g = 1, which is the value of the form itself.

    source
    theorem Representation.posDef_toQuadraticMap_sumOfConjugatesForm {k : Type u_1} {G : Type u_2} {W : Type u_3} [CommSemiring k] [PartialOrder k] [IsOrderedAddMonoid k] [Monoid G] [Fintype G] [AddCommMonoid W] [Module k W] {σ : Representation k G W} {B : LinearMap.BilinForm k W} (hB : (LinearMap.BilinMap.toQuadraticMap B).PosDef) :
    (LinearMap.BilinMap.toQuadraticMap (σ.sumOfConjugatesForm B)).PosDef

    The sum over the conjugates of a positive-definite form is positive definite.

    source
    theorem Representation.sumOfConjugatesForm_eq_norm {k : Type u_1} {G : Type u_2} {W : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid W] [Module k W] (σ : Representation k G W) (B : LinearMap.BilinForm k W) :
    σ.sumOfConjugatesForm B = (σ.linHom σ.dual).norm B

    The conjugate sum of a form is the norm of the form for the conjugation action of G on bilinear forms, Representation.linHom σ σ.dual: the two sums differ only by the reindexing g ↦ g⁻¹, since the conjugation action moves σ g⁻¹ into both arguments.

    source
    @[simp]
    theorem Representation.isInvariantForm_sumOfConjugatesForm {k : Type u_1} {G : Type u_2} {W : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid W] [Module k W] (σ : Representation k G W) (B : LinearMap.BilinForm k W) :
    TauCeti.Representation.IsInvariantForm σ (σ.sumOfConjugatesForm B)

    The sum of a bilinear form over the conjugates of a representation of a finite group is invariant: it is a norm for the conjugation action of G on bilinear forms (Representation.sumOfConjugatesForm_eq_norm), and a norm is fixed by that action.

    A nonzero invariant symmetric form over an ordered field #

    source
    theorem Representation.exists_isInvariantForm_isSymm_ne_zero {k : Type u_1} {G : Type u_2} {W : Type u_3} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [Group G] [Finite G] [AddCommGroup W] [Module k W] (σ : Representation k G W) [FiniteDimensional k W] [Nontrivial W] :
    ∃ (B : LinearMap.BilinForm k W), TauCeti.Representation.IsInvariantForm σ B ∧ B.IsSymm ∧ B ≠ 0

    A representation of a finite group over an ordered field carries a nonzero invariant symmetric form. Take the dot product read in a basis and sum it over the conjugates; that sum preserves symmetry, and it dominates its term at g = 1, which is the value B₀ x x of the dot product itself and is positive for x ≠ 0. So the sum does not vanish. This is the input over ℝ to the orthogonality of a representation with a real form.