SemidirectProduct.ext
theorem SemidirectProduct.ext :
∀ {N : Type u_1} {G : Type u_2} {inst : Group N} {inst_1 : Group G} {φ : G →* MulAut N} (x y : N ⋊[φ] G),
x.left = y.left → x.right = y.right → x = y
This theorem, `SemidirectProduct.ext`, states that for any two elements `x` and `y` in the semidirect product `N ⋊[φ] G` of two groups `N` and `G`, if the left components and the right components of `x` and `y` are equal then `x` and `y` are equal. Here, `N` and `G` are types with group structures, and `φ` is a homomorphism from `G` to the group of multiplicative automorphisms of `N`. The semidirect product `N ⋊[φ] G` typically encodes a nontrivial interaction between `N` and `G` mediated by the homomorphism `φ`.
More concisely: In the semidirect product of groups `N ⋊[φ] G`, if `x` and `y` have equal left components and equal right components, then `x` and `y` are equal.
|
SemidirectProduct.hom_ext
theorem SemidirectProduct.hom_ext :
∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
{φ : G →* MulAut N} {f g : N ⋊[φ] G →* H},
f.comp SemidirectProduct.inl = g.comp SemidirectProduct.inl →
f.comp SemidirectProduct.inr = g.comp SemidirectProduct.inr → f = g
The theorem `SemidirectProduct.hom_ext` states that for any three types `N`, `G`, and `H` with group structures, and given a map `φ` from `G` to the group of multiplicative automorphisms of `N`, if there exist two homomorphisms `f` and `g` from the semidirect product of `N` and `G` with respect to `φ` to `H`, then `f` is equal to `g` if and only if their compositions with the canonical map (named `inl`) from `N` to the semidirect product and with the canonical map (named `inr`) from `G` to the semidirect product are equal. The canonical maps `inl` and `inr` send an element from `N` and `G` respectively to the semidirect product by pairing it with the identity element of the other group.
More concisely: Given groups N, G, and H, and a map φ from G to the automorphisms of N, if there exist homomorphisms f and g from the semidirect product N ⋊ G with respect to φ to H such that inl ∘ f = inl ∘ g and inr ∘ f = inr ∘ g, then f = g.
|