finite_iff_isIntegral_and_finiteType

English

For an algebra A over R, finite generation of A as an R-module is equivalent to A being integral over R together with finite type over R.

Русский

Для алгебры A над R конечная порождаемость как R-модуля эквивалентна тому, что A интегральна над R и имеет конечный тип над R.

LaTeX

$$$Module.Finite\\ R A \\;\\ \\leftrightarrow\\; (Algebra.IsIntegral R A) \\land (Algebra.FiniteType R A)$$$

Lean4

/-- finite = integral + finite type -/
theorem finite_iff_isIntegral_and_finiteType : Module.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A :=
  ⟨fun _ ↦ ⟨⟨.of_finite R⟩, inferInstance⟩, fun ⟨h, _⟩ ↦ h.finite⟩

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