English
If A has finite presentation, then B ⊗_R A has finite presentation over B.
Русский
Если A имеет конечную презентацию над R, то B ⊗_R A имеет конечную презентацию над B.
LaTeX
$$$[\\text{Algebra.FinitePresentation } R A] \\Rightarrow \\text{Algebra.FinitePresentation } B (B\\otimes_R A)$$$
Lean4
instance baseChange [FinitePresentation R A] : FinitePresentation B (B ⊗[R] A) :=
by
obtain ⟨n, f, hsurj, hfg⟩ := ‹FinitePresentation R A›
let g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := Algebra.TensorProduct.map (AlgHom.id B B) f
have hgsurj : Function.Surjective g := Algebra.FiniteType.baseChangeAux_surj B hsurj
have hker_eq : RingHom.ker g = Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker f) :=
Algebra.TensorProduct.lTensor_ker f hsurj
have hfgg : Ideal.FG (RingHom.ker g) := by
rw [hker_eq]
exact Ideal.FG.map hfg _
let g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := AlgHom.comp g (MvPolynomial.algebraTensorAlgEquiv R B).symm.toAlgHom
refine ⟨n, g', ?_, Ideal.fg_ker_comp _ _ ?_ hfgg ?_⟩
· simp_all [g, g']
· change Ideal.FG (RingHom.ker (AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)))
simp only [RingHom.ker_equiv]
exact Submodule.fg_bot
· simpa using EquivLike.surjective _
