ReleaseGluingFinite.lean

1 import KomorebiVerification.PaperII.ReleaseGluingDVR
2 import KomorebiVerification.PaperII.ReleaseGluingSmith
3 
4 /-!
5 # Finiteness of the genuine gluing module
6 
7 The split submodule is proved to be a full lattice.  A finite uniform
8 clearing exponent also makes the actual gluing quotient finite length;
9 no finiteness of the residue field is required.
10 -/
11 
12 set_option autoImplicit false
13 open scoped BigOperators
14 
15 namespace Komorebi.PaperII.ReleaseGluing
16 
17 universe u v w
18 variable {O : Type u} {K : Type v} {V : Type w}
19 variable [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
20 variable [Field K] [Algebra O K] [IsFractionRing O K]
21 variable [AddCommGroup V] [Module O V] [Module K V] [IsScalarTower O K V]
22 variable {I : Type*} [Fintype I]
23 
24 /-- The actual finite sum of packet intersections is a full lattice. -/
25 theorem splitLattice_isLattice
26     {ι : Type*} [Fintype ι] (Λ : Submodule O V) [Submodule.IsLattice K Λ]
27     (b : Module.Basis ι O Λ) (pi : O) (hpi : Irreducible pi)
28     (P : Projectors K V I) :
29     Submodule.IsLattice K (splitLattice (P.restrictScalars (O := O)) Λ) := by
30   let Q := P.restrictScalars (O := O)
31   let finite := full_lattice_packet_clearing_exists Λ b pi hpi P
32   obtain ⟨s, hs⟩ := gluing_finite_exponent Q Λ pi finite
33   have hclear := (annihilates_gluing_iff Q Λ (pi ^ s)).mp hs
34   refine ⟨?_, ?_⟩
35   · have : IsNoetherian O (splitLattice Q Λ) :=
36       isNoetherian_of_le (splitLattice_le Q Λ)
37     rw [← Module.Finite.iff_fg]
38     infer_instance
39   · apply eq_top_iff.mpr
40     rw [← Submodule.IsLattice.span_eq_top (A := K) (M := Λ)]
41     apply Submodule.span_le.mpr
42     intro x hx
43     have hmem : (pi ^ s) • x ∈ Submodule.span K (splitLattice Q Λ : Set V) :=
44       Submodule.subset_span (hclear x hx)
45     have hn : algebraMap O K (pi ^ s) ≠ 0 :=
46       (map_ne_zero_iff (algebraMap O K) (IsFractionRing.injective O K)).mpr
47         (pow_ne_zero s hpi.ne_zero)
48     have hinv := (Submodule.span K (splitLattice Q Λ : Set V)).smul_mem
49       ((algebraMap O K (pi ^ s))⁻¹) hmem
50     rw [← algebraMap_smul K (pi ^ s) x, smul_smul, inv_mul_cancel₀ hn, one_smul] at hinv
51     exact hinv
52 
53 /-- A finite basis and a uniform annihilator give finite length of an actual quotient. -/
54 theorem finiteLength_quotient_of_power_annihilates
55     {W : Type*} [AddCommGroup W] [Module O W]
56     {ι : Type*} [Fintype ι] [DecidableEq ι]
57     (S : Submodule O W) (b : Module.Basis ι O W)
58     (pi : O) (hpi : Irreducible pi) (s : ℕ)
59     (hann : ∀ z : W ⧸ S, (pi ^ s) • z = 0) :
60     IsFiniteLength O (W ⧸ S) := by
61   let f := smithCoordinateMap b pi (fun _ => s)
62   have hker : LinearMap.ker f ≤ S := by
63     intro x hx
64     have hdiv : ∀ i, pi ^ s ∣ b.repr x i := by
65       have hz : f x = 0 := hx
66       intro i
67       have hi := congrFun hz i
68       change (Ideal.span {pi ^ s}).mkQ (b.repr x i) = 0 at hi
69       rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Ideal.mem_span_singleton] at hi
70       exact hi
71     rw [← b.sum_repr x]
72     apply S.sum_mem
73     intro i _hi
74     obtain ⟨c, hc⟩ := hdiv i
75     have ha := hann (S.mkQ (b i))
76     rw [← map_smul, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at ha
77     rw [hc, mul_comm, mul_smul]
78     exact S.smul_mem c ha
79   have hlen : Module.length O (∀ _ : ι, O ⧸ Ideal.span {pi ^ s}) = ∑ _ : ι, (s : ℕ∞) := by
80     rw [Module.length_pi_of_fintype]
81     apply Finset.sum_congr rfl
82     intro i _hi
83     have heq : Ideal.span {pi ^ s} = IsLocalRing.maximalIdeal O ^ s := by
84       rw [hpi.maximalIdeal_eq, Ideal.span_singleton_pow]
85     rw [(Submodule.quotEquivOfEq _ _ heq).length_eq]
86     exact IsDiscreteValuationRing.length_quotient_pow_maximalIdeal (R := O) s
87   have hfinite : IsFiniteLength O (∀ _ : ι, O ⧸ Ideal.span {pi ^ s}) := by
88     apply Module.length_ne_top_iff.mp
89     rw [hlen, ← Nat.cast_sum]
90     exact ENat.natCast_ne_top _
91   have hsource : IsFiniteLength O (W ⧸ LinearMap.ker f) :=
92     (f.quotKerEquivOfSurjective (smithCoordinateMap_surjective b pi (fun _ => s))).symm.isFiniteLength hfinite
93   exact hsource.of_surjective (Submodule.factor_surjective hker)
94 
95 /-- The manuscript's gluing module is finite length for every full DVR lattice. -/
96 theorem dvr_gluing_finiteLength
97     {ι : Type*} [Fintype ι] (Λ : Submodule O V) [Submodule.IsLattice K Λ]
98     (b : Module.Basis ι O Λ) (pi : O) (hpi : Irreducible pi)
99     (P : Projectors K V I) :
100     IsFiniteLength O (GluingModule (P.restrictScalars (O := O)) Λ) := by
101   classical
102   let finite := full_lattice_packet_clearing_exists Λ b pi hpi P
103   obtain ⟨s, hs⟩ := gluing_finite_exponent (P.restrictScalars (O := O)) Λ pi finite
104   exact finiteLength_quotient_of_power_annihilates _ b pi hpi s hs
105 
106 end Komorebi.PaperII.ReleaseGluing

Back to source controls