English
The C : R → R[X] case of Chevalley's theorem with a complexity bound asserts existence of a bound T describing the image of a constructible set S under comap Polynomial.C with explicit degree and growth control.
Русский
Случай функции C : R → R[X] в теореме Чевалле о конструктивности с ограничением сложности утверждает существование множества описывающего образ конструктируемого множества S под comap Polynomial.C с явным ограничением степеней и роста.
LaTeX
$$∃ T,\\; comap Polynomial.C '' S.toSet = T.toSet ∧ ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ i, C.g i ∈ M ^ S.degBound ^ S.degBound$$
Lean4
/-- The `C : R → R[X]` case of **Chevalley's theorem** with complexity bound. -/
theorem chevalley_polynomialC {R : Type*} [CommRing R] (M : Submodule ℤ R) (hM : 1 ∈ M) (S : ConstructibleSetData R[X])
(hS : ∀ C ∈ S, ∀ j k, (C.g j).coeff k ∈ M) :
∃ T : ConstructibleSetData R,
comap Polynomial.C '' S.toSet = T.toSet ∧ ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ i, C.g i ∈ M ^ S.degBound ^ S.degBound :=
by
classical
choose f hf₁ hf₂ hf₃ using fun C : BasicConstructibleSetData R[X] ↦ statement (R₀ := ℤ) ⟨C.g⟩ C.f
refine ⟨S.biUnion f, ?_, ?_⟩
·
simp only [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.image_iUnion,
Finset.set_biUnion_biUnion, hf₁]
· simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
intro x y hy hx
have H : degBound ⟨y.g⟩ ≤ S.degBound := Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
gcongr
· simpa [Submodule.one_eq_span]
· refine Submodule.span_le.mpr ?_
simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]
· delta powBound
by_cases h : S.degBound = 0
· have : degBound ⟨y.g⟩ = 0 := by nlinarith
rw [h, this]
gcongr
rwa [Nat.one_le_iff_ne_zero]
