SchrodingerSeparation.lean

1 import Mathlib.LinearAlgebra.Dual.Lemmas
2 import Mathlib.Algebra.Group.AddChar
3 import Mathlib.Basic.Complex.Basic
4 
5 /-! A nontrivial scalar additive character, composed with the full linear dual,
6 separates points of a vector space. No finiteness assumption is required. -/
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperXI.SchrodingerSeparation
11 
12 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
13 
14 /-- The modulation characters distinguish any two distinct points. -/
15 theorem exists_dual_character_ne {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
16     {u v : X} (huv : u ≠ v) :
17     ∃ ξ : Module.Dual K X, ψ (ξ u) ≠ ψ (ξ v) := by
18   obtain ⟨a, ha⟩ := AddChar.ne_one_iff.mp hψ
19   obtain ⟨ℓ, hℓ⟩ := Module.Projective.exists_dual_eq_one K (sub_ne_zero.mpr huv)
20   let ξ : Module.Dual K X := a • ℓ
21   have hξ : ξ (u - v) = a := by
22     simp only [ξ, LinearMap.smul_apply, hℓ, smul_eq_mul, mul_one]
23   refine ⟨ξ, ?_⟩
24   intro h
25   apply ha
26   calc
27     ψ a = ψ (ξ (u - v)) := congrArg ψ hξ.symm
28     _ = ψ (ξ u) * ψ (-ξ v) := by rw [map_sub, sub_eq_add_neg, AddChar.map_add_eq_mul]
29     _ = ψ (ξ v) * ψ (-ξ v) := by rw [h]
30     _ = 1 := by rw [← AddChar.map_add_eq_mul, add_neg_cancel, AddChar.map_zero_eq_one]
31 
32 end PaperXI.SchrodingerSeparation

Back to source controls