English
If R is a ring and A finitely presented, then the polynomial ring in finitely many indeterminates over A is finitely presented as an R-algebra.
Русский
Если R — кольцо и A имеет конечную презентацию, то кольцо многочленов в конечном числе переменных над A является finitely presented как R-алгебра.
LaTeX
$$$[\\text{FinitePresentation } R A] \\Rightarrow \\text{FinitePresentation } R (\\mathrm{MvPolynomial } \\iota A)\\quad (\\iota\\text{ finite})$$$
Lean4
/-- If `A` is a finitely presented `R`-algebra, then `MvPolynomial (Fin n) A` is finitely presented
as `R`-algebra. -/
theorem mvPolynomial_of_finitePresentation [FinitePresentation R A] (ι : Type v) [Finite ι] :
FinitePresentation R (MvPolynomial ι A) :=
by
have hfp : FinitePresentation R A := inferInstance
rw [iff_quotient_mvPolynomial'] at hfp ⊢
classical
-- Make universe level `v` explicit so it matches that of `ι`
obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp
let g := (MvPolynomial.mapAlgHom f).comp (MvPolynomial.sumAlgEquiv R ι ι').toAlgHom
cases nonempty_fintype (ι ⊕ ι')
refine
⟨ι ⊕ ι', by infer_instance, g, (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩
· rw [AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]
exact Submodule.fg_bot
· rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]
exact hf_ker.map MvPolynomial.C
