τ_apply_infinity — Mathlib

English

Let f: A → B be a group homomorphism. The distinguished point at infinity in the X-with-infinity construction is mapped by τ to the canonical left coset represented by the range of f, i.e. τ(∞) = fromCoset(⟨range(f), 1, 1_leftCoset⟩).

Русский

Пусть f: A → B — гомоморф группы. Обозначенная точка на бесконечности в конструкции X с бесконечностью отображается τ в каноническую левую косету, порожденную множеством образов f: τ(∞) = fromCoset(⟨range(f), 1, 1_leftCoset⟩).

LaTeX

$$$$ \tau(\infty) = \mathrm{fromCoset}\left\langle \operatorname{range}(f), 1, 1_{\text{leftCoset}} \right\rangle. $$$$

Lean4

theorem τ_apply_infinity : τ ∞ = fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ :=
  Equiv.swap_apply_right _ _

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