One-dimensional representations from linear characters

A linear character of a monoid G over a commutative semiring k is a multiplicative character χ : G →* kˣ. It acts on the one-dimensional k-module k by scalar multiplication. This file packages that action as Representation.ofLinearCharacter χ, bundles it as an object FDRep.ofLinearCharacter χ of FDRep k G, and records the facts every consumer of a linear character needs: its character is χ, it is a line, it is simple, it restricts along a homomorphism by pulling χ back, and two of them are isomorphic exactly when the two characters are equal.

The construction is the common core of the linear characters of the Borel subgroup and of GL₂; keeping it here avoids separate scalar-action implementations for each group. It is also the smallest nonzero representation there is, and it is what the induction machinery is fed in the classical worked examples: Ind_H^G of a linear character of a subgroup is a monomial representation, and its irreducibility is what the Mackey criterion decides.

Main definitions

• Representation.ofLinearCharacter: the one-dimensional representation associated to a unit-valued multiplicative character.
• FDRep.ofLinearCharacter: the same representation as an object of FDRep k G.

Main results

• TauCeti.val_apply_neg_one_eq_one_or_eq_neg_one: a unit-valued character on a commutative ring with coefficients in an integral domain takes the value 1 or -1 at -1.
• Representation.ofLinearCharacter_apply: the action is multiplication by the character value.
• Representation.ofLinearCharacter_comp: restriction of the representation is precomposition of the character.
• Representation.ofLinearCharacter_injective: the representation remembers its character.
• Representation.ofLinearCharacter_one: the trivial character carries the trivial representation.
• Representation.char_ofLinearCharacter and FDRep.char_ofLinearCharacter: the trace character is the original character, coerced into the coefficient field.
• Representation.isIrreducible_ofLinearCharacter: a line has no room for a proper nonzero subrepresentation.
• FDRep.ofLinearCharacter_def: the bundled representation is the unbundled one, bundled.
• FDRep.finrank_ofLinearCharacter: it is a line.
• FDRep.simple_ofLinearCharacter: it is a simple object of FDRep k G, being a line.
• FDRep.actionRes_obj_ofLinearCharacter: restricting along f : S →* G gives the one-dimensional representation of the pulled-back character χ ∘ f.
• FDRep.nonempty_iso_ofLinearCharacter_iff: two of these are isomorphic exactly when the two linear characters are equal.
• FDRep.exists_character_eq_of_commute: over an algebraically closed field, an irreducible representation whose operators commute pairwise has a linear character as its character.

Implementation notes

Neither definition is exposed: consumers go through the lemmas rather than the body. FDRep.ofLinearCharacter_def is the defining equation the dependent API is derived from, and with Mathlib's FDRep.of_ρ' it recovers the action. That the carrier is the line k on the nose is recorded once and for all by FDRep.actionRes_obj_ofLinearCharacter, an honest equality of objects rather than an isomorphism; conjugation, restriction and comparison of these objects are then computed inside G →* kˣ through it and FDRep.nonempty_iso_ofLinearCharacter_iff.

theorem TauCeti.val_apply_neg_one_eq_one_or_eq_neg_one {R : Type u_1} {k : Type u_2} [CommRing R] [CommRing k] [IsDomain k] {α : Rˣ →* kˣ} : ↑(α (-1)) = 1 ∨ ↑(α (-1)) = -1

A unit-valued linear character on a commutative ring takes the value 1 or -1 at -1 when its coefficient ring is an integral domain. The character is inferred from the goal.

def Representation.ofLinearCharacter {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] (χ : G →* kˣ) : Representation k G k

The one-dimensional representation associated to a multiplicative character. An element g : G acts on the line k by multiplication by the unit χ g.

Equations

