ReleasePrecisionQuotient.lean

1 import KomorebiVerification.PaperII.ReleaseGluing
2 
3 /-! The precision rule is an actual O-linear map between the stated quotients. -/
4 
5 set_option autoImplicit false
6 
7 namespace Komorebi.PaperII.ReleaseGluing
8 
9 universe u v
10 variable {O : Type u} {V : Type v}
11 variable [CommRing O] [AddCommGroup V] [Module O V]
12 
13 /-- The ambient scalar sublattice pi^n Λ. -/
14 def scaledLattice (Λ : Submodule O V) (pi : O) (n : ℕ) : Submodule O V :=
15   Λ.map ((pi ^ n) • LinearMap.id)
16 
17 /-- The same scalar sublattice, as a submodule of Λ. -/
18 def scaledInside (Λ : Submodule O V) (pi : O) (n : ℕ) : Submodule O Λ :=
19   (⊤ : Submodule O Λ).map ((pi ^ n) • LinearMap.id)
20 
21 def projectedReduction (Λ : Submodule O V) (pi : O) (m : ℕ)
22     (E : Module.End O V) : Λ →ₗ[O] V ⧸ scaledLattice Λ pi m :=
23   (scaledLattice Λ pi m).mkQ.comp (E.comp Λ.subtype)
24 
25 theorem precision_kernel_contains_input_lattice
26     (Λ : Submodule O V) (pi : O) (m s : ℕ) (E : Module.End O V)
27     (hclear : ∀ x : V, x ∈ Λ → (pi ^ s) • E x ∈ Λ) :
28     scaledInside Λ pi (m + s) ≤ LinearMap.ker (projectedReduction Λ pi m E) := by
29   intro x hx
30   obtain ⟨z, _hz, hzx⟩ := hx
31   change (pi ^ (m + s)) • z = x at hzx
32   change (scaledLattice Λ pi m).mkQ (E x) = 0
33   rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
34   refine ⟨(pi ^ s) • E z, hclear z z.property, ?_⟩
35   change (pi ^ m) • ((pi ^ s) • E z) = E x
36   rw [← hzx]
37   simp only [Submodule.coe_smul, map_smul, pow_add, mul_smul]
38 
39 /-- The printed map [x]_(m+s) ↦ [Ex]_m with target V/pi^mΛ, not Λ/pi^mΛ. -/
40 def precisionQuotientMap
41     (Λ : Submodule O V) (pi : O) (m s : ℕ) (E : Module.End O V)
42     (hclear : ∀ x : V, x ∈ Λ → (pi ^ s) • E x ∈ Λ) :
43     (Λ ⧸ scaledInside Λ pi (m + s)) →ₗ[O] V ⧸ scaledLattice Λ pi m :=
44   (scaledInside Λ pi (m + s)).liftQ (projectedReduction Λ pi m E)
45     (precision_kernel_contains_input_lattice Λ pi m s E hclear)
46 
47 theorem precisionQuotientMap_mk
48     (Λ : Submodule O V) (pi : O) (m s : ℕ) (E : Module.End O V)
49     (hclear : ∀ x : V, x ∈ Λ → (pi ^ s) • E x ∈ Λ) (x : Λ) :
50     precisionQuotientMap Λ pi m s E hclear ((scaledInside Λ pi (m + s)).mkQ x) =
51       (scaledLattice Λ pi m).mkQ (E x) := rfl
52 
53 end Komorebi.PaperII.ReleaseGluing

Back to source controls