FiniteFiberCounts.lean

1 module
2 public import Mathlib.Algebra.Torsor.Basic
3 public import Mathlib.FieldTheory.Finiteness
4 public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
5 public import Mathlib.Algebra.Field.ZMod
6 
7 /-!
8 # Linear correction fibers, torsors, and exact finite-field cardinalities
9 
10 A fiber is the set of actual correction digits satisfying `b + A t = 0`.
11 No nonsingularity hypothesis is imposed. Choosing a point identifies the fiber
12 with the kernel. The action itself is independent of this choice.
13 -/
14 
15 @[expose] public section
16 noncomputable section
17 set_option autoImplicit false
18 open scoped Classical
19 
20 namespace Komorebi.FiniteFiberCounts
21 
22 section General
23 variable {K U V : Type*} [Ring K] [AddCommGroup U] [AddCommGroup V]
24   [Module K U] [Module K V]
25 
26 /-- The correction equation has the sign used by the Taylor obstruction. -/
27 def Fiber (A : U →ₗ[K] V) (b : V) := {t : U // b + A t = 0}
28 
29 /-- Kernel vectors act by translation on correction digits. -/
30 def translate (A : U →ₗ[K] V) (b : V) (v : A.ker) (t : Fiber A b) : Fiber A b :=
31   ⟨v.1 + t.1, by
32     have hv : A v.1 = 0 := v.2
33     simpa only [map_add, hv, zero_add] using t.2⟩
34 
35 /-- The difference of two correction digits is a kernel vector. -/
36 def difference (A : U →ₗ[K] V) (b : V) (t u : Fiber A b) : A.ker :=
37   ⟨t.1 - u.1, by
38     change A (t.1 - u.1) = 0
39     rw [map_sub, sub_eq_zero]
40     exact add_left_cancel (t.2.trans u.2.symm)⟩
41 
42 theorem translate_zero (A : U →ₗ[K] V) (b : V) (t : Fiber A b) :
43     translate A b 0 t = t := by
44   apply Subtype.ext
45   exact zero_add _
46 
47 theorem translate_add (A : U →ₗ[K] V) (b : V) (v w : A.ker) (t : Fiber A b) :
48     translate A b (v + w) t = translate A b v (translate A b w t) := by
49   apply Subtype.ext
50   exact add_assoc _ _ _
51 
52 theorem translate_difference (A : U →ₗ[K] V) (b : V) (t u : Fiber A b) :
53     translate A b (difference A b t u) u = t := by
54   apply Subtype.ext
55   exact sub_add_cancel _ _
56 
57 theorem difference_translate (A : U →ₗ[K] V) (b : V) (v : A.ker) (t : Fiber A b) :
58     difference A b (translate A b v t) t = v := by
59   apply Subtype.ext
60   exact add_sub_cancel_right _ _
61 
62 /-- Actual free and transitive kernel action on every nonempty correction fiber.
63 This is an explicit structure rather than a global typeclass instance. -/
64 @[instance_reducible] def fiberAddTorsor (A : U →ₗ[K] V) (b : V) (h : Nonempty (Fiber A b)) :
65     AddTorsor A.ker (Fiber A b) where
66   vadd := translate A b
67   zero_vadd := translate_zero A b
68   add_vadd := translate_add A b
69   vsub := difference A b
70   nonempty := h
71   vsub_vadd' := translate_difference A b
72   vadd_vsub' := difference_translate A b
73 
74 /-- A chosen solution identifies all correction digits with the kernel. -/
75 def fiberEquivKernel (A : U →ₗ[K] V) (b : V) (u : Fiber A b) : Fiber A b ≃ A.ker where
76   toFun t := difference A b t u
77   invFun v := translate A b v u
78   left_inv t := translate_difference A b t u
79   right_inv v := difference_translate A b v u
80 
81 theorem translate_exists_unique (A : U →ₗ[K] V) (b : V) (u t : Fiber A b) :
82     ∃! v : A.ker, translate A b v u = t := by
83   refine ⟨difference A b t u, translate_difference A b t u, ?_⟩
84   intro v hv
85   rw [← hv, difference_translate]
86 
87 /-- Vanishing of the actual quotient class is exactly correction existence. -/
88 theorem fiber_nonempty_iff_class_zero (A : U →ₗ[K] V) (b : V) :
89     Nonempty (Fiber A b) ↔ (Submodule.Quotient.mk b : V ⧸ A.range) = 0 := by
90   rw [Submodule.Quotient.mk_eq_zero]
91   constructor
92   · rintro ⟨t⟩
93     refine ⟨-t.1, ?_⟩
94     rw [map_neg]
95     exact (eq_neg_of_add_eq_zero_left t.2).symm
96   · rintro ⟨t, ht⟩
97     refine ⟨⟨-t, ?_⟩⟩
98     rw [map_neg, ht, add_neg_cancel]
99 
100 theorem fiber_card_eq_kernel (A : U →ₗ[K] V) (b : V) (h : Nonempty (Fiber A b)) :
101     Nat.card (Fiber A b) = Nat.card A.ker := by
102   obtain ⟨u⟩ := h
103   exact Nat.card_congr (fiberEquivKernel A b u)
104 
105 theorem fiber_card_of_empty (A : U →ₗ[K] V) (b : V) (h : ¬ Nonempty (Fiber A b)) :
106     Nat.card (Fiber A b) = 0 := by
107   have : IsEmpty (Fiber A b) := not_nonempty_iff.mp h
108   exact Nat.card_eq_zero.mpr (Or.inl inferInstance)
109 
110 end General
111 
112 section PrimeField
113 variable (p : ℕ) [Fact (Nat.Prime p)] {d e : ℕ}
114 
115 /-- Rank of the actual correction map over the prime field. -/
116 def rank (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p)) : ℕ :=
117   Module.finrank (ZMod p) A.range
118 
119 theorem kernel_finrank (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p)) :
120     Module.finrank (ZMod p) A.ker = d - rank p A := by
121   have hr := A.finrank_range_add_finrank_ker
122   rw [Module.finrank_fin_fun] at hr
123   unfold rank
124   omega
125 
126 theorem kernel_card (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p)) :
127     Nat.card A.ker = p ^ (d - rank p A) := by
128   rw [Module.natCard_eq_pow_finrank (K := ZMod p), kernel_finrank p]
129   simp only [Nat.card_eq_fintype_card, ZMod.card]
130 
131 /-- Every nonempty correction fiber has precisely the kernel cardinality. -/
132 theorem fiber_card_of_nonempty
133     (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p)) (b : Fin e → ZMod p)
134     (h : Nonempty (Fiber A b)) : Nat.card (Fiber A b) = p ^ (d - rank p A) := by
135   rw [fiber_card_eq_kernel A b h, kernel_card p A]
136 
137 /-- Empty fibers have zero points; nonempty fibers obey rank-nullity. -/
138 theorem fiber_card (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p))
139     (b : Fin e → ZMod p) :
140     Nat.card (Fiber A b) = if Nonempty (Fiber A b) then p ^ (d - rank p A) else 0 := by
141   classical
142   split_ifs with h
143   · exact fiber_card_of_nonempty p A b h
144   · exact fiber_card_of_empty A b h
145 
146 /-- The finite obstruction space has the codomain dimension minus the rank. -/
147 theorem cokernel_finrank (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p)) :
148     Module.finrank (ZMod p) ((Fin e → ZMod p) ⧸ A.range) = e - rank p A := by
149   rw [Submodule.finrank_quotient, Module.finrank_fin_fun]
150   rfl
151 
152 theorem cokernel_card (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p)) :
153     Nat.card ((Fin e → ZMod p) ⧸ A.range) = p ^ (e - rank p A) := by
154   rw [Module.natCard_eq_pow_finrank (K := ZMod p), cokernel_finrank p]
155   simp only [Nat.card_eq_fintype_card, ZMod.card]
156 
157 end PrimeField
158 end Komorebi.FiniteFiberCounts

Back to source controls