isMax_toLocalSubring — Mathlib

English

For any valuation subring R, the associated local subring R.toLocalSubring is maximal.

Русский

Для любой дуальной верифицируемой подкольца R, соответствующее локальное подкольцо R.toLocalSubring является максимальным.

LaTeX

$$$\\forall R:\\mathrm{ValuationSubring}(K), \\; \\mathrm{IsMax}(R^{\\mathrm{toLocalSubring}}).$$$

Lean4

@[stacks 052K]
theorem isMax_toLocalSubring (R : ValuationSubring K) : IsMax R.toLocalSubring :=
  by
  intro S hS
  suffices R.toLocalSubring = S from this.ge
  refine LocalSubring.toSubring_injective (le_antisymm hS.1 ?_)
  intro x hx
  refine (R.2 x).elim id fun h ↦ ?_
  by_contra h'
  have hx0 : x ≠ 0 := by rintro rfl; exact h' (zero_mem R)
  have : IsUnit (Subring.inclusion hS.1 ⟨x⁻¹, h⟩) :=
    isUnit_iff_exists_inv.mpr ⟨⟨x, hx⟩, Subtype.ext (inv_mul_cancel₀ hx0)⟩
  obtain ⟨x', hx'⟩ := isUnit_iff_exists_inv.mp (hS.2.1 _ this)
  have : x'.1 = x := by simpa [Subtype.ext_iff, inv_mul_eq_iff_eq_mul₀ hx0] using hx'
  exact h' (this ▸ x'.2)

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