coeHom — Mathlib

English

There is a canonical monoid homomorphism from SL(2, ℤ) to GL⁺(2, ℝ) aligning with the standard inclusion, i.e., coeHom(g) = the corresponding real matrix.

Русский

Существует каноническое гомоморфизм-моноид из SL(2, ℤ) в GL⁺(2, ℝ), являющееся включением.

LaTeX

$$$\mathrm{coeHom} : SL(2, \mathbb{Z}) \to GL^+(2, \mathbb{R})$ является гомоморфизмом моноидов: $\mathrm{coeHom}(gh) = \mathrm{coeHom}(g)\mathrm{coeHom}(h)$.$$

Lean4

/-- Canonical embedding of `SL(2, ℤ)` into `GL(2, ℝ)⁺`, bundled as a group hom. -/
def coeHom : SL(2, ℤ) →* GL(2, ℝ)⁺ :=
  toGLPos.comp <| map <| Int.castRingHom _

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