principalUnitGroupOrderEmbedding — Mathlib

English

The map sending a valuation subring to its principal unit group is an order embedding into the opposite order on unit groups, i.e., inclusions reverse under taking principal unit groups.

Русский

Отображение, отправляющее ценностное подкольцо в его главную единичную группу, является вложением по порядку в противоположном порядке: вложение сохраняет порядок в обратном отношении.

LaTeX

$$$\mathrm{principalUnitGroupOrderEmbedding} : \mathrm{ValuationSubring}(K) \hookrightarrow_o (\mathrm{Subgroup}(K^\times))^{\mathrm{op}}$$$

Lean4

/-- The map on valuation subrings to their principal unit groups is an order embedding. -/
def principalUnitGroupOrderEmbedding : ValuationSubring K ↪o (Subgroup Kˣ)ᵒᵈ
    where
  toFun A := A.principalUnitGroup
  inj' := principalUnitGroup_injective
  map_rel_iff' {_A _B} := principalUnitGroup_le_principalUnitGroup

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