Theorems · Theorem · commutative algebra

Algebra.IsIntegral.finite

∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] [h' : Algebra.FiniteType R A], Module.Finite R A

The [Kurosh problem](https://en.wikipedia.org/wiki/Kurosh_problem) asks to show that this is still true when A is not necessarily commutative and R is a field, but it has been solved in the negative. See https://arxiv.org/pdf/1706.02383.pdf for criteria for a finitely generated algebraic (= integral) algebra over a field to be finite dimensional. This could be an instance, but we tend to go from Module.Finite to IsIntegral/IsAlgebraic, and making it an instance will cause the search to be complicated a lot.

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Cited by

5 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAlgebra.IsIntegralAlgebra.FiniteType