Group actions on projectivization

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

Prove that these actions are 2-transitive.

TODO

Generalize to the special linear group over a division ring.

@[implicit_reducible]

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, mul_smul := ⋯, one_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) ⋯

instance Projectivization.linearEquiv_is_two_pretransitive (K : Type u_2) (V : Type u_3) [AddCommGroup V] [DivisionRing K] [Module K V] : MulAction.IsMultiplyPretransitive (V ≃ₗ[K] V) (Projectivization K V) 2

instance Projectivization.generalLinearGroup_is_two_pretransitive (K : Type u_2) (V : Type u_3) [AddCommGroup V] [DivisionRing K] [Module K V] : MulAction.IsMultiplyPretransitive (LinearMap.GeneralLinearGroup K V) (Projectivization K V) 2

theorem Projectivization.specialLinearGroup_smul_def {K : Type u_1} {V : Type u_2} [AddCommGroup V] [Field K] [Module K V] (g : SpecialLinearGroup K V) (D : Projectivization K V) : g • D = SpecialLinearGroup.toLinearEquiv g • D

instance Projectivization.specialLinearGroup_is_two_pretransitive (K : Type u_1) (V : Type u_2) [AddCommGroup V] [Field K] [Module K V] : MulAction.IsMultiplyPretransitive (SpecialLinearGroup K V) (Projectivization K V) 2

instance Projectivization.instIsPreprimitiveSpecialLinearGroup {K : Type u_1} {V : Type u_2} [AddCommGroup V] [Field K] [Module K V] : MulAction.IsPreprimitive (SpecialLinearGroup K V) (Projectivization K V)

The special linear group SpecialLinearGroup K V acts primitively on ℙ K V.