TypeNormalizerAction.lean

1 import Mathlib.GroupTheory.QuotientGroup.Basic
2 import Mathlib.Algebra.Group.IsCommutative
3 import Mathlib.Tactic.Group
4 
5 /-! The actual ambient conjugation action on N/H and its descent to J/N.
6 The quotient action is constructed from groups, not from choices of operators. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.TypeNormalizerAction
10 open scoped IsMulCommutative
11 
12 variable {J : Type*} [Group J]
13 
14 /-- Restriction of ambient conjugation to the actual normal subgroup. -/
15 def conjugation (N : Subgroup J) [N.Normal] : J →* MulAut N where
16   toFun j :=
17     { toFun x := ⟨j * (x : J) * j⁻¹, Subgroup.Normal.conj_mem (inferInstance : N.Normal) x x.property j⟩
18       invFun x := ⟨j⁻¹ * (x : J) * (j⁻¹)⁻¹, Subgroup.Normal.conj_mem (inferInstance : N.Normal) x x.property j⁻¹⟩
19       left_inv x := by apply Subtype.ext; simp [mul_assoc]
20       right_inv x := by apply Subtype.ext; simp [mul_assoc]
21       map_mul' x y := by apply Subtype.ext; simp [mul_assoc] }
22   map_one' := by ext x; simp
23   map_mul' j k := by ext x; simp [mul_assoc]
24 
25 @[simp] theorem conjugation_coe (N : Subgroup J) [N.Normal] (j : J) (x : N) :
26     ((conjugation N j x : N) : J) = j * (x : J) * j⁻¹ := rfl
27 
28 @[simp] theorem conjugation_inner (N : Subgroup J) [N.Normal] (n x : N) :
29     conjugation N (n : J) x = n * x * n⁻¹ := by
30   apply Subtype.ext
31   rfl
32 
33 /-- Stability under all ambient conjugations, including their inverses. -/
34 def Stable (N : Subgroup J) [N.Normal] (H : Subgroup N) : Prop :=
35   ∀ j x, x ∈ H → conjugation N j x ∈ H
36 
37 theorem stable_map (N : Subgroup J) [N.Normal] (H : Subgroup N)
38     (hH : Stable N H) (j : J) : H.map (conjugation N j).toMonoidHom = H := by
39   apply le_antisymm
40   · rintro x ⟨y, hy, rfl⟩
41     exact hH j y hy
42   · intro x hx
43     refine ⟨conjugation N j⁻¹ x, hH j⁻¹ x hx, ?_⟩
44     apply Subtype.ext
45     simp
46 
47 /-- The induced action before quotienting the normalizing group. -/
48 def action (N : Subgroup J) [N.Normal] (H : Subgroup N) [H.Normal]
49     (hH : Stable N H) : J →* MulAut (N ⧸ H) where
50   toFun j := QuotientGroup.congr H H (conjugation N j) (stable_map N H hH j)
51   map_one' := by
52     ext x
53     induction x using QuotientGroup.induction_on with | H n =>
54       change QuotientGroup.mk (conjugation N 1 n) = QuotientGroup.mk n
55       rw [map_one]
56       rfl
57   map_mul' j k := by
58     ext x
59     induction x using QuotientGroup.induction_on with | H n =>
60       change QuotientGroup.mk (conjugation N (j*k) n) =
61         QuotientGroup.mk (conjugation N j (conjugation N k n))
62       rw [map_mul]
63       rfl
64 
65 @[simp] theorem action_mk (N : Subgroup J) [N.Normal] (H : Subgroup N) [H.Normal]
66     (hH : Stable N H) (j : J) (x : N) :
67     action N H hH j (QuotientGroup.mk' H x) =
68       QuotientGroup.mk' H (conjugation N j x) := rfl
69 
70 /-- N acts trivially on its abelian quotient, so no operator lift is needed
71 for the honest J/N action. -/
72 theorem subgroup_le_kernel (N : Subgroup J) [N.Normal] (H : Subgroup N)
73     [H.Normal] [IsMulCommutative (N ⧸ H)] (hH : Stable N H) :
74     N ≤ (action N H hH).ker := by
75   intro n hn
76   change action N H hH n = 1
77   ext x
78   induction x using QuotientGroup.induction_on with | H t =>
79     change QuotientGroup.mk' H (conjugation N n t) = QuotientGroup.mk' H t
80     have h : n = ((⟨n,hn⟩ : N) : J) := rfl
81     rw [h, conjugation_inner]
82     simp [mul_comm]
83 
84 /-- The honest quotient action on the actual symplectic quotient. -/
85 def quotientAction (N : Subgroup J) [N.Normal] (H : Subgroup N)
86     [H.Normal] [IsMulCommutative (N ⧸ H)] (hH : Stable N H) :
87     (J ⧸ N) →* MulAut (N ⧸ H) :=
88   QuotientGroup.lift N (action N H hH) (subgroup_le_kernel N H hH)
89 
90 @[simp] theorem quotientAction_mk (N : Subgroup J) [N.Normal] (H : Subgroup N)
91     [H.Normal] [IsMulCommutative (N ⧸ H)] (hH : Stable N H) (j : J) (x : N) :
92     quotientAction N H hH (QuotientGroup.mk' N j) (QuotientGroup.mk' H x) =
93       QuotientGroup.mk' H (conjugation N j x) := rfl
94 
95 /-- The representative formula uniquely specifies the action. -/
96 theorem quotientAction_unique (N : Subgroup J) [N.Normal] (H : Subgroup N)
97     [H.Normal] [IsMulCommutative (N ⧸ H)] (hH : Stable N H)
98     (a : (J ⧸ N) →* MulAut (N ⧸ H))
99     (ha : ∀ j x, a (QuotientGroup.mk' N j) (QuotientGroup.mk' H x) =
100       QuotientGroup.mk' H (conjugation N j x)) : a = quotientAction N H hH := by
101   apply MonoidHom.ext
102   intro j
103   obtain ⟨g,rfl⟩ := QuotientGroup.mk_surjective j
104   ext x
105   obtain ⟨n,rfl⟩ := QuotientGroup.mk_surjective x
106   exact ha g n
107 
108 end PaperXI.TypeNormalizerAction

Back to source controls