isMax_iff — Mathlib

English

A local subring A is maximal iff it is the local part of some valuation subring.

Русский

Локальное подкольцо A максимально тогда и только тогда, когда оно является локальной частью некоторого оценочного подкольца.

LaTeX

$$$\\forall A:\\mathrm{LocalSubring}(K), \\; \\mathrm{IsMax}(A) \\iff \\exists B:\\mathrm{ValuationSubring}(K), \\; B^{\\mathrm{toLocalSubring}} = A.$$$

Lean4

/-- A local subring is maximal with respect to the domination order
  if and only if it is a valuation ring. -/
theorem isMax_iff {A : LocalSubring K} : IsMax A ↔ ∃ B : ValuationSubring K, B.toLocalSubring = A :=
  ⟨exists_valuationRing_of_isMax, fun ⟨B, e⟩ ↦ e ▸ B.isMax_toLocalSubring⟩

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