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} [AddGroup G] (hG : AddMonoid.exponent G = 2) (x : G) : -x = x

theorem inv_eq_self_of_exponent_two {G : Type u_1} [Group G] (hG : Monoid.exponent G = 2) (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} [AddGroup G] {x : G} (hx : addOrderOf x = 2) : -x = x

theorem inv_eq_self_of_orderOf_eq_two {G : Type u_1} [Group G] {x : G} (hx : orderOf x = 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} [AddGroup G] (hG : AddMonoid.exponent G = 2) {x : G} : addOrderOf x = 2 ↔ x ≠ 0

theorem orderOf_eq_two_iff {G : Type u_1} [Group G] (hG : Monoid.exponent G = 2) {x : G} : orderOf x = 2 ↔ x ≠ 1

theorem add_comm_of_exponent_two {G : Type u_1} [AddGroup G] (hG : AddMonoid.exponent G = 2) (x : G) (y : G) : x + y = y + x

theorem mul_comm_of_exponent_two {G : Type u_1} [Group G] (hG : Monoid.exponent G = 2) (x : G) (y : G) : x * y = y * x

In a group of exponent two, all elements commute.

@[reducible]

def instAddCommGroupOfExponentTwo {G : Type u_1} [AddGroup G] (hG : AddMonoid.exponent G = 2) : AddCommGroup G

Any additive group of exponent two is abelian.

Equations

• instAddCommGroupOfExponentTwo hG = AddCommGroup.mk (_ : ∀ (x y : G), x + y = y + x)

@[reducible]

def instCommGroupOfExponentTwo {G : Type u_1} [Group G] (hG : Monoid.exponent G = 2) : CommGroup G

Any group of exponent two is abelian.

Equations

• instCommGroupOfExponentTwo hG = CommGroup.mk (_ : ∀ (x y : G), x * y = y * x)

theorem add_not_mem_of_addOrderOf_eq_two {G : Type u_2} [AddGroup G] {x : G} {y : G} (hx : addOrderOf x = 2) (hy : addOrderOf y = 2) (hxy : x ≠ y) : x + y ∉ {x, y, 0}

theorem mul_not_mem_of_orderOf_eq_two {G : Type u_2} [Group G] {x : G} {y : G} (hx : orderOf x = 2) (hy : orderOf y = 2) (hxy : x ≠ y) : x * y ∉ {x, y, 1}

theorem add_not_mem_of_exponent_two {G : Type u_2} [AddGroup G] (h : AddMonoid.exponent G = 2) {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} [Group G] (h : Monoid.exponent G = 2) {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) [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 instIsAddKleinFourProdZModOfNatNatInstOfNatNatInstAddGroupToAddGroupToAddGroupWithOneToRingToDivisionRingInstFieldZModFact_prime_two : IsAddKleinFour (ZMod 2 × ZMod 2)

Equations

• instIsAddKleinFourProdZModOfNatNatInstOfNatNatInstAddGroupToAddGroupToAddGroupWithOneToRingToDivisionRingInstFieldZModFact_prime_two = (_ : IsAddKleinFour (ZMod 2 × ZMod 2))

instance instIsKleinFourDihedralGroupOfNatNatInstOfNatNatInstGroupDihedralGroup : IsKleinFour (DihedralGroup 2)

Equations

• instIsKleinFourDihedralGroupOfNatNatInstOfNatNatInstGroupDihedralGroup = (_ : IsKleinFour (DihedralGroup 2))

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

Equations

• (_ : IsAddKleinFour (Additive G)) = (_ : IsAddKleinFour (Additive G))

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

Equations

• (_ : IsKleinFour (Multiplicative G)) = (_ : IsKleinFour (Multiplicative G))

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

Equations

• (_ : Finite G) = (_ : Finite G)

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

Equations

• (_ : Finite G) = (_ : Finite G)

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem IsAddKleinFour.eq_finset_univ {G : Type u_1} [AddGroup G] [IsAddKleinFour G] [Fintype G] [DecidableEq G] {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} [Group G] [IsKleinFour G] [Fintype G] [DecidableEq G] {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} [AddGroup G] [IsAddKleinFour G] {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} [Group G] [IsKleinFour G] {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₂] [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' := (_ : ∀ (x y : G₁), e.toFun (x + y) = e.toFun x + e.toFun y) }

theorem IsAddKleinFour.addEquiv'.proof_1 {G₁ : Type u_2} {G₂ : Type u_1} [AddGroup G₁] [AddGroup G₂] [IsAddKleinFour G₁] (e : G₁ ≃ G₂) (he : e 0 = 0) (h : AddMonoid.exponent G₂ = 2) (x : G₁) (y : G₁) : e.toFun (x + y) = e.toFun x + e.toFun 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' := (_ : ∀ (x y : G₁), e.toFun (x * y) = e.toFun x * e.toFun y) }

@[reducible]

def 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 (_ : AddMonoid.exponent G₂ = 2)

@[reducible]

def 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 (_ : Monoid.exponent G₂ = 2)

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.

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.