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

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

# 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
@[simp]
theorem IsAddKleinFour.card_four {G : Type u_1} [] [self : ] :
= 4
@[simp]
theorem IsAddKleinFour.exponent_two {G : Type u_1} [] [self : ] :
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
@[simp]
theorem IsKleinFour.card_four {G : Type u_1} [] [self : ] :
= 4
@[simp]
theorem IsKleinFour.exponent_two {G : Type u_1} [] [self : ] :
Equations
Equations
• =
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 IsAddKleinFour.not_isAddCyclic {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
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₁) :
e.toFun (x + y) = e.toFun x + e.toFun 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' := }
Instances For
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' := }
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
theorem IsAddKleinFour.nonempty_addEquiv {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [] [] :
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.