Group actions on projectivization

Show that (among other groups), the general linear group of V acts on ℙ K V.

instance Projectivization.instMulAction {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] [Group G] [DistribMulAction G V] [SMulCommClass G K V] : MulAction G (Projectivization K V)

Any group acting K-linearly on V (such as the general linear group) acts on ℙ V.

Equations

• Projectivization.instMulAction = { smul := fun (g : G) (x : Projectivization K V) => Projectivization.map ((DistribMulAction.toModuleEnd K V) g) ⋯ x, one_smul := ⋯, mul_smul := ⋯ }

theorem Projectivization.smul_def {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] [Group G] [DistribMulAction G V] [SMulCommClass G K V] (g : G) (x : Projectivization K V) : SMul.smul g x = map ((DistribMulAction.toModuleEnd K V) g) ⋯ x

theorem Projectivization.generalLinearGroup_smul_def {K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] (g : LinearMap.GeneralLinearGroup K V) (x : Projectivization K V) : g • x = map ↑g.toLinearEquiv ⋯ x

@[simp]

theorem Projectivization.smul_mk {G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] [Group G] [DistribMulAction G V] [SMulCommClass G K V] (g : G) {v : V} (hv : v ≠ 0) : g • mk K v hv = mk K (g • v) ⋯