finite_of_algHom_finiteType_of_isJacobsonRing

English

Let K be a Jacobson Noetherian ring and f: K → L, g: L → A be ring homomorphisms with (g ∘ f) of finite type. Then L is finite over K (i.e., L is a finite K-algebra).

Русский

Пусть K — кольцо Якобсона и Ноттерн, f: K → L, g: L → A — гомоморфизмы колец, such что композиция g ∘ f имеет конечный тип. Тогда L конечно над K.

LaTeX

$$$(g \circ f).\text{FiniteType} \Rightarrow f.Finite$$$

Lean4

/-- If `K` is a Jacobson Noetherian ring, `A` a nontrivial `K`-algebra of finite type,
then any `K`-subfield of `A` is finite over `K`. -/
nonrec theorem finite_of_algHom_finiteType_of_isJacobsonRing {K L A : Type*} [CommRing K] [Field L] [CommRing A]
    [IsJacobsonRing K] [IsNoetherianRing K] [Nontrivial A] (f : K →+* L) (g : L →+* A) (hfg : (g.comp f).FiniteType) :
    f.Finite := by
  algebraize [f, (g.comp f)]
  exact finite_of_algHom_finiteType_of_isJacobsonRing ⟨g, fun _ ↦ rfl⟩

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