FinitePresentation — Mathlib

English

An algebra homomorphism is of finite presentation precisely when its underlying ring homomorphism is finitely presented.

Русский

Гомоморфизм А-алгебры имеет конечную презентацию тогда и только тогда, когда соответствующий гомоморфизм колец имеет конечную презентацию.

LaTeX

$$$\\text{FinitePresentation}(f:A\\to[R] B) \\iff \\text{FinitePresentation}(f.toRingHom)$$$

Lean4

/-- An algebra morphism `A →ₐ[R] B` is of `AlgHom.FinitePresentation` if it is of finite
presentation as ring morphism. In other words, if `B` is finitely presented as `A`-algebra. -/
def FinitePresentation (f : A →ₐ[R] B) : Prop :=
  f.toRingHom.FinitePresentation

Похожие утверждения