Semidirect product #
This file defines semidirect products of groups, and the canonical maps in and out of the
semidirect product. The semidirect product of N
and G
given a hom φ
from
G
to the automorphism group of N
is the product of sets with the group
⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩
Key definitions #
There are two homs into the semidirect product inl : N →* N ⋊[φ] G
and
inr : G →* N ⋊[φ] G
, and lift
can be used to define maps N ⋊[φ] G →* H
out of the semidirect product given maps fn : N →* H
and fg : G →* H
that satisfy the
condition ∀ n g, fn (φ g n) = fg g * fn n * fg g⁻¹
Notation #
This file introduces the global notation N ⋊[φ] G
for SemidirectProduct N G φ
Tags #
group, semidirect product
The semidirect product of groups N
and G
, given a map φ
from G
to the automorphism
group of N
. It the product of sets with the group operation
⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩
- left : N
The element of N
- right : G
The element of G
Instances For
Equations
- instDecidableEqSemidirectProduct = decEqSemidirectProduct✝
The semidirect product of groups N
and G
, given a map φ
from G
to the automorphism
group of N
. It the product of sets with the group operation
⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩
Equations
- One or more equations did not get rendered due to their size.
Instances For
Define a group hom N ⋊[φ] G →* H
, by defining maps N →* H
and G →* H
Equations
- SemidirectProduct.lift fn fg h = { toFun := fun (a : N ⋊[φ] G) => fn a.left * fg a.right, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Two maps out of the semidirect product are equal if they're equal after composition
with both inl
and inr
The homomorphism from a semidirect product of subgroups to the ambient group.
Equations
- SemidirectProduct.monoidHomSubgroup h = SemidirectProduct.lift H.subtype K.subtype ⋯
Instances For
The isomorphism from a semidirect product of complementary subgroups to the ambient group.
Equations
Instances For
Define a map from N₁ ⋊[φ₁] G₁
to N₂ ⋊[φ₂] G₂
given maps N₁ →* N₂
and G₁ →* G₂
that
satisfy a commutativity condition ∀ n g, fn (φ₁ g n) = φ₂ (fg g) (fn n)
.
Equations
- SemidirectProduct.map fn fg h = { toFun := fun (x : N₁ ⋊[φ₁] G₁) => { left := fn x.left, right := fg x.right }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Define an isomorphism from N₁ ⋊[φ₁] G₁
to N₂ ⋊[φ₂] G₂
given isomorphisms N₁ ≃* N₂
and
G₁ ≃* G₂
that satisfy a commutativity condition ∀ n g, fn (φ₁ g n) = φ₂ (fg g) (fn n)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Define a isomorphism from N₁ ⋊[φ₁] G₁
to N₂ ⋊[φ₂] G₂
without specifying φ₂
.
Equations
- SemidirectProduct.congr' fn fg = SemidirectProduct.congr fn fg ⋯