Dilatransvections generate the special linear group

We prove the theorem of [dieudonne-1955][J. Dieudonné, “Sur les générateurs des groupes classiques”].

Let K be a division ring and V be a K-module.

• LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_fixedReduce_eq_one: If e.fixedReduce = 1, then e can be written as the product of finrank K (V ⧸ e.fixedSubmodule) - 1 transvections and one dilatransvection. This is the first part of the non-exceptional case in Dieudonné's theorem. (This statement is not interesting when e = 1.)

• LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_fixedReduce_ne_smul_id: If e.fixedReduce is not a homothety, then e can be written as the product of finrank K (V ⧸ e.fixedSubmodule) - 1 transvections and one dilatransvection. This is the second part of the non-exceptional case in Dieudonné's theorem.

• LinearEquiv.IsExceptional: A linear equivalence e : V ≃ₗ[K] V is exceptional if 1 < finrank K (V ⧸ e.fixedSubmodule) and if e.fixedReduce is a nontrivial homothety.

• LinearEquiv.mem_dilatransvections_pow_of_not_isExceptional: This is the non-exceptional case in Dieudonné's theorem, as a combination of the two preceding statements.

TODO

• Prove the third and fourth cases of Dieudonné's theorem that concern the case where e is exceptional: e can be written as the product of finrank K (V ⧸ e.fixedSubmodule) transvections and one dilatransvection but not less.

• Prove that the general linear group is generated by dilatransvections.

• Prove that the special linear group is generated by transvections (with a bound on the minimal number of transvections needed).

• In the statements above, the dilatransvection is at the right of the product; show that it can be inserted anywhere. (The point is that transvections normalize dilatransvections.)

theorem LinearEquiv.finrank_fixedSubmodule_add_le {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] (e f : V ≃ₗ[K] V) : Module.finrank K ↥(↑e).fixedSubmodule + Module.finrank K ↥(↑f).fixedSubmodule ≤ Module.finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + Module.finrank K ↥(↑(e * f)).fixedSubmodule

theorem LinearEquiv.finrank_le_one_add_finrank_fixedSubmodule_dilatransvection {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] (e : V ≃ₗ[K] V) (he : e ∈ dilatransvections K V) : Module.finrank K V ≤ 1 + Module.finrank K ↥(↑e).fixedSubmodule

theorem LinearEquiv.le_one_add_finrank_fixedSubmodule_dilatransvection_mul {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] (e f : V ≃ₗ[K] V) (hf : f ∈ dilatransvections K V) : Module.finrank K ↥(↑e).fixedSubmodule ≤ 1 + Module.finrank K ↥(↑(f * e)).fixedSubmodule

theorem LinearEquiv.finrank_fixedSubmodule_dilatransvection_mul_le {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] (e f : V ≃ₗ[K] V) (hf : f ∈ dilatransvections K V) : Module.finrank K ↥(↑(f * e)).fixedSubmodule ≤ 1 + Module.finrank K ↥(↑e).fixedSubmodule

theorem LinearEquiv.le_one_add_finrank_fixedSubmodule_mul_dilatransvection {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] (e f : V ≃ₗ[K] V) (hf : f ∈ dilatransvections K V) : Module.finrank K ↥(↑e).fixedSubmodule ≤ 1 + Module.finrank K ↥(↑(e * f)).fixedSubmodule

theorem LinearEquiv.finrank_fixedSubmodule_mul_dilatransvection_le {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] (e f : V ≃ₗ[K] V) (hf : f ∈ dilatransvections K V) : Module.finrank K ↥(↑(e * f)).fixedSubmodule ≤ 1 + Module.finrank K ↥(↑e).fixedSubmodule

theorem LinearEquiv.fixedSubmodule_transvection_mul {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] (e : V ≃ₗ[K] V) {f : Module.Dual K V} {v : V} (hv : v ∉ (↑e).fixedSubmodule) (hf : Submodule.map f (↑e).fixedSubmodule = ⊥) (hfv : f (v - e v) = 0) (hfv' : f (e v) = 1) : (↑(transvection hfv * e)).fixedSubmodule = (↑e).fixedSubmodule ⊔ K ∙ v

@[reducible, inline]

abbrev LinearEquiv.IsExceptional {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (e : V ≃ₗ[K] V) : Prop

A linear equivalence u : V ≃ₗ[K] V is exceptional if it is a nontrivial homothety modulo u.fixedSubmodule.

Equations

• e.IsExceptional = (1 < Module.finrank K (V ⧸ (↑e).fixedSubmodule) ∧ e.fixedReduce ≠ 1 ∧ ∃ (a : K), ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x)

theorem LinearEquiv.finrank_quotient_sup_span_singleton {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] {W : Submodule K V} {v : V} (hv : v ∉ W) : Module.finrank K (V ⧸ W ⊔ K ∙ v) + 1 = Module.finrank K (V ⧸ W)

theorem LinearEquiv.sup_span_singleton_lt_top {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] {W : Submodule K V} (v : V) (hW : 1 < Module.finrank K (V ⧸ W)) : W ⊔ K ∙ v < ⊤

theorem LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_fixedReduce_eq_one {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] {e : V ≃ₗ[K] V} (he : e.fixedReduce = 1) : e ∈ transvections K V ^ (Module.finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V

If e : V ≃ₗ[K] V is such that e.fixedReduce = 1, then e is the product of at most finrank K (V ⧸ e.fixedSubmodule) - 1 transvections and one dilatransvection.

This is the first non-exceptional case in Dieudonné's theorem.

theorem LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_fixedReduce_ne_smul_id {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] {e : V ≃ₗ[K] V} (he : ∀ (a : K), ∃ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x ≠ a • x) : e ∈ transvections K V ^ (Module.finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V

If an element e : V ≃ₗ[K] V is such that e.fixedReduce is not a homothety, then e is the product of at most finrank K (V ⧸ e.fixedSubmodule) - 1 transvections and one dilatransvection.

This is the second non-exceptional case in Dieudonné's theorem.

theorem LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_not_isExceptional {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] [Module.Finite K V] {e : V ≃ₗ[K] V} (he : ¬e.IsExceptional) : e ∈ transvections K V ^ (Module.finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V

If an element e : V ≃ₗ[K] V is not exceptional, then it is the product of at most finrank K (V ⧸ e.fixedSubmodule) dilatransvections.

This is the non-exceptional case in Dieudonné's theorem.