Real forms of a complex representation

A real form of a representation ρ of G on a complex vector space V is a real representation σ on a real vector space W whose complexification is ρ: a ℂ-linear isomorphism ℂ ⊗[ℝ] W ≃ₗ[ℂ] V intertwining 1 ⊗ σ g with ρ g. Only the values on the pure tensors 1 ⊗ₜ w are asked for, which is enough because those generate ℂ ⊗[ℝ] W over ℂ: Representation.isRealForm_iff_nonempty_equiv upgrades the condition to an equivalence of representations (Representation.baseChange ℂ σ).Equiv ρ, which is the statement that ρ is the complexification of σ. A representation is realizable over ℝ when it admits a real form.

Representation.IsRealForm allows any carrier for the real form, while Representation.IsRealizableOverReal pins it to Fin (finrank ℂ V) → ℝ, so that the predicate needs no type existential; nothing is lost by pinning it, because Representation.IsRealForm.isRealizableOverReal transports a real form of a finite-dimensional representation to the pinned carrier along a real basis (the carrier of the real form is then finite-dimensional too, by Representation.IsRealForm.finiteDimensional_iff). The pinned predicate needs no finite-dimensionality hypothesis either: the pinned carrier is finite-dimensional, so it already implies FiniteDimensional ℂ V (Representation.IsRealizableOverReal.finiteDimensional). For an infinite-dimensional V it is therefore simply false, and Representation.IsRealForm is the notion to use there.

Everything here is for a representation of an arbitrary monoid: the real-form vocabulary and its transports never invert a group element, and the passage to the Frobenius-Schur indicator that consumes them -- Representation.frobeniusSchurIndicator_eq_one_of_isRealizableOverReal, in TauCeti.RepresentationTheory.CharacterTable.FrobeniusSchur.RealForm -- asks for a finite group only where it sums over the group.

A real form is a statement about an auxiliary carrier W; the equivalent statement inside V is a real structure, a conjugation K of V -- a conjugate-linear involution -- commuting with the action. Its real points TauCeti.realPoints K carry a real representation whose complexification is ρ (Representation.IsRealStructure.isRealForm), and conversely a real form transports the conjugation c ⊗ₜ w ↦ conj c ⊗ₜ w of ℂ ⊗[ℝ] W to V (Representation.IsRealForm.exists_isRealStructure). So the two notions agree (Representation.isRealizableOverReal_iff_exists_isRealStructure). This is the form in which realizability is produced: the route to it for an irreducible representation with Frobenius-Schur indicator 1 is to build the conjugation out of an invariant symmetric bilinear form and an invariant Hermitian inner product, and a real form on a carrier is not something one writes down directly. That route is taken in TauCeti/RepresentationTheory/InvariantForm/StructureMap.lean, and read off as a criterion on the indicator in TauCeti/RepresentationTheory/CharacterTable/FrobeniusSchur/Realizability.lean.

Main definitions

• Representation.IsRealForm: σ is a real form of ρ.
• Representation.IsRealizableOverReal: ρ admits a real form on a carrier pinned by the dimension of V.
• Representation.IsRealStructure: K is a real structure on ρ, that is, a conjugation of V commuting with the action; it is stated over any commutative star ring, ℂ being the case the rest of the file treats.
• Representation.IsRealStructure.rep: the real representation it induces on the real points.

Main results

