FiniteType — Mathlib

English

A ring homomorphism given by an algebra map is of finite type iff the target is a finitely generated algebra over the source.

Русский

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

LaTeX

$$(algebraMap\\ A\\ B).FiniteType ↔ Algebra.FiniteType A B$$

Lean4

/-- A ring morphism `A →+* B` is of `FiniteType` if `B` is finitely generated as `A`-algebra. -/
@[algebraize]
def FiniteType (f : A →+* B) : Prop :=
  @Algebra.FiniteType A B _ _ f.toAlgebra

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