• Representation.ofLinearCharacter χ = { toFun := fun (g : G) => (LinearMap.lsmul k k) ↑(χ g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Representation.ofLinearCharacter_apply {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] (χ : G →* kˣ) (g : G) (x : k) : ((ofLinearCharacter χ) g) x = ↑(χ g) * x

The representation associated to χ acts by multiplication by χ.

@[simp]

theorem Representation.ofLinearCharacter_comp {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] {H : Type u_1} [Monoid H] (χ : G →* kˣ) (f : H →* G) : MonoidHom.comp (ofLinearCharacter χ) f = ofLinearCharacter (χ.comp f)

Restricting a one-dimensional representation is precomposition of its character.

theorem Representation.ofLinearCharacter_injective {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] : Function.Injective ofLinearCharacter

The one-dimensional representation remembers its multiplicative character.

@[simp]

theorem Representation.ofLinearCharacter_one {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] : ofLinearCharacter 1 = trivial k G k

The trivial linear character carries the trivial representation. This is the sanity check that fixes the convention: χ = 1 acts by the scalar 1.

@[simp]

theorem Representation.char_ofLinearCharacter {k : Type u} {G : Type v} [Field k] [Monoid G] (χ : G →* kˣ) (g : G) : (ofLinearCharacter χ).character g = ↑(χ g)

The trace character of a one-dimensional representation is its multiplicative character.

instance Representation.isIrreducible_ofLinearCharacter {k : Type u} {G : Type v} [Field k] [Monoid G] (χ : G →* kˣ) : (ofLinearCharacter χ).IsIrreducible

A one-dimensional representation is irreducible, having no room for a proper nonzero subrepresentation.

noncomputable def FDRep.ofLinearCharacter {k : Type u} {G : Type v} [CommRing k] [Monoid G] (χ : G →* kˣ) : FDRep k G

The one-dimensional representation carrying a linear character, as an object of FDRep k G. This is the shape induction consumes.

Equations

• FDRep.ofLinearCharacter χ = FDRep.of (Representation.ofLinearCharacter χ)

theorem FDRep.ofLinearCharacter_def {k : Type u} {G : Type v} [CommRing k] [Monoid G] (χ : G →* kˣ) : ofLinearCharacter χ = of (Representation.ofLinearCharacter χ)

The bundled one-dimensional representation is the unbundled one, bundled. This is the defining equation of FDRep.ofLinearCharacter; with FDRep.of_ρ' it recovers the action, so consumers never need to unfold the definition.

@[simp]

theorem FDRep.actionRes_obj_ofLinearCharacter {k : Type u} {G : Type v} [CommRing k] [Monoid G] {S : Type u_1} [Monoid S] (f : S →* G) (χ : G →* kˣ) : (Action.res (FGModuleCat k) f).obj (ofLinearCharacter χ) = ofLinearCharacter (χ.comp f)

Restricting a linear character along a homomorphism pulls the character back. Both sides are the line k with s acting by the scalar χ (f s), so this is an equality of objects, not merely an isomorphism; it is what lets conjugation and restriction of a one-dimensional representation be computed inside G →* kˣ.

@[simp]

theorem FDRep.finrank_ofLinearCharacter {k : Type u} {G : Type v} [Field k] [Monoid G] (χ : G →* kˣ) : Module.finrank k ↑(ofLinearCharacter χ).V = 1

A linear character is carried by a line.

@[simp]

theorem FDRep.char_ofLinearCharacter {k : Type u} {G : Type v} [Field k] [Monoid G] (χ : G →* kˣ) (g : G) : (ofLinearCharacter χ).character g = ↑(χ g)

The character of FDRep.ofLinearCharacter is the linear character it was built from.

instance FDRep.simple_ofLinearCharacter {k : Type u} {G : Type v} [Field k] [Monoid G] (χ : G →* kˣ) : CategoryTheory.Simple (ofLinearCharacter χ)

The one-dimensional representation of a linear character is a simple object, being a line.

@[simp]

theorem FDRep.nonempty_iso_ofLinearCharacter_iff {k : Type u} {G : Type v} [CommRing k] [Monoid G] (χ ψ : G →* kˣ) : Nonempty (ofLinearCharacter χ ≅ ofLinearCharacter ψ) ↔ χ = ψ

Two one-dimensional representations are isomorphic exactly when their linear characters agree. An isomorphism of lines is multiplication by the unit f 1, so equivariance reads χ g * f 1 = ψ g * f 1, which that unit cancels from; conversely equal characters give literally the same object.

theorem FDRep.exists_character_eq_of_commute {k : Type u} {G : Type v} [Field k] [IsAlgClosed k] [Group G] (W : FDRep k G) [CategoryTheory.Simple W] (hcomm : ∀ (g h : G), Commute (W.ρ g) (W.ρ h)) : ∃ (χ : G →* kˣ), W.character = fun (g : G) => ↑(χ g)

An irreducible representation whose operators commute has a linear character. Over an algebraically closed field, if the operators of an irreducible representation W commute pairwise, Schur's lemma makes each a scalar, so W is a line and its character is the linear character of those scalars.