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.

@[instance_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

theorem Projectivization.matrixSpecialLinearGroup_smul_def {ι : Type u_4} {F : Type u_5} [Fintype ι] [DecidableEq ι] [Field F] (g : Matrix.SpecialLinearGroup ι F) (x : Projectivization F (ι → F)) : g • x = Matrix.SpecialLinearGroup.toLin'_equiv g • 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.

instance Projectivization.instIsMultiplyPretransitiveSpecialLinearGroupForallOfNatNat {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : MulAction.IsMultiplyPretransitive (Matrix.SpecialLinearGroup ι K) (Projectivization K (ι → K)) 2

instance Projectivization.prePrimitive_SL {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : MulAction.IsPreprimitive (Matrix.SpecialLinearGroup ι K) (Projectivization K (ι → K))

theorem Projectivization.SL_mulAction_ker {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : (MulAction.toPermHom (Matrix.SpecialLinearGroup ι K) (Projectivization K (ι → K))).ker = Subgroup.center (Matrix.SpecialLinearGroup ι K)

def Projectivization.PSLAction.toPermHom {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : Matrix.ProjectiveSpecialLinearGroup ι K →* Equiv.Perm (Projectivization K (ι → K))

The action of the special linear group on ℙ F (ι → F) factors through the projective special linear group PSL = SL ⧸ Z(SL).

Equations

• Projectivization.PSLAction.toPermHom = QuotientGroup.lift (Subgroup.center (Matrix.SpecialLinearGroup ι K)) (MulAction.toPermHom (Matrix.SpecialLinearGroup ι K) (Projectivization K (ι → K))) ⋯

@[instance_reducible]

instance Projectivization.instMulActionProjectiveSpecialLinearGroupForall {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : MulAction (Matrix.ProjectiveSpecialLinearGroup ι K) (Projectivization K (ι → K))

Equations

• Projectivization.instMulActionProjectiveSpecialLinearGroupForall = MulAction.compHom (Projectivization K (ι → K)) Projectivization.PSLAction.toPermHom

theorem Matrix.ProjectiveSpecialLinearGroup.smul_proj_mk {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (g : SpecialLinearGroup ι K) (p : Projectivization K (ι → K)) : ↑g • p = g • p

theorem Matrix.ProjectiveSpecialLinearGroup.toPermHom_injective {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : Function.Injective ⇑Projectivization.PSLAction.toPermHom

instance Projectivization.instFaithfulSMulProjectiveSpecialLinearGroupForall {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : FaithfulSMul (Matrix.ProjectiveSpecialLinearGroup ι K) (Projectivization K (ι → K))

instance Projectivization.instIsPreprimitiveProjectiveSpecialLinearGroupForall {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : MulAction.IsPreprimitive (Matrix.ProjectiveSpecialLinearGroup ι K) (Projectivization K (ι → K))

@[instance_reducible]

instance Projectivization.instMulActionProjGenLinGroupForall {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : MulAction (Matrix.ProjGenLinGroup ι K) (Projectivization K (ι → K))

Equations

• Projectivization.instMulActionProjGenLinGroupForall = Matrix.ProjGenLinGroup.mulActionOfGL ⋯

@[simp]

theorem Projectivization.PGL.mk_smul_mk {K : Type u_1} [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (g : GL ι K) {v : ι → K} (hv : v ≠ 0) : Matrix.ProjGenLinGroup.mk g • mk K v hv = mk K (g • v) ⋯