IntegerFiniteCokernel.lean

1 module
2 public import AffineObstructionCore
3 public import Mathlib.SetTheory.Cardinal.Finite
4 
5 /-!
6 # Integer and residue-ring cokernels
7 
8 Reduction from integer vectors onto residue vectors identifies the range of an
9 integer coefficient map modulo `q` with the range of its residue-ring-linear
10 model. The resulting quotient equivalence preserves actual residual classes.
11 This bridge works for every natural modulus, including zero and composites.
12 -/
13 
14 @[expose] public section
15 noncomputable section
16 set_option autoImplicit false
17 
18 namespace Komorebi.IntegerFiniteCokernel
19 
20 open NativeAffine
21 
22 variable {d e : ℕ}
23 
24 theorem reduction_surjective (q n : ℕ) : Function.Surjective (reduction q n) := by
25   intro u
26   choose t ht using fun i => ZMod.intCast_surjective (u i)
27   exact ⟨t, funext ht⟩
28 
29 /-- The two coefficient maps have exactly the same range after scalar restriction. -/
30 theorem digit_range_eq_restrict (q : ℕ)
31     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
32     (B : (Fin d → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q))
33     (h : ∀ t, B (reduction q d t) = reduction q e (A t)) :
34     LinearMap.range (digitMap q A) = (LinearMap.range B).restrictScalars ℤ := by
35   ext u
36   constructor
37   · rintro ⟨t, rfl⟩
38     exact ⟨reduction q d t, h t⟩
39   · rintro ⟨v, rfl⟩
40     obtain ⟨t, rfl⟩ := reduction_surjective q d v
41     exact ⟨t, (h t).symm⟩
42 
43 /-- The previous integer-module obstruction is the residue-ring cokernel. -/
44 def cokernelEquiv (q : ℕ)
45     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
46     (B : (Fin d → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q))
47     (h : ∀ t, B (reduction q d t) = reduction q e (A t)) :
48     Obstruction q A ≃ₗ[ℤ] ((Fin e → ZMod q) ⧸ LinearMap.range B) :=
49   (Submodule.quotEquivOfEq _ _ (digit_range_eq_restrict q A B h)).trans
50     (Submodule.Quotient.restrictScalarsEquiv ℤ (LinearMap.range B))
51 
52 @[simp]
53 theorem cokernelEquiv_mk (q : ℕ)
54     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
55     (B : (Fin d → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q))
56     (h : ∀ t, B (reduction q d t) = reduction q e (A t))
57     (u : Fin e → ZMod q) :
58     cokernelEquiv q A B h (Submodule.Quotient.mk u) =
59       Submodule.Quotient.mk u := by
60   rfl
61 
62 @[simp]
63 theorem cokernelEquiv_obstruction (q : ℕ)
64     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
65     (B : (Fin d → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q))
66     (h : ∀ t, B (reduction q d t) = reduction q e (A t))
67     (r : Fin e → ℤ) :
68     cokernelEquiv q A B h (obstruction q A r) =
69       Submodule.Quotient.mk (reduction q e r) := by
70   rfl
71 
72 theorem cokernel_card_eq (q : ℕ)
73     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
74     (B : (Fin d → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q))
75     (h : ∀ t, B (reduction q d t) = reduction q e (A t)) :
76     Nat.card (Obstruction q A) =
77       Nat.card ((Fin e → ZMod q) ⧸ LinearMap.range B) := by
78   exact Nat.card_congr (cokernelEquiv q A B h).toEquiv
79 
80 #print axioms reduction_surjective
81 #print axioms digit_range_eq_restrict
82 #print axioms cokernelEquiv
83 #print axioms cokernelEquiv_mk
84 #print axioms cokernelEquiv_obstruction
85 #print axioms cokernel_card_eq
86 
87 end Komorebi.IntegerFiniteCokernel

Back to source controls