Klein Four Group #
The Klein (Vierergruppe) four-group is a non-cyclic abelian group with four elements, in which each element is self-inverse and in which composing any two of the three non-identity elements produces the third one.
Main definitions #
IsKleinFour
: A mixin class which states that the group has order four and exponent two.mulEquiv'
: An equivalence between a Klein four-group and a group of exponent two which preserves the identity is in fact an isomorphism.mulEquiv
: Any two Klein four-groups are isomorphic via any identity preserving equivalence.
References #
TODO #
Prove an
IsKleinFour
group is isomorphic to the normal subgroup ofalternatingGroup (Fin 4)
with the permutation cyclesV = {(), (1 2)(3 4), (1 3)(2 4), (1 4)(2 3)}
. This is the kernel of the surjection ofalternatingGroup (Fin 4)
ontoalternatingGroup (Fin 3) ≃ (ZMod 3)
. In other words, we have the exact sequenceV → A₄ → A₃
.The outer automorphism group of
A₆
is the Klein four-groupV = (ZMod 2) × (ZMod 2)
, and is related to the outer automorphism ofS₆
. The extra outer automorphism inA₆
swaps the 3-cycles (like(1 2 3)
) with elements of shape3²
(like(1 2 3)(4 5 6)
).
Tags #
non-cyclic abelian group
Klein four-groups as a mixin class #
An (additive) Klein four-group is an (additive) group of cardinality four and exponent two.
Instances
A Klein four-group is a group of cardinality four and exponent two.
Instances
An equivalence between an IsKleinFour
group G₁
and a group G₂
of exponent two which sends
1 : G₁
to 1 : G₂
is in fact an isomorphism.
Equations
Instances For
An equivalence between an IsAddKleinFour
group G₁
and a group G₂
of exponent
two which sends 0 : G₁
to 0 : G₂
is in fact an isomorphism.
Equations
Instances For
Any two IsKleinFour
groups are isomorphic via any equivalence which sends the identity of one
group to the identity of the other.
Instances For
Any two IsAddKleinFour
groups are isomorphic via any
equivalence which sends the identity of one group to the identity of the other.
Instances For
Any two IsKleinFour
groups are isomorphic.
Any two IsAddKleinFour
groups are isomorphic.