ProductNormalizerQuotient59.lean

1 import PaperXI.NormalizerExtensionInducing58
2 import Mathlib.GroupTheory.QuotientGroup.Basic
3 import Mathlib.GroupTheory.Subgroup.Centralizer
4 
5 /-!
6 # Product subgroups and the action of a centralizing normalizer
7 
8 For actual subgroups `H,N` of an ambient group, with `H` normalizing `N`,
9 the quotient of `H ⊔ N` by `N` is the quotient of `H` by its intersection
10 with `N`. An ambient element centralizing `H` and normalizing `N` acts
11 trivially on this quotient. No identification with a simple-character group
12 is asserted here.
13 -/
14 set_option autoImplicit false
15 noncomputable section
16 namespace PaperXI.ProductNormalizerQuotient59
17 
18 variable {G : Type*} [Group G]
19 variable (H N : Subgroup G) (t : G)
20 variable (hH : ∀ h ∈ H, t * h = h * t)
21 variable (hN : t ∈ Subgroup.normalizer (N : Set G))
22 
23 include hH hN in
24 /-- Centralizing one factor and normalizing the other normalizes their product. -/
25 theorem normalizes_sup : t ∈ Subgroup.normalizer ((H ⊔ N : Subgroup G) : Set G) := by
26   apply H.inf_normalizer_le_normalizer_sup N
27   refine ⟨?_, hN⟩
28   apply Subgroup.centralizer_le_normalizer
29   exact Subgroup.mem_centralizer_iff.mpr fun h hh => (hH h hh).symm
30 
31 /-- The literal ambient conjugation automorphism of the product subgroup. -/
32 def conjugation : MulAut (H ⊔ N : Subgroup G) :=
33   NormalizerExtensionInducing58.conjugation (H ⊔ N) t (normalizes_sup H N t hH hN)
34 
35 @[simp] theorem conjugation_coe (j : (H ⊔ N : Subgroup G)) :
36     ((conjugation H N t hH hN j : (H ⊔ N : Subgroup G)) : G) =
37       t * (j : G) * t⁻¹ := rfl
38 
39 /-- Every homomorphism killing the second factor is unchanged by conjugation. -/
40 theorem map_conjugation {Q : Type*} [Group Q]
41     (hHN : H ≤ Subgroup.normalizer (N : Set G))
42     (q : (H ⊔ N : Subgroup G) →* Q)
43     (hq : N.subgroupOf (H ⊔ N) ≤ q.ker)
44     (j : (H ⊔ N : Subgroup G)) :
45     q (conjugation H N t hH hN j) = q j := by
46   have hj := j.property
47   rw [← SetLike.mem_coe, Subgroup.coe_mul_of_left_le_normalizer_right H N hHN] at hj
48   obtain ⟨h, hh, n, hn, he⟩ := hj
49   let a : (H ⊔ N : Subgroup G) := ⟨h, (show H ≤ H ⊔ N from le_sup_left) hh⟩
50   let b : (H ⊔ N : Subgroup G) := ⟨n, (show N ≤ H ⊔ N from le_sup_right) hn⟩
51   have hj' : j = a * b := Subtype.ext he.symm
52   have ha : conjugation H N t hH hN a = a := by
53     apply Subtype.ext
54     change t * h * t⁻¹ = h
55     rw [hH h hh, mul_assoc, mul_inv_cancel, mul_one]
56   have hb : q b = 1 := hq hn
57   have hcb : q (conjugation H N t hH hN b) = 1 := by
58     apply hq
59     exact (Subgroup.mem_normalizer_iff.mp hN n).mp hn
60   simp only [hj', map_mul, ha, hcb, hb]
61 
62 /-- The actual quotient projection is unchanged by the normalizer action. -/
63 theorem quotient_conjugation (hHN : H ≤ Subgroup.normalizer (N : Set G))
64     (j : (H ⊔ N : Subgroup G)) :
65     letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hHN
66     QuotientGroup.mk' (N.subgroupOf (H ⊔ N)) (conjugation H N t hH hN j) =
67       QuotientGroup.mk' (N.subgroupOf (H ⊔ N)) j := by
68   let := Subgroup.normal_subgroupOf_sup_of_le_normalizer hHN
69   apply map_conjugation H N t hH hN hHN
70   rw [QuotientGroup.ker_mk']
71 
72 /-- The second isomorphism theorem gives the literal product quotient. -/
73 def productQuotientEquiv (hHN : H ≤ Subgroup.normalizer (N : Set G)) :
74     letI := Subgroup.normal_subgroupOf_of_le_normalizer hHN
75     letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hHN
76     (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N) ≃* H ⧸ N.subgroupOf H := by
77   letI := Subgroup.normal_subgroupOf_of_le_normalizer hHN
78   letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hHN
79   exact (QuotientGroup.quotientInfEquivProdNormalizerQuotient H N hHN).symm
80 
81 /-- A concrete surjective map on the first factor identifies the full product
82 quotient once its kernel is the actual intersection with the second factor. -/
83 def quotientEquivOfKernel {Q : Type*} [Group Q]
84     (hHN : H ≤ Subgroup.normalizer (N : Set G))
85     (q : H →* Q) (hq : Function.Surjective q)
86     (hker : N.subgroupOf H = q.ker) :
87     letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hHN
88     (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N) ≃* Q := by
89   letI := Subgroup.normal_subgroupOf_of_le_normalizer hHN
90   letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hHN
91   exact (productQuotientEquiv H N hHN).trans
92     ((QuotientGroup.quotientMulEquivOfEq hker).trans
93       (QuotientGroup.quotientKerEquivOfSurjective q hq))
94 
95 end PaperXI.ProductNormalizerQuotient59

Back to source controls