Twisting a representation by a linear character

Tensoring a representation ρ with a one-dimensional representation does not change its carrier: the line can be absorbed by TensorProduct.lid, leaving the same module with the action rescaled by the character. This file records that rescaled action directly as Representation.charTwist χ ρ, g ↦ χ g • ρ g for a linear character χ : G →* kˣ, and proves that it is the tensor product with Representation.ofLinearCharacter χ (Representation.tprodEquivCharTwist).

Working with the twist rather than with the tensor product is what makes its basic theory transparent. Because every value of χ is a unit, a submodule is stable under χ g • ρ g exactly when it is stable under ρ g, so the twist has literally the same subrepresentations (Representation.subrepresentationCharTwistOrderIso) and is irreducible exactly when ρ is (Representation.isIrreducible_charTwist_iff). Neither statement is visible through the tensor product without transporting along TensorProduct.lid first.

The twists form an action of the character group: twisting by 1 changes nothing and twisting twice multiplies the characters. The main consumer is the determinant twist of the general linear group, where χ = det ^ m turns a polynomial representation into a rational one.

This is a module of its own rather than a section of TauCeti/RepresentationTheory/LinearCharacter/Basic.lean, which it extends: the twist needs the tensor product and the subrepresentation lattice. Consumers of the bare one-dimensional representation need neither.

Main definitions

• Representation.charTwist: the representation g ↦ χ g • ρ g.
• Representation.subrepresentationCharTwistOrderIso: the twist has the same lattice of subrepresentations as ρ, by the identity on carriers.
• Representation.tprodEquivCharTwist and Representation.tprodOfLinearCharacterEquivCharTwist: the tensor product of ρ with ofLinearCharacter χ is the twist, on either side, along TensorProduct.lid and TensorProduct.rid.

Main results

• Representation.charTwist_one and Representation.charTwist_charTwist: twisting is an action of the character group G →* kˣ.
• Representation.charTwist_trivial: twisting the trivial representation of the line gives the one-dimensional representation of the character.
• Representation.lid_ofLinearCharacter_tprod_apply and Representation.rid_tprod_ofLinearCharacter_apply: TensorProduct.lid and TensorProduct.rid carry the action of (ofLinearCharacter χ) ⊗ ρ and of ρ ⊗ (ofLinearCharacter χ) to the action of ρ rescaled by χ.
• Representation.isIrreducible_charTwist_iff: the twist of an irreducible representation is irreducible, and conversely.
• Representation.char_charTwist: the trace character of the twist is χ times the character of ρ.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15, where the rational representations of GL n are the determinant twists of the polynomial ones.

def Representation.charTwist {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) : Representation k G V

The twist of a representation by a linear character: the same carrier, with ρ g rescaled by the unit χ g. It is the tensor product with the one-dimensional representation of χ (Representation.tprodEquivCharTwist), with the line absorbed.

Equations

