[Merged by Bors] - feat(group_theory): add definition of solvable group

[pglutz]

Defines solvable groups using the definition that a group is solvable if its nth commutator is eventually trivial. Defines the nth commutator of a group and provides some lemmas for working with it. More facts about solvable groups will come in future PRs.

---

[ocfnash]

I think the following are probably worth including here:

@[simp] lemma bot_general_commutator_eq_bot (H : subgroup G) : general_commutator ⊥ H = ⊥ := sorry

@[simp] lemma general_commutator_bot_eq_bot (H : subgroup G) : general_commutator H ⊥ = ⊥ := sorry

lemma general_commutator_comm (H₁ H₂ : subgroup G) :
  general_commutator H₁ H₂ = general_commutator H₂ H₁ := sorry

lemma general_commutator_le_right (H₁ H₂ : subgroup G) [normal H₁] :
  general_commutator H₁ H₂ ≤ H₂ := sorry

lemma general_commutator_le_left (H₁ H₂ : subgroup G) [normal H₂] :
  general_commutator H₁ H₂ ≤ H₁ := sorry

lemma general_commutator_le_inf (H₁ H₂ : subgroup G) [normal H₁] [normal H₂] :
  general_commutator H₁ H₂ ≤ H₁ ⊓ H₂ := sorry

[pglutz]

I think the following are probably worth including here:

@[simp] lemma bot_general_commutator_eq_bot (H : subgroup G) : general_commutator ⊥ H = ⊥ := sorry

@[simp] lemma general_commutator_bot_eq_bot (H : subgroup G) : general_commutator H ⊥ = ⊥ := sorry

lemma general_commutator_comm (H₁ H₂ : subgroup G) :
  general_commutator H₁ H₂ = general_commutator H₂ H₁ := sorry

lemma general_commutator_le_right (H₁ H₂ : subgroup G) [normal H₁] :
  general_commutator H₁ H₂ ≤ H₂ := sorry

lemma general_commutator_le_left (H₁ H₂ : subgroup G) [normal H₂] :
  general_commutator H₁ H₂ ≤ H₁ := sorry

lemma general_commutator_le_inf (H₁ H₂ : subgroup G) [normal H₁] [normal H₂] :
  general_commutator H₁ H₂ ≤ H₁ ⊓ H₂ := sorry

@ocfnash assuming that the assumption in general_commutator_le_right was supposed to be [normal H₂] rather than [normal H₁] (and similarly for general_commutator_le_left) I've now proved all of these.

[pglutz]

@ocfnash When I write the left "square with quill" bracket in VS Code, it automatically completes with an ordinary right square bracket rather than a right "square with quill" bracket and so I have to manually change the right bracket to a "square with quill" bracket each time. Do you know if there's a way around this?

[ocfnash]

@ocfnash When I write the left "square with quill" bracket in VS Code, it automatically completes with an ordinary right square bracket rather than a right "square with quill" bracket and so I have to manually change the right bracket to a "square with quill" bracket each time. Do you know if there's a way around this?

Argh, that sounds so painful! Sorry you had to suffer this. If you're using VSCode then the shortcuts you're missing are [- and -]. See for example here.

I usually use liel and lier myself but trying now I see now that [- generates ⁅ but autocompletes with ]. Yuck! I have just asked about this on Zulip. I have also opened a PR for the VSCode extension which should resolve this issue. In the meantime maybe just use liel and lier.

[pglutz]

@jcommelin Does everything look okay now? Also, sorry for the confusion about general_commutator_comm.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests