ReleaseGluingEquivSmith.lean

1 import KomorebiVerification.PaperII.ReleaseGluingSmith
2 
3 /-!
4 # Smith data supplied as an actual module equivalence
5 
6 These endpoints accept any cyclic-module decomposition of the actual
7 gluing quotient, as in the manuscript.  Inclusion bases are one source
8 of such an equivalence, not an additional premise of these statements.
9 -/
10 
11 set_option autoImplicit false
12 open scoped BigOperators
13 
14 namespace Komorebi.PaperII.ReleaseGluing
15 
16 universe u v w
17 variable {O : Type u} {G : Type v} {I : Type w}
18 variable [CommRing O] [IsDomain O] [AddCommGroup G] [Module O G]
19 variable [Fintype I]
20 
21 omit [Fintype I] in
22 /-- An arbitrary actual cyclic decomposition determines all uniform annihilators. -/
23 theorem cyclicProduct_annihilated_iff_weights_le
24     (pi : O) (hpi : pi ≠ 0) (hunit : ¬ IsUnit pi) (a : I → ℕ) (s : ℕ) :
25     (∀ z : ∀ i, O ⧸ Ideal.span {pi ^ a i}, (pi ^ s) • z = 0) ↔
26       ∀ i, a i ≤ s := by
27   constructor
28   · intro h i
29     have hi := congrFun (h (fun j => (Ideal.span {pi ^ a j}).mkQ 1)) i
30     change (pi ^ s) • (Ideal.span {pi ^ a i}).mkQ 1 = 0 at hi
31     rw [← map_smul, smul_eq_mul, mul_one, Submodule.mkQ_apply,
32       Submodule.Quotient.mk_eq_zero, Ideal.mem_span_singleton] at hi
33     exact (pow_dvd_pow_iff hpi hunit).mp hi
34   · intro h z
35     ext i
36     obtain ⟨r, hr⟩ := (Ideal.span {pi ^ a i}).mkQ_surjective (z i)
37     change (pi ^ s) • z i = 0
38     rw [← hr, ← map_smul, smul_eq_mul, Submodule.mkQ_apply,
39       Submodule.Quotient.mk_eq_zero, Ideal.mem_span_singleton]
40     exact dvd_mul_of_dvd_left ((pow_dvd_pow_iff hpi hunit).mpr (h i)) r
41 
42 /-- Transport of the exact annihilator threshold through any actual module equivalence. -/
43 theorem annihilated_iff_smith_max_of_equiv
44     (pi : O) (hpi : pi ≠ 0) (hunit : ¬ IsUnit pi) (a : I → ℕ)
45     (e : G ≃ₗ[O] (∀ i, O ⧸ Ideal.span {pi ^ a i})) (s : ℕ) :
46     (∀ z : G, (pi ^ s) • z = 0) ↔ Finset.univ.sup a ≤ s := by
47   have htransport : (∀ z : G, (pi ^ s) • z = 0) ↔
48       ∀ z : ∀ i, O ⧸ Ideal.span {pi ^ a i}, (pi ^ s) • z = 0 := by
49     constructor
50     · intro h z
51       obtain ⟨x, rfl⟩ := e.surjective z
52       rw [← map_smul, h x, map_zero]
53     · intro h z
54       apply e.injective
55       rw [map_smul, h (e z), map_zero]
56   rw [htransport, cyclicProduct_annihilated_iff_weights_le pi hpi hunit a s]
57   simp only [Finset.sup_le_iff, Finset.mem_univ, true_implies]
58 
59 /-- The length formula only needs the supplied cyclic decomposition. -/
60 theorem length_eq_smith_sum_of_equiv [IsDiscreteValuationRing O]
61     (pi : O) (hpi : Irreducible pi) (a : I → ℕ)
62     (e : G ≃ₗ[O] (∀ i, O ⧸ Ideal.span {pi ^ a i})) :
63     Module.length O G = ∑ i, (a i : ℕ∞) := by
64   rw [e.length_eq, Module.length_pi_of_fintype]
65   apply Finset.sum_congr rfl
66   intro i _hi
67   have heq : Ideal.span {pi ^ a i} = IsLocalRing.maximalIdeal O ^ a i := by
68     rw [hpi.maximalIdeal_eq, Ideal.span_singleton_pow]
69   rw [(Submodule.quotEquivOfEq _ _ heq).length_eq]
70   exact IsDiscreteValuationRing.length_quotient_pow_maximalIdeal (R := O) (a i)
71 
72 /-- The manuscript's maximum formula for any given Smith decomposition of G. -/
73 theorem globalWeight_eq_smith_max_of_equiv
74     {V : Type*} [AddCommGroup V] [Module O V]
75     {J : Type*} [Fintype J] (P : Projectors O V J) (Λ : Submodule O V)
76     (pi : O) (hpi : pi ≠ 0) (hunit : ¬ IsUnit pi) (a : I → ℕ)
77     (e : GluingModule P Λ ≃ₗ[O] (∀ i, O ⧸ Ideal.span {pi ^ a i}))
78     (finite : ∀ j, ∃ s, ClearsPacket P Λ pi j s) :
79     globalWeight P Λ pi finite = Finset.univ.sup a := by
80   apply le_antisymm
81   · apply (gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mp
82     exact (annihilated_iff_smith_max_of_equiv pi hpi hunit a e _).mpr le_rfl
83   · apply (annihilated_iff_smith_max_of_equiv pi hpi hunit a e _).mp
84     exact (gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mpr le_rfl
85 
86 end Komorebi.PaperII.ReleaseGluing

Back to source controls