ReleaseGluingDVR.lean

1 import KomorebiVerification.PaperII.ReleaseGluing
2 import Mathlib.Algebra.Module.Lattice
3 import Mathlib.RingTheory.DiscreteValuationRing.Basic
4 import Mathlib.RingTheory.Localization.Integer
5 
6 /-!
7 # DVR lattices supply the finite clearing exponents
8 
9 The full-lattice hypotheses are Mathlib's finite-generation and spanning
10 conditions.  Finite denominators are constructed from an actual extended
11 lattice basis and the fraction-ring localization theorem.  A DVR
12 uniformizer factorization then replaces the nonzero scalar denominator by
13 a power of pi.  Thus no clearing-existence conclusion is assumed.
14 -/
15 
16 set_option autoImplicit false
17 open scoped BigOperators nonZeroDivisors
18 
19 namespace Komorebi.PaperII.ReleaseGluing
20 
21 universe u v w
22 variable {O : Type u} {K : Type v} {V : Type w}
23 variable [CommRing O] [IsDomain O] [Field K] [Algebra O K] [IsFractionRing O K]
24 variable [AddCommGroup V] [Module O V] [Module K V] [IsScalarTower O K V]
25 
26 theorem endomorphism_has_nonzero_integral_multiple
27     {ι : Type*} [Fintype ι] (Λ : Submodule O V) [Submodule.IsLattice K Λ]
28     (b : Module.Basis ι O Λ) (E : Module.End K V) :
29     ∃ r : O, r ≠ 0 ∧ ∀ x : V, x ∈ Λ → r • E x ∈ Λ := by
30   classical
31   let B := b.extendOfIsLattice K
32   obtain ⟨r, hr⟩ := IsLocalization.exist_integer_multiples_of_finite O⁰
33     (fun ij : ι × ι => B.repr (E (b ij.1)) ij.2)
34   have hb : ∀ j : ι, (r : O) • E (b j) ∈ Λ := by
35     intro j
36     rw [← B.sum_repr (E (b j)), Finset.smul_sum]
37     apply Λ.sum_mem
38     intro i _hi
39     obtain ⟨c, hc⟩ := hr (j, i)
40     rw [← smul_assoc, ← hc]
41     simpa only [B, Module.Basis.extendOfIsLattice_apply, algebraMap_smul] using
42       Λ.smul_mem c (b i).property
43   refine ⟨r, nonZeroDivisors.coe_ne_zero r, ?_⟩
44   intro x hx
45   have hxsum : (∑ i, b.repr (⟨x, hx⟩ : Λ) i • (b i : V)) = x := by
46     simpa only [Submodule.coe_sum, Submodule.coe_smul] using
47       congrArg (fun y : Λ => (y : V)) (b.sum_repr ⟨x, hx⟩)
48   rw [← hxsum, map_sum, Finset.smul_sum]
49   apply Λ.sum_mem
50   intro i _hi
51   rw [E.map_smul_of_tower]
52   rw [smul_comm]
53   exact Λ.smul_mem _ (hb i)
54 
55 theorem endomorphism_has_uniformizer_clearing_exponent
56     [IsDiscreteValuationRing O]
57     {ι : Type*} [Fintype ι] (Λ : Submodule O V) [Submodule.IsLattice K Λ]
58     (b : Module.Basis ι O Λ) (pi : O) (hpi : Irreducible pi)
59     (E : Module.End K V) :
60     ∃ s : ℕ, ∀ x : V, x ∈ Λ → (pi ^ s) • E x ∈ Λ := by
61   obtain ⟨r, hr, hclear⟩ := endomorphism_has_nonzero_integral_multiple Λ b E
62   obtain ⟨s, u, hu⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hr hpi
63   refine ⟨s, ?_⟩
64   intro x hx
65   have h := Λ.smul_mem (↑u⁻¹ : O) (hclear x hx)
66   rw [hu, ← mul_smul, ← mul_assoc] at h
67   simpa only [Units.inv_mul, one_mul] using h
68 
69 /-- A known integral clearing scalar gives the exact normalized-valuation bound.
70 The conclusion uses its valuation, not an unspecified existential exponent. -/
71 theorem uniformizer_valuation_clears_of_scalar_clears
72     [IsDiscreteValuationRing O]
73     (Λ : Submodule O V) (pi : O) (hpi : Irreducible pi)
74     (r : O) (hr : r ≠ 0) (E : V → V)
75     (hclear : ∀ x : V, x ∈ Λ → r • E x ∈ Λ) :
76     ∀ x : V, x ∈ Λ →
77       (pi ^ (IsDiscreteValuationRing.addVal O r).toNat) • E x ∈ Λ := by
78   obtain ⟨s, u, hu⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hr hpi
79   have hv : IsDiscreteValuationRing.addVal O r = (s : ℕ∞) :=
80     IsDiscreteValuationRing.addVal_def r u hpi s hu
81   intro x hx
82   rw [hv, ENat.toNat_natCast]
83   have h := Λ.smul_mem (↑u⁻¹ : O) (hclear x hx)
84   rw [hu, ← mul_smul, ← mul_assoc] at h
85   simpa only [Units.inv_mul, one_mul] using h
86 
87 variable {I : Type*} [Fintype I]
88 
89 /-- Restricting a rational projector family to O changes neither the operators nor their ranges. -/
90 def Projectors.restrictScalars (P : Projectors K V I) : Projectors O V I where
91   proj i := (P.proj i).restrictScalars O
92   idem i := by
93     ext x
94     exact proj_idem P i x
95   orthogonal i j hij := by
96     ext x
97     exact proj_other P i j hij x
98   complete := by
99     ext x
100     simpa only [LinearMap.sum_apply, LinearMap.restrictScalars_apply, Module.End.one_apply]
101       using reconstruct P x
102 
103 theorem full_lattice_packet_clearing_exists
104     [IsDiscreteValuationRing O]
105     {ι : Type*} [Fintype ι] (Λ : Submodule O V) [Submodule.IsLattice K Λ]
106     (b : Module.Basis ι O Λ) (pi : O) (hpi : Irreducible pi)
107     (P : Projectors K V I) :
108     ∀ i, ∃ s, ClearsPacket (P.restrictScalars (O := O)) Λ pi i s := by
109   intro i
110   exact endomorphism_has_uniformizer_clearing_exponent Λ b pi hpi (P.proj i)
111 
112 /-- Exact gluing exponent for a full DVR lattice and rational packet decomposition.
113 All least exponents here exist by the preceding denominator construction. -/
114 theorem dvr_gluing_exponent_eq_globalWeight
115     [IsDiscreteValuationRing O]
116     {ι : Type*} [Fintype ι] (Λ : Submodule O V) [Submodule.IsLattice K Λ]
117     (b : Module.Basis ι O Λ) (pi : O) (hpi : Irreducible pi)
118     (P : Projectors K V I) :
119     let finite := full_lattice_packet_clearing_exists Λ b pi hpi P
120     gluingExponent (P.restrictScalars (O := O)) Λ pi finite =
121       globalWeight (P.restrictScalars (O := O)) Λ pi finite := by
122   exact gluing_exponent_eq_globalWeight _ _ _ _
123 
124 end Komorebi.PaperII.ReleaseGluing

Back to source controls