CliffordAction.lean

1 import PaperXI.CliffordIrreducible
2 import PaperXI.CliffordChoices
3 
4 /-! The full Clifford choice comparison and irreducibility for every
5 section, intertwiner family, and equivariant tensor identification. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CliffordAction
9 open CliffordDatum CliffordMultiplicity CliffordIrreducible
10 open scoped TensorProduct
11 
12 variable {G W X : Type*} [Group G] [Finite G]
13 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
14 variable (N : Subgroup G) [N.Normal]
15 variable (ρ : Representation ℂ N W) (π : Representation ℂ G X)
16 variable [Representation.IsIrreducible ρ] [Representation.IsIrreducible π]
17 variable (h : Isotypic N ρ π) (hρ : Invariant N ρ)
18 variable (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
19 variable (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a)))
20 variable (E : W ⊗[ℂ] Space N ρ π ≃ₗ[ℂ] X)
21 variable (hE : ∀ (n : N) (w : W) (f : Space N ρ π),
22   E ((ρ n w) ⊗ₜ[ℂ] f) = π (n : G) (E (w ⊗ₜ[ℂ] f)))
23 variable (T : G ⧸ N → Module.End ℂ (Space N ρ π))
24 variable (hT : ∀ (a : G ⧸ N) (w : W) (f : Space N ρ π),
25   E ((I a w) ⊗ₜ[ℂ] T a f) = π (s a) (E (w ⊗ₜ[ℂ] f)))
26 
27 include h hρ s hs I E hE T hT
28 
29 /-- All three Clifford choices are compared simultaneously with the constructed
30 canonical action. The tensor equivalence on the right is proved from isotypy. -/
31 theorem all_choices :
32     ∃ (L : Space N ρ π ≃ₗ[ℂ] Space N ρ π) (γ : G ⧸ N → ℂˣ),
33       (∀ (w : W) (f : Space N ρ π),
34         E (w ⊗ₜ[ℂ] f) = evaluation N ρ π h (w ⊗ₜ[ℂ] L f)) ∧
35       ∀ (a : G ⧸ N) (f : Space N ρ π),
36         T a f = (γ a : ℂ) • L.symm (sectionOperator N ρ π hρ a (L f)) := by
37   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
38   let : FiniteDimensional ℂ X := FiniteRepresentation.finiteDimensional π
39   let L := CliffordEvaluation.choiceEquiv ρ (restriction N π) E hE
40   let γ := CliffordChoices.choiceCochain N ρ hρ s hs I
41   refine ⟨L, γ, ?_, ?_⟩
42   · intro w f
43     rfl
44   · intro a f
45     have ht := CliffordEvaluation.choice_operator_conjugation N π ρ (s a) (I a)
46       E hE (T a) (hT a) f
47     have hc := LinearMap.congr_fun (CliffordChoices.arbitrary_choices N ρ π hρ s hs I a) (L f)
48     change operator N ρ π (s a) (I a) (L f) =
49       (γ a : ℂ) • sectionOperator N ρ π hρ a (L f) at hc
50     change T a f = L.symm (operator N ρ π (s a) (I a) (L f)) at ht
51     rw [ht, hc, map_smul]
52 
53 /-- Every action obtained from any of the three choices is irreducible on
54 the actual multiplicity space. No invertibility of the alternative operators
55 or multiplicity dimension is assumed. -/
56 theorem irreducible_all_choices (S : Submodule ℂ (Space N ρ π))
57     (hS : ∀ a f, f ∈ S → T a f ∈ S) : S = ⊥ ∨ S = ⊤ := by
58   obtain ⟨L, γ, _, hcomp⟩ := all_choices N ρ π h hρ s hs I E hE T hT
59   let P : Submodule ℂ (Space N ρ π) := S.map L.toLinearMap
60   have hP (a : G ⧸ N) (f : Space N ρ π) (hf : f ∈ P) :
61       sectionOperator N ρ π hρ a f ∈ P := by
62     obtain ⟨g, hg, rfl⟩ := hf
63     have heq : L (T a g) = (γ a : ℂ) • sectionOperator N ρ π hρ a (L g) := by
64       rw [hcomp, map_smul, LinearEquiv.apply_symm_apply]
65     refine ⟨(((γ a)⁻¹ : ℂˣ) : ℂ) • T a g, S.smul_mem _ (hS a g hg), ?_⟩
66     change L ((((γ a)⁻¹ : ℂˣ) : ℂ) • T a g) = sectionOperator N ρ π hρ a (L g)
67     rw [map_smul, heq, smul_smul]
68     simp
69   rcases CliffordIrreducible.irreducible N ρ π h hρ P hP with hb | ht
70   · left
71     apply le_antisymm _ bot_le
72     intro f hf
73     change f = 0
74     apply L.injective
75     have hm : L f ∈ P := ⟨f, hf, rfl⟩
76     rw [hb] at hm
77     change L f = 0 at hm
78     exact hm.trans L.map_zero.symm
79   · right
80     apply top_unique
81     intro f _
82     have hm : L f ∈ P := ht ▸ (show L f ∈ (⊤ : Submodule ℂ (Space N ρ π)) from trivial)
83     obtain ⟨g, hg, hgf⟩ := hm
84     exact L.injective hgf ▸ hg
85 
86 end PaperXI.CliffordAction

Back to source controls