English
A refined version of the previous result, providing an equivalence describing when a first-order sentence realized by the generic polynomial map surjectivity holds, in terms of surjectivity of a constructed map for all assignments.
Русский
Уточненная версия предыдущего вывода, устанавливающая эквивалентность для реализации предложения первого порядка о сюръективности полиномов.
LaTeX
$$$ \\text{(realization equivalence for } \\text{genericPolyMapSurjOnOfInjOn}) $$$
Lean4
theorem realize_genericPolyMapSurjOnOfInjOn [Finite ι] (φ : ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) :
(K ⊨ genericPolyMapSurjOnOfInjOn φ mons) ↔
∀ (v : α → K) (p : { p : ι → MvPolynomial ι K // (∀ i, (p i).support ⊆ mons i) }),
let f : (ι → K) → (ι → K) := fun v i => eval v (p.1 i)
let S : Set (ι → K) := {x | φ.Realize (Sum.elim v x)}
S.MapsTo f S → S.InjOn f → S.SurjOn f S :=
by
classical
have injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → (ι → K)), S.InjOn f ↔ ∀ x y, x ∈ S → y ∈ S → f x = f y → x = y :=
by simp [Set.InjOn]; tauto
simp only [Sentence.Realize, Formula.Realize, genericPolyMapSurjOnOfInjOn, Formula.relabel, Function.comp_def,
Sum.map, id_eq, Equiv.sumAssoc, Equiv.coe_fn_symm_mk, Sum.elim_inr, realize_iAlls, realize_imp, realize_relabel,
Fin.natAdd_zero, realize_subst, realize_iInf, realize_bdEqual, Term.realize_relabel,
Equiv.forall_congr_left (Equiv.curry (Fin 2) ι K), Equiv.curry_symm_apply, Fin.forall_fin_succ_pi,
Fin.forall_fin_zero_pi, realize_iExs, realize_inf, Sum.forall_sum, Set.MapsTo, Set.mem_setOf_eq, injOnAlt,
funext_iff, Set.SurjOn, Set.image, Set.subset_def, Equiv.forall_congr_left (mvPolynomialSupportLEEquiv mons)]
simp +singlePass only [← Sum.elim_comp_inl_inr]
-- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)
simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, Fin.castAdd_zero, Fin.cast_eq_self, Nat.add_zero,
Term.realize_var, Term.realize_relabel, realize_termOfFreeCommRing, lift_genericPolyMap, Nat.reduceAdd, Fin.isValue,
Function.uncurry_apply_pair, Fin.cons_zero, Fin.cons_one, ↓reduceIte, one_ne_zero]
