English
There exists s and a injective integral algebra hom g from a polynomial ring in Fin s to R, as in Noether normalization.
Русский
Существует s и инъективный интегральный алгебра-гомоморфизм из полиномиальной кольцевой области в R.
LaTeX
$$∃ s ≤ n, ∃ g: (MvPolynomial (Fin s) k) →ₐ[k] R, Injective g ∧ g.IsIntegral$$
Lean4
/-- There exists some `s ≤ n` and an integral injective algebra homomorphism
from `k[X_0,...,X_(s-1)]` to `k[X_0,...,X_(n-1)]/I` if `I ≠ ⊤`. -/
theorem exists_integral_inj_algHom_of_quotient (I : Ideal (MvPolynomial (Fin n) k)) (hi : I ≠ ⊤) :
∃ s ≤ n, ∃ g : (MvPolynomial (Fin s) k) →ₐ[k] ((MvPolynomial (Fin n) k) ⧸ I), Function.Injective g ∧ g.IsIntegral :=
by
induction n with
|
zero =>
refine ⟨0, le_rfl, Quotient.mkₐ k I, fun a b hab ↦ ?_, isIntegral_of_surjective _ (Quotient.mkₐ_surjective k I)⟩
rw [Quotient.mkₐ_eq_mk, Ideal.Quotient.eq] at hab
by_contra neq
have eq := eq_C_of_isEmpty (a - b)
have ne : coeff 0 (a - b) ≠ 0 := fun h ↦ h ▸ eq ▸ sub_ne_zero_of_ne neq <| map_zero _
obtain ⟨c, _, eqr⟩ := isUnit_iff_exists.mp ne.isUnit
have one : c • (a - b) = 1 := by rw [MvPolynomial.smul_eq_C_mul, eq, ← RingHom.map_mul, eqr, MvPolynomial.C_1]
exact hi ((eq_top_iff_one I).mpr (one ▸ I.smul_of_tower_mem c hab))
| succ d hd =>
by_cases eqi : I = 0
· have bij : Function.Bijective (Quotient.mkₐ k I) := (Quotient.mk_bijective_iff_eq_bot I).mpr eqi
exact ⟨d + 1, le_rfl, _, bij.1, isIntegral_of_surjective _ bij.2⟩
· obtain ⟨f, fi, fne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot eqi
set ϕ := kerLiftAlg <| hom2 f I
have := Quotient.nontrivial hi
obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)
have comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k <| ker <| hom2 f I) = (hom2 f I) :=
AlgHom.ext fun a ↦ by simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk]
exact
⟨s, by cutsat, ϕ.comp g, (ϕ.coe_comp g) ▸ (kerLiftAlg_injective _).comp injg,
intg.trans _ _ <| (comp ▸ hom2_isIntegral f I fne fi).tower_top _ _⟩
