Removing a rank-one twist

For a one-dimensional representation V, a linear equivalence e : V ≃ k identifies V⁺ ⊗ P with Hom(V, P). This file packages the elementary equivariance calculation used when an isomorphism P ≃ H is equivariant up to the character of V.

Main definitions

• LinearEquiv.rankOneHomEquiv: the coordinate isomorphism P ≃ Hom(V, P).
• Representation.rankOneTwistEquiv: an isomorphism H ≃ V⁺ ⊗ P from an isomorphism P ≃ H equivariant up to the character of V.

def LinearEquiv.rankOneHomEquiv {k : Type u} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] {P : Type x} [AddCommMonoid P] [Module k P] (e : V ≃ₗ[k] k) : P ≃ₗ[k] V →ₗ[k] P

A choice of coordinate on a rank-one module identifies a vector with the linear map obtained by multiplying that coordinate by the vector.

@[simp]

theorem LinearEquiv.rankOneHomEquiv_apply_apply {k : Type u} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] {P : Type x} [AddCommMonoid P] [Module k P] (e : V ≃ₗ[k] k) (x : P) (v : V) : (e.rankOneHomEquiv x) v = e v • x

Evaluation of the coordinate identification P ≃ Hom(V, P).

@[simp]

theorem LinearEquiv.rankOneHomEquiv_symm_apply {k : Type u} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] {P : Type x} [AddCommMonoid P] [Module k P] (e : V ≃ₗ[k] k) (f : V →ₗ[k] P) : e.rankOneHomEquiv.symm f = f (e.symm 1)

The inverse coordinate identification evaluates a linear map on the vector with coordinate 1.

def Representation.rankOneCharacter {k : Type u} {G : Type v} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] [Monoid G] (rho : Representation k G V) (e : V ≃ₗ[k] k) : G →* k

The character through which a monoid acts on a representation with a chosen rank-one coordinate: g acts by the coordinate of the image of the vector with coordinate 1.

@[simp]

theorem Representation.rankOneCharacter_apply {k : Type u} {G : Type v} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] [Monoid G] (rho : Representation k G V) (e : V ≃ₗ[k] k) (g : G) : (rho.rankOneCharacter e) g = e ((rho g) (e.symm 1))

The value of the rank-one character at g is the coordinate of g applied to the vector with coordinate 1.

theorem Representation.rankOneCharacter_smul {k : Type u} {G : Type v} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] [Monoid G] (rho : Representation k G V) (e : V ≃ₗ[k] k) (g : G) (v : V) : (rho g) v = (rho.rankOneCharacter e) g • v

A representation on a module with a coordinate V ≃ k acts through its rank-one character.

theorem Representation.isUnit_rankOneCharacter {k : Type u} {G : Type v} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] [Group G] (rho : Representation k G V) (e : V ≃ₗ[k] k) (g : G) : IsUnit ((rho.rankOneCharacter e) g)

The rank-one character of a group representation takes unit values.

theorem Representation.rankOneCharacter_ne_zero {k : Type u} {G : Type v} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] [Group G] [Nontrivial k] (rho : Representation k G V) (e : V ≃ₗ[k] k) (g : G) : (rho.rankOneCharacter e) g ≠ 0

The rank-one character of a representation is nonzero.

noncomputable def Representation.rankOneTwistEquiv {k : Type u} {G : Type v} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] {P : Type x} [AddCommMonoid P] [Module k P] [Group G] {H : Type u_1} [AddCommMonoid H] [Module k H] (rho : Representation k G V) (sigma : Representation k G P) (tau : Representation k G H) (e : V ≃ₗ[k] k) (Psi : P ≃ₗ[k] H) (hPsi : ∀ (g : G) (x : P), (rho.rankOneCharacter e) g • (tau g) (Psi x) = Psi ((sigma g) x)) : tau.Equiv (rho.dual.tprod sigma)

Removal of a rank-one twist. If Psi : P ≃ H satisfies chi(g) · g(Psi x) = Psi(gx) for the character of the rank-one representation rho, then H is equivariantly isomorphic to rho⁺ ⊗ P.

@[simp]

theorem Representation.dualTensorHom_rankOneTwistEquiv {k : Type u} {G : Type v} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] {P : Type x} [AddCommMonoid P] [Module k P] [Group G] {H : Type u_1} [AddCommMonoid H] [Module k H] (rho : Representation k G V) (sigma : Representation k G P) (tau : Representation k G H) (e : V ≃ₗ[k] k) (Psi : P ≃ₗ[k] H) (hPsi : ∀ (g : G) (x : P), (rho.rankOneCharacter e) g • (tau g) (Psi x) = Psi ((sigma g) x)) (y : H) : (dualTensorHom k V P) ((rho.rankOneTwistEquiv sigma tau e Psi hPsi) y) = e.rankOneHomEquiv (Psi.symm y)

After contraction, the twist-removal equivalence sends y to the coordinate map of Psi⁻¹ y.

@[simp]

theorem Representation.rankOneTwistEquiv_symm_apply {k : Type u} {G : Type v} [CommSemiring k] {V : Type w} [AddCommMonoid V] [Module k V] {P : Type x} [AddCommMonoid P] [Module k P] [Group G] {H : Type u_1} [AddCommMonoid H] [Module k H] (rho : Representation k G V) (sigma : Representation k G P) (tau : Representation k G H) (e : V ≃ₗ[k] k) (Psi : P ≃ₗ[k] H) (hPsi : ∀ (g : G) (x : P), (rho.rankOneCharacter e) g • (tau g) (Psi x) = Psi ((sigma g) x)) (t : TensorProduct k (Module.Dual k V) P) : (rho.rankOneTwistEquiv sigma tau e Psi hPsi).symm t = Psi (((dualTensorHom k V P) t) (e.symm 1))

The inverse of the twist-removal equivalence evaluates the contracted tensor on the vector with coordinate 1 and applies Psi.