ReleaseSmithCharacters.lean

1 import KomorebiVerification.PaperII.ResidueFourierCRT
2 import KomorebiVerification.PaperII.ResultantSeparation
3 
4 /-! Integral character averages preserve actual scalar submodules. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace Komorebi.PaperII.IntegralCharacters
8 universe u v w
9 variable {O : Type u} [CommRing O]
10 variable {K : Type v} [Field K] [Algebra O K]
11 variable {V : Type w} [AddCommGroup V] [Module K V] [Module O V]
12 variable [IsScalarTower O K V]
13 
14 omit [Algebra O K] [IsScalarTower O K V] in
15 /-- Stability under one linear map implies stability under every actual operator power. -/
16 theorem power_preserves (L : Submodule O V) (U : Module.End K V)
17     (hU : ∀ x ∈ L, U x ∈ L) (k : Nat) : ∀ x ∈ L, (U ^ k) x ∈ L := by
18   induction k with
19   | zero => simp
20   | succ k ih =>
21       intro x hx
22       rw [pow_succ', Module.End.mul_apply]
23       exact hU _ (ih x hx)
24 
25 /-- Actual field-valued operator character average. -/
26 def characterAverage (N : Nat) (omega : O) (U : Module.End K V) (j : Nat) :
27     Module.End K V :=
28   (N : K)⁻¹ • ∑ k : Fin N,
29     ((algebraMap O K omega)⁻¹ ^ (j * k.val)) • (U ^ k.val)
30 
31 /-- Away from the group order, the field average is an integral linear combination of
32 powers, so it preserves every U-stable O-submodule, in particular every lattice. -/
33 theorem characterAverage_preserves (L : Submodule O V)
34     (N : Nat) (hN : 0 < N) (hunit : IsUnit (N : O))
35     (omega : O) (homega : IsPrimitiveRoot omega N)
36     (U : Module.End K V) (hU : ∀ x ∈ L, U x ∈ L) (j : Nat) :
37     ∀ x ∈ L, characterAverage N omega U j x ∈ L := by
38   obtain ⟨nunit, hnunit⟩ := hunit
39   obtain ⟨wunit, hwunit⟩ := homega.isUnit (Nat.ne_of_gt hN)
40   have hn : (N : K)⁻¹ = algebraMap O K (↑nunit⁻¹ : O) := by
41     rw [map_units_inv, hnunit, map_natCast]
42   have hw : (algebraMap O K omega)⁻¹ = algebraMap O K (↑wunit⁻¹ : O) := by
43     rw [map_units_inv, hwunit]
44   intro x hx
45   simp only [characterAverage, LinearMap.smul_apply, LinearMap.sum_apply]
46   rw [hn, algebraMap_smul]
47   apply L.smul_mem
48   apply L.sum_mem
49   intro k _
50   rw [hw, ← map_pow, algebraMap_smul]
51   exact L.smul_mem _ (power_preserves L U hU k.val x hx)
52 
53 /-- The manuscript situation U^N=I is a specialization; no spectral conclusion is
54 assumed to prove integrality. -/
55 theorem manuscript_character_integrality (L : Submodule O V)
56     (N : Nat) (hN : 0 < N) (hunit : IsUnit (N : O))
57     (omega : O) (homega : IsPrimitiveRoot omega N)
58     (U : Module.End K V) (_horder : U ^ N = 1)
59     (hU : ∀ x ∈ L, U x ∈ L) (j : Nat) :
60     ∀ x ∈ L, characterAverage N omega U j x ∈ L :=
61   characterAverage_preserves L N hN hunit omega homega U hU j
62 
63 end Komorebi.PaperII.IntegralCharacters
64 #print axioms Komorebi.PaperII.IntegralCharacters.characterAverage_preserves

Back to source controls