MatrixSpanCompletion.lean

1 import PaperX.SplitTemplateRigidity
2 import PaperX.ComparisonCertificates
3 
4 /-! A fixed full-span rational representation type is preserved by completion
5 from integral finite-condition approximants. Existence of those approximants
6 is explicit; arbitrary torsion representations are not assumed to lift. -/
7 set_option autoImplicit false
8 namespace PaperX.MatrixSpanCompletion
9 open PaperX.RepresentationLimits PaperX.RepresentationForests
10 open PaperX.RepresentationClasses PaperX.ComparisonCertificates
11 variable {R G ι K : Type} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
12   [Group G] [Fintype ι] [DecidableEq ι] [Field K] [Algebra R K] [IsFractionRing R K]
13 variable (π : R) (hπ : Irreducible π)
14 variable (C : Conditions (G := G) (ι := ι) (Ideal.span {π}))
15 variable (τ : MatrixRep R G ι)
16 
17 /-- Ordinary finite-condition approximation in the field-isomorphism class.
18 Each precision may use a different integral representation and comparison. -/
19 def Approximation : Prop := ∀ k, ∃ ρ : MatrixRep R G ι,
20     Conjugate (changeCoefficients (algebraMap R K) τ)
21       (changeCoefficients (algebraMap R K) ρ) ∧
22     C.allowed k (reduce (Ideal.span {π}) ρ k)
23 
24 include hπ
25 
26 /-- The fixed bound derived from the template produces augmented finite nodes
27 without any assumed uniform determinant certificate. -/
28 theorem certificate_levels_from_approximation
29     (hspan : Submodule.span K
30       (Set.range (fun g => (τ g).map (algebraMap R K))) = ⊤)
31     (occupied : Approximation (K := K) π C τ) :
32     ∃ c : ℕ, ∀ k, Nonempty (Node (Ideal.span {π}) C
33       (fun _ : Unit => MonoidHom.id G) (fun _ : Unit => τ)
34       (fun _ : Unit => c * Fintype.card ι + 1) k) := by
35   obtain ⟨c, hc⟩ := MatrixSpanBound.uniform_detector_for_conjugates (K := K) τ π hπ hspan
36   refine ⟨c, fun k => ?_⟩
37   obtain ⟨ρ, hρ, ha⟩ := occupied k
38   obtain ⟨P, hP, hd⟩ := hc ρ hρ
39   refine ⟨{ rep := reduce (Ideal.span {π}) ρ k
40             allowed := ha
41             comparison := fun _ => P.map (Ideal.Quotient.mk ((Ideal.span {π})^k))
42             intertwines := ?_
43             detected := ?_ }⟩
44   · intro s g
45     change (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^k)) *
46       P.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
47       P.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) *
48       (τ g).map (Ideal.Quotient.mk ((Ideal.span {π})^k))
49     simpa only [Matrix.map_mul] using
50       congrArg (fun A => A.map (Ideal.Quotient.mk ((Ideal.span {π})^k))) (hP g)
51   · intro s hs
52     change Ideal.Quotient.factorPow (Ideal.span {π}) hs
53       ((Ideal.Quotient.mk ((Ideal.span {π})^k)).mapMatrix P).det ≠ 0
54     rw [← RingHom.map_det, Ideal.Quotient.factor_mk]
55     change ((Ideal.Quotient.mk ((Ideal.span {π}) ^ (c * Fintype.card ι + 1))).mapMatrix P).det ≠ 0 at hd
56     rw [← RingHom.map_det] at hd
57     exact hd
58 
59 /-- Completion preserves this actual rational isomorphism type. The proof
60 constructs finite witnesses with the uniform bound and invokes the existing
61 simultaneous certificate theorem. -/
62 theorem full_span_completion [IsAdicComplete (Ideal.span {π}) R]
63     (hspan : Submodule.span K
64       (Set.range (fun g => (τ g).map (algebraMap R K))) = ⊤)
65     (finiteR : ∀ k, Finite (R ⧸ (Ideal.span {π})^k))
66     (finiteC : ∀ k, Finite {ρ : MatrixRep (R ⧸ (Ideal.span {π})^k) G ι // C.allowed k ρ})
67     (occupied : Approximation (K := K) π C τ) :
68     ∃ ρ : MatrixRep R G ι, Realizes (Ideal.span {π}) C ρ ∧
69       Conjugate (changeCoefficients (algebraMap R K) τ)
70         (changeCoefficients (algebraMap R K) ρ) := by
71   obtain ⟨c, hc⟩ := certificate_levels_from_approximation π hπ C τ hspan occupied
72   obtain ⟨ρ, P, hρ, hP, hd⟩ := exists_comparison_realization (Ideal.span {π}) C
73     (fun _ : Unit => MonoidHom.id G) (fun _ : Unit => τ)
74     (fun _ : Unit => c * Fintype.card ι + 1) finiteR finiteC hc
75   refine ⟨ρ, hρ, ?_⟩
76   apply PaperX.CertificateIsomorphisms.conjugate_of_finite_certificate (Ideal.span {π})
77     (algebraMap R K) (IsFractionRing.injective R K) ρ τ (P ())
78     (c * Fintype.card ι + 1)
79   · change ((Ideal.Quotient.mk ((Ideal.span {π}) ^ (c * Fintype.card ι + 1))).mapMatrix (P ())).det ≠ 0
80     rw [← RingHom.map_det]
81     exact hd ()
82   · exact hP ()
83 
84 end PaperX.MatrixSpanCompletion

Back to source controls