freeGroupUnitEquivInt — Mathlib

English

There is a canonical bijection between FreeGroup Unit and the integers, built as sum and z-powers.

Русский

Существует каноническая биекция между FreeGroup Unit и целыми числами через сумму и z-степени.

LaTeX

$$$ freeGroupUnitEquivInt : FreeGroup Unit \\simeq \\mathbb{Z} $$$

Lean4

/-- The bijection between the free group on a singleton, and the integers. -/
def freeGroupUnitEquivInt : FreeGroup Unit ≃ ℤ
    where
  toFun
    x :=
    sum
      (by
        revert x
        exact ↑(map fun _ => (1 : ℤ)))
  invFun x := of () ^ x
  left_inv := by
    rintro ⟨L⟩
    simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]
    exact List.recOn L (by rfl) (fun ⟨⟨⟩, b⟩ tl ih => by cases b <;> simp [zpow_add] at ih ⊢ <;> rw [ih] <;> rfl)
  right_inv
    x :=
    Int.induction_on x (by simp)
      (fun i ih => by
        simp only [zpow_natCast, map_pow, map.of] at ih
        simp [zpow_add, ih])
      (fun i ih =>
        by
        simp only [zpow_neg, zpow_natCast, map_inv, map_pow, map.of, sum.map_inv, neg_inj] at ih
        simp [zpow_add, ih, sub_eq_add_neg])

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