Base change of representations

This file extends a representation's scalars to a possibly noncommutative algebra by base-changing each linear endomorphism. A nonzero common fixed vector after scalar extension to a base-field algebra descends to 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 intertwiner space between two representations of a finite monoid commutes with flat scalar extension of commutative rings when the source is finite free. An intertwiner is a linear map killed by the finite family of conditions σ g ∘ₗ f = f ∘ₗ ρ g, so its space is a kernel, and flat extension commutes with that kernel (LinearMap.tensorKerEquiv). Over a base field, extension to any nontrivial commutative algebra preserves its dimension; in particular an endomorphism space of dimension one retains that dimension.

For a finite group, the whole invariant submodule also commutes with a flat scalar extension. Indeed, invariants are the kernel of the finite family of maps ρ(g) - 1; flatness preserves that kernel, and the finite product comparison identifies the base-changed family with the invariance conditions after extending scalars.

Permutation representations are preserved outright. A G-set X gives the free module R[X] with G permuting its basis, and extending the scalars along R → A gives A[X] with the same permutation: both sides are free on the basis X, and the identification matches the basis vectors, which the two actions permute in the same way. The permutation module also occurs in the unbundled form X →₀ R with the DistribMulAction that pushes the support forward (Finsupp.comapDistribMulAction); that form is the same representation read on coefficients (TauCeti.ofDistribMulActionComapEquiv, in TauCeti.RepresentationTheory.PermutationModule), so its scalar extension is a permutation representation too. Over R = ℤ this says that the reduction of a permutation lattice ℤ[X] modulo a prime is k[X] and its rationalization is ℚ[X].

Main declarations

• Representation.baseChange: scalar extension of a representation.
• Representation.invariantsBaseChangeEquiv: flat scalar extension commutes with taking the invariants of a finite group.
• 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.
• FDRep.character_baseChange: the same for the scalar extension of an object of FDRep.
• TauCeti.ClassFunction.ofFDRep_baseChange: the same as class functions, the coefficients changed along algebraMap K L.
• Representation.intertwiningMapBaseChangeEquiv: flat scalar extension of commutative rings commutes with intertwiner spaces for finite monoids and finite free source modules.
• Representation.finrank_intertwiningMap_baseChange: scalar extension to a nontrivial commutative base-field algebra preserves the dimension of an intertwiner space.
• Representation.IntertwiningMap.baseChange: base change transports an intertwining map.
• Representation.Equiv.baseChange: base change transports an equivalence of representations.
• TauCeti.baseChangeOfMulActionEquiv: the base change of R[X] is A[X].
• TauCeti.baseChangeComapEquiv: the base change of the permutation module X →₀ R is A[X].

