import data.bracket

import group_theory.subgroup.finite

import tactic.group

variables {G G' F : Type*} [group G] [group G'] [monoid_hom_class F G G'] (f : F) {g₁ g₂ g₃ g : G}

lemma commutator_element_eq_one_iff_mul_comm : ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁ :=

by rw [commutator_element_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]

lemma commutator_element_eq_one_iff_commute : ⁅g₁, g₂⁆ = 1 ↔ commute g₁ g₂ :=

commutator_element_eq_one_iff_mul_comm

lemma commute.commutator_eq (h : commute g₁ g₂) : ⁅g₁, g₂⁆ = 1 :=

commutator_element_eq_one_iff_commute.mpr h

variables (g₁ g₂ g₃ g)

@[simp] lemma commutator_element_one_right : ⁅g, (1 : G)⁆ = 1 :=

(commute.one_right g).commutator_eq

@[simp] lemma commutator_element_one_left : ⁅(1 : G), g⁆ = 1 :=

(commute.one_left g).commutator_eq

@[simp] lemma commutator_element_self : ⁅g, g⁆ = 1 :=

(commute.refl g).commutator_eq

@[simp] lemma commutator_element_inv : ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆ :=

by simp_rw [commutator_element_def, mul_inv_rev, inv_inv, mul_assoc]

lemma map_commutator_element : (f ⁅g₁, g₂⁆ : G') = ⁅f g₁, f g₂⁆ :=

by simp_rw [commutator_element_def, map_mul f, map_inv f]

lemma conjugate_commutator_element : g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆ :=

map_commutator_element (mul_aut.conj g₃).to_monoid_hom g₁ g₂

namespace subgroup

instance commutator : has_bracket (subgroup G) (subgroup G) :=

⟨λ H₁ H₂, closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g}⟩

lemma commutator_def (H₁ H₂ : subgroup G) :

⁅H₁, H₂⁆ = closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g} := rfl

variables {g₁ g₂ g₃} {H₁ H₂ H₃ K₁ K₂ : subgroup G}

lemma commutator_mem_commutator (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=

subset_closure ⟨g₁, h₁, g₂, h₂, rfl⟩

lemma commutator_le : ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ ∈ H₃ :=

H₃.closure_le.trans ⟨λ h a b c d, h ⟨a, b, c, d, rfl⟩, λ h g ⟨a, b, c, d, h_eq⟩, h_eq ▸ h a b c d⟩

lemma commutator_mono (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) : ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=

commutator_le.mpr (λ g₁ hg₁ g₂ hg₂, commutator_mem_commutator (h₁ hg₁) (h₂ hg₂))

lemma commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer H₂ :=

rw [eq_bot_iff, commutator_le],

refine forall_congr (λ p, forall_congr (λ hp, forall_congr (λ q, forall_congr (λ hq, _)))),

rw [mem_bot, commutator_element_eq_one_iff_mul_comm, eq_comm],

lemma commutator_commutator_eq_bot_of_rotate

(h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥) (h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥) : ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥ :=

simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le,

mem_centralizer_iff_commutator_eq_one, ←commutator_element_def] at h1 h2 ⊢,

intros x hx y hy z hz,

transitivity x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹,

{ group },

{ rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy],

group },

variables (H₁ H₂)

lemma commutator_comm_le : ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆ :=

commutator_le.mpr (λ g₁ h₁ g₂ h₂,

commutator_element_inv g₂ g₁ ▸ ⁅H₂, H₁⁆.inv_mem_iff.mpr (commutator_mem_commutator h₂ h₁))

lemma commutator_comm : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=

le_antisymm (commutator_comm_le H₁ H₂) (commutator_comm_le H₂ H₁)

section normal

instance commutator_normal [h₁ : H₁.normal] [h₂ : H₂.normal] : normal ⁅H₁, H₂⁆ :=

let base : set G := {x | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = x},

change (closure base).normal,

suffices h_base : base = group.conjugates_of_set base,

{ rw h_base,

exact subgroup.normal_closure_normal },

refine set.subset.antisymm group.subset_conjugates_of_set (λ a h, _),

simp_rw [group.mem_conjugates_of_set_iff, is_conj_iff] at h,

rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩,

exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutator_element c e d).symm⟩,

lemma commutator_def' [H₁.normal] [H₂.normal] :

⁅H₁, H₂⁆ = normal_closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g} :=

le_antisymm closure_le_normal_closure (normal_closure_le_normal subset_closure)

