TypeNormalizerForm.lean

1 import PaperXI.TypeNormalizerPairing
2 
3 /-! The source-facing field-valued form: the ambient quotient action is
4 transported to the declared vector-space coordinates, then preservation is
5 proved from the actual character commutator. Residue-field linearity is explicit. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TypeNormalizerForm
9 open TypeNormalizerAction TypeNormalizerPairing
10 open scoped IsMulCommutative
11 
12 variable {J k X : Type*} [Group J] [Field k] [AddCommGroup X] [Module k X]
13 
14 /-- The genuine quotient action in the supplied vector-space coordinates. -/
15 def coordinateAction (N : Subgroup J) [N.Normal] (H : Subgroup N)
16     [H.Normal] [IsMulCommutative (N ⧸ H)] (hH : Stable N H)
17     (e : (N ⧸ H) ≃* Multiplicative X) : (J ⧸ N) →* MulAut (Multiplicative X) where
18   toFun j := (e.symm.trans (quotientAction N H hH j)).trans e
19   map_one' := by
20     ext x
21     simp [MulEquiv.trans_apply]
22   map_mul' a b := by
23     ext x
24     simp [MulEquiv.trans_apply]
25 
26 @[simp] theorem coordinateAction_apply (N : Subgroup J) [N.Normal]
27     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)] (hH : Stable N H)
28     (e : (N ⧸ H) ≃* Multiplicative X) (j : J ⧸ N) (x : Multiplicative X) :
29     coordinateAction N H hH e j x = e (quotientAction N H hH j (e.symm x)) := rfl
30 
31 /-- Scalar compatibility upgrades the actual additive automorphism to a linear
32 one; it does not assume form preservation. -/
33 def linearAut (a : MulAut (Multiplicative X))
34     (hs : ∀ c : k, ∀ x : X, (a (Multiplicative.ofAdd (c • x))).toAdd =
35       c • (a (Multiplicative.ofAdd x)).toAdd) : X ≃ₗ[k] X where
36   toFun x := (a (Multiplicative.ofAdd x)).toAdd
37   invFun x := (a.symm (Multiplicative.ofAdd x)).toAdd
38   left_inv x := congrArg Multiplicative.toAdd (a.symm_apply_apply (Multiplicative.ofAdd x))
39   right_inv x := congrArg Multiplicative.toAdd (a.apply_symm_apply (Multiplicative.ofAdd x))
40   map_add' x y := congrArg Multiplicative.toAdd (a.map_mul (Multiplicative.ofAdd x) (Multiplicative.ofAdd y))
41   map_smul' c x := hs c x
42 
43 /-- The action on the actual source vector space. -/
44 def vectorAction (N : Subgroup J) [N.Normal] (H : Subgroup N)
45     [H.Normal] [IsMulCommutative (N ⧸ H)] (hH : Stable N H)
46     (e : (N ⧸ H) ≃* Multiplicative X)
47     (hs : ∀ j : J ⧸ N, ∀ c : k, ∀ x : X,
48       (coordinateAction N H hH e j (Multiplicative.ofAdd (c • x))).toAdd =
49         c • (coordinateAction N H hH e j (Multiplicative.ofAdd x)).toAdd) :
50     (J ⧸ N) →* (X ≃ₗ[k] X) where
51   toFun j := linearAut (coordinateAction N H hH e j) (hs j)
52   map_one' := by
53     ext x
54     change (coordinateAction N H hH e 1 (Multiplicative.ofAdd x)).toAdd = x
55     rw [map_one]
56     rfl
57   map_mul' a b := by
58     ext x
59     change (coordinateAction N H hH e (a*b) (Multiplicative.ofAdd x)).toAdd =
60       (coordinateAction N H hH e a (coordinateAction N H hH e b (Multiplicative.ofAdd x))).toAdd
61     rw [map_mul]
62     rfl
63 
64 /-- Corrected source 10.3: an honest quotient action preserves the given
65 field-valued form. The nontrivial character may have a nontrivial kernel. -/
66 theorem source_form_preserved (N : Subgroup J) [N.Normal]
67     (H : Subgroup N) [H.Normal] [IsMulCommutative (N ⧸ H)]
68     (hH : Stable N H) (θ : H →* ℂˣ) (hθ : CharacterInvariant N H hH θ)
69     (e : (N ⧸ H) ≃* Multiplicative X)
70     (hs : ∀ j : J ⧸ N, ∀ c : k, ∀ x : X,
71       (coordinateAction N H hH e j (Multiplicative.ofAdd (c • x))).toAdd =
72         c • (coordinateAction N H hH e j (Multiplicative.ofAdd x)).toAdd)
73     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
74     (hsource : ∀ a b, ψ (B (e a).toAdd (e b).toAdd) = pairing N H hH θ hθ a b)
75     (j : J ⧸ N) (x y : X) :
76     B (vectorAction N H hH e hs j x) (vectorAction N H hH e hs j y) = B x y := by
77   apply fieldForm_preserved B (vectorAction N H hH e hs j) ψ hψ
78   intro u v
79   let a := e.symm (Multiplicative.ofAdd u)
80   let b := e.symm (Multiplicative.ofAdd v)
81   have hp := (hsource (quotientAction N H hH j a) (quotientAction N H hH j b)).trans
82     ((quotientAction_preserves_pairing N H hH θ hθ j a b).trans (hsource a b).symm)
83   simpa [vectorAction, linearAut, coordinateAction, a, b] using hp
84 
85 end PaperXI.TypeNormalizerForm

Back to source controls