CliffordChoices.lean

1 import PaperXI.CliffordMultiplicity
2 import PaperXI.ProjectiveCocycle
3 
4 /-! Choice comparisons on the literal Clifford multiplicity operators.
5 The comparing scalar is derived from Schur's lemma. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CliffordChoices
9 open CliffordDatum CliffordMultiplicity
10 
11 variable {G W X : Type*} [Group G]
12 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
13 
14 /-- Changing a chosen subgroup intertwiner changes the actual Hom operator by
15 its inverse scalar, with that inverse forced by the literal formula. -/
16 theorem operator_rescale (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
17     (π : Representation ℂ G X) (g : G)
18     (I J : Representation.Equiv ρ (conjugate N ρ g))
19     (μ : ℂˣ) (hμ : ∀ w, J w = (μ : ℂ) • I w) :
20     (operator N ρ π g J).toLinearMap =
21       ((μ⁻¹ : ℂˣ) : ℂ) • (operator N ρ π g I).toLinearMap := by
22   have hinv (w : W) : J.symm w = ((μ⁻¹ : ℂˣ) : ℂ) • I.symm w := by
23     apply J.injective
24     change J (J.symm w) = J (((μ⁻¹ : ℂˣ) : ℂ) • I.symm w)
25     rw [J.apply_symm_apply, map_smul, hμ, I.apply_symm_apply, smul_smul]
26     simp
27   ext f w
28   change π g (f (J.symm w)) = ((μ⁻¹ : ℂˣ) : ℂ) • π g (f (I.symm w))
29   rw [hinv, map_smul, map_smul]
30 
31 /-- Any two actual conjugation intertwiners differ by a unique unit scalar. -/
32 theorem existsUnique_intertwiner_scalar (N : Subgroup G) [N.Normal]
33     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ]
34     [FiniteDimensional ℂ W] (g : G)
35     (I J : Representation.Equiv ρ (conjugate N ρ g)) :
36     ∃! μ : ℂˣ, ∀ w, J w = (μ : ℂ) • I w := by
37   apply SchurScalar.bridge_unique ρ (conjugate N ρ g) I.toLinearEquiv J.toLinearEquiv
38   · intro n w
39     exact Representation.IntertwiningMap.isIntertwining ρ (conjugate N ρ g)
40       I.toIntertwiningMap n w
41   · intro n w
42     exact Representation.IntertwiningMap.isIntertwining ρ (conjugate N ρ g)
43       J.toIntertwiningMap n w
44 
45 /-- The actual scalar comparing arbitrary choices, chosen from its proved uniqueness. -/
46 def intertwinerScalar (N : Subgroup G) [N.Normal]
47     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ]
48     [FiniteDimensional ℂ W] (g : G)
49     (I J : Representation.Equiv ρ (conjugate N ρ g)) : ℂˣ :=
50   Classical.choose (existsUnique_intertwiner_scalar N ρ g I J)
51 
52 theorem intertwinerScalar_spec (N : Subgroup G) [N.Normal]
53     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ]
54     [FiniteDimensional ℂ W] (g : G)
55     (I J : Representation.Equiv ρ (conjugate N ρ g)) (w : W) :
56     J w = (intertwinerScalar N ρ g I J : ℂ) • I w :=
57   (Classical.choose_spec (existsUnique_intertwiner_scalar N ρ g I J)).1 w
58 
59 /-- The unit scalar comparison of actual multiplicity operators is derived,
60 rather than required as a hypothesis on alternative choices. -/
61 theorem operator_choice (N : Subgroup G) [N.Normal]
62     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ]
63     [FiniteDimensional ℂ W] (π : Representation ℂ G X) (g : G)
64     (I J : Representation.Equiv ρ (conjugate N ρ g)) :
65     (operator N ρ π g J).toLinearMap =
66       (((intertwinerScalar N ρ g I J)⁻¹ : ℂˣ) : ℂ) • (operator N ρ π g I).toLinearMap := by
67   exact operator_rescale N ρ π g I J (intertwinerScalar N ρ g I J)
68     (intertwinerScalar_spec N ρ g I J)
69 
70 
71 /-- The actual subgroup factor relating any representative of `a` to the chosen one. -/
72 def representativeFactor (N : Subgroup G) [N.Normal] (a : G ⧸ N) (g : G)
73     (hg : QuotientGroup.mk' N g = a) : N :=
74   ⟨g * (sectionMap N a)⁻¹, by
75     apply (QuotientGroup.eq_one_iff _).mp
76     change (QuotientGroup.mk' N) (g * (sectionMap N a)⁻¹) = 1
77     rw [map_mul, map_inv, hg, quotient_section, mul_inv_cancel]⟩
78 
79 theorem representative_factorization (N : Subgroup G) [N.Normal]
80     (a : G ⧸ N) (g : G) (hg : QuotientGroup.mk' N g = a) :
81     g = (representativeFactor N a g hg : G) * sectionMap N a := by
82   simp [representativeFactor, mul_assoc]
83 
84 /-- The section intertwiner adjusted by the actual subgroup representative factor. -/
85 def representativeIntertwiner (N : Subgroup G) [N.Normal]
86     (ρ : Representation ℂ N W) (hρ : Invariant N ρ)
87     (a : G ⧸ N) (g : G) (hg : QuotientGroup.mk' N g = a) :
88     Representation.Equiv ρ (conjugate N ρ g) :=
89   Representation.Equiv.mk
90     (subgroupIntertwiner N ρ (representativeFactor N a g hg) (sectionMap N a)
91       (sectionIntertwiner N ρ hρ a)).toLinearEquiv (by
92     intro n
93     apply LinearMap.ext
94     intro w
95     have h := intertwiner_apply N ρ
96       ((representativeFactor N a g hg : G) * sectionMap N a)
97       (subgroupIntertwiner N ρ (representativeFactor N a g hg) (sectionMap N a)
98         (sectionIntertwiner N ρ hρ a)) n w
99     simp only [subgroupIntertwiner_apply] at h
100     rw [← representative_factorization] at h
101     exact h)
102 
103 @[simp] theorem representativeIntertwiner_apply (N : Subgroup G) [N.Normal]
104     (ρ : Representation ℂ N W) (hρ : Invariant N ρ)
105     (a : G ⧸ N) (g : G) (hg : QuotientGroup.mk' N g = a) (w : W) :
106     representativeIntertwiner N ρ hρ a g hg w =
107       ρ (representativeFactor N a g hg) (sectionIntertwiner N ρ hρ a w) := rfl
108 
109 /-- The subgroup correction cancels on the actual multiplicity space. -/
110 theorem operator_representative (N : Subgroup G) [N.Normal]
111     (ρ : Representation ℂ N W) (π : Representation ℂ G X) (hρ : Invariant N ρ)
112     (a : G ⧸ N) (g : G) (hg : QuotientGroup.mk' N g = a) :
113     operator N ρ π g (representativeIntertwiner N ρ hρ a g hg) =
114       sectionOperator N ρ π hρ a := by
115   have h := operator_subgroup_mul N ρ π (representativeFactor N a g hg)
116     (sectionMap N a) (sectionIntertwiner N ρ hρ a)
117   ext f w
118   have hh := congrArg (fun e : Space N ρ π ≃ₗ[ℂ] Space N ρ π => e f w) h
119   change π ((representativeFactor N a g hg : G) * sectionMap N a)
120     (f ((sectionIntertwiner N ρ hρ a).symm (ρ (representativeFactor N a g hg)⁻¹ w))) = _ at hh
121   rw [← representative_factorization] at hh
122   exact hh
123 
124 /-- The inverse cochain comparing an arbitrary quotient section and arbitrary
125 conjugation intertwiners to the normalized baseline. -/
126 def choiceCochain (N : Subgroup G) [N.Normal]
127     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ]
128     [FiniteDimensional ℂ W] (hρ : Invariant N ρ)
129     (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
130     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a))) (a : G ⧸ N) : ℂˣ :=
131   (intertwinerScalar N ρ (s a) (representativeIntertwiner N ρ hρ a (s a) (hs a)) (I a))⁻¹
132 
133 /-- All actual section and intertwiner choices have the same projective class,
134 with a constructed inverse cochain. The alternative choices need not be normalized. -/
135 theorem arbitrary_choices (N : Subgroup G) [N.Normal]
136     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ]
137     [FiniteDimensional ℂ W] (π : Representation ℂ G X) (hρ : Invariant N ρ)
138     (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
139     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a))) (a : G ⧸ N) :
140     (operator N ρ π (s a) (I a)).toLinearMap =
141       (choiceCochain N ρ hρ s hs I a : ℂ) • (sectionOperator N ρ π hρ a).toLinearMap := by
142   have h := operator_choice N ρ π (s a)
143     (representativeIntertwiner N ρ hρ a (s a) (hs a)) (I a)
144   rw [operator_representative] at h
145   exact h
146 
147 end PaperXI.CliffordChoices
148 

Back to source controls