LeanPool.OrderPQ.SemidirectProduct

theorem Subgroup.comm_of_normal_and_inf_eq_bot {G : Type u_5} [Group G] (N H : Subgroup G) (hN : N.Normal) (hH : H.Normal) (inf_eq_bot : N ⊓ H = ⊥) (n : ↥N) (h : ↥H) : ↑n * ↑h = ↑h * ↑n

noncomputable def mulEquivSemidirectProduct {G : Type u_5} [Group G] {N H : Subgroup G} (h : N.Normal) (inf_eq_bot : N ⊓ H = ⊥) (sup_eq_top : N ⊔ H = ⊤) {φ : ↥H →* MulAut ↥N} (conj : φ = MulAut.conjNormal.domRestrict H) : G ≃* ↥N ⋊[φ] ↥H

If N is a normal subgroup of G and H is a subgroup with N ⊓ H = ⊥ and N ⊔ H = ⊤, then G is isomorphic to the semidirect product N ⋊[φ] H for φ the conjugation action.

Equations

• mulEquivSemidirectProduct h inf_eq_bot sup_eq_top conj = (MulEquiv.ofBijective { toFun := fun (x : ↥N ⋊[φ] ↥H) => ↑x.left * ↑x.right, map_mul' := ⋯ } ⋯).symm

def Subgroup.subgroupOfMulEquiv {G : Type u_6} [Group G] (H K : Subgroup G) (h : H ≤ K) : ↥(H.subgroupOf K) ≃* ↥H

If H ≤ K are subgroups of G, then H.subgroupOf K is canonically isomorphic to H.

Equations

• H.subgroupOfMulEquiv K h = { toFun := fun (x : ↥(H.subgroupOf K)) => ⟨↑↑x, ⋯⟩, invFun := fun (x : ↥H) => ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem Subgroup.subgroupOfMulEquiv_symm_apply_coe_coe {G : Type u_6} [Group G] (H K : Subgroup G) (h : H ≤ K) (x : ↥H) : ↑↑((H.subgroupOfMulEquiv K h).symm x) = ↑x

@[simp]

theorem Subgroup.subgroupOfMulEquiv_apply_coe {G : Type u_6} [Group G] (H K : Subgroup G) (h : H ≤ K) (x : ↥(H.subgroupOf K)) : ↑((H.subgroupOfMulEquiv K h) x) = ↑↑x

theorem Subgroup.subgroupOf_inf {G : Type u_5} [Group G] {H K L : Subgroup G} : (H ⊓ K).subgroupOf L = H.subgroupOf L ⊓ K.subgroupOf L

theorem AddSubgroup.addSubgroupOf_inf {G : Type u_5} [AddGroup G] {H K L : AddSubgroup G} : (H ⊓ K).addSubgroupOf L = H.addSubgroupOf L ⊓ K.addSubgroupOf L

noncomputable def mulEquivSemidirectProduct' {G : Type u_5} [Group G] {N H : Subgroup G} (h : N.Normal) (inf_eq_bot : N ⊓ H = ⊥) {φ : ↥H →* MulAut ↥N} (conj : φ = MulAut.conjNormal.domRestrict H) : ↥(N ⊔ H) ≃* ↥N ⋊[φ] ↥H

Variant of mulEquivSemidirectProduct that works within the subgroup N ⊔ H rather than requiring N ⊔ H = ⊤.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def mulEquivProd {G : Type u_5} [Group G] {N H : Subgroup G} (hN : N.Normal) (hH : H.Normal) (inf_eq_bot : N ⊓ H = ⊥) (sup_eq_top : N ⊔ H = ⊤) : G ≃* ↥N × ↥H

If N and H are normal subgroups of G with trivial intersection that span G, then G is isomorphic to the direct product N × H.

Equations

• mulEquivProd hN hH inf_eq_bot sup_eq_top = (mulEquivSemidirectProduct hN inf_eq_bot sup_eq_top ⋯).trans (have this := ⋯; ⋯ ▸ SemidirectProduct.mulEquivProd)