ReleaseSmithRectangular.lean

1 import KomorebiVerification.PaperII.ReleaseSmithDVR
2 import Mathlib.Data.Matrix.Block
3 import Mathlib.LinearAlgebra.Matrix.ToLin
4 
5 /-! Rectangular Smith fibres: actual active, free-column and zero-row coordinates. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace Komorebi.PaperII.SmithDVR
9 open IsLocalRing
10 open scoped Matrix
11 universe u
12 variable {O : Type u} [CommRing O]
13 
14 /-- The actual reduced rectangular diagonal map, including every free column and zero row. -/
15 def rectangularDiagonal (pi : O) (L : Nat) {r f z : Nat} (s : Fin r → Nat)
16     (x : (Fin r ⊕ Fin f) → QuotientAt pi L) : (Fin r ⊕ Fin z) → QuotientAt pi L :=
17   Sum.elim (fun i => multiplyPower pi (s i) L (x (.inl i))) (fun _ => 0)
18 
19 abbrev RectangularFiber (pi : O) (L : Nat) {r f z : Nat} (s : Fin r → Nat)
20     (b : (Fin r ⊕ Fin z) → O) :=
21   {x : (Fin r ⊕ Fin f) → QuotientAt pi L //
22     rectangularDiagonal pi L s x = fun i => (powerIdeal pi L).mkQ (b i)}
23 
24 theorem quotient_target_zero_iff (pi : O) (L : Nat) (b : O) :
25     (powerIdeal pi L).mkQ b = 0 ↔ pi ^ L ∣ b := by
26   rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, powerIdeal, Ideal.mem_span_singleton]
27 
28 /-- Explicit product decomposition of a diagonal solution fibre. -/
29 def rectangularFiberEquiv (pi : O) (L : Nat) {r f z : Nat} (s : Fin r → Nat)
30     (b : (Fin r ⊕ Fin z) → O) (hz : ∀ i : Fin z, pi ^ L ∣ b (.inr i)) :
31     RectangularFiber (f := f) pi L s b ≃
32       (∀ i : Fin r, ScalarFiber pi (s i) L (b (.inl i))) × (Fin f → QuotientAt pi L) where
33   toFun x := ⟨fun i => ⟨x.val (.inl i), congrFun x.property (.inl i)⟩,
34     fun i => x.val (.inr i)⟩
35   invFun x := ⟨Sum.elim (fun i => (x.1 i).val) x.2, by
36     funext i
37     cases i with
38     | inl i => exact (x.1 i).property
39     | inr i => exact ((quotient_target_zero_iff pi L _).mpr (hz i)).symm⟩
40   left_inv x := by
41     apply Subtype.ext
42     funext i
43     cases i <;> rfl
44   right_inv x := by
45     apply Prod.ext
46     · funext i
47       apply Subtype.ext
48       rfl
49     · rfl
50 
51 theorem rectangularFiber_nonempty_iff (pi : O) (L : Nat) {r f z : Nat}
52     (s : Fin r → Nat) (b : (Fin r ⊕ Fin z) → O) :
53     Nonempty (RectangularFiber (f := f) pi L s b) ↔
54       (∀ i : Fin r, pi ^ min (s i) L ∣ b (.inl i)) ∧
55       (∀ i : Fin z, pi ^ L ∣ b (.inr i)) := by
56   constructor
57   · rintro ⟨x⟩
58     constructor
59     · intro i
60       apply (scalarFiber_nonempty_iff pi (s i) L _).mp
61       exact ⟨⟨x.val (.inl i), congrFun x.property (.inl i)⟩⟩
62     · intro i
63       apply (quotient_target_zero_iff pi L _).mp
64       exact (congrFun x.property (.inr i)).symm
65   · rintro ⟨ha, hz⟩
66     exact ⟨(rectangularFiberEquiv pi L s b hz).symm
67       ⟨fun i => Classical.choice ((scalarFiber_nonempty_iff pi (s i) L _).mpr (ha i)),
68        fun _ => 0⟩⟩
69 
70 /-- Every independent free column contributes q^L; no square/full-rank hypothesis occurs. -/
71 theorem rectangularFiber_card [IsDomain O] [IsDiscreteValuationRing O]
72     [Finite (ResidueField O)] (pi : O) (hpi : Irreducible pi) (L : Nat)
73     {r f z : Nat} (s : Fin r → Nat) (b : (Fin r ⊕ Fin z) → O)
74     (ha : ∀ i : Fin r, pi ^ min (s i) L ∣ b (.inl i))
75     (hz : ∀ i : Fin z, pi ^ L ∣ b (.inr i)) :
76     Nat.card (RectangularFiber (f := f) pi L s b) =
77       Nat.card (ResidueField O) ^ (f * L + ∑ i : Fin r, min (s i) L) := by
78   rw [Nat.card_congr (rectangularFiberEquiv (f := f) pi L s b hz), Nat.card_prod,
79     Nat.card_pi, Nat.card_fun, Nat.card_fin, quotientAt_card pi hpi]
80   simp_rw [scalarFiber_card pi hpi _ _ _ (ha _)]
81   rw [Finset.prod_pow_eq_pow_sum, ← pow_mul, ← pow_add, Nat.mul_comm L f, Nat.add_comm]
82 
83 /-- Integral rectangular diagonal matrix giving the preceding coordinate formula. -/
84 def rectangularMatrix (pi : O) {r f z : Nat} (s : Fin r → Nat) :
85     Matrix (Fin r ⊕ Fin z) (Fin r ⊕ Fin f) O :=
86   Matrix.fromBlocks (Matrix.diagonal (fun i => pi ^ s i)) 0 0 0
87 
88 /-- Reducing the displayed integral diagonal matrix gives the actual quotient map. -/
89 theorem rectangularMatrix_mulVec (pi : O) (L : Nat) {r f z : Nat} (s : Fin r → Nat)
90     (x : (Fin r ⊕ Fin f) → QuotientAt pi L) :
91     (rectangularMatrix (f := f) (z := z) pi s).map (Ideal.Quotient.mk (powerIdeal pi L)) *ᵥ x =
92       rectangularDiagonal pi L s x := by
93   funext i
94   cases i with
95   | inl i =>
96       simp [rectangularMatrix, rectangularDiagonal, Matrix.mulVec, dotProduct,
97         Matrix.fromBlocks, Matrix.diagonal, multiplyPower, Algebra.smul_def, apply_ite, ite_mul]
98   | inr i =>
99       simp [rectangularMatrix, rectangularDiagonal, Matrix.mulVec, dotProduct, Matrix.fromBlocks]
100 
101 end Komorebi.PaperII.SmithDVR
102 #print axioms Komorebi.PaperII.SmithDVR.rectangularFiber_nonempty_iff
103 #print axioms Komorebi.PaperII.SmithDVR.rectangularFiber_card

Back to source controls