finiteType — Mathlib

English

A module finite over a base ring remains finite type after a base change to any algebra B.

Русский

Модуль, конечный над базовым кольцом, сохраняет конечность по типу после базового изменения на любую алгебру B.

LaTeX

$$$\\text{Module.Finite}.\\text{finiteType}$ under base change: $B\\otimes_R A$ is finite type over B$$

Lean4

instance (priority := 100) finiteType {R : Type*} (A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
    [hRA : Module.Finite R A] : Algebra.FiniteType R A :=
  ⟨Subalgebra.fg_of_submodule_fg hRA.1⟩

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