• Representation.isRealForm_iff_nonempty_equiv: a real form is exactly an equivalence of representations from the complexification of σ to ρ.
• Representation.IsRealStructure.isRealForm: the real points of a real structure are a real form, and Representation.IsRealForm.exists_isRealStructure is the converse.
• Representation.IsRealStructure.isRealizableOverReal: a real structure on a finite-dimensional ρ realizes it over ℝ in the pinned sense.
• Representation.isRealizableOverReal_iff_exists_isRealStructure: over a finite-dimensional V, realizability over ℝ is exactly the existence of a real structure.
• Representation.IsRealStructure.finrank_realPoints: the real points of a real structure have ℝ-dimension finrank ℂ V.
• Representation.IsRealForm.char_eq: the character of a representation with a real form is the character of that real form, in particular real-valued (Representation.IsRealForm.conj_char).
• Representation.IsRealForm.exists_isInvariantForm_isSymm_ne_zero: a real form transports a nonzero invariant symmetric real form to a nonzero invariant symmetric complex form.
• Representation.IsRealForm.finiteDimensional_iff: a real form is finite-dimensional exactly when the representation it is a form of is.
• Representation.IsRealForm.isRealizableOverReal: a real form of a finite-dimensional representation makes ρ realizable over ℝ in the pinned sense.
• Representation.IsRealizableOverReal.finiteDimensional: a representation realizable over ℝ is finite-dimensional.

References

This builds the IsRealForm and IsRealizableOverReal targets of Layer 7 of TauCetiRoadmap/RepresentationTheory/CharacterTheory/README.md.

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §13.2.
• I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 4.

Real forms

def Representation.IsRealForm {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] (ρ : Representation ℂ G V) (σ : Representation ℝ G W) : Prop

σ is a real form of ρ when the complexification ℂ ⊗[ℝ] W of the space of σ is ℂ-linearly isomorphic to the space of ρ by an isomorphism intertwining the two actions. The condition is stated on the pure tensors 1 ⊗ₜ w, which generate ℂ ⊗[ℝ] W over ℂ.

theorem Representation.isRealForm_iff {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} : ρ.IsRealForm σ ↔ ∃ (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V), ∀ (g : G) (w : W), e (1 ⊗ₜ[ℝ] (σ g) w) = (ρ g) (e (1 ⊗ₜ[ℝ] w))

Representation.IsRealForm unfolded: an intertwining ℂ-linear isomorphism from the complexification.

theorem Representation.isRealForm_iff_nonempty_equiv {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} : ρ.IsRealForm σ ↔ Nonempty ((baseChange ℂ σ).Equiv ρ)

A real form is an equivalence of representations from the complexification. This is the characterization of Representation.IsRealForm against Representation.baseChange: checking the intertwining condition on the pure tensors 1 ⊗ₜ w is the same as producing a Representation.Equiv out of the whole complexification.

theorem Representation.IsRealForm.char_eq {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} (h : ρ.IsRealForm σ) (g : G) : ρ.character g = ↑(σ.character g)

The character of a representation with a real form is the character of that real form. In particular it takes real values (Representation.IsRealForm.conj_char).

theorem Representation.IsRealForm.conj_char {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} (h : ρ.IsRealForm σ) (g : G) : (starRingEnd ℂ) (ρ.character g) = ρ.character g

The character of a representation with a real form is fixed by complex conjugation.

theorem Representation.IsRealForm.finrank_eq {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} (h : ρ.IsRealForm σ) : Module.finrank ℝ W = Module.finrank ℂ V

The complex dimension of a representation is the real dimension of any of its real forms: complexification does not change the dimension.

theorem Representation.IsRealForm.finiteDimensional_iff {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} (h : ρ.IsRealForm σ) : FiniteDimensional ℝ W ↔ FiniteDimensional ℂ V

A real form is finite-dimensional exactly when the representation it is a form of is. Finiteness passes from W to V because V is the complexification ℂ ⊗[ℝ] W up to isomorphism, and back down because ℂ is faithfully flat over ℝ (Module.Finite.of_finite_tensorProduct_of_faithfullyFlat). Both directions are available with no finiteness in the ambient context, so a consumer holding finiteness on either side gets it on the other; comparing dimensions instead (Representation.IsRealForm.finrank_eq) would say nothing when the common dimension is 0.

