addMonoidHom — Mathlib

English

For a linearly ordered cancellative additive monoid G with LocallyFiniteOrder, there exists a canonical order-preserving monoid hom from G to ℤ, often giving an embedding into the integers via φ(g) = |Ico(0,g)| − |Ico(0,−g)|; this map is monotone and either surjective or trivial.

Русский

Для линейно упорядоченного кассального аддитивного моноида G с LocallyFiniteOrder существует каноническое моноид-гомоморфизм, сохраняющий порядок, из G в ℤ; обычно он задаётся φ(g) = |Ico(0,g)| − |Ico(0,−g)| и либо является сюръективным, либо нулевым.

LaTeX

$$$$ \exists \varphi: G \to_o \mathbb{Z},\ \varphi(g) = |Ico(0,g)| - |Ico(0,-g)|. $$$$

Lean4

/-- The canonical embedding (as a monoid hom) from a linearly ordered cancellative additive monoid
into `ℤ`. This is either surjective or zero. -/
def addMonoidHom : G →+ ℤ where
  toFun a := #(Ico 0 a) - #(Ico 0 (-a))
  map_zero' := by simp
  map_add' a
    b := by
    wlog hab : a ≤ b generalizing a b
    · convert this b a (le_of_not_ge hab) using 1 <;> simp only [add_comm]
    obtain ha | ha := le_total 0 a <;> obtain hb | hb := le_total 0 b
    · have : -b ≤ a := by trans 0 <;> simp [ha, hb]
      simp [ha, hb, card_Ico_zero_add, this]
    · obtain rfl := hb.antisymm (ha.trans hab)
      obtain rfl := ha.antisymm hab
      simp
    · simp only [neg_add_rev, ha, Ico_eq_empty_of_le, card_empty, Nat.cast_zero, zero_sub, Left.neg_nonpos_iff, hb,
        sub_zero]
      obtain ⟨b, rfl⟩ : ∃ r, b = r - a := ⟨a + b, by abel⟩
      simp only [add_sub_cancel, neg_sub, sub_add_eq_add_sub, add_neg_cancel, zero_sub]
      obtain hb' | hb' := le_total 0 b
      · simp [hb', neg_add_eq_sub, eq_sub_iff_add_eq, ← Nat.cast_add, ← card_Ico_zero_add, ha, ← sub_eq_add_neg]
      ·
        simp [hb', neg_add_eq_sub, eq_sub_iff_add_eq, sub_eq_iff_eq_add, ← Nat.cast_add, ← card_Ico_zero_add, hb,
          sub_add_eq_add_sub]
    · have : ¬0 < a + b := by simpa using add_nonpos ha hb
      simp [ha, hb, card_Ico_zero_add, Ico_eq_empty, this]

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