TypeProjectiveImplementation.lean

1 import PaperXI.TypeNormalizerPairing
2 import PaperXI.SchurScalar
3 import PaperXI.CliffordDatum
4 
5 /-! Implementation by an actual extension representation. Scalars compare
6 intertwiners for the same automorphism, not arbitrary quotient representatives.
7 The section defect is retained as an operator until scalarity is proved. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.TypeProjectiveImplementation
11 open TypeNormalizerAction TypeNormalizerPairing TypeSideDescent TypeSideExtension
12 open scoped IsMulCommutative
13 
14 variable {J V : Type*} [Group J] [AddCommGroup V] [Module ℂ V]
15 
16 /-- The invertible linear operator supplied by an actual representation. -/
17 def operator (κ : Representation ℂ J V) (j : J) : V ≃ₗ[ℂ] V where
18   toFun := κ j
19   invFun := κ j⁻¹
20   left_inv v := by
21     change (κ j⁻¹ * κ j) v = v
22     rw [← map_mul, inv_mul_cancel, map_one]
23     rfl
24   right_inv v := by
25     change (κ j * κ j⁻¹) v = v
26     rw [← map_mul, mul_inv_cancel, map_one]
27     rfl
28   map_add' := (κ j).map_add
29   map_smul' := (κ j).map_smul
30 
31 @[simp] theorem operator_apply (κ : Representation ℂ J V) (j : J) (v : V) :
32     operator κ j v = κ j v := rfl
33 
34 /-- Conjugation is implemented by the supplied extension, without an extra
35 intertwining assumption. -/
36 theorem implements_conjugation (N : Subgroup J) [N.Normal]
37     (κ : Representation ℂ J V) (j : J) (n : N) (v : V) :
38     operator κ j (κ (n : J) v) =
39       κ (conjugation N j n : J) (operator κ j v) := by
40   change (κ j * κ (n : J)) v = (κ (conjugation N j n : J) * κ j) v
41   rw [← map_mul, ← map_mul]
42   congr 2
43   simp [mul_assoc]
44 
45 section Schur
46 variable [FiniteDimensional ℂ V]
47 
48 /-- Two implementers of the same ambient conjugation differ by a unique unit
49 scalar. The result is Schur's lemma for the actual irreducible N-action. -/
50 theorem implementer_unique (N : Subgroup J) [N.Normal]
51     (κ : Representation ℂ J V) [Representation.IsIrreducible (κ.comp N.subtype)]
52     (j : J) (T : V ≃ₗ[ℂ] V)
53     (hT : ∀ (n : N) v, T (κ (n : J) v) = κ (conjugation N j n : J) (T v)) :
54     ∃! c : ℂˣ, ∀ v, T v = (c : ℂ) • operator κ j v := by
55   exact SchurScalar.bridge_unique (κ.comp N.subtype)
56     ((κ.comp N.subtype).comp (conjugation N j).toMonoidHom)
57     (operator κ j) T (implements_conjugation N κ j) hT
58 
59 /-- Any two choices for the same automorphism have the same scalar ambiguity. -/
60 theorem two_implementers (N : Subgroup J) [N.Normal]
61     (κ : Representation ℂ J V) [Representation.IsIrreducible (κ.comp N.subtype)]
62     (j : J) (T U : V ≃ₗ[ℂ] V)
63     (hT : ∀ (n : N) v, T (κ (n : J) v) = κ (conjugation N j n : J) (T v))
64     (hU : ∀ (n : N) v, U (κ (n : J) v) = κ (conjugation N j n : J) (U v)) :
65     ∃! c : ℂˣ, ∀ v, U v = (c : ℂ) • T v :=
66   SchurScalar.bridge_unique (κ.comp N.subtype)
67     ((κ.comp N.subtype).comp (conjugation N j).toMonoidHom) T U hT hU
68 
69 end Schur
70 
71 /-- The lift of a quotient representative has an operator-valued multiplication
72 defect. It is not automatically a scalar multiplier. -/
73 theorem section_operators_mul (N : Subgroup J) [N.Normal]
74     (κ : Representation ℂ J V) (a b : J ⧸ N) :
75     κ (CliffordDatum.sectionMap N a) * κ (CliffordDatum.sectionMap N b) =
76       κ (CliffordDatum.defect N a b : J) * κ (CliffordDatum.sectionMap N (a*b)) := by
77   rw [← map_mul, ← map_mul, CliffordDatum.section_mul]
78 
79 /-- Changing a quotient representative multiplies the implementer by the
80 actual N-operator. This factor need not be scalar. -/
81 theorem representative_change (N : Subgroup J) (κ : Representation ℂ J V)
82     (j : J) (n : N) : κ ((n : J)*j) = κ (n : J) * κ j := map_mul κ _ _
83 
84 /-- Projective constancy on quotient fibers, expressed without choosing PGL
85 coordinates or a quotient section. -/
86 def ProjectiveDescends (N : Subgroup J) [N.Normal] (κ : Representation ℂ J V) : Prop :=
87   ∀ j k, QuotientGroup.mk' N j = QuotientGroup.mk' N k →
88     ∃ c : ℂˣ, κ j = (c : ℂ) • κ k
89 
90 /-- Exact descent criterion: the subgroup being quotiented must act by scalars. -/
91 theorem projectiveDescends_iff (N : Subgroup J) [N.Normal] (κ : Representation ℂ J V) :
92     ProjectiveDescends N κ ↔ ∀ n : N, ∃ c : ℂˣ, κ (n : J) = (c : ℂ) • LinearMap.id := by
93   constructor
94   · intro hd n
95     obtain ⟨c,hc⟩ := hd n 1 (by simp)
96     exact ⟨c, by simpa [Module.End.one_eq_id] using hc⟩
97   · intro hs j k hjk
98     have hm : j * k⁻¹ ∈ N := by
99       apply (QuotientGroup.eq_one_iff _).mp
100       change QuotientGroup.mk' N (j*k⁻¹) = 1
101       rw [map_mul, map_inv, hjk, mul_inv_cancel]
102     obtain ⟨c,hc⟩ := hs ⟨j*k⁻¹,hm⟩
103     refine ⟨c, ?_⟩
104     calc
105       κ j = κ (j*k⁻¹) * κ k := by rw [← map_mul]; simp
106       _ = (c : ℂ) • κ k := by
107         rw [hc]
108         ext v
109         rfl
110 
111 /-- An element represented by a scalar has trivial operator commutator with
112 all other elements. -/
113 theorem scalar_element_commutator (κ : Representation ℂ J V) (x y : J)
114     (c : ℂ) (hx : κ x = c • LinearMap.id) :
115     κ (x*y*x⁻¹*y⁻¹) = 1 := by
116   have hcomm : κ x * κ y = κ y * κ x := by
117     rw [hx]
118     ext v
119     exact ((κ y).map_smul c v).symm
120   calc
121     κ (x*y*x⁻¹*y⁻¹) = ((κ x * κ y) * κ x⁻¹) * κ y⁻¹ := by simp only [map_mul]
122     _ = ((κ y * κ x) * κ x⁻¹) * κ y⁻¹ := by rw [hcomm]
123     _ = 1 := by rw [mul_assoc (κ y) (κ x), ← map_mul, mul_inv_cancel, map_one,
124                     mul_one, ← map_mul, mul_inv_cancel, map_one]
125 
126 /-- The representation realizes exactly the character's commutator scalar. -/
127 theorem source_operator_commutator (N : Subgroup J) [N.Normal]
128     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
129     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ)
130     (κ : Representation ℂ J V) [Representation.IsIrreducible (κ.comp N.subtype)]
131     (hcontains : Contains H θ (κ.comp N.subtype)) (x y : N) :
132     κ ((x*y*x⁻¹*y⁻¹ : N) : J) = (characterCommutator H θ x y : ℂ) • LinearMap.id :=
133   scalar_restriction H θ (inertiaInvariant N H hH θ hθ)
134     (κ.comp N.subtype) hcontains ⟨x*y*x⁻¹*y⁻¹,commutator_mem H x y⟩
135 
136 /-- A nontrivial Heisenberg commutator prevents the ambient implementers
137 from being projectively constant on J/N. -/
138 theorem nontrivial_pairing_obstructs_descent (N : Subgroup J) [N.Normal]
139     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
140     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ)
141     (κ : Representation ℂ J V) [Representation.IsIrreducible (κ.comp N.subtype)]
142     (hcontains : Contains H θ (κ.comp N.subtype))
143     (x y : N) (hxy : characterCommutator H θ x y ≠ 1) :
144     ¬ ProjectiveDescends N κ := by
145   intro hd
146   obtain ⟨c,hc⟩ := (projectiveDescends_iff N κ).mp hd x
147   have ht := source_operator_commutator N H hH θ hθ κ hcontains x y
148   have hz := scalar_element_commutator κ (x : J) (y : J) (c : ℂ) hc
149   have : Nontrivial V := GeneratedIrreducibility.nontrivial_space (κ.comp N.subtype)
150   obtain ⟨v,hv⟩ := exists_ne (0 : V)
151   apply hxy
152   apply Units.ext
153   have he : (characterCommutator H θ x y : ℂ) • v = (1 : ℂ) • v := by
154     simpa using LinearMap.congr_fun (ht.symm.trans hz) v
155   exact (smul_left_injective ℂ hv) he
156 
157 end PaperXI.TypeProjectiveImplementation

Back to source controls