theorem Representation.IsRealForm.exists_isInvariantForm_isSymm_ne_zero {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} (h : ρ.IsRealForm σ) {B : LinearMap.BilinForm ℝ W} (hB : TauCeti.Representation.IsInvariantForm σ B) (hsymm : B.IsSymm) (hB0 : B ≠ 0) : ∃ (C : LinearMap.BilinForm ℂ V), TauCeti.Representation.IsInvariantForm ρ C ∧ C.IsSymm ∧ C ≠ 0

A real form transports invariant symmetric forms. The base change to ℂ of a nonzero invariant symmetric form on the real side, read through the isomorphism, is a nonzero invariant symmetric form on the complex side.

Realizability over the reals

def Representation.IsRealizableOverReal {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] (ρ : Representation ℂ G V) : Prop

Realizability over ℝ: ρ admits a real form on the carrier Fin (finrank ℂ V) → ℝ. Pinning the carrier avoids a type existential; a real form on an arbitrary carrier is Representation.IsRealForm, and every result about the indicator is proved from that more general notion.

Pinning the carrier by the dimension costs nothing: the pinned carrier is finite-dimensional, so a real form on it already forces V to be finite-dimensional (Representation.IsRealizableOverReal.finiteDimensional), and conversely every real form on a finite-dimensional carrier transports to the pinned one (Representation.IsRealForm.isRealizableOverReal). For an infinite-dimensional V the predicate is therefore simply false -- finrank ℂ V is then 0 and the pinned carrier is the zero space -- and Representation.IsRealForm is the notion to use there.

theorem Representation.isRealizableOverReal_iff {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} : ρ.IsRealizableOverReal ↔ ∃ (σ : Representation ℝ G (Fin (Module.finrank ℂ V) → ℝ)), ρ.IsRealForm σ

Representation.IsRealizableOverReal unfolded: it is the existence of a real form on the pinned carrier, and this is the elimination principle for it.

theorem Representation.IsRealizableOverReal.finiteDimensional {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} (h : ρ.IsRealizableOverReal) : FiniteDimensional ℂ V

A representation realizable over ℝ is finite-dimensional. The pinned carrier Fin (finrank ℂ V) → ℝ is finite-dimensional, so V, being the complexification of it, is too. This is what makes pinning the carrier by the dimension faithful.

theorem Representation.IsRealForm.isRealizableOverReal {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} [FiniteDimensional ℂ V] (h : ρ.IsRealForm σ) : ρ.IsRealizableOverReal

A real form on an arbitrary carrier realizes ρ over ℝ. Reading σ in a real basis of W moves it to the pinned carrier: complexification does not change the dimension (Representation.IsRealForm.finrank_eq), so a basis of W is indexed by Fin (finrank ℂ V), and conjugating σ by the resulting coordinate isomorphism turns the real form into one on Fin (finrank ℂ V) → ℝ. This is what makes Representation.IsRealizableOverReal usable from a real form carried by whatever space it naturally lives on.

Finiteness is asked of V, the representation the conclusion speaks about; the carrier W of the real form inherits it through Representation.IsRealForm.finiteDimensional_iff, which also takes a consumer who has finiteness on the real side the other way.

Real structures

structure Representation.IsRealStructure {G : Type u_1} [Monoid G] {k : Type u_2} {V : Type u_3} [CommSemiring k] [StarRing k] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (K : V →ₗ⋆[k] V) : Prop

A real structure on a representation over a commutative star ring k: an involution K of the underlying space, semilinear for starRingEnd k, that commutes with the action. For k = ℂ it is a conjugation of V -- a conjugate-linear involution -- and the predicate is the intrinsic form of Representation.IsRealForm, phrased inside V instead of on an auxiliary real carrier; it is the form in which realizability over ℝ is produced.

The conjugation is carried unbundled, matching Representation.IsInvariantForm; for k = ℂ the two fields are exactly the data of a TauCeti.Hodge.Conjugation together with equivariance.

• involutive : Function.Involutive ⇑K

  The conjugation is an involution.

