Artinian rings over Jacobson rings

Main results

• Module.finite_iff_isArtinianRing: If A is a finite type algebra over an Artinian ring R, then A is finite over R if and only if A is an Artinian ring.

theorem Module.finite_of_isSemisimpleRing (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [Algebra.FiniteType R A] [IsJacobsonRing R] [IsSemisimpleRing A] : Module.Finite R A

theorem Module.finite_of_isArtinianRing (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [Algebra.FiniteType R A] [IsJacobsonRing R] [IsArtinianRing A] : Module.Finite R A

If A is a finite type algebra over R, then A is an Artinian ring and R is Jacobson implies A is finite over R.

theorem Module.finite_iff_isArtinianRing (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [Algebra.FiniteType R A] [IsArtinianRing R] : Module.Finite R A ↔ IsArtinianRing A

If A is a finite type algebra over an Artinian ring R, then A is finite over R if and only if A is an Artinian ring.

theorem Module.finite_iff_krullDimLE_zero (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [Algebra.FiniteType R A] [IsArtinianRing R] : Module.Finite R A ↔ Ring.KrullDimLE 0 A

If A is a finite type algebra over an Artinian ring R, then A is finite over R if and only if dim A = 0.