WeakCoverageBoundary.lean

1 import PaperX.IrreducibleCharacterRigidity
2 import Mathlib.Data.ZMod.Basic
3 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
4 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
5 import Mathlib.NumberTheory.Cyclotomic.Basic
6 
7 /-! A generating sample that meets every rational power-conjugacy class need
8 not separate all absolutely irreducible characters over their splitting field.
9 The finite group is C3 and the samples are its identity and one generator. -/
10 set_option autoImplicit false
11 noncomputable section
12 
13 namespace PaperX.WeakCoverageBoundary
14 
15 abbrev C3 := Multiplicative (ZMod 3)
16 def generator : C3 := Multiplicative.ofAdd 1
17 def sample (j : Fin 2) : C3 := if j = 0 then 1 else generator
18 
19 theorem rational_power_coverage :
20     ∀ g : C3, ∃ j : Fin 2, ∃ k : Fin 3,
21       Nat.Coprime k.val 3 ∧ g = sample j ^ k.val := by
22   decide +kernel
23 
24 theorem generator_squared_missed :
25     ∀ j : Fin 2, sample j ≠ generator ^ 2 := by
26   decide +kernel
27 
28 theorem sample_generates : Subgroup.closure (Set.range sample) = ⊤ := by
29   apply top_unique
30   intro g _
31   obtain ⟨j, k, _, rfl⟩ := rational_power_coverage g
32   exact (Subgroup.closure (Set.range sample)).pow_mem
33     (Subgroup.subset_closure (Set.mem_range_self j)) k.val
34 
35 /-- Both sampled classes recur at arbitrarily many distinct indices. -/
36 def recurringSample (p : ℕ × Fin 2) : C3 := sample p.2
37 
38 theorem cofinite_rational_power_coverage (bad : Finset (ℕ × Fin 2)) (g : C3) :
39     ∃ p : ℕ × Fin 2, p ∉ bad ∧ ∃ k : Fin 3,
40       Nat.Coprime k.val 3 ∧ g = recurringSample p ^ k.val := by
41   obtain ⟨j, k, hk, hg⟩ := rational_power_coverage g
42   refine ⟨(bad.sup Prod.fst + 1, j), ?_, k, hk, hg⟩
43   intro hp
44   have hh := Finset.le_sup (f := Prod.fst) hp
45   omega
46 
47 variable {E : Type*} [Field E] (ζ : E) (hζ : IsPrimitiveRoot ζ 3)
48 
49 /-- Actual scalar-valued characters on the finite cyclic group. -/
50 def scalarCharacter (i : Fin 3) : C3 →* E where
51   toFun g := ζ ^ (i.val * g.toAdd.val)
52   map_one' := by simp
53   map_mul' g h := by
54     change ζ ^ (i.val * ((g.toAdd + h.toAdd).val)) = _
55     rw [ZMod.val_add]
56     calc
57       ζ ^ (i.val * ((g.toAdd.val + h.toAdd.val) % 3)) =
58           (ζ ^ i.val) ^ ((g.toAdd.val + h.toAdd.val) % 3) := by rw [pow_mul]
59       _ = (ζ ^ i.val) ^ (g.toAdd.val + h.toAdd.val) := by
60         symm
61         apply pow_eq_pow_mod
62         rw [← pow_mul, Nat.mul_comm, pow_mul, hζ.pow_eq_one, one_pow]
63       _ = ζ ^ (i.val * g.toAdd.val) * ζ ^ (i.val * h.toAdd.val) := by
64         rw [pow_add, ← pow_mul, ← pow_mul]
65 
66 /-- The actual one-dimensional representations whose traces are the characters. -/
67 def scalarRepresentation (i : Fin 3) : Representation E C3 E :=
68   (algebraMap E (Module.End E E)).toMonoidHom.comp (scalarCharacter ζ hζ i)
69 
70 theorem scalarRepresentation_irreducible (i : Fin 3) :
71     (scalarRepresentation ζ hζ i).IsIrreducible := by
72   change IsSimpleOrder (Subrepresentation (scalarRepresentation ζ hζ i))
73   refine { exists_pair_ne := ?_, eq_bot_or_eq_top := ?_ }
74   · refine ⟨⊥, ⊤, ?_⟩
75     intro h
76     have hh := congrArg Subrepresentation.toSubmodule h
77     exact bot_ne_top hh
78   · intro W
79     rcases eq_bot_or_eq_top W.toSubmodule with h | h
80     · exact Or.inl (Subrepresentation.toSubmodule_injective h)
81     · exact Or.inr (Subrepresentation.toSubmodule_injective h)
82 
83 theorem character_scalarRepresentation (i : Fin 3) (g : C3) :
84     Representation.character (scalarRepresentation ζ hζ i) g =
85       scalarCharacter ζ hζ i g := by
86   simp [Representation.character, scalarRepresentation, Algebra.algebraMap_eq_smul_one]
87 
88 theorem generator_character (i : Fin 3) :
89     Representation.character (scalarRepresentation ζ hζ i) generator = ζ ^ i.val := by
90   rw [character_scalarRepresentation]
91   norm_num [scalarCharacter, generator, ZMod.val_one_eq_one_mod]
92 
93 theorem pairwise_nonisomorphic (i j : Fin 3) (hij : i ≠ j) :
94     ¬ Nonempty (Representation.Equiv
95       (scalarRepresentation ζ hζ i) (scalarRepresentation ζ hζ j)) := by
96   intro he
97   have hc := PaperX.IrreducibleCharacterRigidity.character_eq_of_equiv
98     (scalarRepresentation ζ hζ i) (scalarRepresentation ζ hζ j) he
99   have hg := congrFun hc generator
100   rw [generator_character, generator_character] at hg
101   exact hij (Fin.ext (hζ.pow_inj i.isLt j.isLt hg))
102 
103 /-- A nonzero coefficient vector annihilating all sampled trace rows. -/
104 def annihilator : Fin 3 → E := ![ζ ^ 2 - ζ, 1 - ζ ^ 2, ζ - 1]
105 
106 include hζ in
107 theorem annihilator_nonzero : annihilator ζ ≠ 0 := by
108   intro h
109   have hh := congrFun h 2
110   simp [annihilator] at hh
111   exact hζ.ne_one (by decide) (sub_eq_zero.mp hh)
112 
113 theorem sampled_character_relation (j : Fin 2) :
114     ∑ i : Fin 3, annihilator ζ i *
115       Representation.character (scalarRepresentation ζ hζ i) (sample j) = 0 := by
116   fin_cases j
117   · simp [sample, annihilator, Fin.sum_univ_succ]
118   · simp [sample, character_scalarRepresentation, scalarCharacter, generator,
119       annihilator, Fin.sum_univ_succ, ZMod.val_one_eq_one_mod]
120     ring
121 
122 theorem recurring_character_relation (p : ℕ × Fin 2) :
123     ∑ i : Fin 3, annihilator ζ i *
124       Representation.character (scalarRepresentation ζ hζ i) (recurringSample p) = 0 :=
125   sampled_character_relation ζ hζ p.2
126 
127 theorem every_sample_matrix_singular (p : Fin 3 → ℕ × Fin 2) :
128     Matrix.det (fun j i : Fin 3 =>
129       Representation.character (scalarRepresentation ζ hζ i) (recurringSample (p j))) = 0 := by
130   have hn : ¬ Function.Injective (fun j : Fin 3 => (p j).2) := by
131     intro hi
132     have hh := Fintype.card_le_of_injective _ hi
133     norm_num at hh
134   obtain ⟨i, j, hij, hne⟩ := Function.not_injective_iff.mp hn
135   apply Matrix.det_zero_of_row_eq hne
136   simp only [recurringSample, hij]
137 
138 /-- An actual number-field realization of the primitive-root hypothesis. -/
139 abbrev CoefficientField := CyclotomicField 3 ℚ
140 
141 theorem coefficient_root_exists : ∃ z : CoefficientField, IsPrimitiveRoot z 3 := by
142   let : Algebra ℚ CoefficientField := CyclotomicField.algebra 3 ℚ
143   exact IsCyclotomicExtension.exists_isPrimitiveRoot ℚ CoefficientField
144     (by simp : 3 ∈ ({3} : Set ℕ)) (by decide)
145 
146 def coefficientRoot : CoefficientField := coefficient_root_exists.choose
147 
148 theorem coefficientRoot_primitive : IsPrimitiveRoot coefficientRoot 3 :=
149   coefficient_root_exists.choose_spec
150 
151 /-- Three inequivalent irreducible representations over a number field, with
152 no invertible three-row trace matrix drawn from the recurring sample. -/
153 theorem actual_number_field_boundary :
154     (∀ i : Fin 3,
155       (scalarRepresentation coefficientRoot coefficientRoot_primitive i).IsIrreducible) ∧
156     (∀ i j : Fin 3, i ≠ j → ¬ Nonempty (Representation.Equiv
157       (scalarRepresentation coefficientRoot coefficientRoot_primitive i)
158       (scalarRepresentation coefficientRoot coefficientRoot_primitive j))) ∧
159     (∀ p : Fin 3 → ℕ × Fin 2, Matrix.det (fun j i : Fin 3 =>
160       Representation.character
161         (scalarRepresentation coefficientRoot coefficientRoot_primitive i)
162         (recurringSample (p j))) = 0) := by
163   exact ⟨scalarRepresentation_irreducible _ _, pairwise_nonisomorphic _ _,
164     every_sample_matrix_singular _ _⟩
165 
166 end PaperX.WeakCoverageBoundary

Back to source controls