instGLAction — Mathlib

English

There is an action of GL(2,K) on OnePoint(K) induced by the projectivization identification with the projective line.

Русский

Существует действие GL(2,K) на OnePoint(K), полученное через эквивалентность к проективной линии.

LaTeX

$$$\\text{GL}(2,K)\\curvearrowright \\mathrm{OnePoint}(K).$$$

Lean4

/-- For a field `K`, the group `GL(2, K)` acts on `OnePoint K`, via the canonical identification
with the `ℙ¹(K)` (which is given explicitly by Möbius transformations). -/
instance instGLAction : MulAction (GL (Fin 2) K) (OnePoint K) :=
  (equivProjectivization K).mulAction (GL (Fin 2) K)

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