ReleaseGluingPrecisionBridge.lean

1 import KomorebiVerification.PaperII.ReleaseGluingDVR
2 import KomorebiVerification.PaperII.ReleasePrecision
3 
4 set_option autoImplicit false
5 
6 namespace Komorebi.PaperII.ReleaseGluing
7 
8 universe u v w
9 variable {O : Type u} {K : Type v} {V : Type w}
10 variable [CommRing O] [Field K] [Algebra O K]
11 variable [AddCommGroup V] [Module O V] [Module K V] [IsScalarTower O K V]
12 variable {I : Type*} [Fintype I]
13 
14 /-- The O-submodule clearing condition is the original additive-lattice condition after scalar restriction. -/
15 theorem clearsPacket_iff_original
16     (P : Projectors K V I) (Λ : Submodule O V) (pi : O) (i : I) (s : ℕ) :
17     ClearsPacket (P.restrictScalars (O := O)) Λ pi i s ↔
18       ResultantSeparation.IsSeparationWeight (algebraMap O K pi) (P.proj i)
19         Λ.toAddSubgroup s := by
20   simp only [ClearsPacket, Projectors.restrictScalars,
21     ResultantSeparation.IsSeparationWeight, ResultantSeparation.PreservesLattice,
22     LinearMap.smul_apply, LinearMap.restrictScalars_apply,
23     ← map_pow, algebraMap_smul, Submodule.mem_toAddSubgroup]
24 
25 theorem original_finite_of_packet_finite
26     (P : Projectors K V I) (Λ : Submodule O V) (pi : O) (i : I)
27     (finite : ∃ s, ClearsPacket (P.restrictScalars (O := O)) Λ pi i s) :
28     ResultantSeparation.HasFiniteSeparationWeight (algebraMap O K pi)
29       (P.proj i) Λ.toAddSubgroup := by
30   obtain ⟨s, hs⟩ := finite
31   exact ⟨s, (clearsPacket_iff_original P Λ pi i s).mp hs⟩
32 
33 /-- The new quotient theorem uses precisely the pre-existing least separation weight. -/
34 theorem packetWeight_eq_original_separationWeight
35     (P : Projectors K V I) (Λ : Submodule O V) (pi : O) (i : I)
36     (finite : ∃ s, ClearsPacket (P.restrictScalars (O := O)) Λ pi i s) :
37     packetWeight (P.restrictScalars (O := O)) Λ pi i finite =
38       ResultantSeparation.separationWeight
39         (original_finite_of_packet_finite P Λ pi i finite) := by
40   classical
41   unfold packetWeight ResultantSeparation.separationWeight
42   exact Nat.find_congr' (clearsPacket_iff_original P Λ pi i _)
43 
44 variable [IsDomain O] [IsFractionRing O K]
45 
46 omit [IsDomain O] in
47 /-- The exact least delay for the actual O-lattice is the actual packet weight. -/
48 theorem uniformPrecisionDelay_iff_packetWeight_le
49     (P : Projectors K V I) (Λ : Submodule O V) (pi : O) (hpi : pi ≠ 0) (i : I)
50     (finite : ∃ s, ClearsPacket (P.restrictScalars (O := O)) Λ pi i s) (d : ℕ) :
51     ResultantSeparation.UniformPrecisionDelay (algebraMap O K pi) (P.proj i)
52       Λ.toAddSubgroup d ↔ packetWeight (P.restrictScalars (O := O)) Λ pi i finite ≤ d := by
53   rw [packetWeight_eq_original_separationWeight]
54   apply ResultantSeparation.uniformPrecisionDelay_iff_separationWeight_le
55   · exact (map_ne_zero_iff (algebraMap O K) (IsFractionRing.injective O K)).mpr hpi
56   · intro x hx
57     change (algebraMap O K pi) • x ∈ Λ
58     simpa only [algebraMap_smul] using Λ.smul_mem pi hx
59 
60 omit [IsFractionRing O K] in
61 
62 
63 /-- DVR valuation normalization expressed in the original separation API. -/
64 theorem original_clearing_weight_at_valuation
65     [IsDiscreteValuationRing O]
66     (Λ : Submodule O V) (pi : O) (hpi : Irreducible pi)
67     (r : O) (hr : r ≠ 0) (E : Module.End K V)
68     (hclear : ∀ x : V, x ∈ Λ → r • E x ∈ Λ) :
69     ResultantSeparation.IsSeparationWeight (algebraMap O K pi) E Λ.toAddSubgroup
70       (IsDiscreteValuationRing.addVal O r).toNat := by
71   intro x hx
72   change ((algebraMap O K pi) ^ (IsDiscreteValuationRing.addVal O r).toNat) • E x ∈ Λ
73   rw [← map_pow, algebraMap_smul]
74   exact uniformizer_valuation_clears_of_scalar_clears Λ pi hpi r hr E hclear x hx
75 
76 omit [IsFractionRing O K] in
77 theorem original_finite_of_scalar_clears
78     [IsDiscreteValuationRing O]
79     (Λ : Submodule O V) (pi : O) (hpi : Irreducible pi)
80     (r : O) (hr : r ≠ 0) (E : Module.End K V)
81     (hclear : ∀ x : V, x ∈ Λ → r • E x ∈ Λ) :
82     ResultantSeparation.HasFiniteSeparationWeight (algebraMap O K pi) E Λ.toAddSubgroup :=
83   ⟨_, original_clearing_weight_at_valuation Λ pi hpi r hr E hclear⟩
84 
85 omit [IsFractionRing O K] in
86 /-- In particular, setting r to the actual polynomial resultant gives cor:resultant_bound. -/
87 theorem original_separationWeight_le_valuation
88     [IsDiscreteValuationRing O]
89     (Λ : Submodule O V) (pi : O) (hpi : Irreducible pi)
90     (r : O) (hr : r ≠ 0) (E : Module.End K V)
91     (hclear : ∀ x : V, x ∈ Λ → r • E x ∈ Λ) :
92     ResultantSeparation.separationWeight
93       (original_finite_of_scalar_clears Λ pi hpi r hr E hclear) ≤
94         (IsDiscreteValuationRing.addVal O r).toNat :=
95   ResultantSeparation.separationWeight_le_of_clears _
96     (original_clearing_weight_at_valuation Λ pi hpi r hr E hclear)
97 
98 end Komorebi.PaperII.ReleaseGluing

Back to source controls