of_finiteType — Mathlib

English

If A is Noetherian, then every A→B that is of finite type is also finitely presented as an A-algebra map, and conversely.

Русский

Пусть A - кольцо Нётерово. Тогда отображение A → B является конечной по порождаемости тогда и только тогда, когда оно является конечной презентацией как A-алгебра-морфизм.

LaTeX

$$$\\text{If } A \\text{ is Noetherian, then } f \\text{ is of finite type } \\iff f \\text{ is of finite presentation}. $$$

Lean4

theorem of_finiteType [IsNoetherianRing A] {f : A →+* B} : f.FiniteType ↔ f.FinitePresentation :=
  @Algebra.FinitePresentation.of_finiteType A B _ _ f.toAlgebra _

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