finite_of_isSemisimpleRing — Mathlib

English

If A is a finite type algebra over a Jacobson ring R and A is semisimple, then A is finite over R, and conversely under suitable hypotheses.

Русский

Если A — алгебра конечного типа над кольцом Якобсона R и A — полносемплирована, то A конечно над R, и наоборот при подходящих условиях.

LaTeX

$$Module.Finite R A$$

Lean4

theorem finite_of_isSemisimpleRing [IsJacobsonRing R] [IsSemisimpleRing A] : Module.Finite R A :=
  (Finite.equiv_iff <| (AlgEquiv.ofRingEquiv (f := IsArtinianRing.equivPi A) fun _ ↦ rfl).toLinearEquiv).mpr <|
    have (I : MaximalSpectrum A) := finite_of_finite_type_of_isJacobsonRing R (A ⧸ I.asIdeal)
    Finite.pi

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