CompatibleSystemRigidity.lean

1 import PaperX.IrreducibleCharacterRigidity
2 import PaperX.CofiniteConjugacyCoverage
3 
4 /-! Isomorphism at one coefficient prime reflects componentwise isomorphism
5 of compatible irreducible systems. Comparisons use each pair's good-place
6 overlap. Arithmetic Frobenius density is still an explicit input. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.CompatibleSystemRigidity
10 open PaperX.IrreducibleCharacterRigidity
11 
12 variable {Λ I G X E : Type*} [Group G] [Field E] [TopologicalSpace G]
13 variable {K : Λ → Type*} [∀ l, Field (K l)] [∀ l, CharZero (K l)]
14   [∀ l, TopologicalSpace (K l)] [∀ l, T2Space (K l)]
15 variable {W : Λ → I → Type*} [∀ l i, AddCommGroup (W l i)]
16   [∀ l i, Module (K l) (W l i)] [∀ l i, FiniteDimensional (K l) (W l i)]
17 variable (ρ : (l : Λ) → (i : I) → Representation (K l) G (W l i))
18 variable [∀ l i, (ρ l i).IsIrreducible]
19 variable (hc : ∀ l i, Continuous (ρ l i).character)
20 variable (emb : (l : Λ) → E →+* K l) (t : I → X → E)
21 variable (good : Λ → X → Prop) (s : X → G)
22 variable (compat : ∀ l i x, good l x → (ρ l i).character (s x) = emb l (t i x))
23 variable (overlap : ∀ l m, DenseRange
24   (fun p : {x : X // good l x ∧ good m x} × G => p.2 * s p.1 * p.2⁻¹))
25 
26 /-- Equivalence of systems means actual representation equivalence at every
27 coefficient index, not equality of optional labels or record fields. -/
28 def MemberwiseEquiv (i j : I) : Prop := ∀ l, Nonempty ((ρ l i).Equiv (ρ l j))
29 
30 omit [TopologicalSpace G] [∀ l, TopologicalSpace (K l)] [∀ l, CharZero (K l)] [∀ l, T2Space (K l)]
31   [∀ l i, FiniteDimensional (K l) (W l i)] [∀ l i, (ρ l i).IsIrreducible] in
32 include compat in
33 /-- An isomorphism reflects common algebraic trace equality at all places good
34 for that member, because the coefficient-field embedding is injective. -/
35 theorem common_trace_eq_of_member_equiv (l : Λ) (i j : I)
36     (h : Nonempty ((ρ l i).Equiv (ρ l j))) (x : X) (hx : good l x) :
37     t i x = t j x := by
38   apply (emb l).injective
39   rw [← compat l i x hx, ← compat l j x hx]
40   exact congrFun (character_eq_of_equiv (ρ l i) (ρ l j) h) (s x)
41 
42 include hc compat overlap in
43 /-- Common trace agreement on one member's good set propagates to actual
44 isomorphisms at every member, using the appropriate good-place overlaps. -/
45 theorem memberwiseEquiv_of_common_traces (l₀ : Λ) (i j : I)
46     (ht : ∀ x, good l₀ x → t i x = t j x) : MemberwiseEquiv ρ i j := by
47   intro l
48   apply equiv_of_dense_character_eq (ρ l i) (ρ l j) (hc l i) (hc l j)
49     (fun x : {x : X // good l₀ x ∧ good l x} => s x) (overlap l₀ l)
50   intro x
51   rw [compat l i x x.property.2, compat l j x x.property.2,
52     ht x x.property.1]
53 
54 include hc compat overlap in
55 /-- The previously missing system-to-member bridge, at the exact componentwise
56 notion of equivalence and with overlap density explicitly retained. -/
57 theorem memberwiseEquiv_of_member (l₀ : Λ) (i j : I)
58     (h : Nonempty ((ρ l₀ i).Equiv (ρ l₀ j))) : MemberwiseEquiv ρ i j := by
59   apply memberwiseEquiv_of_common_traces ρ hc emb t good s compat overlap l₀ i j
60   exact common_trace_eq_of_member_equiv ρ emb t good s compat l₀ i j h
61 
62 include hc compat overlap in
63 theorem memberwiseEquiv_iff_member (l₀ : Λ) (i j : I) :
64     MemberwiseEquiv ρ i j ↔ Nonempty ((ρ l₀ i).Equiv (ρ l₀ j)) :=
65   ⟨fun h => h l₀, memberwiseEquiv_of_member ρ hc emb t good s compat overlap l₀ i j⟩
66 
67 include hc compat overlap in
68 /-- Pairwise nonisomorphic systems give pairwise nonisomorphic representations
69 at any selected coefficient prime. This is derived rather than assumed twice. -/
70 theorem nonisomorphic_members (hne : ∀ i j, MemberwiseEquiv ρ i j → i = j)
71     (l₀ : Λ) : ∀ i j, Nonempty ((ρ l₀ i).Equiv (ρ l₀ j)) → i = j := by
72   intro i j h
73   exact hne i j (memberwiseEquiv_of_member ρ hc emb t good s compat overlap l₀ i j h)
74 
75 end PaperX.CompatibleSystemRigidity

Back to source controls