def Representation.baseChange {G : Type w} {V : Type x} [Monoid G] {R : Type u} [CommSemiring R] [AddCommMonoid V] [Module R V] (A : Type v) [Semiring 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] [Semiring 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.

noncomputable def Representation.invariantsBaseChangeEquiv {V : Type x} {G : Type w} [Group G] {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Module.Flat R A] [AddCommGroup V] [Module R V] [Finite G] (ρ : Representation R G V) : TensorProduct R A ↥ρ.invariants ≃ₗ[A] ↥(baseChange A ρ).invariants

Flat scalar extension commutes with finite-group invariants. If A is flat over R and G is finite, the scalar extension of the invariant submodule of ρ is naturally linearly equivalent to the invariants of the scalar-extended representation.

Finiteness of G is used only to identify the scalar extension of G → V with G → A ⊗[R] V; flatness then makes scalar extension commute with the resulting kernel.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Representation.coe_invariantsBaseChangeEquiv {V : Type x} {G : Type w} [Group G] {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Module.Flat R A] [AddCommGroup V] [Module R V] [Finite G] (ρ : Representation R G V) (x : TensorProduct R A ↥ρ.invariants) : ↑(ρ.invariantsBaseChangeEquiv x) = (LinearMap.lTensor A ρ.invariants.subtype) x

The base-change equivalence is the canonical scalar extension of the inclusion of the invariant submodule into the ambient representation.

theorem Representation.exists_common_fixed_vector_of_baseChange {G : Type w} {V : Type x} [Monoid G] {K : Type u} {L : Type v} [Field K] [Semiring 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 scalar extension to a base-field algebra descends to a nonzero common fixed vector over the base field. Neither commutativity nor nontriviality of the coefficient algebra is needed.

@[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 FDRep.character_baseChange {K L : Type u} [Field K] [Field L] [Algebra K L] {G : Type u_4} [Monoid G] (V : FDRep K G) : (of (Representation.baseChange L V.ρ)).character = ⇑(algebraMap K L) ∘ V.character

The character of a scalar extension in FDRep is the character of the original representation read in the larger field: χ_{L ⊗[K] V} = algebraMap K L ∘ χ_V.

Not @[simp]: its left-hand side is not in simp normal form, since simp already rewrites it with FDRep.character_of and then the pointwise Representation.character_baseChange.

@[simp]

theorem TauCeti.ClassFunction.ofFDRep_baseChange {K L : Type u} [Field K] [Field L] [Algebra K L] {G : Type u_4} [Group G] (V : FDRep K G) : ofFDRep (FDRep.of (Representation.baseChange L V.ρ)) = (map (algebraMap K L)) (ofFDRep V)

The class function of a scalar extension in FDRep is the class function of the original representation with its coefficients changed along algebraMap K L.

def Representation.IntertwiningMap.baseChange {R : Type u_1} [CommSemiring R] {G : Type u_2} [Monoid G] {V : Type u_3} {W : Type u_4} [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {ρ : Representation R G V} {σ : Representation R G W} (f : ρ.IntertwiningMap σ) (A : Type u_5) [Semiring A] [Algebra R A] : (Representation.baseChange A ρ).IntertwiningMap (Representation.baseChange A σ)

Base change transports an intertwining map: A ⊗ f : A ⊗[R] V → A ⊗[R] W intertwines the base-changed representations, because the extension acts on the second factor, where f already intertwines the two actions.

Equations

• f.baseChange A = { toLinearMap := LinearMap.baseChange A f.toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.baseChange_tmul {R : Type u_1} [CommSemiring R] {G : Type u_2} [Monoid G] {V : Type u_3} {W : Type u_4} [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {ρ : Representation R G V} {σ : Representation R G W} (f : ρ.IntertwiningMap σ) (A : Type u_5) [Semiring A] [Algebra R A] (a : A) (v : V) : (f.baseChange A) (a ⊗ₜ[R] v) = a ⊗ₜ[R] f v

A base-changed intertwining map acts on the second factor of a pure tensor.

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_baseChange {R : Type u_1} [CommSemiring R] {G : Type u_2} [Monoid G] {V : Type u_3} {W : Type u_4} [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {ρ : Representation R G V} {σ : Representation R G W} (f : ρ.IntertwiningMap σ) (A : Type u_5) [Semiring A] [Algebra R A] : (f.baseChange A).toLinearMap = LinearMap.baseChange A f.toLinearMap

The linear map underlying a base-changed intertwining map is the base change of the underlying linear map.

def Representation.Equiv.baseChange {R : Type u_1} [CommSemiring R] {G : Type u_2} [Monoid G] {V : Type u_3} {W : Type u_4} [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {ρ : Representation R G V} {σ : Representation R G W} (φ : ρ.Equiv σ) (A : Type u_5) [Semiring A] [Algebra R A] : (Representation.baseChange A ρ).Equiv (Representation.baseChange A σ)

Base change transports an equivalence of representations: an equivariant isomorphism ρ ≃ σ becomes an equivariant isomorphism A ⊗[R] V ≃ A ⊗[R] W after extending the scalars, because the extension acts on the second factor, where the equivalence already intertwines the two actions.

Equations

• φ.baseChange A = Representation.Equiv.mk (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl A A) φ.toLinearEquiv) ⋯

@[simp]

theorem Representation.Equiv.baseChange_tmul {R : Type u_1} [CommSemiring R] {G : Type u_2} [Monoid G] {V : Type u_3} {W : Type u_4} [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {ρ : Representation R G V} {σ : Representation R G W} (φ : ρ.Equiv σ) (A : Type u_5) [Semiring A] [Algebra R A] (a : A) (v : V) : (φ.baseChange A) (a ⊗ₜ[R] v) = a ⊗ₜ[R] φ v

A base-changed equivalence acts on the second factor of a pure tensor.

@[simp]

theorem Representation.Equiv.baseChange_symm_tmul {R : Type u_1} [CommSemiring R] {G : Type u_2} [Monoid G] {V : Type u_3} {W : Type u_4} [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {ρ : Representation R G V} {σ : Representation R G W} (φ : ρ.Equiv σ) (A : Type u_5) [Semiring A] [Algebra R A] (a : A) (w : W) : (φ.baseChange A).symm (a ⊗ₜ[R] w) = a ⊗ₜ[R] φ.symm w

The inverse of a base-changed equivalence acts by the inverse on the second factor of a pure tensor.

noncomputable def Representation.intertwiningMapBaseChangeEquiv {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing 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] [Module.Free K V] [Module.Finite K V] [Module.Flat K L] [Finite G] (ρ : Representation K G V) (σ : Representation K G W) : TensorProduct K L (ρ.IntertwiningMap σ) ≃ₗ[L] (baseChange L ρ).IntertwiningMap (baseChange L σ)

Flat scalar extension commutes with the intertwiner space for a finite monoid and a finite free source module. On pure tensors this is scalar multiplication of the base-changed intertwining map (Representation.intertwiningMapBaseChangeEquiv_tmul).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Representation.intertwiningMapBaseChangeEquiv_tmul {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing 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] [Module.Free K V] [Module.Finite K V] [Module.Flat K L] [Finite G] (ρ : Representation K G V) (σ : Representation K G W) (a : L) (f : ρ.IntertwiningMap σ) : (ρ.intertwiningMapBaseChangeEquiv σ) (a ⊗ₜ[K] f) = a • f.baseChange L

Scalar extension of the intertwiner space sends a pure tensor to the corresponding scalar multiple of the base-changed intertwining map.

@[simp]

theorem Representation.intertwiningMapBaseChangeEquiv_symm_baseChange {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing 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] [Module.Free K V] [Module.Finite K V] [Module.Flat K L] [Finite G] (ρ : Representation K G V) (σ : Representation K G W) (f : ρ.IntertwiningMap σ) : (ρ.intertwiningMapBaseChangeEquiv σ).symm (f.baseChange L) = 1 ⊗ₜ[K] f

The inverse comparison sends a base-changed intertwining map to its canonical pure tensor.

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

Scalar extension to a nontrivial commutative algebra preserves the dimension of an intertwiner space for a finite monoid and a finite-dimensional source representation. Over the coefficient algebra the extended intertwiner space is free, with the same rank as the original vector space.

noncomputable def TauCeti.baseChangeOfMulActionEquiv (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (G : Type u_3) [Monoid G] (X : Type u_4) [MulAction G X] : (Representation.baseChange A (Representation.ofMulAction R G X)).Equiv (Representation.ofMulAction A G X)

The base change of a permutation representation is the permutation representation over the target ring: extending the scalars of R[X] along the structure map R → A of an R-algebra A gives A[X], equivariantly for a monoid acting on X. Nothing is asked of that structure map — A need not contain R — beyond its being an R-algebra. Both sides are free on the basis X and the identification matches those basis vectors, which the two actions permute in the same way.

Equations

• TauCeti.baseChangeOfMulActionEquiv R A G X = Representation.Equiv.mk ((Module.Basis.baseChange A (MonoidAlgebra.basis X R)).equiv (MonoidAlgebra.basis X A) (Equiv.refl X)) ⋯

@[simp]

theorem TauCeti.baseChangeOfMulActionEquiv_tmul_single {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (G : Type u_3) [Monoid G] {X : Type u_4} [MulAction G X] (a : A) (x : X) (r : R) : (baseChangeOfMulActionEquiv R A G X) (a ⊗ₜ[R] MonoidAlgebra.single x r) = MonoidAlgebra.single x (r • a)

TauCeti.baseChangeOfMulActionEquiv on the pure tensors spanning the scalar extension.

@[simp]

theorem TauCeti.baseChangeOfMulActionEquiv_symm_single {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (G : Type u_3) [Monoid G] {X : Type u_4} [MulAction G X] (a : A) (x : X) : (baseChangeOfMulActionEquiv R A G X).symm (MonoidAlgebra.single x a) = a ⊗ₜ[R] MonoidAlgebra.single x 1

TauCeti.baseChangeOfMulActionEquiv carries the element of A[X] supported at x with coefficient a back to the pure tensor a ⊗ₜ single x 1; at a = 1 this matches the two bases.

noncomputable def TauCeti.baseChangeComapEquiv (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (G : Type u_3) [Monoid G] (X : Type u_4) [MulAction G X] : (Representation.baseChange A (Representation.ofDistribMulAction R G (X →₀ R))).Equiv (Representation.ofMulAction A G X)

The base change of a permutation module is a permutation representation. At R = ℤ this says that extending the scalars of the permutation lattice ℤ[X] = X →₀ ℤ along ℤ → A gives the permutation representation A[X]: the reduction of ℤ[X] modulo a prime is k[X], and its rationalization is ℚ[X]. It is TauCeti.ofDistribMulActionComapEquiv base-changed along Representation.Equiv.baseChange and followed by TauCeti.baseChangeOfMulActionEquiv.

Equations

• TauCeti.baseChangeComapEquiv R A G X = ((TauCeti.ofDistribMulActionComapEquiv R G X).baseChange A).trans (TauCeti.baseChangeOfMulActionEquiv R A G X)

@[simp]

theorem TauCeti.baseChangeComapEquiv_tmul_single {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (G : Type u_3) [Monoid G] {X : Type u_4} [MulAction G X] (a : A) (x : X) (r : R) : (baseChangeComapEquiv R A G X) (a ⊗ₜ[R] Finsupp.single x r) = MonoidAlgebra.single x (r • a)

TauCeti.baseChangeComapEquiv on the pure tensors spanning the scalar extension.

@[simp]

theorem TauCeti.baseChangeComapEquiv_symm_single {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (G : Type u_3) [Monoid G] {X : Type u_4} [MulAction G X] (a : A) (x : X) : (baseChangeComapEquiv R A G X).symm (MonoidAlgebra.single x a) = a ⊗ₜ[R] Finsupp.single x 1

TauCeti.baseChangeComapEquiv carries the element of A[X] supported at x with coefficient a back to the pure tensor a ⊗ₜ single x 1.