English
If R is a maximal local subring and S a larger subring, the image of the maximal ideal under the inclusion is the top ideal.
Русский
Если R — максимальное локальное подполье, и S больше, образ максимальной идеала R по включению — тождественный верхний идеал.
LaTeX
$$((maximalIdeal R.toSubring).map (Subring.inclusion hS.le)) = ⊤$$
Lean4
theorem map_maximalIdeal_eq_top_of_isMax {R : LocalSubring K} (hR : IsMax R) {S : Subring K} (hS : R.toSubring < S) :
(maximalIdeal R.toSubring).map (Subring.inclusion hS.le) = ⊤ :=
by
let mR := (maximalIdeal R.toSubring).map (Subring.inclusion hS.le)
by_contra h_is_not_top
obtain ⟨M, h_is_max, h_incl⟩ := Ideal.exists_le_maximal _ h_is_not_top
let fSₘ : LocalSubring K := LocalSubring.ofPrime S M
have h_RleSₘ : R ≤ fSₘ := by
refine ⟨hS.le.trans (LocalSubring.le_ofPrime _ _), ⟨?_⟩⟩
rintro ⟨a, h_a_inR⟩ h_fa_isUnit
apply(IsLocalization.AtPrime.isUnit_to_map_iff _ M ⟨a, hS.le h_a_inR⟩).mp at h_fa_isUnit
by_contra h
rw [← mem_nonunits_iff, ← mem_maximalIdeal] at h
apply Ideal.mem_map_of_mem (Subring.inclusion hS.le)at h
exact h_fa_isUnit (h_incl h)
have h_RneSₘ : R ≠ fSₘ := fun e ↦ (hS.trans_le (LocalSubring.le_ofPrime S M)).ne congr(($e).toSubring)
exact h_RneSₘ (hR.eq_of_le h_RleSₘ)
