Lean4
/-- The `C : R → R[X₁, ..., Xₘ]` case of **Chevalley's theorem** with complexity bound. -/
theorem chevalley_mvPolynomialC {M : Submodule ℤ R} (hM : 1 ∈ M) (k : ℕ) (d : Multiset (Fin n))
(S : ConstructibleSetData (MvPolynomial (Fin n) R)) (hSn : ∀ C ∈ S, C.n ≤ k)
(hS : ∀ C ∈ S, ∀ j, C.g j ∈ coeffsIn _ M ⊓ (degreesLE _ _ d).restrictScalars _) :
∃ T : ConstructibleSetData R,
comap MvPolynomial.C '' S.toSet = T.toSet ∧
∀ C ∈ T,
C.n ≤ numBound k (fun i ↦ 1 + (d.map Fin.val).count i) n ∧
∀ i, C.g i ∈ M ^ (degBound k (fun i ↦ 1 + (d.map Fin.val).count i) n) :=
by
classical
induction n generalizing k M with
| zero =>
refine ⟨(S.map (isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩
· rw [ConstructibleSetData.toSet_map]
change _ = (comapEquiv (isEmptyRingEquiv _ _)).symm ⁻¹' _
rw [← OrderIso.image_eq_preimage]
rfl
· simp only [ConstructibleSetData.map, RingEquiv.toRingHom_eq_coe, Finset.mem_image, comp_apply,
BasicConstructibleSetData.map, RingHom.coe_coe, isEmptyRingEquiv_eq_coeff_zero, pow_one, numBound_zero,
degBound_zero, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
exact fun a haS ↦ ⟨hSn a haS, fun i ↦ (hS a haS i).1 0⟩
| succ n IH => ?_
let e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := finSuccEquiv R n
let S' := S.map e.toRingHom
have hS' : S'.degBound ≤ k * (1 + d.count 0) :=
by
apply Finset.sup_le fun x hxS ↦ ?_
simp only [ConstructibleSetData.map, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe,
AlgEquiv.toRingEquiv_toRingHom, Finset.mem_image, BasicConstructibleSetData.map, RingHom.coe_coe, S'] at hxS
obtain ⟨C, hxS, rfl⟩ := hxS
trans ∑ i : Fin C.n, (1 + d.count 0)
· gcongr with j hj
simp only [e, comp_apply]
by_cases hgj : C.g j = 0
· rw [hgj, map_zero]
simp
rw [degree_finSuccEquiv hgj, WithBot.succ_natCast, add_comm]
simp only [Nat.cast_id, add_le_add_iff_left, degreeOf_def]
exact Multiset.count_le_of_le _ (hS _ hxS _).2
· simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul]
gcongr
exact hSn _ hxS
let B : Multiset (Fin n) := (d.toFinsupp.comapDomain Fin.succ (Fin.succ_injective _).injOn).toMultiset
obtain ⟨T, hT₁, hT₂⟩ :=
chevalley_polynomialC (R := MvPolynomial (Fin n) R) (coeffsIn _ M ⊓ (degreesLE _ _ B).restrictScalars ℤ)
(by simpa [MvPolynomial.coeff_one, apply_ite] using hM) S'
(fun x hxS j k ↦
by
simp only [ConstructibleSetData.map, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe,
AlgEquiv.toRingEquiv_toRingHom, Finset.mem_image, BasicConstructibleSetData.map, RingHom.coe_coe, S',
e] at hxS
obtain ⟨C, hxS, rfl⟩ := hxS
simp only [comp_apply, Submodule.mem_inf, mem_coeffsIn, Submodule.restrictScalars_mem, mem_degreesLE]
constructor
· intro d
simp only [finSuccEquiv_coeff_coeff]
exact (hS _ hxS _).1 _
· simp only [B]
replace hS := (hS _ hxS j).2
simp only [Submodule.coe_restrictScalars, SetLike.mem_coe, mem_degreesLE, Multiset.le_iff_count,
Finsupp.count_toMultiset, Finsupp.comapDomain_apply, Multiset.toFinsupp_apply, ← degreeOf_def] at hS ⊢
intro a
exact (degreeOf_coeff_finSuccEquiv (C.g j) a k).trans (hS _))
let N := (k * (1 + d.count 0)) ^ (k * (1 + d.count 0))
have (C) (hCT : C ∈ T) (a) : C.g a ∈ coeffsIn (Fin n) (M ^ N) ⊓ (degreesLE R (Fin n) (N • B)).restrictScalars ℤ :=
by
refine SetLike.le_def.mp ?_ ((hT₂ C hCT).2 a)
refine pow_inf_le.trans (inf_le_inf ?_ ?_)
· refine (pow_le_pow_right' ?_ (Nat.pow_self_mono hS')).trans le_coeffsIn_pow
simpa [MvPolynomial.coeff_one, apply_ite] using hM
· rw [degreesLE_nsmul, Submodule.restrictScalars_pow Nat.pow_self_pos.ne']
refine pow_le_pow_right' ?_ (Nat.pow_self_mono hS')
simp
have h1M : 1 ≤ M := Submodule.one_le.mpr hM
obtain ⟨U, hU₁, hU₂⟩ :=
IH (M := M ^ N) (SetLike.le_def.mp (le_self_pow h1M Nat.pow_self_pos.ne') hM) _ _ T (fun C hCT ↦ (hT₂ C hCT).1)
(fun C hCT k ↦ this C hCT k)
simp only [Multiset.map_nsmul, Multiset.count_nsmul, ← pow_mul, N] at hU₂
have : ∀ i < n + 1, i.casesOn (1 + d.count 0) (1 + (B.map Fin.val).count ·) ≤ 1 + (d.map Fin.val).count i :=
by
intro t ht
change _ ≤ 1 + (d.map Fin.val).count (Fin.mk t ht).val
rw [Multiset.count_map_eq_count' _ _ Fin.val_injective]
obtain - | t := t
· exact le_rfl
· simp only [add_lt_add_iff_right] at ht
change 1 + (B.map Fin.val).count (Fin.mk t ht).val ≤ _
rw [Multiset.count_map_eq_count' _ _ Fin.val_injective]
simp [B]
refine ⟨U, ?_, fun C hCU ↦ ⟨(hU₂ C hCU).1.trans ?_, fun i ↦ pow_le_pow_right' h1M ?_ <| (hU₂ C hCU).2 i⟩⟩
· unfold S' at hT₁
rw [← hU₁, ← hT₁, ← Set.image_comp, ← ContinuousMap.coe_comp, ← comap_comp, ConstructibleSetData.toSet_map]
change _ = _ '' ((comapEquiv e.toRingEquiv).symm ⁻¹' _)
rw [← OrderIso.image_eq_preimage, Set.image_image]
simp only [comapEquiv_apply, ← comap_apply, ← comap_comp_apply]
congr!
exact e.symm.toAlgHom.comp_algebraMap.symm
· refine
(numBound_mono hS' _ fun _ _ ↦ ?_).trans
((numBound_casesOn_succ k _ _ _).symm.trans_le (numBound_mono le_rfl _ this))
simp +contextual [mul_add, Nat.one_le_iff_ne_zero]
· refine
(Nat.mul_le_mul le_rfl (degBound_le_degBound hS' _ fun _ _ ↦ ?_)).trans
((degBound_casesOn_succ k _ _ _).symm.trans_le (degBound_le_degBound le_rfl _ this))
simp +contextual [mul_add, Nat.one_le_iff_ne_zero]
