Products of representations

Mathlib forms the direct sum Representation.directSum and the binary product Representation.prod of representations, but not the product of an arbitrary family. This file defines it: for representations ρ i of a monoid G on modules V i, the representation Representation.pi ρ acts on ∀ i, V i factor by factor. The index type is arbitrary. Infinite products are the case of interest, as in the unit part ∏_v ∏_{w ∣ v} 𝒪_wˣ of the S-ideles of a Galois extension of number fields, which is a product of representations of the Galois group indexed by the places v outside S.

The invariants, the norm and, for a finite monoid, the coinvariant kernel of the product are computed factor by factor. The last of these uses the finiteness of G: an element of the coinvariant kernel is a sum ∑ g, (ρ g (y g) - y g) with one term for each g, and such sums can be chosen in every factor at once.

Main definitions

• Representation.pi ρ: the product of a family of representations.
• Rep.pi M: the product of a family of objects of Rep k G.
• Rep.piLift f: the morphism into Rep.pi M with prescribed components f i : A ⟶ M i.
• Rep.piProj M i: the projection of Rep.pi M onto M i.
• Rep.piMap f: the product of a family of morphisms f i : M i ⟶ N i.
• Rep.resPiIso M f: restriction along f commutes with products.

Main results

• Representation.mem_invariants_pi_iff: an element of the product is invariant exactly when every component is.
• Representation.norm_pi_apply: the norm of the product acts factor by factor.
• Representation.mem_ker_norm_pi_iff: an element of the product has norm zero exactly when every component does.
• Representation.mem_coinvariantsKer_pi_iff: for a finite monoid, an element of the product lies in the coinvariant kernel exactly when every component does.
• Rep.shortExact_pi: a product of short exact sequences of representations is short exact.

noncomputable def Representation.pi {k : Type u_1} {G : Type u_2} {ι : Type u_3} [Semiring k] {V : ι → Type u_4} [(i : ι) → AddCommMonoid (V i)] [(i : ι) → Module k (V i)] [Monoid G] (ρ : (i : ι) → Representation k G (V i)) : Representation k G ((i : ι) → V i)

The product of a family of representations ρ i on V i: the representation of G on ∀ i, V i acting on each component by ρ i.

@[simp]

theorem Representation.pi_apply {k : Type u_1} {G : Type u_2} {ι : Type u_3} [Semiring k] {V : ι → Type u_4} [(i : ι) → AddCommMonoid (V i)] [(i : ι) → Module k (V i)] [Monoid G] (ρ : (i : ι) → Representation k G (V i)) (g : G) (x : (i : ι) → V i) (i : ι) : ((pi ρ) g) x i = ((ρ i) g) (x i)

@[simp]

theorem Representation.norm_pi_apply {k : Type u_1} {G : Type u_2} {ι : Type u_3} [Semiring k] {V : ι → Type u_4} [(i : ι) → AddCommMonoid (V i)] [(i : ι) → Module k (V i)] [Group G] [Fintype G] (ρ : (i : ι) → Representation k G (V i)) (x : (i : ι) → V i) (i : ι) : (pi ρ).norm x i = (ρ i).norm (x i)

The norm of a product of representations of a finite group acts factor by factor.

theorem Representation.mem_ker_norm_pi_iff {k : Type u_1} {G : Type u_2} {ι : Type u_3} [Semiring k] {V : ι → Type u_4} [(i : ι) → AddCommMonoid (V i)] [(i : ι) → Module k (V i)] [Group G] [Fintype G] (ρ : (i : ι) → Representation k G (V i)) {x : (i : ι) → V i} : x ∈ LinearMap.ker (pi ρ).norm ↔ ∀ (i : ι), x i ∈ LinearMap.ker (ρ i).norm

An element of a product of representations of a finite group has norm zero exactly when each of its components does.

theorem Representation.mem_invariants_pi_iff {k : Type u_1} {G : Type u_2} {ι : Type u_3} [CommRing k] {V : ι → Type u_4} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [Group G] (ρ : (i : ι) → Representation k G (V i)) {x : (i : ι) → V i} : x ∈ (pi ρ).invariants ↔ ∀ (i : ι), x i ∈ (ρ i).invariants

An element of a product of representations is invariant exactly when each of its components is.

@[simp]

theorem Representation.mem_coinvariantsKer_pi_iff {k : Type u_1} {G : Type u_2} {ι : Type u_3} [CommRing k] {V : ι → Type u_4} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [Monoid G] [Finite G] (ρ : (i : ι) → Representation k G (V i)) {x : (i : ι) → V i} : x ∈ Coinvariants.ker (pi ρ) ↔ ∀ (i : ι), x i ∈ Coinvariants.ker (ρ i)

For a finite monoid, an element of a product of representations lies in the coinvariant kernel exactly when each of its components does.

