equivHeightOneSpectrum — Mathlib

English

There is a canonical equivalence between FinitePlace K and HeightOneSpectrum(𝓞 K). The two-way correspondence is given by maximalIdeal and mk.

Русский

Существует каноническое эквивалентное соответствие между FinitePlace K и HeightOneSpectrum(𝓞 K). Двусторонняя связь задаются через maximalIdeal и mk.

LaTeX

$$$\\text{equivHeightOneSpectrum} : \\text{FinitePlace }K \\simeq \\text{HeightOneSpectrum}(\\mathscr{O}_K)$$$

Lean4

/-- The equivalence between finite places and maximal ideals. -/
noncomputable def equivHeightOneSpectrum : FinitePlace K ≃ HeightOneSpectrum (𝓞 K)
    where
  toFun := maximalIdeal
  invFun := mk
  left_inv := mk_maximalIdeal
  right_inv := maximalIdeal_mk

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