CompatibleSystemSeparation.lean

1 import PaperX.CompatibleSystemRigidity
2 import PaperX.TraceRecovery
3 
4 /-! The common algebraic separator for pairwise nonisomorphic compatible systems.
5 The system-to-member bridge is derived. Cofinite arithmetic coverage remains
6 explicit; selected-place comparisons retain each coefficient prime's good set. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.CompatibleSystemSeparation
10 open PaperX.CompatibleSystemRigidity PaperX.CofiniteConjugacyCoverage
11 open PaperX.FiniteSeparation PaperX.TraceRecovery
12 
13 variable {Λ I G X E : Type*} [Group G] [Field E] [TopologicalSpace G]
14   [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
15   [Fintype I] [DecidableEq I]
16 variable {K : Λ → Type*} [∀ l, Field (K l)] [∀ l, CharZero (K l)]
17   [∀ l, TopologicalSpace (K l)] [∀ l, IsTopologicalRing (K l)] [∀ l, T2Space (K l)]
18 variable {W : Λ → I → Type*} [∀ l i, AddCommGroup (W l i)]
19   [∀ l i, Module (K l) (W l i)] [∀ l i, FiniteDimensional (K l) (W l i)]
20 variable (ρ : (l : Λ) → (i : I) → Representation (K l) G (W l i))
21 variable [∀ l i, (ρ l i).IsIrreducible]
22 variable (hc : ∀ l i, Continuous (ρ l i).character)
23 variable (emb : (l : Λ) → E →+* K l) (t : I → X → E)
24 variable (good : Λ → X → Prop) (hgood : ∀ l, Set.Finite {x | ¬ good l x})
25 variable (s : X → G) (coverage : CofiniteQuotientCoverage s)
26 variable (compat : ∀ l i x, good l x → (ρ l i).character (s x) = emb l (t i x))
27 variable (hne : ∀ i j, MemberwiseEquiv ρ i j → i = j)
28 
29 include hc hgood coverage compat hne in
30 /-- Distinct common-algebraic trace samples can avoid any prescribed finite set.
31 The matrix remains nonsingular at every embedding. Its entries agree with actual
32 member traces only at the places good for that coefficient prime. -/
33 theorem finite_system_separator (l₀ : Λ) (bad : Finset X) :
34     ∃ v : I → X, Function.Injective v ∧
35       (∀ i, good l₀ (v i)) ∧ (∀ i, v i ∉ bad) ∧
36       (sampleMatrix t v).det ≠ 0 ∧
37       (∀ l, ((emb l).mapMatrix (sampleMatrix t v)).det ≠ 0) ∧
38       ∀ l j i, good l (v j) →
39         (emb l).mapMatrix (sampleMatrix t v) j i = (ρ l i).character (s (v j)) := by
40   classical
41   have hov : ∀ l m, DenseRange
42       (fun p : {x : X // good l x ∧ good m x} × G => p.2 * s p.1 * p.2⁻¹) := by
43     intro l m
44     apply dense_on_cofinite s coverage
45     apply ((hgood l).union (hgood m)).subset
46     intro x hx
47     simpa only [Set.mem_union, Set.mem_ofPred_eq, not_and_or] using hx
48   have hni := nonisomorphic_members ρ hc emb t good s compat hov hne l₀
49   have hi := PaperX.GeneralCharacters.independent_irreducible_characters (ρ l₀) hni
50   have hd : DenseRange
51       (fun p : {x : X // good l₀ x ∧ x ∉ bad} × G => p.2 * s p.1 * p.2⁻¹) := by
52     apply dense_on_cofinite s coverage
53     apply ((hgood l₀).union bad.finite_toSet).subset
54     intro x hx
55     by_cases hg : good l₀ x
56     · exact Or.inr (by simpa only [Finset.mem_coe, Set.mem_ofPred_eq, hg, true_and, not_not] using hx)
57     · exact Or.inl hg
58   obtain ⟨v, hv, hdet⟩ := common_trace_separator (emb l₀)
59     (fun i (x : {x : X // good l₀ x ∧ x ∉ bad}) => t i x)
60     (fun i => (ρ l₀ i).character) (hc l₀) hi
61     (fun x : {x : X // good l₀ x ∧ x ∉ bad} => s x) hd
62     (fun i g x => (ρ l₀ i).char_conj (s x) g)
63     (fun i x => (compat l₀ i x x.property.1).symm)
64   refine ⟨fun i => (v i).val, Subtype.val_injective.comp hv,
65     fun i => (v i).property.1, fun i => (v i).property.2, hdet, ?_, ?_⟩
66   · intro l
67     exact (determinant_transport (emb l) _).mpr hdet
68   · intro l j i hj
69     exact (compat l i (v j) hj).symm
70 
71 end PaperX.CompatibleSystemSeparation

Back to source controls