SchrodingerIrreducible.lean

1 import PaperXI.SchrodingerFourier
2 import PaperXI.SchrodingerSeparation
3 import Mathlib.RepresentationTheory.Irreducible
4 
5 /-! Irreducibility of the finite Schrödinger action from its actual translation
6 and dual-character multiplication operators. The proof uses coordinate
7 projections and spans all functions, including the zero-dimensional case. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.SchrodingerIrreducible
11 
12 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X] [Fintype X]
13 
14 /-- Every subspace invariant under translations and all nontrivial scalar
15 character modulations is either zero or the full function space. -/
16 theorem invariant_eq_bot_or_top (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
17     (S : Submodule ℂ (X → ℂ))
18     (htranslation : ∀ x f, f ∈ S → (fun u => f (u + x)) ∈ S)
19     (hmodulation : ∀ (ξ : Module.Dual K X) f, f ∈ S →
20       (fun u => ψ (ξ u) * f u) ∈ S) : S = ⊥ ∨ S = ⊤ := by
21   classical
22   by_cases hbot : S = ⊥
23   · exact Or.inl hbot
24   right
25   obtain ⟨f, hf, hfne⟩ := S.ne_bot_iff.mp hbot
26   have hex : ∃ u : X, f u ≠ 0 := by
27     by_contra h
28     push Not at h
29     exact hfne (funext h)
30   obtain ⟨u, hu⟩ := hex
31   have hsep : ∀ u v : X, u ≠ v →
32       ∃ ξ : Module.Dual K X, ψ (ξ u) ≠ ψ (ξ v) :=
33     fun _ _ huv => SchrodingerSeparation.exists_dual_character_ne hψ huv
34   have hunit : (fun x => if x = u then (1 : ℂ) else 0) ∈ S :=
35     SchrodingerFourier.coordinate_unit_mem (fun (ξ : Module.Dual K X) x => ψ (ξ x)) hsep S
36       hmodulation u f hf hu
37   have hall : ∀ v : X, (fun x => if x = v then (1 : ℂ) else 0) ∈ S := by
38     intro v
39     have h := htranslation (u - v) _ hunit
40     convert h using 1
41     funext x
42     have heq : x + (u - v) = u ↔ x = v := by
43       constructor
44       · intro he
45         calc
46           x = (x + (u - v)) - u + v := by abel
47           _ = v := by rw [he]; abel
48       · rintro rfl
49         abel
50     simp only [heq]
51   apply top_unique
52   intro g _
53   rw [pi_eq_sum_univ g]
54   apply S.sum_mem
55   intro v _
56   apply S.smul_mem
57   simpa only [eq_comm] using hall v
58 
59 /-- Any actual representation containing every translation and dual modulation
60 is irreducible in Mathlib's subrepresentation sense. -/
61 theorem irreducible_of_actions {G : Type*} [Monoid G]
62     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (ρ : Representation ℂ G (X → ℂ))
63     (htranslation : ∀ x : X, ∃ g : G, ∀ (f : X → ℂ) (u : X),
64       ρ g f u = f (u + x))
65     (hmodulation : ∀ ξ : Module.Dual K X, ∃ g : G, ∀ (f : X → ℂ) (u : X),
66       ρ g f u = ψ (ξ u) * f u) : Representation.IsIrreducible ρ := by
67   change IsSimpleOrder (Subrepresentation ρ)
68   refine { exists_pair_ne := ?_, eq_bot_or_eq_top := ?_ }
69   · refine ⟨⊥, ⊤, fun h => ?_⟩
70     exact bot_ne_top (congrArg Subrepresentation.toSubmodule h)
71   · intro S
72     have ht : ∀ x f, f ∈ S.toSubmodule → (fun u => f (u + x)) ∈ S.toSubmodule := by
73       intro x f hf
74       obtain ⟨g, hg⟩ := htranslation x
75       have h := S.apply_mem_toSubmodule g hf
76       convert h using 1
77       exact (funext (hg f)).symm
78     have hm : ∀ (ξ : Module.Dual K X) f, f ∈ S.toSubmodule →
79         (fun u => ψ (ξ u) * f u) ∈ S.toSubmodule := by
80       intro ξ f hf
81       obtain ⟨g, hg⟩ := hmodulation ξ
82       have h := S.apply_mem_toSubmodule g hf
83       convert h using 1
84       exact (funext (hg f)).symm
85     rcases invariant_eq_bot_or_top ψ hψ S.toSubmodule ht hm with h | h
86     · exact Or.inl (Subrepresentation.toSubmodule_injective h)
87     · exact Or.inr (Subrepresentation.toSubmodule_injective h)
88 end PaperXI.SchrodingerIrreducible

Back to source controls