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

Klein four-groups as a mixin class

class IsAddKleinFour (G : Type u_1) [AddGroup G] : Prop

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

• card_four : Nat.card G = 4
• exponent_two : AddMonoid.exponent G = 2

class IsKleinFour (G : Type u_1) [Group G] : Prop

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

• card_four : Nat.card G = 4
• exponent_two : Monoid.exponent G = 2

instance instIsAddKleinFourProdZModOfNatNat : IsAddKleinFour (ZMod 2 × ZMod 2)

instance instIsAddKleinFourAdditiveOfIsKleinFour {G : Type u_1} [Group G] [IsKleinFour G] : IsAddKleinFour (Additive G)

instance instIsKleinFourMultiplicativeOfIsAddKleinFour {G : Type u_1} [AddGroup G] [IsAddKleinFour G] : IsKleinFour (Multiplicative G)

theorem IsKleinFour.instFinite {G : Type u_1} [Group G] [IsKleinFour G] : Finite G

This instance is scoped, because it always applies (which makes linting and typeclass inference potentially a lot slower).

theorem IsAddKleinFour.instFinite {G : Type u_1} [AddGroup G] [IsAddKleinFour G] : Finite G

@[simp]

theorem IsKleinFour.card_four' {G : Type u_1} [Group G] [Fintype G] [IsKleinFour G] : Fintype.card G = 4

@[simp]

theorem IsAddKleinFour.card_four' {G : Type u_1} [AddGroup G] [Fintype G] [IsAddKleinFour G] : Fintype.card G = 4

theorem IsKleinFour.not_isCyclic {G : Type u_1} [Group G] [IsKleinFour G] : ¬IsCyclic G

theorem IsAddKleinFour.not_isAddCyclic {G : Type u_1} [AddGroup G] [IsAddKleinFour G] : ¬IsAddCyclic G

theorem IsKleinFour.inv_eq_self {G : Type u_1} [Group G] [IsKleinFour G] (x : G) : x⁻¹ = x

theorem IsAddKleinFour.neg_eq_self {G : Type u_1} [AddGroup G] [IsAddKleinFour G] (x : G) : -x = x

theorem IsKleinFour.mul_self {G : Type u_1} [Group G] [IsKleinFour G] (x : G) : x * x = 1

theorem IsAddKleinFour.add_self {G : Type u_1} [AddGroup G] [IsAddKleinFour G] (x : G) : x + x = 0

theorem IsKleinFour.eq_finset_univ {G : Type u_1} [Group G] [IsKleinFour G] [Fintype G] [DecidableEq G] {x y : G} (hx : x ≠ 1) (hy : y ≠ 1) (hxy : x ≠ y) : {x * y, x, y, 1} = Finset.univ

theorem IsAddKleinFour.eq_finset_univ {G : Type u_1} [AddGroup G] [IsAddKleinFour G] [Fintype G] [DecidableEq G] {x y : G} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x ≠ y) : {x + y, x, y, 0} = Finset.univ

theorem IsKleinFour.eq_mul_of_ne_all {G : Type u_1} [Group G] [IsKleinFour G] {x y 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.eq_add_of_ne_all {G : Type u_1} [AddGroup G] [IsAddKleinFour G] {x y z : G} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x ≠ y) (hz : z ≠ 0) (hzx : z ≠ x) (hzy : z ≠ y) : z = x + y

def IsKleinFour.mulEquiv' {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [IsKleinFour G₁] (e : G₁ ≃ G₂) (he : e 1 = 1) (h : Monoid.exponent G₂ = 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

• IsKleinFour.mulEquiv' e he h = { toEquiv := e, map_mul' := ⋯ }

def IsAddKleinFour.addEquiv' {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [IsAddKleinFour G₁] (e : G₁ ≃ G₂) (he : e 0 = 0) (h : AddMonoid.exponent G₂ = 2) : 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

• IsAddKleinFour.addEquiv' e he h = { toEquiv := e, map_add' := ⋯ }

@[reducible, inline]

abbrev IsKleinFour.mulEquiv {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [IsKleinFour G₁] [IsKleinFour 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

• IsKleinFour.mulEquiv e he = IsKleinFour.mulEquiv' e he ⋯

@[reducible, inline]

abbrev IsAddKleinFour.addEquiv {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [IsAddKleinFour G₁] [IsAddKleinFour 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

• IsAddKleinFour.addEquiv e he = IsAddKleinFour.addEquiv' e he ⋯

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

Any two IsKleinFour groups are isomorphic.

theorem IsAddKleinFour.nonempty_addEquiv {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [IsAddKleinFour G₁] [IsAddKleinFour G₂] : Nonempty (G₁ ≃+ G₂)

Any two IsAddKleinFour groups are isomorphic.