finite_iff_finiteType_of_isJacobsonRing

English

There is equivalence between RingHom being finite and finiteType when the target is a field and source Jacobson.

Русский

Существуют эквивалентности между конечностью RingHom и конечным типом в случае целевого поля и источника Якобсонова.

LaTeX

$$f.Finite \\leftrightarrow f.FiniteType$$

Lean4

/-- If `f : R →+* S` is a ring homomorphism from a Jacobson ring to a field,
then it is finite if and only if it is finite type.
-/
theorem finite_iff_finiteType_of_isJacobsonRing {R S : Type*} [CommRing R] [IsJacobsonRing R] [Field S] {f : R →+* S} :
    f.Finite ↔ f.FiniteType :=
  ⟨RingHom.FiniteType.of_finite, by intro; algebraize [f]; exact finite_of_finite_type_of_isJacobsonRing R S⟩

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