CliffordDatum.lean

1 import PaperXI.QuotientRepresentation
2 import Mathlib.Analysis.Complex.Basic
3 
4 /-! Actual restriction, conjugation and normalized quotient representatives
5 for the Clifford multiplicity construction. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CliffordDatum
9 
10 variable {G W X : Type*} [Group G]
11 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
12 
13 /-- Restriction to the actual subgroup. -/
14 abbrev restriction (N : Subgroup G) (π : Representation ℂ G X) : Representation ℂ N X :=
15   π.comp N.subtype
16 
17 /-- Ambient conjugation, with membership supplied by normality. -/
18 def conjugation (N : Subgroup G) [N.Normal] (g : G) : N →* N where
19   toFun n := ⟨g * n * g⁻¹, Subgroup.Normal.conj_mem (inferInstance : N.Normal) (n : G) n.property g⟩
20   map_one' := by apply Subtype.ext; simp
21   map_mul' n m := by apply Subtype.ext; simp [mul_assoc]
22 
23 @[simp] theorem conjugation_coe (N : Subgroup G) [N.Normal] (g : G) (n : N) :
24     (conjugation N g n : G) = g * n * g⁻¹ := rfl
25 
26 @[simp] theorem conjugation_one (N : Subgroup G) [N.Normal] (n : N) :
27     conjugation N 1 n = n := by apply Subtype.ext; simp
28 
29 @[simp] theorem conjugation_mul (N : Subgroup G) [N.Normal] (g h : G) (n : N) :
30     conjugation N (g * h) n = conjugation N g (conjugation N h n) := by
31   apply Subtype.ext
32   simp [mul_assoc]
33 
34 @[simp] theorem conjugation_inv_cancel (N : Subgroup G) [N.Normal] (g : G) (n : N) :
35     conjugation N g (conjugation N g⁻¹ n) = n := by
36   rw [← conjugation_mul]
37   simp
38 
39 /-- The representation obtained by the actual ambient conjugation. -/
40 abbrev conjugate (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W) (g : G) :=
41   ρ.comp (conjugation N g)
42 
43 /-- The source invariance hypothesis is equivalence of actual representations. -/
44 def Invariant (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W) : Prop :=
45   ∀ g : G, Nonempty (Representation.Equiv ρ (conjugate N ρ g))
46 
47 /-- A normalized sectionMap of the actual quotient map. -/
48 def sectionMap (N : Subgroup G) [N.Normal] (a : G ⧸ N) : G :=
49   by
50   classical
51   exact if a = 1 then 1 else Classical.choose (QuotientGroup.mk_surjective a)
52 
53 @[simp] theorem section_one (N : Subgroup G) [N.Normal] : sectionMap N 1 = 1 := by
54   simp [sectionMap]
55 
56 @[simp] theorem quotient_section (N : Subgroup G) [N.Normal] (a : G ⧸ N) :
57     QuotientGroup.mk' N (sectionMap N a) = a := by
58   classical
59   by_cases ha : a = 1
60   · subst a; simp
61   · simpa [sectionMap, ha] using (Classical.choose_spec (QuotientGroup.mk_surjective a))
62 
63 /-- The actual subgroup-valued multiplication defect of the chosen sectionMap. -/
64 def defect (N : Subgroup G) [N.Normal] (a b : G ⧸ N) : N :=
65   ⟨sectionMap N a * sectionMap N b * (sectionMap N (a * b))⁻¹, by
66     apply (QuotientGroup.eq_one_iff _).mp
67     change QuotientGroup.mk' N (_ * _ * _⁻¹) = 1
68     rw [map_mul, map_mul, map_inv, quotient_section, quotient_section, quotient_section]
69     exact mul_inv_cancel _⟩
70 
71 @[simp] theorem defect_coe (N : Subgroup G) [N.Normal] (a b : G ⧸ N) :
72     (defect N a b : G) = sectionMap N a * sectionMap N b * (sectionMap N (a * b))⁻¹ := rfl
73 
74 theorem section_mul (N : Subgroup G) [N.Normal] (a b : G ⧸ N) :
75     sectionMap N a * sectionMap N b = (defect N a b : G) * sectionMap N (a * b) := by
76   simp [mul_assoc]
77 
78 @[simp] theorem defect_one_left (N : Subgroup G) [N.Normal] (a : G ⧸ N) :
79     defect N 1 a = 1 := by apply Subtype.ext; simp
80 
81 @[simp] theorem defect_one_right (N : Subgroup G) [N.Normal] (a : G ⧸ N) :
82     defect N a 1 = 1 := by apply Subtype.ext; simp
83 
84 /-- The subgroup part of an arbitrary representative's normal form. -/
85 def coordinate (N : Subgroup G) [N.Normal] (g : G) : N :=
86   ⟨g * (sectionMap N (QuotientGroup.mk' N g))⁻¹, by
87     apply (QuotientGroup.eq_one_iff _).mp
88     change QuotientGroup.mk' N (g * (sectionMap N (QuotientGroup.mk' N g))⁻¹) = 1
89     rw [map_mul, map_inv, quotient_section]
90     exact mul_inv_cancel _⟩
91 
92 theorem normal_form (N : Subgroup G) [N.Normal] (g : G) :
93     g = (coordinate N g : G) * sectionMap N (QuotientGroup.mk' N g) := by
94   simp [coordinate, mul_assoc]
95 
96 /-- An invertible intertwiner chosen from invariance, normalized at the identity. -/
97 def sectionIntertwiner (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
98     (hρ : Invariant N ρ) (a : G ⧸ N) :
99     Representation.Equiv ρ (conjugate N ρ (sectionMap N a)) := by
100   classical
101   by_cases ha : a = 1
102   · subst a
103     exact Representation.Equiv.mk (LinearEquiv.refl ℂ W) (by intro n; simp [conjugate])
104   · exact Classical.choice (hρ (sectionMap N a))
105 
106 @[simp] theorem sectionIntertwiner_one (N : Subgroup G) [N.Normal]
107     (ρ : Representation ℂ N W) (hρ : Invariant N ρ) (w : W) :
108     sectionIntertwiner N ρ hρ 1 w = w := by
109   simp only [sectionIntertwiner, dite_true]
110   rfl
111 
112 end PaperXI.CliffordDatum

Back to source controls