English
If R is Jacobson, S is a field, and S is a finite type algebra over R, then S is module-finite over R.
Русский
Если R — кольцо Якобсона, S — поле, и S является алгеброй конечного типа над R, то S является модулем конечной степени над R.
LaTeX
$$$Algebra.IsIntegral R S \\Rightarrow Module.Finite R S$$$
Lean4
theorem isMaximal_comap_C_of_isMaximal [IsJacobsonRing R] [Nontrivial R] (hP' : ∀ x : R, C x ∈ P → x = 0) :
IsMaximal (comap (C : R →+* R[X]) P : Ideal R) :=
by
let P' := comap (C : R →+* R[X]) P
have hP'_prime : P'.IsPrime := comap_isPrime C P
obtain ⟨⟨m, hmem_P⟩, hm⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_of_maximal P polynomial_not_isField)
have hm' : m ≠ 0 := by simpa [Submodule.coe_eq_zero] using hm
let φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P (C : R →+* R[X]) le_rfl
let a : R ⧸ P' := (m.map (Ideal.Quotient.mk P')).leadingCoeff
let M : Submonoid (R ⧸ P') := Submonoid.powers a
rw [← bot_quotient_isMaximal_iff]
have hp0 : a ≠ 0 := fun hp0' =>
hm' <|
map_injective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R))
((injective_iff_map_eq_zero (Ideal.Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R))).2 fun x hx => by
rwa [Quotient.eq_zero_iff_mem, (by rwa [eq_bot_iff] : (P.comap C : Ideal R) = ⊥)] at hx)
(by simpa only [a, leadingCoeff_eq_zero, Polynomial.map_zero] using hp0')
have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ => hp0 (pow_eq_zero hn)
suffices (⊥ : Ideal (Localization M)).IsMaximal
by
rw [←
IsLocalization.comap_map_of_isPrime_disjoint M (Localization M) ⊥ bot_prime
(disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))]
exact ((IsLocalization.isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp (by rwa [Ideal.map_bot])).1
let M' : Submonoid (R[X] ⧸ P) := M.map φ
have hM' : (0 : R[X] ⧸ P) ∉ M' := fun ⟨z, hz⟩ => hM (quotientMap_injective (_root_.trans hz.2 φ.map_zero.symm) ▸ hz.1)
suffices (⊥ : Ideal (Localization M')).IsMaximal
by
rw [le_antisymm bot_le
(comap_bot_le_of_injective _
(IsLocalization.map_injective_of_injective M (Localization M) (Localization M') quotientMap_injective))]
refine isMaximal_comap_of_isIntegral_of_isMaximal' _ ?_ ⊥
have isloc : IsLocalization (Submonoid.map φ M) (Localization M') := by infer_instance
exact
@isIntegral_isLocalization_polynomial_quotient R _ (Localization M) (Localization M') _ _ P m hmem_P _ _ _ isloc
rw [(map_bot.symm : (⊥ : Ideal (Localization M')) = Ideal.map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥)]
let bot_maximal := (bot_quotient_isMaximal_iff _).mpr hP
refine bot_maximal.map_bijective (algebraMap (R[X] ⧸ P) (Localization M')) ?_
apply IsField.localization_map_bijective hM'
rwa [← Quotient.maximal_ideal_iff_isField_quotient, ← bot_quotient_isMaximal_iff]
