FinEqs main file

Vendored from nasqret/fineqs. See LeanPool/Fineqs.lean for the project overview.

def LeanPool.Fineqs.ZeroSet {X : Type u_1} {F : Type u_2} [Zero F] (S : Set (X → F)) : Set X

The zero set of a set of functions X → F.

Equations

• LeanPool.Fineqs.ZeroSet S = {x : X | ∀ f ∈ S, f x = 0}

theorem LeanPool.Fineqs.card_projectivization_minus_point {F : Type u_1} [Field F] [Fintype F] (n : ℕ) (α : Projectivization F (Fin (n + 1) → F)) : Nat.card { x : Projectivization F (Fin (n + 1) → F) // x ≠ α } = (Fintype.card F ^ (n + 1) - Fintype.card F) / (Fintype.card F - 1)

Cardinality of projective space minus a point: |P^n(F) \ {α}| = (q^{n+1} - q) / (q - 1).

theorem LeanPool.Fineqs.card_projectivization_eq_bound_add_one {F : Type u_1} [Field F] [Fintype F] (n : ℕ) : Nat.card (Projectivization F (Fin (n + 1) → F)) = (Fintype.card F ^ (n + 1) - Fintype.card F) / (Fintype.card F - 1) + 1

The cardinality of P^n(F) in the form used by the sharpness example.

theorem LeanPool.Fineqs.theorem_1_aux {F : Type u_1} [Field F] [Fintype F] {X : Type u_2} [Finite X] (n : ℕ) (f : X → Fin (n + 1) → F) (hX : Nat.card X ≤ (Fintype.card F ^ (n + 1) - Fintype.card F) / (Fintype.card F - 1)) : ∃ (M : (Fin (n + 1) → F) →ₗ[F] Fin n → F), {x : X | M (f x) = 0} = {x : X | f x = 0}

Auxiliary form of Theorem 1: a map into F^(n+1) over a small finite set admits a linear projection to F^n whose kernel misses all nonzero image points.

theorem LeanPool.Fineqs.theorem_1_base_case {F : Type u_1} [Field F] [Fintype F] {X : Type u_2} [Finite X] (n : ℕ) (S : Set (X → F)) (hS : S.Finite) (h_card : S.ncard = n + 1) (hX : Nat.card X ≤ (Fintype.card F ^ (n + 1) - Fintype.card F) / (Fintype.card F - 1)) : ∃ T ⊆ ↑(Submodule.span F S), T.Finite ∧ T.ncard ≤ n ∧ ZeroSet T = ZeroSet S

Base case of Theorem 1: n + 1 equations over a small finite set can be replaced by at most n equations in their span.

theorem LeanPool.Fineqs.theorem_1 {F : Type u_1} [Field F] [Fintype F] {X : Type u_2} [Finite X] (n : ℕ) (S : Set (X → F)) (hS : S.Finite) (hn : S.ncard > n) (hX : Nat.card X ≤ (Fintype.card F ^ (n + 1) - Fintype.card F) / (Fintype.card F - 1)) : ∃ T ⊆ ↑(Submodule.span F S), T.Finite ∧ T.ncard ≤ n ∧ ZeroSet T = ZeroSet S

Theorem 1: over a small finite set, any finite family of more than n functions can be reduced to at most n functions in its span without changing its zero set.

theorem LeanPool.Fineqs.corollary_2 {K : Type u_2} [Field K] [Finite K] (n : ℕ) (hn : n > 0) (V : Type u_3) [AddCommGroup V] [Module K V] (φ : V →ₗ[K] (Fin n → K) → K) (S : Set V) (hS : S.Finite) : ∃ (T : Set V), T.Finite ∧ T.ncard ≤ n ∧ T ⊆ ↑(Submodule.span K S) ∧ ZeroSet (⇑φ '' T) = ZeroSet (⇑φ '' S)

Corollary 2: zero loci in affine n-space over a finite field can be defined using at most n members of the original span.

theorem LeanPool.Fineqs.corollary_3 {K : Type u_2} [Field K] [Finite K] (n : ℕ) (V : Type u_3) [AddCommGroup V] [Module K V] (φ : V →ₗ[K] Projectivization K (Fin (n + 1) → K) → K) (S : Set V) (hS : S.Finite) (h_nonempty : ZeroSet (⇑φ '' S) ≠ ∅) : ∃ (T : Set V), T.Finite ∧ T.ncard ≤ n ∧ T ⊆ ↑(Submodule.span K S) ∧ ZeroSet (⇑φ '' T) = ZeroSet (⇑φ '' S)

Corollary 3: a nonempty projective zero locus in P^n(F) can be defined using at most n members of the original span.

theorem LeanPool.Fineqs.prop_1 {F : Type u_1} [Field F] [Fintype F] (n : ℕ) (hn : n > 0) : ∃ (X : Set (Fin (n + 1) → F)) (f : Fin (n + 1) → ↑X → F), X.ncard = (Fintype.card F ^ (n + 1) - Fintype.card F) / (Fintype.card F - 1) + 1 ∧ (∀ (x : ↑X), ∃ (i : Fin (n + 1)), f i x ≠ 0) ∧ ∀ (g : Fin n → ↑X → F), (∀ (j : Fin n), g j ∈ Submodule.span F (Set.range f)) → ∃ (x : ↑X), ∀ (j : Fin n), g j x = 0

Proposition 1: the cardinality bound in Theorem 1 is sharp.

theorem LeanPool.Fineqs.remark_example {F : Type u_1} [Field F] [Fintype F] (n : ℕ) (hn : n > 0) : have f := fun (i : Fin n) (x : Fin n → F) => x i; ZeroSet (Set.range f) = {0} ∧ ∀ (g : Fin (n - 1) → (Fin n → F) → F), (∀ (j : Fin (n - 1)), g j ∈ Submodule.span F (Set.range f)) → (ZeroSet (Set.range g)).ncard ≥ Fintype.card F

The coordinate functions on affine n-space need n equations to cut out the origin: any n - 1 linear combinations have at least |F| common zeros.