# Documentation

Mathlib.GroupTheory.SpecificGroups.KleinFour

# 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 #

• https://en.wikipedia.org/wiki/Klein_four-group
• https://en.wikipedia.org/wiki/Alternating_group

## TODO #

• Prove an IsKleinFour group is isomorphic to the normal subgroup of alternatingGroup (Fin 4) with the permutation cycles V = {(), (1 2)(3 4), (1 3)(2 4), (1 4)(2 3)}. This is the kernel of the surjection of alternatingGroup (Fin 4) onto alternatingGroup (Fin 3) ≃ (ZMod 3). In other words, we have the exact sequence V → A₄ → A₃.

• The outer automorphism group of A₆ is the Klein four-group V = (ZMod 2) × (ZMod 2), and is related to the outer automorphism of S₆. The extra outer automorphism in A₆ swaps the 3-cycles (like (1 2 3)) with elements of shape 3² (like (1 2 3)(4 5 6)).

## Tags #

non-cyclic abelian group

# Properties of groups with exponent two #

theorem neg_eq_self_of_exponent_two {G : Type u_1} [] (hG : ) (x : G) :
-x = x
theorem inv_eq_self_of_exponent_two {G : Type u_1} [] (hG : ) (x : G) :
x⁻¹ = x

In a group of exponent two, every element is its own inverse.

theorem neg_eq_self_of_addOrderOf_eq_two {G : Type u_1} [] {x : G} (hx : = 2) :
-x = x
theorem inv_eq_self_of_orderOf_eq_two {G : Type u_1} [] {x : G} (hx : = 2) :
x⁻¹ = x

If an element in a group has order two, then it is its own inverse.

theorem addOrderOf_eq_two_iff {G : Type u_1} [] (hG : ) {x : G} :
= 2 x 0
theorem orderOf_eq_two_iff {G : Type u_1} [] (hG : ) {x : G} :
= 2 x 1
theorem add_comm_of_exponent_two {G : Type u_1} [] (hG : ) (x : G) (y : G) :
x + y = y + x
theorem mul_comm_of_exponent_two {G : Type u_1} [] (hG : ) (x : G) (y : G) :
x * y = y * x

In a group of exponent two, all elements commute.

@[reducible]
def instAddCommGroupOfExponentTwo {G : Type u_1} [] (hG : ) :

Any additive group of exponent two is abelian.

Equations
Instances For
@[reducible]
def instCommGroupOfExponentTwo {G : Type u_1} [] (hG : ) :

Any group of exponent two is abelian.

Equations
Instances For
theorem add_not_mem_of_addOrderOf_eq_two {G : Type u_2} [] {x : G} {y : G} (hx : = 2) (hy : = 2) (hxy : x y) :
x + y{x, y, 0}
theorem mul_not_mem_of_orderOf_eq_two {G : Type u_2} [] {x : G} {y : G} (hx : = 2) (hy : = 2) (hxy : x y) :
x * y{x, y, 1}
theorem add_not_mem_of_exponent_two {G : Type u_2} [] (h : ) {x : G} {y : G} (hx : x 0) (hy : y 0) (hxy : x y) :
x + y{x, y, 0}
theorem mul_not_mem_of_exponent_two {G : Type u_2} [] (h : ) {x : G} {y : G} (hx : x 1) (hy : y 1) (hxy : x y) :
x * y{x, y, 1}

# Klein four-groups as a mixin class #

class IsAddKleinFour (G : Type u_1) [] :

An (additive) Klein four-group is an (additive) group of cardinality four and exponent two.

• card_four : = 4
• exponent_two :
Instances
class IsKleinFour (G : Type u_1) [] :

A Klein four-group is a group of cardinality four and exponent two.

• card_four : = 4
• exponent_two :
Instances
Equations
• (_ : ) = (_ : )
instance instIsKleinFourMultiplicativeGroup {G : Type u_1} [] [] :
Equations
• (_ : ) = (_ : )
instance IsAddKleinFour.instFinite {G : Type u_1} [] [] :
Equations
• (_ : ) = (_ : )
instance IsKleinFour.instFinite {G : Type u_1} [] [] :
Equations
• (_ : ) = (_ : )
@[simp]
theorem IsAddKleinFour.card_four' {G : Type u_1} [] [] [] :
@[simp]
theorem IsKleinFour.card_four' {G : Type u_1} [] [] [] :
theorem IsKleinFour.not_isCyclic {G : Type u_1} [] [] :
theorem IsAddKleinFour.neg_eq_self {G : Type u_1} [] [] (x : G) :
-x = x
theorem IsKleinFour.inv_eq_self {G : Type u_1} [] [] (x : G) :
x⁻¹ = x
theorem IsAddKleinFour.add_self {G : Type u_1} [] [] (x : G) :
x + x = 0
theorem IsKleinFour.mul_self {G : Type u_1} [] [] (x : G) :
x * x = 1
theorem IsAddKleinFour.eq_finset_univ {G : Type u_1} [] [] [] [] {x : G} {y : G} (hx : x 0) (hy : y 0) (hxy : x y) :
{x + y, x, y, 0} = Finset.univ
theorem IsKleinFour.eq_finset_univ {G : Type u_1} [] [] [] [] {x : G} {y : G} (hx : x 1) (hy : y 1) (hxy : x y) :
{x * y, x, y, 1} = Finset.univ
theorem IsAddKleinFour.eq_add_of_ne_all {G : Type u_1} [] [] {x : G} {y : G} {z : G} (hx : x 0) (hy : y 0) (hxy : x y) (hz : z 0) (hzx : z x) (hzy : z y) :
z = x + y
theorem IsKleinFour.eq_mul_of_ne_all {G : Type u_1} [] [] {x : G} {y : G} {z : G} (hx : x 1) (hy : y 1) (hxy : x y) (hz : z 1) (hzx : z x) (hzy : z y) :
z = x * y
def IsAddKleinFour.addEquiv' {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [] (e : G₁ G₂) (he : e 0 = 0) (h : ) :
G₁ ≃+ G₂

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
• = { toEquiv := e, map_add' := (_ : ∀ (x y : G₁), Equiv.toFun e (x + y) = + ) }
Instances For
theorem IsAddKleinFour.addEquiv'.proof_1 {G₁ : Type u_2} {G₂ : Type u_1} [AddGroup G₁] [AddGroup G₂] [] (e : G₁ G₂) (he : e 0 = 0) (h : ) (x : G₁) (y : G₁) :
Equiv.toFun e (x + y) = +
def IsKleinFour.mulEquiv' {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [] (e : G₁ G₂) (he : e 1 = 1) (h : = 2) :
G₁ ≃* G₂

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
• = { toEquiv := e, map_mul' := (_ : ∀ (x y : G₁), Equiv.toFun e (x * y) = * ) }
Instances For
@[reducible]
def IsAddKleinFour.addEquiv {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [] [] (e : G₁ G₂) (he : e 0 = 0) :
G₁ ≃+ G₂

Any two IsAddKleinFour groups are isomorphic via any equivalence which sends the identity of one group to the identity of the other.

Equations
Instances For
@[reducible]
def IsKleinFour.mulEquiv {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [] [] (e : G₁ G₂) (he : e 1 = 1) :
G₁ ≃* G₂

Any two IsKleinFour groups are isomorphic via any equivalence which sends the identity of one group to the identity of the other.

Equations
Instances For
Nonempty (G₁ ≃+ G₂)

Any two IsAddKleinFour groups are isomorphic.

theorem IsKleinFour.nonempty_mulEquiv {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [] [] :
Nonempty (G₁ ≃* G₂)

Any two IsKleinFour groups are isomorphic.