FiniteFiberCountsContract.lean

1 module
2 public import FiniteFiberCounts
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.FiniteFiberCountsContract
8 
9 /-- The rank refers to the range of the supplied prime-field linear map. -/
10 theorem explicit_fiber_and_obstruction_counts (p : ℕ) [Fact (Nat.Prime p)]
11     {d e : ℕ} (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p))
12     (b : Fin e → ZMod p) (h : ∃ t, b + A t = 0) :
13     Nat.card {t : Fin d → ZMod p // b + A t = 0} =
14       p ^ (d - Module.finrank (ZMod p) A.range) ∧
15     Nat.card ((Fin e → ZMod p) ⧸ A.range) =
16       p ^ (e - Module.finrank (ZMod p) A.range) := by
17   exact ⟨FiniteFiberCounts.fiber_card_of_nonempty p A b
18     (by rcases h with ⟨t, ht⟩; exact ⟨⟨t, ht⟩⟩),
19     FiniteFiberCounts.cokernel_card p A⟩
20 
21 /-- Translation is explicitly free and transitive, not merely an equal count. -/
22 theorem explicit_free_transitive (p : ℕ) [Fact (Nat.Prime p)] {d e : ℕ}
23     (A : (Fin d → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p)) (b : Fin e → ZMod p)
24     (u t : {t : Fin d → ZMod p // b + A t = 0}) :
25     ∃! v : A.ker, FiniteFiberCounts.translate A b v u = t := by
26   exact FiniteFiberCounts.translate_exists_unique A b u t
27 
28 end Komorebi.FiniteFiberCountsContract

Back to source controls