• isIntertwining (g : G) (v : V) : K ((ρ g) v) = (ρ g) (K v)

  The conjugation intertwines the action with itself.

theorem Representation.IsRealStructure.apply_mem_realPoints {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {K : V →ₗ⋆[ℂ] V} (h : ρ.IsRealStructure K) (g : G) (v : V) : v ∈ TauCeti.realPoints K → (↑ℝ (ρ g)) v ∈ TauCeti.realPoints K

The action preserves the real points of a real structure: that is exactly the commutation K (ρ g v) = ρ g (K v) read on a fixed vector. It is stated for the ℝ-linear restriction (ρ g).restrictScalars ℝ of the action, which is the shape Representation.subrepresentation consumes in Representation.IsRealStructure.rep.

def Representation.IsRealStructure.rep {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {K : V →ₗ⋆[ℂ] V} (h : ρ.IsRealStructure K) : Representation ℝ G ↥(TauCeti.realPoints K)

The real representation carried by the real points of a real structure: reading ρ with only its ℝ-linearity, the real points are an invariant subspace, and Representation.subrepresentation restricts the action to them.

@[simp]

theorem Representation.IsRealStructure.coe_rep_apply {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {K : V →ₗ⋆[ℂ] V} (h : ρ.IsRealStructure K) (g : G) (w : ↥(TauCeti.realPoints K)) : ↑((h.rep g) w) = (ρ g) ↑w

theorem Representation.IsRealStructure.isRealForm {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {K : V →ₗ⋆[ℂ] V} (h : ρ.IsRealStructure K) : ρ.IsRealForm h.rep

The real points of a real structure are a real form. The ℂ-linear isomorphism is TauCeti.realPointsEquiv, which says that V is the complexification of the real points, and it intertwines the two actions because ρ g acts on a real point by its restriction.

theorem Representation.IsRealStructure.isRealizableOverReal {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {K : V →ₗ⋆[ℂ] V} (h : ρ.IsRealStructure K) [FiniteDimensional ℂ V] : ρ.IsRealizableOverReal

A real structure realizes ρ over ℝ in the pinned sense, once V is finite-dimensional.

theorem Representation.IsRealStructure.finrank_realPoints {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} {K : V →ₗ⋆[ℂ] V} (h : ρ.IsRealStructure K) : Module.finrank ℝ ↥(TauCeti.realPoints K) = Module.finrank ℂ V

The real points of a real structure have the ℝ-dimension that V has over ℂ; with Mathlib's finrank_real_of_complex this says they halve the real dimension of V. Equivariance plays no part, so this is the conjugation-level TauCeti.finrank_realPoints read on a real structure.

theorem Representation.IsRealForm.exists_isRealStructure {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] {ρ : Representation ℂ G V} {σ : Representation ℝ G W} (h : ρ.IsRealForm σ) : ∃ (K : V →ₗ⋆[ℂ] V), ρ.IsRealStructure K

A real form produces a real structure. Transport the conjugation c ⊗ₜ w ↦ conj c ⊗ₜ w of the complexification (TauCeti.tmulConj) along the isomorphism ℂ ⊗[ℝ] W ≃ₗ[ℂ] V. It commutes with the action because the action on the complexification is 1 ⊗ σ g, which leaves the first tensor factor -- the one being conjugated -- alone.

theorem Representation.isRealizableOverReal_iff_exists_isRealStructure {G : Type u_1} [Monoid G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] {ρ : Representation ℂ G V} [FiniteDimensional ℂ V] : ρ.IsRealizableOverReal ↔ ∃ (K : V →ₗ⋆[ℂ] V), ρ.IsRealStructure K

Realizability over ℝ is the existence of a real structure. This is the working form of realizability: the two implications are Representation.IsRealStructure.isRealizableOverReal and Representation.IsRealForm.exists_isRealStructure applied to a real form on the pinned carrier.