ReleaseGluingSmith.lean

1 import KomorebiVerification.PaperII.ReleaseGluing
2 import Mathlib.LinearAlgebra.Basis.Defs
3 import Mathlib.Algebra.GroupWithZero.Divisibility
4 import Mathlib.RingTheory.Ideal.Span
5 import Mathlib.LinearAlgebra.Isomorphisms
6 import Mathlib.RingTheory.DiscreteValuationRing.Basic
7 
8 /-!
9 # Smith inclusion data and exact quotient exponent
10 
11 The input is an actual basis of a submodule S and an actual basis of W,
12 related by the diagonal inclusion equation.  No quotient isomorphism or
13 annihilator formula is assumed.  This is the precise input supplied by a
14 Smith normal form of a full-rank lattice inclusion.  The proof works over
15 any domain with a nonzero nonunit pi; a DVR uniformizer satisfies these
16 conditions.  Zero exponents and empty bases are included.
17 -/
18 
19 set_option autoImplicit false
20 open scoped BigOperators
21 
22 namespace Komorebi.PaperII.ReleaseGluing
23 
24 universe u v w
25 variable {O : Type u} {W : Type v} {I : Type w}
26 variable [CommRing O] [IsDomain O] [AddCommGroup W] [Module O W]
27 variable [Fintype I] [DecidableEq I]
28 
29 omit [IsDomain O] in
30 theorem mem_submodule_iff_smith_coordinates
31     (S : Submodule O W) (b : Module.Basis I O W) (c : Module.Basis I O S)
32     (pi : O) (a : I → ℕ)
33     (hdiag : ∀ i, (c i : W) = (pi ^ a i) • b i) (x : W) :
34     x ∈ S ↔ ∀ i, pi ^ a i ∣ b.repr x i := by
35   constructor
36   · intro hx i
37     let y : S := ⟨x, hx⟩
38     have hsum : (∑ j, c.repr y j • (c j : W)) = x := by
39       simpa only [Submodule.coe_sum, Submodule.coe_smul] using
40         congrArg (fun z : S => (z : W)) (c.sum_repr y)
41     refine ⟨c.repr y i, ?_⟩
42     rw [← hsum]
43     simp [hdiag, mul_comm, Finsupp.single_apply]
44   · intro hx
45     rw [← b.sum_repr x]
46     apply S.sum_mem
47     intro i _hi
48     obtain ⟨k, hk⟩ := hx i
49     rw [hk, mul_comm, mul_smul, ← hdiag i]
50     exact S.smul_mem k (c i).property
51 
52 /-- The coordinate map into the actual cyclic O-module quotients. -/
53 noncomputable def smithCoordinateMap (b : Module.Basis I O W) (pi : O) (a : I → ℕ) :
54     W →ₗ[O] (∀ i, O ⧸ Ideal.span {pi ^ a i}) :=
55   LinearMap.pi fun i => (Ideal.span {pi ^ a i}).mkQ.comp (b.coord i)
56 
57 omit [IsDomain O] in
58 theorem smithCoordinateMap_ker
59     (S : Submodule O W) (b : Module.Basis I O W) (c : Module.Basis I O S)
60     (pi : O) (a : I → ℕ)
61     (hdiag : ∀ i, (c i : W) = (pi ^ a i) • b i) :
62     LinearMap.ker (smithCoordinateMap b pi a) = S := by
63   ext x
64   rw [mem_submodule_iff_smith_coordinates S b c pi a hdiag]
65   change (smithCoordinateMap b pi a x = 0) ↔ _
66   simp only [smithCoordinateMap, LinearMap.pi_apply, LinearMap.comp_apply,
67     funext_iff, Pi.zero_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero,
68     Ideal.mem_span_singleton, Module.Basis.coord_apply]
69 
70 omit [IsDomain O] [DecidableEq I] in
71 theorem smithCoordinateMap_surjective (b : Module.Basis I O W) (pi : O) (a : I → ℕ) :
72     Function.Surjective (smithCoordinateMap b pi a) := by
73   classical
74   intro y
75   choose r hr using fun i => (Ideal.span {pi ^ a i}).mkQ_surjective (y i)
76   refine ⟨b.equivFun.symm r, ?_⟩
77   ext i
78   change (Ideal.span {pi ^ a i}).mkQ (b.repr (b.equivFun.symm r) i) = y i
79   rw [← b.equivFun_apply, b.equivFun.apply_symm_apply]
80   exact hr i
81 
82 /-- Smith diagonalization of an inclusion produces the actual quotient decomposition. -/
83 noncomputable def smithInclusionQuotientEquiv
84     (S : Submodule O W) (b : Module.Basis I O W) (c : Module.Basis I O S)
85     (pi : O) (a : I → ℕ)
86     (hdiag : ∀ i, (c i : W) = (pi ^ a i) • b i) :
87     (W ⧸ S) ≃ₗ[O] (∀ i, O ⧸ Ideal.span {pi ^ a i}) :=
88   (Submodule.quotEquivOfEq S _ (smithCoordinateMap_ker S b c pi a hdiag).symm).trans
89     ((smithCoordinateMap b pi a).quotKerEquivOfSurjective
90       (smithCoordinateMap_surjective b pi a))
91 
92 /-- The length of the actual Smith cokernel is the sum of its directional weights. -/
93 theorem length_smith_inclusion_quotient [IsDiscreteValuationRing O]
94     (S : Submodule O W) (b : Module.Basis I O W) (c : Module.Basis I O S)
95     (pi : O) (hpi : Irreducible pi) (a : I → ℕ)
96     (hdiag : ∀ i, (c i : W) = (pi ^ a i) • b i) :
97     Module.length O (W ⧸ S) = ∑ i, (a i : ℕ∞) := by
98   rw [(smithInclusionQuotientEquiv S b c pi a hdiag).length_eq,
99     Module.length_pi_of_fintype]
100   apply Finset.sum_congr rfl
101   intro i _hi
102   have heq : Ideal.span {pi ^ a i} = IsLocalRing.maximalIdeal O ^ a i := by
103     rw [hpi.maximalIdeal_eq, Ideal.span_singleton_pow]
104   rw [(Submodule.quotEquivOfEq _ _ heq).length_eq]
105   exact IsDiscreteValuationRing.length_quotient_pow_maximalIdeal (R := O) (a i)
106 
107 theorem quotient_annihilated_iff_smith_weights_le
108     (S : Submodule O W) (b : Module.Basis I O W) (c : Module.Basis I O S)
109     (pi : O) (hpi : pi ≠ 0) (hunit : ¬ IsUnit pi) (a : I → ℕ)
110     (hdiag : ∀ i, (c i : W) = (pi ^ a i) • b i) (s : ℕ) :
111     (∀ z : W ⧸ S, (pi ^ s) • z = 0) ↔ ∀ i, a i ≤ s := by
112   constructor
113   · intro h i
114     have hk := h (S.mkQ (b i))
115     rw [← map_smul, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at hk
116     have hdvd := (mem_submodule_iff_smith_coordinates S b c pi a hdiag _).mp hk i
117     simp only [map_smul, Finsupp.smul_apply, b.repr_self_apply, ite_true,
118       smul_eq_mul, mul_one] at hdvd
119     exact (pow_dvd_pow_iff hpi hunit).mp hdvd
120   · intro h z
121     obtain ⟨x, rfl⟩ := S.mkQ_surjective z
122     rw [← map_smul, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
123     apply (mem_submodule_iff_smith_coordinates S b c pi a hdiag _).mpr
124     intro i
125     simp only [map_smul, Finsupp.smul_apply, smul_eq_mul]
126     exact dvd_mul_of_dvd_left ((pow_dvd_pow_iff hpi hunit).mpr (h i)) _
127 
128 theorem quotient_annihilated_iff_smith_max_le
129     (S : Submodule O W) (b : Module.Basis I O W) (c : Module.Basis I O S)
130     (pi : O) (hpi : pi ≠ 0) (hunit : ¬ IsUnit pi) (a : I → ℕ)
131     (hdiag : ∀ i, (c i : W) = (pi ^ a i) • b i) (s : ℕ) :
132     (∀ z : W ⧸ S, (pi ^ s) • z = 0) ↔ Finset.univ.sup a ≤ s := by
133   rw [quotient_annihilated_iff_smith_weights_le S b c pi hpi hunit a hdiag]
134   simp only [Finset.sup_le_iff, Finset.mem_univ, true_implies]
135 
136 /-- Given a Smith basis of the actual split-lattice inclusion, its maximum weight
137 is exactly the maximum of the least projector denominator weights. -/
138 theorem globalWeight_eq_smith_max
139     {V : Type*} [AddCommGroup V] [Module O V]
140     {J : Type*} [Fintype J] (P : Projectors O V J) (Λ : Submodule O V)
141     (b : Module.Basis I O Λ) (c : Module.Basis I O (splitInside P Λ))
142     (pi : O) (hpi : pi ≠ 0) (hunit : ¬ IsUnit pi) (a : I → ℕ)
143     (hdiag : ∀ i, (c i : Λ) = (pi ^ a i) • b i)
144     (finite : ∀ j, ∃ s, ClearsPacket P Λ pi j s) :
145     globalWeight P Λ pi finite = Finset.univ.sup a := by
146   apply le_antisymm
147   · apply (gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mp
148     exact (quotient_annihilated_iff_smith_max_le
149       (splitInside P Λ) b c pi hpi hunit a hdiag _).mpr le_rfl
150   · apply (quotient_annihilated_iff_smith_max_le
151       (splitInside P Λ) b c pi hpi hunit a hdiag _).mp
152     exact (gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mpr le_rfl
153 
154 end Komorebi.PaperII.ReleaseGluing

Back to source controls