• Representation.charTwist χ ρ = { toFun := fun (g : G) => ↑(χ g) • ρ g, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Representation.charTwist_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (g : G) : (charTwist χ ρ) g = ↑(χ g) • ρ g

theorem Representation.charTwist_apply_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (g : G) (v : V) : ((charTwist χ ρ) g) v = ↑(χ g) • (ρ g) v

@[simp]

theorem Representation.charTwist_one {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : charTwist 1 ρ = ρ

Twisting by the trivial character changes nothing.

theorem Representation.charTwist_charTwist {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ ψ : G →* kˣ) (ρ : Representation k G V) : charTwist χ (charTwist ψ ρ) = charTwist (χ * ψ) ρ

Twisting twice multiplies the characters: the twists are an action of G →* kˣ.

@[simp]

theorem Representation.charTwist_trivial {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] (χ : G →* kˣ) : charTwist χ (trivial k G k) = ofLinearCharacter χ

Twisting the trivial representation of the coefficient line by χ gives the one-dimensional representation of χ. So the one-dimensional representations are the twists of the trivial one, and Representation.charTwist extends Representation.ofLinearCharacter.

theorem Representation.charTwist_apply_mem_of_apply_mem {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {χ : G →* kˣ} {ρ : Representation k G V} {p : Submodule k V} (hp : ∀ (g : G) ⦃v : V⦄, v ∈ p → (ρ g) v ∈ p) (g : G) ⦃v : V⦄ (hv : v ∈ p) : ((charTwist χ ρ) g) v ∈ p

A submodule stable under ρ is stable under any twist of ρ.

theorem Representation.apply_mem_of_charTwist_apply_mem {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {χ : G →* kˣ} {ρ : Representation k G V} {p : Submodule k V} (hp : ∀ (g : G) ⦃v : V⦄, v ∈ p → ((charTwist χ ρ) g) v ∈ p) (g : G) ⦃v : V⦄ (hv : v ∈ p) : (ρ g) v ∈ p

Conversely a submodule stable under a twist of ρ is stable under ρ, the character values being units.

def Representation.subrepresentationCharTwistOrderIso {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) : Subrepresentation (charTwist χ ρ) ≃o Subrepresentation ρ

A twist has the same subrepresentations as the representation it twists, by the identity on carriers: the character values are units, so they scale a stable submodule into itself and back.

Equations

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

@[simp]

theorem Representation.toSubmodule_subrepresentationCharTwistOrderIso {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (p : Subrepresentation (charTwist χ ρ)) : ((subrepresentationCharTwistOrderIso χ ρ) p).toSubmodule = p.toSubmodule

@[simp]

theorem Representation.toSubmodule_subrepresentationCharTwistOrderIso_symm {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (p : Subrepresentation ρ) : ((subrepresentationCharTwistOrderIso χ ρ).symm p).toSubmodule = p.toSubmodule

theorem Representation.lid_ofLinearCharacter_tprod_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (g : G) (x : TensorProduct k k V) : (_root_.TensorProduct.lid k V) ((((ofLinearCharacter χ).tprod ρ) g) x) = ↑(χ g) • (ρ g) ((_root_.TensorProduct.lid k V) x)

TensorProduct.lid carries the action of (ofLinearCharacter χ) ⊗ ρ to the action of ρ rescaled by χ. This is the equivariance datum behind Representation.tprodEquivCharTwist, recorded on elements so that it can be used without unfolding that equivalence.

noncomputable def Representation.tprodEquivCharTwist {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) : ((ofLinearCharacter χ).tprod ρ).Equiv (charTwist χ ρ)

The tensor product with the one-dimensional representation of a character is the twist by that character, along TensorProduct.lid. This is the identification that lets the twist be read as the usual tensor product χ ⊗ ρ, and conversely lets a tensor product with a line be computed on the original carrier.

Equations

• Representation.tprodEquivCharTwist χ ρ = Representation.Equiv.mk (TensorProduct.lid k V) ⋯

@[simp]

theorem Representation.toLinearMap_tprodEquivCharTwist {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) : (↑(tprodEquivCharTwist χ ρ)).toLinearMap = ↑(_root_.TensorProduct.lid k V)

@[simp]

theorem Representation.tprodEquivCharTwist_tmul {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (x : k) (v : V) : (tprodEquivCharTwist χ ρ) (x ⊗ₜ[k] v) = x • v

theorem Representation.rid_tprod_ofLinearCharacter_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (g : G) (x : TensorProduct k V k) : (_root_.TensorProduct.rid k V) (((ρ.tprod (ofLinearCharacter χ)) g) x) = ↑(χ g) • (ρ g) ((_root_.TensorProduct.rid k V) x)

TensorProduct.rid carries the action of ρ ⊗ (ofLinearCharacter χ) to the action of ρ rescaled by χ. This is the mirror of Representation.lid_ofLinearCharacter_tprod_apply for a line on the right, and the equivariance datum behind Representation.tprodOfLinearCharacterEquivCharTwist.

noncomputable def Representation.tprodOfLinearCharacterEquivCharTwist {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) : (ρ.tprod (ofLinearCharacter χ)).Equiv (charTwist χ ρ)

The tensor product with the one-dimensional representation of a character on the right is also the twist by that character, along TensorProduct.rid: the mirror of Representation.tprodEquivCharTwist, so that a consumer holding ρ ⊗ χ reaches the twist theory without flipping the factors first.

Equations

• Representation.tprodOfLinearCharacterEquivCharTwist χ ρ = Representation.Equiv.mk (TensorProduct.rid k V) ⋯

@[simp]

theorem Representation.toLinearMap_tprodOfLinearCharacterEquivCharTwist {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) : (↑(tprodOfLinearCharacterEquivCharTwist χ ρ)).toLinearMap = ↑(_root_.TensorProduct.rid k V)

@[simp]

theorem Representation.tprodOfLinearCharacterEquivCharTwist_tmul {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (v : V) (x : k) : (tprodOfLinearCharacterEquivCharTwist χ ρ) (v ⊗ₜ[k] x) = x • v

@[simp]

theorem Representation.isIrreducible_charTwist_iff {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) : (charTwist χ ρ).IsIrreducible ↔ ρ.IsIrreducible

A twist of an irreducible representation is irreducible, and only a twist of an irreducible one is: twisting by a character does not change the lattice of subrepresentations.

instance Representation.isIrreducible_charTwist {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) [ρ.IsIrreducible] : (charTwist χ ρ).IsIrreducible

The instance form of Representation.isIrreducible_charTwist_iff: a twist of an irreducible representation is irreducible.

@[simp]

theorem Representation.char_charTwist {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] (χ : G →* kˣ) (ρ : Representation k G V) (g : G) : (charTwist χ ρ).character g = ↑(χ g) * ρ.character g

The character of a twist is the pointwise product of the twisting character with the character of the representation.