DualCharacterSums.lean

1 import PaperXI.SchrodingerTrace
2 import PaperXI.SchrodingerSeparation
3 import PaperXI.HeisenbergDimension
4 
5 /-! Literal finite character orthogonality on a vector space and its full dual. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.DualCharacters
9 open scoped Classical
10 
11 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
12 
13 /-- Orthogonality over points, including the trivial functional. -/
14 theorem sum_over_points [Fintype X] {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
15     (ξ : Module.Dual K X) :
16     (∑ a : X, ψ (ξ a)) = if ξ = 0 then (Fintype.card X : ℂ) else 0 := by
17   by_cases hξ : ξ = 0
18   · simp [hξ]
19   · simp [hξ, SchrodingerTrace.sum_functional_character hψ hξ]
20 
21 /-- Evaluation at a point as an additive character of the full dual. -/
22 def evaluationCharacter (ψ : AddChar K ℂ) (a : X) : AddChar (Module.Dual K X) ℂ :=
23   ψ.compAddMonoidHom
24     { toFun := fun ξ => ξ a
25       map_zero' := by simp
26       map_add' := by intros; simp }
27 
28 @[simp] theorem evaluationCharacter_apply (ψ : AddChar K ℂ) (a : X)
29     (ξ : Module.Dual K X) : evaluationCharacter ψ a ξ = ψ (ξ a) := rfl
30 
31 theorem evaluationCharacter_ne_one {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
32     {a : X} (ha : a ≠ 0) : evaluationCharacter ψ a ≠ 1 := by
33   obtain ⟨ξ, hξ⟩ := SchrodingerSeparation.exists_dual_character_ne hψ ha
34   intro h
35   apply hξ
36   have hh := congrArg (fun χ : AddChar (Module.Dual K X) ℂ => χ ξ) h
37   simpa using hh
38 
39 /-- Orthogonality over the actual full linear dual. -/
40 theorem sum_over_dual [Fintype (Module.Dual K X)] {ψ : AddChar K ℂ}
41     (hψ : ψ ≠ 1) (a : X) :
42     (∑ ξ : Module.Dual K X, ψ (ξ a)) =
43       if a = 0 then (Fintype.card (Module.Dual K X) : ℂ) else 0 := by
44   by_cases ha : a = 0
45   · simp [ha]
46   · simpa [ha] using
47       AddChar.sum_eq_zero_of_ne_one (evaluationCharacter_ne_one hψ ha)
48 
49 /-- Cardinalities agree without any assumption on the complex target space. -/
50 theorem card_dual [FiniteDimensional K X] [Fintype X]
51     [Fintype (Module.Dual K X)] : Fintype.card (Module.Dual K X) = Fintype.card X := by
52   simpa only [Nat.card_eq_fintype_card] using
53     HeisenbergDimension.natCard_dual (K := K) (X := X)
54 
55 end PaperXI.DualCharacters

Back to source controls