TameDegree.lean

1 import PaperXI.TameTensorOrbits
2 import Mathlib.Algebra.Group.Subgroup.Ker
3 import Mathlib.Algebra.Group.TypeTags.Hom
4 
5 /-! Degree subgroups and their actual cyclic translation actions. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TameDegree
9 
10 variable {G : Type*} [Group G] (ν : G →* Multiplicative ℤ)
11 
12 /-- The integer degree of a group element. -/
13 def degree (g : G) : ℤ := (ν g).toAdd
14 
15 @[simp] theorem degree_one : degree ν 1 = 0 := by simp [degree]
16 
17 @[simp] theorem degree_mul (g h : G) : degree ν (g*h) = degree ν g + degree ν h := by
18   simp [degree]
19 
20 @[simp] theorem degree_zpow (g : G) (k : ℤ) : degree ν (g^k) = k * degree ν g := by
21   simp [degree, toAdd_zpow]
22 
23 @[simp] theorem degree_inv (g : G) : degree ν g⁻¹ = -degree ν g := by
24   simp [degree]
25 
26 @[simp] theorem degree_conjugate (a g : G) : degree ν (a*g*a⁻¹) = degree ν g := by
27   simp
28 
29 /-- Reduction of degree modulo `n`, in multiplicative notation for induction. -/
30 def degreeMod (n : ℕ) : G →* Multiplicative (ZMod n) where
31   toFun g := Multiplicative.ofAdd ((degree ν g : ℤ) : ZMod n)
32   map_one' := by simp
33   map_mul' g h := by simp [degree_mul, Int.cast_add]
34 
35 @[simp] theorem degreeMod_apply (n : ℕ) (g : G) :
36     degreeMod ν n g = Multiplicative.ofAdd ((degree ν g : ℤ) : ZMod n) := rfl
37 
38 /-- The subgroup of elements whose degree is divisible by `n`. -/
39 def degreeSubgroup (n : ℕ) : Subgroup G := (degreeMod ν n).ker
40 
41 @[simp] theorem mem_degreeSubgroup (n : ℕ) (g : G) :
42     g ∈ degreeSubgroup ν n ↔ (n : ℤ) ∣ degree ν g := by
43   change (((degree ν g : ℤ) : ZMod n) = 0) ↔ _
44   exact ZMod.intCast_zmod_eq_zero_iff_dvd _ _
45 
46 theorem degreeSubgroup_inter (n m : ℕ) :
47     degreeSubgroup ν n ⊓ degreeSubgroup ν m = degreeSubgroup ν (Nat.lcm n m) := by
48   ext g
49   simp only [Subgroup.mem_inf, mem_degreeSubgroup]
50   simpa using (Int.coe_lcm_dvd_iff (a := (n : ℤ)) (b := (m : ℤ))
51     (c := degree ν g)).symm
52 
53 /-- Divisibility of degrees gives the subgroup inclusions used to restrict characters. -/
54 theorem degreeSubgroup_le (n l : ℕ) (h : n ∣ l) :
55     degreeSubgroup ν l ≤ degreeSubgroup ν n := by
56   intro g hg
57   rw [mem_degreeSubgroup] at hg ⊢
58   exact (Int.natCast_dvd_natCast.mpr h).trans hg
59 
60 /-- The explicit conjugation map for a shifted character restricted from level `n` to `l`. -/
61 def conjugationInto (n l : ℕ) (h : n ∣ l) (a : G) :
62     degreeSubgroup ν l →* degreeSubgroup ν n where
63   toFun g := ⟨a*g.val*a⁻¹, by
64     rw [mem_degreeSubgroup, degree_conjugate]
65     exact (mem_degreeSubgroup ν n g.val).mp (degreeSubgroup_le ν n l h g.property)⟩
66   map_one' := by apply Subtype.ext; simp
67   map_mul' g k := by apply Subtype.ext; simp [mul_assoc]
68 
69 @[simp] theorem conjugationInto_apply (n l : ℕ) (h : n ∣ l) (a : G)
70     (g : degreeSubgroup ν l) : (conjugationInto ν n l h a g).val = a*g.val*a⁻¹ := rfl
71 
72 /-- Actual action on the quotient indices: addition of degree. -/
73 def translationAction (n : ℕ) : G →* Equiv.Perm (ZMod n) where
74   toFun g := Equiv.addRight ((degree ν g : ℤ) : ZMod n)
75   map_one' := by ext x; simp
76   map_mul' g h := by
77     ext x
78     change x + ((degree ν (g*h) : ℤ) : ZMod n) =
79       (x + ((degree ν h : ℤ) : ZMod n)) + ((degree ν g : ℤ) : ZMod n)
80     rw [degree_mul, Int.cast_add]
81     abel
82 
83 @[simp] theorem translationAction_apply (n : ℕ) (g : G) (x : ZMod n) :
84     translationAction ν n g x = x + ((degree ν g : ℤ) : ZMod n) := rfl
85 
86 theorem translationAction_fixed_iff (n : ℕ) (g : G) (x : ZMod n) :
87     translationAction ν n g x = x ↔ g ∈ degreeSubgroup ν n := by
88   rw [translationAction_apply, add_eq_left, mem_degreeSubgroup]
89   exact ZMod.intCast_zmod_eq_zero_iff_dvd _ _
90 
91 /-- The product action on the two factors. -/
92 def pairAction (n m : ℕ) : G →* Equiv.Perm (ZMod n × ZMod m) where
93   toFun g := (translationAction ν n g).prodCongr (translationAction ν m g)
94   map_one' := by ext x <;> simp
95   map_mul' g h := by
96     ext x <;> simp [Equiv.Perm.mul_apply, add_comm, add_left_comm]
97 
98 @[simp] theorem pairAction_apply (n m : ℕ) (g : G) (x : ZMod n × ZMod m) :
99     pairAction ν n m g x = TameTensorOrbits.translate n m (degree ν g) x := rfl
100 
101 /-- The stabilizer of each actual pair-index is the degree-lcm subgroup. -/
102 theorem pairAction_fixed_iff (n m : ℕ) (g : G) (x : ZMod n × ZMod m) :
103     pairAction ν n m g x = x ↔ g ∈ degreeSubgroup ν (Nat.lcm n m) := by
104   rw [pairAction_apply, TameTensorOrbits.translate_eq_iff, mem_degreeSubgroup]
105 
106 /-- The block-index is fixed and the lcm-cycle coordinate is translated. -/
107 def blockAction (n m : ℕ) : G →* Equiv.Perm (Fin (Nat.gcd n m) × ZMod (Nat.lcm n m)) where
108   toFun g := (Equiv.refl _).prodCongr (translationAction ν (Nat.lcm n m) g)
109   map_one' := by ext x <;> simp
110   map_mul' g h := by
111     ext x <;> simp [Equiv.Perm.mul_apply, add_comm, add_left_comm]
112 
113 @[simp] theorem blockAction_apply (n m : ℕ) (g : G)
114     (x : Fin (Nat.gcd n m) × ZMod (Nat.lcm n m)) :
115     blockAction ν n m g x = (x.1, x.2 + ((degree ν g : ℤ) : ZMod (Nat.lcm n m))) := rfl
116 
117 theorem orbitMap_intertwines (n m : ℕ) (g : G)
118     (x : Fin (Nat.gcd n m) × ZMod (Nat.lcm n m)) :
119     TameTensorOrbits.orbitMap n m (blockAction ν n m g x) =
120       pairAction ν n m g (TameTensorOrbits.orbitMap n m x) :=
121   TameTensorOrbits.orbitMap_translate_int n m x.1 x.2 (degree ν g)
122 
123 theorem orbitEquiv_intertwines (n m : ℕ) [NeZero n] [NeZero m] (g : G)
124     (x : Fin (Nat.gcd n m) × ZMod (Nat.lcm n m)) :
125     TameTensorOrbits.orbitEquiv n m (blockAction ν n m g x) =
126       pairAction ν n m g (TameTensorOrbits.orbitEquiv n m x) :=
127   orbitMap_intertwines ν n m g x
128 
129 variable (φ : G) (hφ : ν φ = Multiplicative.ofAdd (1 : ℤ))
130 
131 include hφ in
132 theorem degree_phi : degree ν φ = 1 := by simp [degree, hφ]
133 
134 include hφ in
135 theorem degree_phi_zpow (k : ℤ) : degree ν (φ^k) = k := by
136   rw [degree_zpow, degree_phi ν φ hφ, mul_one]
137 
138 include hφ in
139 theorem degreeMod_phi_zpow (n : ℕ) (k : ℤ) :
140     degreeMod ν n (φ^k) = Multiplicative.ofAdd (k : ZMod n) := by
141   rw [degreeMod_apply, degree_phi_zpow ν φ hφ]
142 
143 include hφ in
144 theorem degreeMod_surjective (n : ℕ) : Function.Surjective (degreeMod ν n) := by
145   intro q
146   obtain ⟨k,hk⟩ := ZMod.intCast_surjective q.toAdd
147   refine ⟨φ^k, ?_⟩
148   rw [degreeMod_phi_zpow ν φ hφ, hk]
149   rfl
150 
151 include hφ in
152 theorem translationAction_phi_zpow (n : ℕ) (k : ℤ) (x : ZMod n) :
153     translationAction ν n (φ^k) x = x + (k : ZMod n) := by
154   rw [translationAction_apply, degree_phi_zpow ν φ hφ]
155 
156 include hφ in
157 theorem pairAction_phi_zpow (n m : ℕ) (k : ℤ) (x : ZMod n × ZMod m) :
158     pairAction ν n m (φ^k) x = TameTensorOrbits.translate n m k x := by
159   rw [pairAction_apply, degree_phi_zpow ν φ hφ]
160 
161 include hφ in
162 /-- The powers of the degree-one element act transitively inside each actual gcd fiber. -/
163 theorem fiber_transitive (n m : ℕ) [NeZero n] [NeZero m]
164     (x y : ZMod n × ZMod m) (h : TameTensorOrbits.difference n m x =
165       TameTensorOrbits.difference n m y) :
166     ∃ k : ℤ, pairAction ν n m (φ^k) x = y := by
167   obtain ⟨k,hk⟩ := (TameTensorOrbits.sameOrbit_iff n m x y).mpr h
168   exact ⟨k, (pairAction_phi_zpow ν φ hφ n m k x).trans hk⟩
169 
170 end PaperXI.TameDegree

Back to source controls