PolynomialMinorSelection.lean

1 module
2 public import Mathlib.LinearAlgebra.Basis.VectorSpace
3 public import Mathlib.LinearAlgebra.Dimension.Constructions
4 public import Mathlib.Logic.Equiv.Fintype
5 public import Mathlib.Algebra.Field.ZMod
6 
7 @[expose] public section
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.PolynomialMinorSelection
12 
13 variable {K : Type*} [Field K] {d e q : ℕ}
14 
15 /-- A surjective finite-dimensional linear map has a surjective square selection
16 of its actual coordinate columns. -/
17 theorem exists_selected_columns
18     (A : (Fin d → K) →ₗ[K] (Fin e → K)) (hA : Function.Surjective A) :
19     ∃ s : Fin e → Fin d, Function.Injective s ∧
20       Function.Surjective (fun u : Fin e → K => ∑ k, u k • A (Pi.single (s k) 1)) := by
21   classical
22   let v : Fin d → (Fin e → K) := fun i => A (Pi.single i 1)
23   have hv : Submodule.span K (Set.range v) = ⊤ := by
24     apply eq_top_iff.mpr
25     intro y _
26     obtain ⟨x, rfl⟩ := hA y
27     have hsum : ∑ i, x i • v i = A x := by
28       dsimp [v]
29       simp only [← map_smul, ← map_sum]
30       congr 1
31       simpa only [Pi.basisFun_repr, Pi.basisFun_apply] using
32         (Pi.basisFun K (Fin d)).sum_repr x
33     rw [← hsum]
34     exact Submodule.sum_mem _ (fun i _ => Submodule.smul_mem _ _
35       (Submodule.subset_span (Set.mem_range_self i)))
36   obtain ⟨κ, a, ha, hspan, hli⟩ := exists_linearIndependent' K v
37   let : Fintype κ := Fintype.ofInjective a ha
38   let b : Module.Basis κ K (Fin e → K) := Module.Basis.mk hli (by rw [hspan, hv])
39   have hcard : Fintype.card κ = e := by
40     rw [← Module.finrank_eq_card_basis b, Module.finrank_pi, Fintype.card_fin]
41   let ε : Fin e ≃ κ := Fintype.equivOfCardEq (by simp only [Fintype.card_fin, hcard])
42   let c : Module.Basis (Fin e) K (Fin e → K) := b.reindex ε.symm
43   refine ⟨a ∘ ε, ha.comp ε.injective, ?_⟩
44   intro y
45   refine ⟨fun i => c.repr y i, ?_⟩
46   simpa only [c, Module.Basis.reindex_apply, Equiv.symm_symm, b,
47     Module.Basis.mk_apply, Function.comp_apply, v] using c.sum_repr y
48 
49 /-- A coordinate selection can be extended to a permutation, putting a
50 surjective square block in the first coordinates. -/
51 theorem exists_permuted_columns
52     (A : (Fin (e + q) → K) →ₗ[K] (Fin e → K)) (hA : Function.Surjective A) :
53     ∃ σ : Equiv.Perm (Fin (e + q)),
54       Function.Surjective (fun u : Fin e → K =>
55         ∑ k, u k • A (Pi.single (σ (Fin.castAdd q k)) 1)) := by
56   obtain ⟨s, hs, hsurj⟩ := exists_selected_columns A hA
57   obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair (Fin.castAdd q) s
58     (Fin.castAdd_injective e q) hs
59   refine ⟨σ, ?_⟩
60   simpa only [hσ] using hsurj
61 
62 /-- Prime-field form used for an actual polynomial Jacobian modulo p. -/
63 theorem exists_prime_permuted_columns (p : ℕ) [Fact (Nat.Prime p)]
64     (A : (Fin (e + q) → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p))
65     (hA : Function.Surjective A) :
66     ∃ σ : Equiv.Perm (Fin (e + q)),
67       Function.Surjective (fun u : Fin e → ZMod p =>
68         ∑ k, u k • A (Pi.single (σ (Fin.castAdd q k)) 1)) :=
69   exists_permuted_columns A hA
70 
71 end Komorebi.PolynomialMinorSelection

Back to source controls