LocalFactorIdentification.lean

1 import PaperXI.AtomicReconstruction
2 import PaperXI.CharacterProjector
3 
4 /-! Explicit realization and factor-characterization interfaces for the last
5 arithmetic step. Realizers need not be unique. Their isomorphism class becomes
6 unique by equality on a genuinely characterizing test family. No reference
7 comparison map or final equality is stored in either input interface. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.LocalFactorIdentification
11 
12 /-- All normalization choices and the admissible comparison range must be part
13 of the concrete instantiation. `separates` is the external local converse input. -/
14 structure FactorSystem {Atom : Type*} (s : Setoid Atom) (Test Value : Type*) where
15   admissible : Atom → Prop
16   profile : Atom → Test → Value
17   invariant : ∀ a b, s.r a b → profile a = profile b
18   separates : ∀ a b, admissible a → admissible b → profile a = profile b → s.r a b
19 
20 variable {Atom Test Value D : Type*} {s : Setoid Atom}
21 variable (S : FactorSystem s Test Value)
22 
23 /-- Existence of an atom realizing a finite datum is a distinct arithmetic input.
24 Neither uniqueness nor agreement with a reference atom is assumed here. -/
25 structure Realization (D : Type*) where
26   realizes : D → Atom → Prop
27   exists_atom : ∀ d, ∃ a, realizes d a
28   admissible : ∀ d a, realizes d a → S.admissible a
29 
30 variable (R : Realization S D)
31 
32 def chosenAtom (d : D) : Atom := Classical.choose (R.exists_atom d)
33 
34 theorem chosenAtom_realizes (d : D) : R.realizes d (chosenAtom S R d) :=
35   Classical.choose_spec (R.exists_atom d)
36 
37 def candidate (d : D) : Quotient s := Quotient.mk s (chosenAtom S R d)
38 
39 /-- Matching factors characterize equality of isomorphism classes on the declared range. -/
40 theorem class_eq_iff {a b : Atom} (ha : S.admissible a) (hb : S.admissible b) :
41     Quotient.mk s a = Quotient.mk s b ↔ S.profile a = S.profile b := by
42   constructor
43   · intro h
44     exact S.invariant a b (Quotient.exact h)
45   · intro h
46     exact Quotient.sound (S.separates a b ha hb h)
47 
48 /-- The reference map and factor identity enter here, not in the finite construction. -/
49 theorem candidate_eq_reference (d : D) (reference : Atom)
50     (hr : S.admissible reference) (expected : Test → Value)
51     (hreal : ∀ a, R.realizes d a → S.profile a = expected)
52     (href : S.profile reference = expected) :
53     candidate S R d = Quotient.mk s reference := by
54   apply (class_eq_iff S (R.admissible d _ (chosenAtom_realizes S R d)) hr).mpr
55   exact (hreal _ (chosenAtom_realizes S R d)).trans href.symm
56 
57 /-- A stronger non-vacuous statement: all realized atoms belong to one class.
58 Existence comes from Realization; separation is used only for uniqueness. -/
59 theorem unique_realized_class (d : D) (expected : Test → Value)
60     (hreal : ∀ a, R.realizes d a → S.profile a = expected) :
61     ∃! c : Quotient s, ∃ a, R.realizes d a ∧ Quotient.mk s a = c := by
62   refine ⟨candidate S R d, ⟨chosenAtom S R d, chosenAtom_realizes S R d, rfl⟩, ?_⟩
63   rintro c ⟨a, ha, rfl⟩
64   apply (class_eq_iff S (R.admissible d a ha)
65     (R.admissible d _ (chosenAtom_realizes S R d))).mpr
66   exact (hreal a ha).trans (hreal _ (chosenAtom_realizes S R d)).symm
67 
68 /-- Two realization mechanisms give the same class when the tested factor
69 profile agrees; finite data alone are not a uniqueness theorem. -/
70 theorem realization_independence (R' : Realization S D) (d : D)
71     (expected : Test → Value)
72     (h : ∀ a, R.realizes d a → S.profile a = expected)
73     (h' : ∀ a, R'.realizes d a → S.profile a = expected) :
74     candidate S R d = candidate S R' d := by
75   apply candidate_eq_reference S R d (chosenAtom S R' d)
76     (R'.admissible d _ (chosenAtom_realizes S R' d)) expected h
77   exact h' _ (chosenAtom_realizes S R' d)
78 
79 /-- Pointwise equality of factor profiles on raw data makes the candidate descend
80 through any declared source equivalence relation. -/
81 theorem candidate_congr {d e : D} (expected : D → Test → Value)
82     (hreal : ∀ d a, R.realizes d a → S.profile a = expected d)
83     (h : expected d = expected e) : candidate S R d = candidate S R e := by
84   apply (class_eq_iff S (R.admissible d _ (chosenAtom_realizes S R d))
85     (R.admissible e _ (chosenAtom_realizes S R e))).mpr
86   exact (hreal d _ (chosenAtom_realizes S R d)).trans
87     (h.trans (hreal e _ (chosenAtom_realizes S R e)).symm)
88 
89 def onClasses (sD : Setoid D) (expected : D → Test → Value)
90     (hreal : ∀ d a, R.realizes d a → S.profile a = expected d)
91     (hinv : ∀ d e, sD.r d e → expected d = expected e) : Quotient sD → Quotient s :=
92   Quotient.lift (candidate S R) (fun d e h => candidate_congr S R expected hreal (hinv d e h))
93 
94 /-- The factor comparison need only be proved for the actual constructed datum. -/
95 theorem constructed_comparison {Input : Type*} (build : Input → D) (x : Input)
96     (reference : Input → Atom) (hr : S.admissible (reference x))
97     (expected : Input → Test → Value)
98     (hreal : ∀ a, R.realizes (build x) a → S.profile a = expected x)
99     (href : S.profile (reference x) = expected x) :
100     candidate S R (build x) = Quotient.mk s (reference x) :=
101   candidate_eq_reference S R (build x) (reference x) hr (expected x) hreal href
102 
103 /-- Conditional atomic agreement propagates through the already constructed
104 monodromy/multiset reconstruction. This is equality of candidates, not bijectivity. -/
105 theorem reconstructed_comparison {P A B Target : Type*} {sP : Setoid P}
106     (f g : A → B) (D0 : AtomicReconstruction.Decomposition sP A)
107     (L : AtomicReconstruction.OrderedQuotient B Target) (h : ∀ a, f a = g a) :
108     AtomicReconstruction.candidate f D0 L = AtomicReconstruction.candidate g D0 L := by
109   have he : f = g := funext h
110   rw [he]
111 
112 section FiniteCharacterInstance
113 variable {G V : Type*} [Group G] [Fintype G]
114 variable [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
115 
116 /-- A concrete isomorphism relation, not an arbitrary stand-in for a representation. -/
117 def representationSetoid : Setoid (Representation ℂ G V) where
118   r ρ σ := Nonempty (Representation.Equiv ρ σ)
119   iseqv := ⟨fun ρ => ⟨Representation.Equiv.refl ρ⟩,
120     fun ⟨e⟩ => ⟨e.symm⟩, fun ⟨e⟩ ⟨f⟩ => ⟨e.trans f⟩⟩
121 
122 /-- All actual finite-group character values separate irreducibles. This gives a
123 concrete instance of the interface; it is NOT a local-Weil converse theorem. -/
124 theorem finite_character_separates (ρ σ : Representation ℂ G V)
125     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
126     (h : ρ.character = σ.character) : Nonempty (Representation.Equiv ρ σ) := by
127   classical
128   by_contra hn
129   let := CharacterProjector.nontrivial_space σ
130   have he : CharacterProjector.element ρ = CharacterProjector.element σ := by
131     simp only [CharacterProjector.element, h]
132   have hz := CharacterProjector.irreducible_action ρ σ
133   have hi := CharacterProjector.irreducible_action σ σ
134   have hself : Nonempty (Representation.Equiv σ σ) := ⟨Representation.Equiv.refl σ⟩
135   simp only [ite_eq_right hn] at hz
136   simp only [ite_eq_left hself] at hi
137   rw [he, hi] at hz
138   exact one_ne_zero hz
139 
140 def finiteCharacterSystem : FactorSystem (representationSetoid (G := G) (V := V)) G ℂ where
141   admissible ρ := Representation.IsIrreducible ρ
142   profile ρ := ρ.character
143   invariant ρ σ h := by obtain ⟨e⟩ := h; exact Representation.char_iso e
144   separates ρ σ hρ hσ h := by
145     let := hρ
146     let := hσ
147     exact finite_character_separates ρ σ h
148 
149 end FiniteCharacterInstance
150 end PaperXI.LocalFactorIdentification

Back to source controls