TypeNormalizerPairing.lean

1 import PaperXI.TypeNormalizerAction
2 import PaperXI.TypeSideExtension
3 import Mathlib.Tactic.FieldSimp
4 import Mathlib.Tactic.Ring
5 
6 /-! Character invariance yields preservation of the actual quotient pairing.
7 No form-preservation hypothesis is inserted into the normalizer theorem. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.TypeNormalizerPairing
11 open TypeNormalizerAction TypeSideDescent TypeSideExtension
12 open scoped IsMulCommutative
13 
14 variable {J : Type*} [Group J]
15 
16 /-- Ambient conjugation restricted to the character subgroup. -/
17 def subgroupAut (N : Subgroup J) [N.Normal] (H : Subgroup N)
18     (hH : Stable N H) (j : J) : MulAut H where
19   toFun x := ⟨conjugation N j x, hH j x x.property⟩
20   invFun x := ⟨conjugation N j⁻¹ x, hH j⁻¹ x x.property⟩
21   left_inv x := by apply Subtype.ext; apply Subtype.ext; simp
22   right_inv x := by apply Subtype.ext; apply Subtype.ext; simp
23   map_mul' x y := by apply Subtype.ext; exact map_mul (conjugation N j) (x : N) (y : N)
24 
25 /-- The source hypothesis that the ambient normalizer fixes the character. -/
26 def CharacterInvariant (N : Subgroup J) [N.Normal] (H : Subgroup N)
27     (hH : Stable N H) (θ : H →* ℂˣ) : Prop :=
28   ∀ j h, θ (subgroupAut N H hH j h) = θ h
29 
30 /-- Ambient invariance includes the subgroup invariance required for the
31 actual central extension N/ker(theta). -/
32 theorem inertiaInvariant (N : Subgroup J) [N.Normal] (H : Subgroup N)
33     [H.Normal] (hH : Stable N H) (θ : H →* ℂˣ)
34     (hθ : CharacterInvariant N H hH θ) : Invariant H θ := by
35   intro n h
36   have he : conjugate H n h = subgroupAut N H hH (n : J) h := by
37     apply Subtype.ext
38     exact (conjugation_inner N n h).symm
39   rw [he]
40   exact hθ (n : J) h
41 
42 /-- The invariant is theta evaluated on the actual group commutator. -/
43 theorem characterCommutator_preserved (N : Subgroup J) [N.Normal]
44     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
45     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ)
46     (j : J) (x y : N) :
47     characterCommutator H θ (conjugation N j x) (conjugation N j y) =
48       characterCommutator H θ x y := by
49   let h : H := ⟨x * y * x⁻¹ * y⁻¹, commutator_mem H x y⟩
50   have he : (⟨conjugation N j x * conjugation N j y *
51       (conjugation N j x)⁻¹ * (conjugation N j y)⁻¹,
52       commutator_mem H (conjugation N j x) (conjugation N j y)⟩ : H) =
53       subgroupAut N H hH j h := by
54     apply Subtype.ext
55     simp [subgroupAut, h]
56   change θ _ = θ h
57   rw [he]
58   exact hθ j h
59 
60 /-- The canonical scalar pairing on the actual quotient N/H. -/
61 def pairing (N : Subgroup J) [N.Normal] (H : Subgroup N)
62     [H.Normal] [IsMulCommutative (N ⧸ H)] (hH : Stable N H)
63     (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ) :
64     (N ⧸ H) → (N ⧸ H) → ℂˣ :=
65   CocycleCommutator.commutator
66     (CentralExtension.scalarCocycle (datum H θ (inertiaInvariant N H hH θ hθ))
67       (centralCharacter H θ))
68 
69 @[simp] theorem pairing_on_representatives (N : Subgroup J) [N.Normal]
70     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
71     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ) (x y : N) :
72     pairing N H hH θ hθ (QuotientGroup.mk' H x) (QuotientGroup.mk' H y) =
73       characterCommutator H θ x y :=
74   scalar_commutator_source H θ (inertiaInvariant N H hH θ hθ) x y
75 
76 /-- The honest J/N action preserves the pairing, independently of projective lifts. -/
77 theorem quotientAction_preserves_pairing (N : Subgroup J) [N.Normal]
78     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
79     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ)
80     (j : J ⧸ N) (x y : N ⧸ H) :
81     pairing N H hH θ hθ (quotientAction N H hH j x) (quotientAction N H hH j y) =
82       pairing N H hH θ hθ x y := by
83   obtain ⟨g,rfl⟩ := QuotientGroup.mk_surjective j
84   obtain ⟨a,rfl⟩ := QuotientGroup.mk_surjective x
85   obtain ⟨b,rfl⟩ := QuotientGroup.mk_surjective y
86   change pairing N H hH θ hθ
87     (QuotientGroup.mk' H (conjugation N g a))
88     (QuotientGroup.mk' H (conjugation N g b)) =
89     pairing N H hH θ hθ (QuotientGroup.mk' H a) (QuotientGroup.mk' H b)
90   simp only [pairing_on_representatives]
91   exact characterCommutator_preserved N H hH θ hθ g a b
92 
93 theorem pairing_alternating (N : Subgroup J) [N.Normal]
94     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
95     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ) (x : N ⧸ H) :
96     pairing N H hH θ hθ x x = 1 := CocycleCommutator.commutator_self _ x
97 
98 theorem pairing_mul_left (N : Subgroup J) [N.Normal]
99     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
100     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ)
101     (x y z : N ⧸ H) :
102     pairing N H hH θ hθ (x*y) z =
103       pairing N H hH θ hθ x z * pairing N H hH θ hθ y z :=
104   CocycleCommutator.commutator_mul_left _ x y z
105 
106 theorem pairing_mul_right (N : Subgroup J) [N.Normal]
107     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
108     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ)
109     (x y z : N ⧸ H) :
110     pairing N H hH θ hθ x (y*z) =
111       pairing N H hH θ hθ x y * pairing N H hH θ hθ x z :=
112   CocycleCommutator.commutator_mul_right _ x y z
113 
114 section FieldValued
115 variable {k X : Type*} [Field k] [AddCommGroup X] [Module k X]
116 
117 /-- Equality after a nontrivial additive character determines a bilinear form.
118 The character need not be injective: varying a scalar recovers every field value. -/
119 theorem bilinear_character_separates (B C : X →ₗ[k] X →ₗ[k] k)
120     (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
121     (h : ∀ x y, ψ (B x y) = ψ (C x y)) : B = C := by
122   ext x y
123   by_contra hn
124   have hd : B x y - C x y ≠ 0 := sub_ne_zero.mpr hn
125   obtain ⟨t,ht⟩ : ∃ t : k, ψ t ≠ 1 := by
126     by_contra hnone
127     apply hψ
128     apply AddChar.ext
129     intro t
130     exact not_not.mp (not_exists.mp hnone t)
131   let a := t / (B x y - C x y)
132   have hm : ψ (a * (B x y - C x y)) = 1 := by
133     rw [mul_sub, AddChar.map_sub_eq_div]
134     have hs := h (a • x) y
135     simpa only [map_smul, LinearMap.smul_apply, smul_eq_mul] using
136       (div_eq_one.mpr hs)
137   have he : a * (B x y - C x y) = t := div_mul_cancel₀ t hd
138   exact ht (he ▸ hm)
139 
140 /-- Scalar-pairing preservation plus the declared residue-field linearity
141 recovers preservation of the actual field-valued form. -/
142 theorem fieldForm_preserved (B : X →ₗ[k] X →ₗ[k] k) (L : X ≃ₗ[k] X)
143     (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
144     (h : ∀ x y, ψ (B (L x) (L y)) = ψ (B x y)) (x y : X) :
145     B (L x) (L y) = B x y := by
146   let C : X →ₗ[k] X →ₗ[k] k :=
147     { toFun x := (B (L x)).comp L.toLinearMap
148       map_add' x y := by ext z; simp
149       map_smul' a x := by ext z; simp }
150   have he : C = B := bilinear_character_separates C B ψ hψ h
151   exact LinearMap.congr_fun (LinearMap.congr_fun he x) y
152 
153 end FieldValued
154 end PaperXI.TypeNormalizerPairing

Back to source controls