lemma commutator_le_right [h : H₂.normal] : ⁅H₁, H₂⁆ ≤ H₂ :=

commutator_le.mpr (λ g₁ h₁ g₂ h₂, H₂.mul_mem (h.conj_mem g₂ h₂ g₁) (H₂.inv_mem h₂))

lemma commutator_le_left [H₁.normal] : ⁅H₁, H₂⁆ ≤ H₁ :=

commutator_comm H₂ H₁ ▸ commutator_le_right H₂ H₁

@[simp] lemma commutator_bot_left : ⁅(⊥ : subgroup G), H₁⁆ = ⊥ :=

le_bot_iff.mp (commutator_le_left ⊥ H₁)

@[simp] lemma commutator_bot_right : ⁅H₁, ⊥⁆ = (⊥ : subgroup G) :=

le_bot_iff.mp (commutator_le_right H₁ ⊥)

lemma commutator_le_inf [normal H₁] [normal H₂] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂ :=

le_inf (commutator_le_left H₁ H₂) (commutator_le_right H₁ H₂)

end normal

lemma map_commutator (f : G →* G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆ :=

simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutator_element],

split,

{ intros p hp q hq,

exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq), },

{ rintros _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩,

rw ← map_commutator_element,

exact mem_map_of_mem _ (commutator_mem_commutator hp hq) }

variables {H₁ H₂}

lemma commutator_le_map_commutator {f : G →* G'} {K₁ K₂ : subgroup G'}

(h₁ : K₁ ≤ H₁.map f) (h₂ : K₂ ≤ H₂.map f) : ⁅K₁, K₂⁆ ≤ ⁅H₁, H₂⁆.map f :=

(commutator_mono h₁ h₂).trans (ge_of_eq (map_commutator H₁ H₂ f))

variables (H₁ H₂)

instance commutator_characteristic [h₁ : characteristic H₁] [h₂ : characteristic H₂] :

characteristic ⁅H₁, H₂⁆ :=

characteristic_iff_le_map.mpr (λ ϕ, commutator_le_map_commutator

(characteristic_iff_le_map.mp h₁ ϕ) (characteristic_iff_le_map.mp h₂ ϕ))

lemma commutator_prod_prod (K₁ K₂ : subgroup G') :

⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ :=

apply le_antisymm,

{ rw commutator_le,

rintros ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩,

exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩ },

{ rw prod_le_iff, split;

{ rw map_commutator,

apply commutator_mono;

simp [le_prod_iff, map_map, monoid_hom.fst_comp_inl, monoid_hom.snd_comp_inl,

monoid_hom.fst_comp_inr, monoid_hom.snd_comp_inr ], }, }

lemma commutator_pi_pi_le {η : Type*} {Gs : η → Type*} [∀ i, group (Gs i)]

(H K : Π i, subgroup (Gs i)) :

⁅subgroup.pi set.univ H, subgroup.pi set.univ K⁆ ≤ subgroup.pi set.univ (λ i, ⁅H i, K i⁆) :=

commutator_le.mpr $ λ p hp q hq i hi, commutator_mem_commutator (hp i hi) (hq i hi)

lemma commutator_pi_pi_of_finite {η : Type*} [finite η] {Gs : η → Type*}

[∀ i, group (Gs i)] (H K : Π i, subgroup (Gs i)) :

⁅subgroup.pi set.univ H, subgroup.pi set.univ K⁆ = subgroup.pi set.univ (λ i, ⁅H i, K i⁆) :=

classical,

apply le_antisymm (commutator_pi_pi_le H K),

{ rw pi_le_iff, intros i hi,

rw map_commutator,

apply commutator_mono;

{ rw le_pi_iff,

intros j hj,

rintros _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩,

by_cases h : j = i,

{ subst h, simpa using hx, },

{ simp [h, one_mem] }, }, },

end subgroup

variables (G)

def commutator_set : set G :=

{g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g}

lemma commutator_set_def : commutator_set G = {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} := rfl

lemma one_mem_commutator_set : (1 : G) ∈ commutator_set G :=

⟨1, 1, commutator_element_self 1⟩

instance : nonempty (commutator_set G) :=

⟨⟨1, one_mem_commutator_set G⟩⟩

variables {G g}

lemma mem_commutator_set_iff : g ∈ commutator_set G ↔ ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g :=

iff.rfl

lemma commutator_mem_commutator_set : ⁅g₁, g₂⁆ ∈ commutator_set G :=

⟨g₁, g₂, rfl⟩