ax-grothendieck-finite.lean

import data.mv_polynomial.variables
import field_theory.is_alg_closed.basic
import data.finset.lattice
import data.zmod.basic

noncomputable theory

/-- the data of a polynomial map consists of n polynomials in n variables -/
@[simp] def poly_map (K : Type*) [comm_semiring K] (n : ℕ) : Type* :=
fin n → mv_polynomial (fin n) K

namespace poly_map

open mv_polynomial

variables {K : Type*} [comm_semiring K] {n : ℕ}

/-- a polynomial map evaluates those polynomials that it consists of -/
def eval {n : ℕ} : poly_map K n → (fin n → K) → (fin n → K) :=
λ ps as k, mv_polynomial.eval as (ps k)

lemma _root_.mv_polynomial.eval_mem {σ : Type*} [decidable_eq K]
  (p : mv_polynomial σ K) (s : subsemiring K)
  (hs : ∀ i, p.coeff i ∈ s) (v : σ → K) (hv : ∀ i, v i ∈ s) :
     mv_polynomial.eval v p ∈ s :=
begin
  classical,
  revert hs,
  refine mv_polynomial.induction_on''' p _ _,
  { intros a hs,
    simpa using hs 0 },
  { intros a b f ha hb0 ih hs,
    rw [map_add],
    refine subsemiring.add_mem _ _ _,
    { rw [eval_monomial],
      refine subsemiring.mul_mem _ _ _,
      { have := hs a,
        rwa [coeff_add, coeff_monomial, if_pos rfl, not_mem_support_iff.1 ha, add_zero] at this },
      { refine subsemiring.prod_mem _ (λ i hi, _),
        refine subsemiring.pow_mem _ _ _,
        exact hv _ } },
    { refine ih (λ i, _),
      have := hs i,
      rw [coeff_add, coeff_monomial] at this,
      split_ifs at this with h h,
      { subst h,
        rw [not_mem_support_iff.1 ha],
        exact subsemiring.zero_mem _ },
      { rwa zero_add at this } } }
end

lemma eval_mem_aux {σ : Type*} [decidable_eq K]
  (p : fin n → mv_polynomial σ K) (s : subsemiring K)
  (hs : ∀ i, ↑((p i).support.image (λ x, coeff x (p i))) ⊆ (s : set K)) :
  ∀ (v : σ → K) (hv : ∀ i, v i ∈ s) (i : fin n), mv_polynomial.eval v (p i) ∈ s :=
begin
  induction n with n ih,
  { intros _ _ i,
    exact i.elim0 },
  { intros v hv i,
    refine fin.cases _ _ i,
    { apply mv_polynomial.eval_mem (p 0) s,
      { intros m,
        by_cases hm : m ∈ (p 0).support,
        { exact hs 0 (finset.mem_image.2 ⟨m, hm, rfl⟩) },
        { rw [not_mem_support_iff.1 hm],
          exact subsemiring.zero_mem _ } },
      { assumption } },
    { intro j,
      apply ih (λ i, p i.succ) _ _ hv,
      intro k,
      apply hs } }
end

lemma eval_mem [decidable_eq K]
  (p : poly_map K n) (s : subsemiring K)
  (hs : ∀ i, ↑((p i).support.image (λ x, coeff x (p i))) ⊆ (s : set K)) :
  ∀ (v : fin n → K) (hv : ∀ i, v i ∈ s) (i : fin n), mv_polynomial.eval v (p i) ∈ s :=
eval_mem_aux p s hs

/-- Any injective polynomial map over an algerbaically closed field of char p is surjective -/
lemma Ax_Groth_of_locally_finite {K : Type*} [comm_ring K] {p : ℕ} [hp : fact p.prime]
  [algebra (zmod p) K] (alg : algebra.is_algebraic (zmod p) K)
  (ps : poly_map K n) (hinj : function.injective (eval ps)) :
  function.surjective (eval ps) :=
begin
  have is_int : ∀ x : K, is_integral (zmod p) x, 
    from λ x, is_algebraic_iff_is_integral.1 (alg x),
  classical,
  intros v,
  let s : finset K :=
    finset.bUnion (finset.univ : finset (fin n))
      (λ i, (ps i).support.image (λ x, coeff x (ps i)))
    ∪ (finset.univ : finset (fin n)).image v,
  have hs₁ : ∀ (i : fin n),
    (finset.image (λ (x : fin n →₀ ℕ), coeff x (ps i)) (ps i).support : set K) ⊆
      subsemiring.closure (s : set K),
    from λ j x hx, subsemiring.subset_closure
      (finset.mem_union_left _
        (finset.mem_bUnion.2 ⟨j, finset.mem_univ _, hx⟩)),
  have hv₁ : ∀ i, v i ∈ subsemiring.closure (s : set K),
    from λ j, subsemiring.subset_closure
        (finset.mem_union_right _
          (finset.mem_image.2 ⟨j, finset.mem_univ _, rfl⟩)),
  have hs : ∀ i, eval ps v i ∈ subsemiring.closure (s : set K),
    from eval_mem ps _ hs₁ v hv₁,
  letI : fintype (subsemiring.closure (s : set K)),
  { letI := is_noetherian_adjoin_finset s (λ x _, is_int x),
    letI := module.is_noetherian.finite (zmod p) (algebra.adjoin (zmod p) (s : set K)), 
    have alg_fintype := finite_dimensional.fintype_of_fintype 
      (zmod p) (algebra.adjoin (zmod p) (s : set K)),
    have hsubset : subsemiring.closure (s : set K) ≤ 
      (algebra.adjoin (zmod p) (s : set K)).to_subsemiring,
      from subsemiring.closure_le.2 
        (galois_connection.le_u_l algebra.gc _),
    exact (set.finite.subset ⟨alg_fintype⟩ hsubset).fintype },
  let res : (fin n → subsemiring.closure (s : set K)) →
      (fin n → subsemiring.closure (s : set K)) :=
    λ x i, ⟨eval ps (λ j, (x j)) i, eval_mem _ _ hs₁ _ (λ j, (x j).2) _⟩,
  have hres_inj : function.injective res,
  { intros x y hxy,
    funext i,
    ext,
    simp only [res, subtype.ext_iff, function.funext_iff] at hxy,
    exact congr_fun (hinj (funext hxy)) i },
  have hres_surj : function.surjective res,
    from fintype.injective_iff_surjective.1 hres_inj,
  cases hres_surj (λ i, ⟨v i, hv₁ i⟩) with w hw,
  use λ i, w i,
  simp only [res, subtype.ext_iff, function.funext_iff] at hw,
  exact funext hw
end

end poly_map