English
If A is an R-algebra finitely presented and B is an A-algebra finitely presented, then B is finitely presented as an R-algebra.
Русский
Если A — алгебра над R с конечной презентацией, и B — A-алгебра c конечной презентацией, то B имеет конечную презентацию над R.
LaTeX
$$$[\\text{Algebra } A B] [\\text{IsScalarTower } R A B] [\\text{FinitePresentation } R A] [\\text{FinitePresentation } A B] :\\; \\text{FinitePresentation } R B$$$
Lean4
/-- If `A` is an `R`-algebra and `S` is an `A`-algebra, both finitely presented, then `S` is
finitely presented as `R`-algebra. -/
theorem trans [Algebra A B] [IsScalarTower R A B] [FinitePresentation R A] [FinitePresentation A B] :
FinitePresentation R B := by
have hfpB : FinitePresentation A B := inferInstance
obtain ⟨n, I, e, hfg⟩ := iff.1 hfpB
letI : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) := (mvPolynomial_of_finitePresentation _).quotient hfg
exact equiv (e.restrictScalars R)
