Base change of representations

This file extends a representation's scalars by base-changing each linear endomorphism. It also records the descent step needed for fixed vectors: a nonzero common fixed vector after a field extension yields a nonzero common fixed vector over the base field.

Two invariants survive the extension unchanged. The character is the trace of a linear map, and the trace of a base-changed endomorphism is the image of the trace (LinearMap.trace_baseChange), so the character of L ⊗[K] V is the character of V read in L. The dimension of an intertwiner space between two representations of a finite monoid, the source finite-dimensional, is unchanged as well: an intertwiner is a linear map killed by the finite family of conditions σ g ∘ₗ f = f ∘ₗ ρ g, so the intertwiner space is the kernel of a single linear map, and the extension is flat, so it commutes with that kernel (LinearMap.tensorKerEquiv). Applied to a representation whose endomorphism algebra is one-dimensional, that equality says the endomorphism algebra after the extension is one-dimensional again, which is the mechanism by which an absolutely irreducible representation stays irreducible over any extension.

Main declarations

• Representation.baseChange: scalar extension of a representation.
• Representation.exists_common_fixed_vector_of_baseChange: descent of a nonzero common fixed vector.
• Representation.character_baseChange: the character of a base-changed representation is the image of the character.
• Representation.finrank_intertwiningMap_baseChange: base change preserves the dimension of an intertwiner space.

def Representation.baseChange {G : Type w} {V : Type x} [Monoid G] {R : Type u} [CommSemiring R] [AddCommMonoid V] [Module R V] (A : Type v) [CommSemiring A] [Algebra R A] (ρ : Representation R G V) : Representation A G (TensorProduct R A V)

Extend the scalars of a representation by base-changing each linear endomorphism.

Equations

• Representation.baseChange A ρ = (↑(Module.End.baseChangeHom R A V)).comp ρ

@[simp]

theorem Representation.baseChange_apply {G : Type w} {V : Type x} [Monoid G] {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (g : G) : (baseChange A ρ) g = LinearMap.baseChange A (ρ g)

The action of a base-changed representation is the base change of the original action.

theorem Representation.exists_common_fixed_vector_of_baseChange {G : Type w} {V : Type x} [Monoid G] {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {w : TensorProduct K L V} (hw : w ≠ 0) (hfixed : ∀ (g : G), ((baseChange L ρ) g) w = w) : ∃ (v : V), v ≠ 0 ∧ ∀ (g : G), (ρ g) v = v

A nonzero common fixed vector after a field extension descends to a nonzero common fixed vector over the base field.

@[simp]

theorem Representation.character_baseChange {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {V : Type u_3} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {G : Type u_4} [Monoid G] (ρ : Representation K G V) (g : G) : (baseChange L ρ).character g = (algebraMap K L) (ρ.character g)

The character is unchanged by base change, read through the structure map: the character of L ⊗[K] V at g is the image in L of the character of V at g, because the trace of a base-changed endomorphism is the image of its trace.

theorem Representation.finrank_intertwiningMap_baseChange {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {G : Type u_3} [Monoid G] {V : Type u_4} [AddCommGroup V] [Module K V] {W : Type u_5} [AddCommGroup W] [Module K W] [FiniteDimensional K V] [Finite G] (ρ : Representation K G V) (σ : Representation K G W) : Module.finrank L ((baseChange L ρ).IntertwiningMap (baseChange L σ)) = Module.finrank K (ρ.IntertwiningMap σ)

Base change preserves the dimension of an intertwiner space. An intertwiner is a linear map annihilated by the finite family of linear conditions σ g ∘ₗ f = f ∘ₗ ρ g, so the intertwiner space is the kernel of a single linear map; L is flat over K, so extending the scalars commutes with taking that kernel (LinearMap.tensorKerEquiv), leaving the dimension unchanged. Only the dimensions are compared here; the underlying identification of the two intertwiner spaces is not exposed. The dimension alone is what makes an absolutely irreducible representation stay irreducible after extending the scalars: a one-dimensional endomorphism algebra stays one-dimensional.