@[reducible, inline]

noncomputable abbrev Rep.pi {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} (M : ι → Rep k G) : Rep k G

The product of a family of representations, as an object of Rep k G.

noncomputable def Rep.piLift {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M : ι → Rep k G} {A : Rep k G} (f : (i : ι) → A ⟶ M i) : A ⟶ pi M

The universal property of the product: the morphism into Rep.pi M whose components are the morphisms f i : A ⟶ M i.

@[simp]

theorem Rep.piLift_hom_apply {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M : ι → Rep k G} {A : Rep k G} (f : (i : ι) → A ⟶ M i) (x : ↑A) (i : ι) : (Hom.hom (piLift f)) x i = (Hom.hom (f i)) x

The components of Rep.piLift f are the morphisms f i.

noncomputable def Rep.piProj {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} (M : ι → Rep k G) (i : ι) : pi M ⟶ M i

The projection of Rep.pi M onto the factor M i.

@[simp]

theorem Rep.piProj_hom_apply {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M : ι → Rep k G} (i : ι) (x : ↑(pi M)) : (Hom.hom (piProj M i)) x = x i

Rep.piProj M i takes the i-th component.

@[simp]

theorem Rep.piLift_piProj {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M : ι → Rep k G} {A : Rep k G} (f : (i : ι) → A ⟶ M i) (i : ι) : CategoryTheory.CategoryStruct.comp (piLift f) (piProj M i) = f i

The i-th component of Rep.piLift f is f i.

@[simp]

theorem Rep.piLift_piProj_assoc {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M : ι → Rep k G} {A : Rep k G} (f : (i : ι) → A ⟶ M i) (i : ι) {Z : Rep k G} (h : M i ⟶ Z) : CategoryTheory.CategoryStruct.comp (piLift f) (CategoryTheory.CategoryStruct.comp (piProj M i) h) = CategoryTheory.CategoryStruct.comp (f i) h

The i-th component of Rep.piLift f is f i.

noncomputable def Rep.piMap {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M N : ι → Rep k G} (f : (i : ι) → M i ⟶ N i) : pi M ⟶ pi N

The product of a family of morphisms f i : M i ⟶ N i, acting factor by factor.

@[simp]

theorem Rep.piMap_hom_apply {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M N : ι → Rep k G} (f : (i : ι) → M i ⟶ N i) (x : ↑(pi M)) (i : ι) : (Hom.hom (piMap f)) x i = (Hom.hom (f i)) (x i)

Rep.piMap f applies f i to the i-th component.

@[simp]

theorem Rep.piMap_piProj {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M N : ι → Rep k G} (f : (i : ι) → M i ⟶ N i) (i : ι) : CategoryTheory.CategoryStruct.comp (piMap f) (piProj N i) = CategoryTheory.CategoryStruct.comp (piProj M i) (f i)

The i-th component of Rep.piMap f is f i on the i-th factor.

@[simp]

theorem Rep.piMap_piProj_assoc {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M N : ι → Rep k G} (f : (i : ι) → M i ⟶ N i) (i : ι) {Z : Rep k G} (h : N i ⟶ Z) : CategoryTheory.CategoryStruct.comp (piMap f) (CategoryTheory.CategoryStruct.comp (piProj N i) h) = CategoryTheory.CategoryStruct.comp (piProj M i) (CategoryTheory.CategoryStruct.comp (f i) h)

The i-th component of Rep.piMap f is f i on the i-th factor.

noncomputable def Rep.resPiIso {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} (M : ι → Rep k G) {H : Type u_3} [Monoid H] (f : H →* G) : res f (pi M) ≅ pi fun (i : ι) => res f (M i)

Restriction commutes with products: the restriction of Rep.pi M along f : H →* G is the product of the restrictions, by the identity of the underlying module.

@[simp]

theorem Rep.resPiIso_hom_hom_apply {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] {ι : Type w} {M : ι → Rep k G} {H : Type u_3} [Monoid H] (f : H →* G) (x : ↑(pi M)) : (Hom.hom (resPiIso M f).hom) x = x

Rep.resPiIso is the identity on underlying elements.

theorem Rep.shortExact_pi {k : Type u_1} {G : Type u_2} [Ring k] [Monoid G] {ι : Type w} (S : ι → CategoryTheory.ShortComplex (Rep k G)) (hS : ∀ (i : ι), (S i).ShortExact) : { X₁ := pi fun (i : ι) => (S i).X₁, X₂ := pi fun (i : ι) => (S i).X₂, X₃ := pi fun (i : ι) => (S i).X₃, f := piMap fun (i : ι) => (S i).f, g := piMap fun (i : ι) => (S i).g, zero := ⋯ }.ShortExact

A product of short exact sequences of representations is short exact: injectivity, surjectivity and exactness of linear maps are all checked factor by factor.