English
The action of a general linear group element g on a point x in projective space is given by applying the corresponding linear map to a representative of x.
Русский
Действие элемента общего линейного пространства g на точку x в проективном пространстве задаётся применением соответствующего линейного отображения к представителю x.
LaTeX
$$$ g \cdot x = x.map\, g.toLinearEquiv.toLinearMap\, g.toLinearEquiv.injective $$$
Lean4
/-- Any group acting `K`-linearly on `V` (such as the general linear group) acts on `ℙ V`. -/
@[simps -isSimp]
instance : MulAction G (ℙ K V)
where
smul g x := x.map (DistribMulAction.toModuleEnd _ _ g) (DistribMulAction.toLinearEquiv _ _ g).injective
one_smul x := show map _ _ _ = _ by simp [map_one, Module.End.one_eq_id]
mul_smul g g'
x :=
show map _ _ _ = map _ _ (map _ _ _) by
simp_rw [map_mul, Module.End.mul_eq_comp]
rw [map_comp, Function.comp_apply]
