ReleaseGluingMatrix.lean

1 import KomorebiVerification.PaperII.ReleaseGluingSmith
2 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
3 
4 /-! Actual invertible matrix changes give Smith bases of an inclusion. -/
5 
6 set_option autoImplicit false
7 open scoped Matrix
8 
9 namespace Komorebi.PaperII.ReleaseGluing
10 
11 universe u v w
12 variable {O : Type u} {W : Type v} {I : Type w}
13 variable [CommRing O] [AddCommGroup W] [Module O W]
14 variable [Fintype I] [DecidableEq I]
15 
16 /-- The matrix Smith equation for the actual inclusion yields actual Smith bases. -/
17 theorem smith_bases_of_inclusion_matrix
18     (S : Submodule O W) (b : Module.Basis I O W) (c : Module.Basis I O S)
19     (U V : Matrix.GeneralLinearGroup I O) (d : I → O)
20     (hmat : (U : Matrix I I O) * LinearMap.toMatrix c b S.subtype *
21       (V : Matrix I I O) = Matrix.diagonal d) :
22     ∃ (b' : Module.Basis I O W) (c' : Module.Basis I O S),
23       ∀ i, (c' i : W) = d i • b' i := by
24   let eU := (Matrix.GeneralLinearGroup.toLin U).toLinearEquiv
25   let eV := (Matrix.GeneralLinearGroup.toLin V).toLinearEquiv
26   let b' := Module.Basis.ofEquivFun (b.equivFun.trans eU)
27   let c' := Module.Basis.ofEquivFun (c.equivFun.trans eV.symm)
28   refine ⟨b', c', ?_⟩
29   intro i
30   have hc : c.equivFun (c' i) = eV (Pi.single i 1) := by
31     have hci : c' i = c.equivFun.symm (eV (Pi.single i 1)) := by
32       change (Module.Basis.ofEquivFun (c.equivFun.trans eV.symm)) i = _
33       rw [Module.Basis.coe_ofEquivFun]
34       rfl
35     rw [hci, c.equivFun.apply_symm_apply]
36   have hb : LinearMap.toMatrix c b S.subtype *ᵥ c.equivFun (c' i) =
37       b.equivFun (c' i : W) := by
38     exact LinearMap.toMatrix_mulVec_repr c b S.subtype (c' i)
39   have hcalc : eU (b.equivFun (c' i : W)) = (Matrix.diagonal d) *ᵥ Pi.single i 1 := by
40     rw [← hb, hc]
41     change (U : Matrix I I O) *ᵥ
42       (LinearMap.toMatrix c b S.subtype *ᵥ ((V : Matrix I I O) *ᵥ Pi.single i 1)) = _
43     rw [Matrix.mulVec_mulVec, Matrix.mulVec_mulVec, hmat]
44   apply b'.repr.injective
45   ext j
46   change eU (b.equivFun (c' i : W)) j = b'.repr (d i • b' i) j
47   rw [hcalc]
48   by_cases hij : i = j
49   · subst j
50     simp [Matrix.mulVec_diagonal]
51   · simp [Matrix.mulVec_diagonal, Ne.symm hij]
52 
53 variable [IsDomain O]
54 
55 omit [IsDomain O] in
56 /-- Smith form of the original inclusion matrix gives the actual quotient decomposition. -/
57 theorem inclusion_matrix_smith_quotient
58     (S : Submodule O W) (b : Module.Basis I O W) (c : Module.Basis I O S)
59     (U V : Matrix.GeneralLinearGroup I O) (pi : O) (a : I → ℕ)
60     (hmat : (U : Matrix I I O) * LinearMap.toMatrix c b S.subtype *
61       (V : Matrix I I O) = Matrix.diagonal (fun i => pi ^ a i)) :
62     Nonempty ((W ⧸ S) ≃ₗ[O] (∀ i, O ⧸ Ideal.span {pi ^ a i})) := by
63   obtain ⟨b', c', hc⟩ := smith_bases_of_inclusion_matrix S b c U V (fun i => pi ^ a i) hmat
64   exact ⟨smithInclusionQuotientEquiv S b' c' pi a hc⟩
65 
66 /-- Exact weight from the Smith form of an arbitrary chosen inclusion matrix. -/
67 theorem globalWeight_eq_smith_max_of_inclusion_matrix
68     {X : Type*} [AddCommGroup X] [Module O X]
69     {J : Type*} [Fintype J] (P : Projectors O X J) (Λ : Submodule O X)
70     (b : Module.Basis I O Λ) (c : Module.Basis I O (splitInside P Λ))
71     (U V : Matrix.GeneralLinearGroup I O) (pi : O) (hpi : pi ≠ 0)
72     (hunit : ¬ IsUnit pi) (a : I → ℕ)
73     (hmat : (U : Matrix I I O) * LinearMap.toMatrix c b (splitInside P Λ).subtype *
74       (V : Matrix I I O) = Matrix.diagonal (fun i => pi ^ a i))
75     (finite : ∀ j, ∃ s, ClearsPacket P Λ pi j s) :
76     globalWeight P Λ pi finite = Finset.univ.sup a := by
77   obtain ⟨b', c', hc⟩ := smith_bases_of_inclusion_matrix _ b c U V (fun i => pi ^ a i) hmat
78   exact globalWeight_eq_smith_max P Λ b' c' pi hpi hunit a hc finite
79 
80 end Komorebi.PaperII.ReleaseGluing

Back to source controls