CliffordIrreducible.lean

1 import PaperXI.CliffordMultiplicity
2 import PaperXI.CliffordEvaluation
3 import PaperXI.TensorSubspace
4 
5 /-! Canonical evaluation and irreducibility on the actual Clifford
6 multiplicity space. All finite dimensions and tensor-image properties are
7 derived from the finite-group irreducibles and genuine module isotypy. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CliffordIrreducible
11 open CliffordDatum CliffordMultiplicity
12 open scoped TensorProduct
13 
14 variable {G W X : Type*} [Group G] [Finite G]
15 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
16 variable (N : Subgroup G)
17 variable (ρ : Representation ℂ N W) (π : Representation ℂ G X)
18 variable [Representation.IsIrreducible ρ] [Representation.IsIrreducible π]
19 
20 /-- The isotypic source condition on the actual restricted group-algebra module. -/
21 abbrev Isotypic : Prop :=
22   IsIsotypicOfType (MonoidAlgebra ℂ N) (restriction N π).asModule ρ.asModule
23 
24 /-- The actual Hom space has finite dimension, derived from the finite-group actions. -/
25 theorem multiplicity_finiteDimensional : FiniteDimensional ℂ (Space N ρ π) := by
26   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
27   let : FiniteDimensional ℂ X := FiniteRepresentation.finiteDimensional π
28   infer_instance
29 
30 /-- Genuine isotypy and the nonzero original representation force nonzero multiplicity. -/
31 theorem multiplicity_nontrivial (h : Isotypic N ρ π) : Nontrivial (Space N ρ π) := by
32   let : FiniteDimensional ℂ X := FiniteRepresentation.finiteDimensional π
33   let : Nontrivial X := GeneratedIrreducibility.nontrivial_space π
34   exact CliffordEvaluation.multiplicity_nontrivial ρ (restriction N π) h
35 
36 /-- The source evaluation equivalence, with its bijectivity proved from isotypy. -/
37 def evaluation (h : Isotypic N ρ π) : W ⊗[ℂ] Space N ρ π ≃ₗ[ℂ] X := by
38   let : FiniteDimensional ℂ X := FiniteRepresentation.finiteDimensional π
39   exact CliffordEvaluation.equiv ρ (restriction N π) h
40 
41 @[simp] theorem evaluation_tmul (h : Isotypic N ρ π) (w : W) (f : Space N ρ π) :
42     evaluation N ρ π h (w ⊗ₜ[ℂ] f) = f w := rfl
43 
44 variable [N.Normal]
45 
46 /-- The literal section action factors through the proved canonical evaluation. -/
47 theorem section_action (h : Isotypic N ρ π) (hρ : Invariant N ρ)
48     (a : G ⧸ N) (t : W ⊗[ℂ] Space N ρ π) :
49     π (sectionMap N a) (evaluation N ρ π h t) =
50       evaluation N ρ π h (TensorProduct.map
51         (sectionIntertwiner N ρ hρ a).toLinearMap
52         (sectionOperator N ρ π hρ a).toLinearMap t) := by
53   induction t using TensorProduct.induction_on with
54   | zero => simp
55   | add s t hs ht => simp [hs, ht]
56   | tmul w f =>
57     simp only [TensorProduct.map_tmul, evaluation_tmul]
58     change π (sectionMap N a) (f w) =
59       π (sectionMap N a) (f ((sectionIntertwiner N ρ hρ a).symm
60         (sectionIntertwiner N ρ hρ a w)))
61     rw [Representation.Equiv.symm_apply_apply]
62 
63 /-- The actual group normal form gives the factorwise action needed for every g. -/
64 theorem group_action (h : Isotypic N ρ π) (hρ : Invariant N ρ)
65     (g : G) (w : W) (f : Space N ρ π) :
66     π g (evaluation N ρ π h (w ⊗ₜ[ℂ] f)) =
67       evaluation N ρ π h
68         (ρ (coordinate N g) (sectionIntertwiner N ρ hρ (QuotientGroup.mk' N g) w) ⊗ₜ[ℂ]
69           sectionOperator N ρ π hρ (QuotientGroup.mk' N g) f) := by
70   rw [evaluation_tmul, evaluation_tmul, space_intertwines]
71   change π g (f w) = π (coordinate N g : G)
72     (π (sectionMap N (QuotientGroup.mk' N g))
73       (f ((sectionIntertwiner N ρ hρ (QuotientGroup.mk' N g)).symm
74         (sectionIntertwiner N ρ hρ (QuotientGroup.mk' N g) w))))
75   rw [Representation.Equiv.symm_apply_apply]
76   change π g (f w) = (π (coordinate N g : G) * π (sectionMap N (QuotientGroup.mk' N g))) (f w)
77   rw [← map_mul, ← normal_form]
78 
79 /-- The projective multiplicity action is actually irreducible. -/
80 theorem irreducible (h : Isotypic N ρ π) (hρ : Invariant N ρ)
81     (L : Submodule ℂ (Space N ρ π))
82     (hL : ∀ a f, f ∈ L → sectionOperator N ρ π hρ a f ∈ L) :
83     L = ⊥ ∨ L = ⊤ := by
84   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
85   let : FiniteDimensional ℂ (Space N ρ π) := multiplicity_finiteDimensional N ρ π
86   let : Nontrivial W := GeneratedIrreducibility.nontrivial_space ρ
87   let E := evaluation N ρ π h
88   have hs : RepresentationStability.Stable π (TensorSubspace.image E L) := by
89     intro g
90     exact TensorSubspace.image_stable E L (π g)
91       ((ρ (coordinate N g)).comp (sectionIntertwiner N ρ hρ (QuotientGroup.mk' N g)).toLinearMap)
92       (sectionOperator N ρ π hρ (QuotientGroup.mk' N g)).toLinearMap
93       (hL (QuotientGroup.mk' N g)) (group_action N ρ π h hρ g)
94   rcases RepresentationStability.eq_bot_or_top π (TensorSubspace.image E L) hs with hb | ht
95   · exact Or.inl ((TensorSubspace.image_eq_bot_iff E L).mp hb)
96   · exact Or.inr ((TensorSubspace.image_eq_top_iff E L).mp ht)
97 
98 end PaperXI.CliffordIrreducible

Back to source controls