ReleaseSmithTransport.lean

1 import KomorebiVerification.PaperII.ReleaseSmithRectangular
2 
3 /-! Invertible Smith row/column changes on the actual quotient matrix fibres. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace Komorebi.PaperII.SmithDVR
7 open scoped Matrix
8 universe u
9 section Change
10 variable {R : Type u} [CommRing R]
11 variable {m n : Type*} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
12 
13 /-- The genuine coordinate equivalence carried by a matrix unit. -/
14 def matrixUnitEquiv (U : (Matrix n n R)ˣ) : (n → R) ≃ₗ[R] (n → R) :=
15   Matrix.toLin'OfInv (show (↑U⁻¹ : Matrix n n R) * ↑U = 1 by exact U.inv_val)
16     (show (↑U : Matrix n n R) * ↑U⁻¹ = 1 by exact U.val_inv)
17 
18 @[simp] theorem matrixUnitEquiv_apply (U : (Matrix n n R)ˣ) (x : n → R) :
19     matrixUnitEquiv U x = (↑U : Matrix n n R) *ᵥ x := rfl
20 
21 abbrev MatrixFiber (M : Matrix m n R) (b : m → R) := {x : n → R // M *ᵥ x = b}
22 
23 /-- Explicit fibre equivalence induced by UMV=D, with the transformed target Ub. -/
24 def smithMatrixFiberEquiv (M : Matrix m n R) (U : (Matrix m m R)ˣ)
25     (V : (Matrix n n R)ˣ) (D : Matrix m n R)
26     (hsmith : (↑U : Matrix m m R) * M * V.val = D) (b : m → R) :
27     MatrixFiber M b ≃ MatrixFiber D ((↑U : Matrix m m R) *ᵥ b) where
28   toFun x := ⟨(matrixUnitEquiv V).symm x.val, by
29     rw [← hsmith, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec]
30     change (↑U : Matrix m m R) *ᵥ
31       (M *ᵥ matrixUnitEquiv V ((matrixUnitEquiv V).symm x.val)) = _
32     rw [LinearEquiv.apply_symm_apply, x.property]⟩
33   invFun y := ⟨matrixUnitEquiv V y.val, by
34     apply (matrixUnitEquiv U).injective
35     change (↑U : Matrix m m R) *ᵥ (M *ᵥ ((↑V : Matrix n n R) *ᵥ y.val)) = _
36     rw [Matrix.mulVec_mulVec, Matrix.mulVec_mulVec, hsmith]
37     exact y.property⟩
38   left_inv x := by apply Subtype.ext; exact LinearEquiv.apply_symm_apply _ _
39   right_inv y := by apply Subtype.ext; exact LinearEquiv.symm_apply_apply _ _
40 end Change
41 
42 section Integral
43 variable {O : Type u} [CommRing O]
44 variable {m n : Type*} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
45 
46 /-- Reducing an integral matrix unit gives an actual unit over O/(pi^L). -/
47 def quotientMatrixUnit (pi : O) (L : Nat) (U : (Matrix n n O)ˣ) :
48     (Matrix n n (QuotientAt pi L))ˣ :=
49   Units.map ((Ideal.Quotient.mk (powerIdeal pi L)).mapMatrix).toMonoidHom U
50 
51 @[simp] theorem quotientMatrixUnit_val (pi : O) (L : Nat) (U : (Matrix n n O)ˣ) :
52     (↑(quotientMatrixUnit pi L U) : Matrix n n (QuotientAt pi L)) =
53       (↑U : Matrix n n O).map (Ideal.Quotient.mk (powerIdeal pi L)) := rfl
54 
55 /-- The equation UMV=D survives reduction; it is not replaced by a fibre-count hypothesis. -/
56 theorem quotient_smith_identity (pi : O) (L : Nat) (M : Matrix m n O)
57     (U : (Matrix m m O)ˣ) (V : (Matrix n n O)ˣ) (D : Matrix m n O)
58     (hsmith : (↑U : Matrix m m O) * M * V.val = D) :
59     (↑(quotientMatrixUnit pi L U) : Matrix m m (QuotientAt pi L)) *
60       M.map (Ideal.Quotient.mk (powerIdeal pi L)) * (quotientMatrixUnit pi L V).val =
61       D.map (Ideal.Quotient.mk (powerIdeal pi L)) := by
62   simp only [quotientMatrixUnit_val, ← Matrix.map_mul, hsmith]
63 
64 /-- Actual integral-congruence solution fibre. -/
65 abbrev CongruenceFiber (pi : O) (L : Nat) (M : Matrix m n O) (b : m → O) :=
66   MatrixFiber (M.map (Ideal.Quotient.mk (powerIdeal pi L)))
67     (fun i => (powerIdeal pi L).mkQ (b i))
68 
69 /-- The fibre of the original matrix is explicitly equivalent to its rectangular Smith fibre. -/
70 def smithCongruenceEquiv (pi : O) (L : Nat) {r f z : Nat}
71     (M : Matrix (Fin r ⊕ Fin z) (Fin r ⊕ Fin f) O)
72     (U : (Matrix (Fin r ⊕ Fin z) (Fin r ⊕ Fin z) O)ˣ)
73     (V : (Matrix (Fin r ⊕ Fin f) (Fin r ⊕ Fin f) O)ˣ)
74     (s : Fin r → Nat) (hsmith : U.val * M * V.val = rectangularMatrix pi s)
75     (b : (Fin r ⊕ Fin z) → O) :
76     CongruenceFiber pi L M b ≃ RectangularFiber (f := f) pi L s (U.val *ᵥ b) := by
77   let e := smithMatrixFiberEquiv
78     (M.map (Ideal.Quotient.mk (powerIdeal pi L))) (quotientMatrixUnit pi L U)
79     (quotientMatrixUnit pi L V)
80     ((rectangularMatrix (f := f) (z := z) pi s).map (Ideal.Quotient.mk (powerIdeal pi L)))
81     (quotient_smith_identity pi L M U V _ hsmith)
82     (fun i => (powerIdeal pi L).mkQ (b i))
83   refine e.trans (Equiv.subtypeEquivRight ?_)
84   intro x
85   rw [rectangularMatrix_mulVec]
86   have ht : (quotientMatrixUnit pi L U).val *ᵥ
87       (fun i => (powerIdeal pi L).mkQ (b i)) =
88       (fun i => (powerIdeal pi L).mkQ ((U.val *ᵥ b) i)) := by
89     funext i
90     exact (RingHom.map_mulVec (Ideal.Quotient.mk (powerIdeal pi L)) U.val b i).symm
91   rw [ht]
92 
93 /-- General DVR Smith obstruction theorem, retaining all rectangular zero rows. -/
94 theorem smith_congruence_nonempty_iff (pi : O) (L : Nat) {r f z : Nat}
95     (M : Matrix (Fin r ⊕ Fin z) (Fin r ⊕ Fin f) O)
96     (U : (Matrix (Fin r ⊕ Fin z) (Fin r ⊕ Fin z) O)ˣ)
97     (V : (Matrix (Fin r ⊕ Fin f) (Fin r ⊕ Fin f) O)ˣ)
98     (s : Fin r → Nat) (hsmith : U.val * M * V.val = rectangularMatrix pi s)
99     (b : (Fin r ⊕ Fin z) → O) :
100     Nonempty (CongruenceFiber pi L M b) ↔
101       (∀ i : Fin r, pi ^ min (s i) L ∣ (U.val *ᵥ b) (.inl i)) ∧
102       (∀ i : Fin z, pi ^ L ∣ (U.val *ᵥ b) (.inr i)) := by
103   rw [(smithCongruenceEquiv pi L M U V s hsmith b).nonempty_congr]
104   exact rectangularFiber_nonempty_iff pi L s _
105 
106 /-- The exact number of solutions is q^((n-r)L+sum min(s_i,L)). -/
107 theorem smith_congruence_card [IsDomain O] [IsDiscreteValuationRing O]
108     [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (L : Nat)
109     {r f z : Nat} (M : Matrix (Fin r ⊕ Fin z) (Fin r ⊕ Fin f) O)
110     (U : (Matrix (Fin r ⊕ Fin z) (Fin r ⊕ Fin z) O)ˣ)
111     (V : (Matrix (Fin r ⊕ Fin f) (Fin r ⊕ Fin f) O)ˣ)
112     (s : Fin r → Nat) (hsmith : U.val * M * V.val = rectangularMatrix pi s)
113     (b : (Fin r ⊕ Fin z) → O)
114     (ha : ∀ i : Fin r, pi ^ min (s i) L ∣ (U.val *ᵥ b) (.inl i))
115     (hz : ∀ i : Fin z, pi ^ L ∣ (U.val *ᵥ b) (.inr i)) :
116     Nat.card (CongruenceFiber pi L M b) =
117       Nat.card (IsLocalRing.ResidueField O) ^ (f * L + ∑ i : Fin r, min (s i) L) := by
118   rw [Nat.card_congr (smithCongruenceEquiv pi L M U V s hsmith b)]
119   exact rectangularFiber_card pi hpi L s _ ha hz
120 end Integral
121 end Komorebi.PaperII.SmithDVR
122 #print axioms Komorebi.PaperII.SmithDVR.smith_congruence_nonempty_iff
123 #print axioms Komorebi.PaperII.SmithDVR.smith_congruence_card

Back to source controls