English
Define g: B →* SX' by g(β)(x) = β • x for x ∈ X'; equivalently g(β) is the left translation by β on X'.
Русский
Определим g: B →* SX' так, что g(β)(x) = β • x; то есть g(β) есть левое перенесение на X' на единичном числе.
LaTeX
$$$$ g:\, B \to SX', \quad g(\beta)(x) = \beta \cdot x \quad( x \in X'). $$$$
Lean4
/-- Let `g : B ⟶ S(X')` be defined as such that, for any `β : B`, `g(β)` is the function sending
point at infinity to point at infinity and sending coset `y` to `β • y`.
-/
def g : B →* SX'
where
toFun
β :=
{ toFun := fun x => β • x
invFun := fun x => β⁻¹ • x
left_inv := fun x => by
dsimp only
rw [← mul_smul, inv_mul_cancel, one_smul]
right_inv := fun x => by
dsimp only
rw [← mul_smul, mul_inv_cancel, one_smul] }
map_one' := by
ext
simp [one_smul]
map_mul' b1
b2 := by
ext
simp [mul_smul]
