English
If R is a maximal local subring of K, there exists a valuation subring R' of K whose local subring equals R.
Русский
Если R является максимальным локальным подкольцом K, то существует valuationSubring R' такого, что R'.toLocalSubring = R.
LaTeX
$$$\\forall R:\\mathrm{LocalSubring}(K), \\; \\mathrm{IsMax}(R) \\Rightarrow \\exists B:\\mathrm{ValuationSubring}(K), \\; B^{\\mathrm{toLocalSubring}} = R.$$$
Lean4
@[stacks 00IB]
theorem exists_valuationRing_of_isMax {R : LocalSubring K} (hR : IsMax R) :
∃ R' : ValuationSubring K, R'.toLocalSubring = R :=
by
suffices ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring from ⟨⟨R.toSubring, fun x ↦ or_iff_not_imp_left.mpr (this x)⟩, rfl⟩
intro x hx
have hx0 : x ≠ 0 := fun e ↦ hx (e ▸ zero_mem _)
apply mem_of_isMax_of_isIntegral hR
let S := Algebra.adjoin R.toSubring { x }
have : R.toSubring < S.toSubring :=
SetLike.lt_iff_le_and_exists.mpr
⟨fun r hr ↦ algebraMap_mem S ⟨r, hr⟩, ⟨x, Algebra.self_mem_adjoin_singleton _ _, hx⟩⟩
have := map_maximalIdeal_eq_top_of_isMax hR this
rw [Ideal.eq_top_iff_one] at this
obtain ⟨p, hp, hp'⟩ := (Algebra.mem_ideal_map_adjoin _ _).mp this
have := IsUnit.invertible (isUnit_iff_ne_zero.mpr hx0)
have : Polynomial.aeval (⅟x) (p - 1).reverse = 0 := by
simpa [← Polynomial.aeval_def, hp'] using Polynomial.eval₂_reverse_eq_zero_iff (algebraMap R.toSubring K) x (p - 1)
rw [invOf_eq_right_inv (mul_inv_cancel₀ hx0)] at this
have H : IsUnit ((p - 1).coeff 0) := by
by_contra h
simpa using sub_mem (hp 0) h
refine ⟨.C (H.unit⁻¹).1 * (p - 1).reverse, ?_, ?_⟩
· have : (p - 1).natTrailingDegree = 0 :=
by
simp only [Polynomial.natTrailingDegree_eq_zero, Polynomial.coeff_sub, Polynomial.coeff_one_zero, ne_eq,
sub_eq_zero]
exact .inr fun h ↦ (IsLocalRing.notMem_maximalIdeal.mpr isUnit_one (h ▸ hp 0))
rw [Polynomial.Monic.def, Polynomial.leadingCoeff_mul', Polynomial.reverse_leadingCoeff, Polynomial.trailingCoeff,
this]
· simp
· have : p - 1 ≠ 0 := fun e ↦ by simp [e] at H
simpa
· simp [← Polynomial.aeval_def, this]
