SystemCompletion.lean

1 import PaperX.RepresentationForests
2 import PaperX.JointOccupancy
3 
4 /-! Conditional system realization. This constructs actual coefficient-indexed
5 matrix representations; it does not assume an unspecified realization map.
6 Every arithmetic admissibility condition beyond the finite congruence conditions
7 is an explicit separate implication. No universal companion or occupancy axiom. -/
8 set_option autoImplicit false
9 namespace PaperX.SystemCompletion
10 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationForests
11 variable {Λ G ι : Type} [Group G] [Fintype ι] [DecidableEq ι]
12 variable (O : Λ → Type) [∀ l, CommRing (O l)] (I : (l : Λ) → Ideal (O l))
13 variable (C : (l : Λ) → Conditions (G := G) (ι := ι) (I l))
14 
15 /-- A completed family of actual representations satisfies every selected finite
16 condition, rather than merely supplying a branch in an unrelated set tower. -/
17 def SystemRealizes (ρ : (l : Λ) → MatrixRep (O l) G ι) : Prop :=
18   ∀ l, Realizes (I l) (C l) (ρ l)
19 
20 theorem exists_system [∀ l, IsAdicComplete (I l) (O l)]
21     (finite : ∀ l k, Finite {ρ : MatrixRep (O l ⧸ (I l)^k) G ι // (C l).allowed k ρ})
22     (occupied : ∀ l k, ∃ ρ, (C l).allowed k ρ) :
23     ∃ ρ : (l : Λ) → MatrixRep (O l) G ι, SystemRealizes O I C ρ := by
24   classical
25   have H := fun l => exists_realization (I l) (C l) (finite l) (occupied l)
26   exact ⟨fun l => Classical.choose (H l), fun l => Classical.choose_spec (H l)⟩
27 
28 /-- Exact two-sided finite-level criterion for the congruence-defined system. -/
29 theorem system_realization_iff [∀ l, IsAdicComplete (I l) (O l)]
30     (finite : ∀ l k, Finite {ρ : MatrixRep (O l ⧸ (I l)^k) G ι // (C l).allowed k ρ}) :
31     (∃ ρ, SystemRealizes O I C ρ) ↔ ∀ l k, ∃ τ, (C l).allowed k τ := by
32   constructor
33   · rintro ⟨ρ,hρ⟩ l k
34     exact ⟨reduce (I l) (ρ l) k, hρ l k⟩
35   · exact exists_system O I C finite
36 
37 theorem system_empty_level_obstruction (l : Λ) (k : ℕ)
38     (h : ¬ ∃ τ, (C l).allowed k τ) : ¬ ∃ ρ, SystemRealizes O I C ρ := by
39   rintro ⟨ρ,hρ⟩
40   exact h ⟨reduce (I l) (ρ l) k, hρ l k⟩
41 
42 /-- Conditional completion together with a separately supplied fixed finite
43 carrier. Nonempty forests and positive carrier occupancy remain independent. -/
44 theorem completion_and_occupancy_iff [∀ l, IsAdicComplete (I l) (O l)]
45     (finite : ∀ l k, Finite {ρ : MatrixRep (O l ⧸ (I l)^k) G ι // (C l).allowed k ρ})
46     {K V J : Type*} [Field K] [CharZero K] [AddCommGroup V] [Module K V]
47     [FiniteDimensional K V]
48     (T : J → Module.End K V) (a : J → K) (indices : List J)
49     (hs : ∀ j, PaperX.SpectralProjectors.Split (T j))
50     (hc : ∀ i j, Commute (T i) (T j)) :
51     (∃ ρ, SystemRealizes O I C ρ ∧ PaperX.JointOccupancy.Occupied T a indices) ↔
52       (∀ l k, ∃ τ, (C l).allowed k τ) ∧
53         LinearMap.trace K V (PaperX.JointOccupancy.joint T a indices) ≠ 0 := by
54   rw [show (∃ ρ, SystemRealizes O I C ρ ∧ PaperX.JointOccupancy.Occupied T a indices) ↔
55       (∃ ρ, SystemRealizes O I C ρ) ∧ PaperX.JointOccupancy.Occupied T a indices from
56     ⟨fun ⟨ρ,hρ,ho⟩ => ⟨⟨ρ,hρ⟩,ho⟩, fun ⟨⟨ρ,hρ⟩,ho⟩ => ⟨ρ,hρ,ho⟩⟩]
57   rw [system_realization_iff O I C finite,
58     PaperX.JointOccupancy.occupied_iff_trace_ne_zero T a hs hc indices]
59 
60 variable [TopologicalSpace G]
61 
62 /-- Every local-property assertion below is an explicit hypothesis on the
63 realized congruence conditions. In particular, this does not prove p-adic Hodge
64 conditions are closed, or supply a compatible-system carrier. -/
65 theorem continuous_system_completion [∀ l, IsAdicComplete (I l) (O l)]
66     (finite : ∀ l k, Finite {ρ : MatrixRep (O l ⧸ (I l)^k) G ι // (C l).allowed k ρ})
67     (occupied : ∀ l k, ∃ ρ, (C l).allowed k ρ)
68     (continuous : ∀ l k ρ, (C l).allowed k ρ → FiniteRepContinuous ρ)
69     (Local : (l : Λ) → MatrixRep (O l) G ι → Prop)
70     (stable : ∀ l ρ, Realizes (I l) (C l) ρ → Local l ρ) :
71     ∃ ρ : (l : Λ) → MatrixRep (O l) G ι,
72       SystemRealizes O I C ρ ∧ ∀ l, AdicRepContinuous (I l) (ρ l) ∧ Local l (ρ l) := by
73   classical
74   have H := fun l => completion_with_local_condition (I l) (C l)
75     (finite l) (occupied l) (continuous l) (Local l) (stable l)
76   refine ⟨fun l => Classical.choose (H l), ?_, ?_⟩
77   · intro l
78     exact (Classical.choose_spec (H l)).1
79   · intro l
80     exact (Classical.choose_spec (H l)).2
81 
82 end PaperX.SystemCompletion

Back to source controls