Addenda to the group theory in mathlib

This file adds some basic results about group theory and more specificially finite group quotiented by their center.

Main results

We create the set of representatives of G⧸ (Subgroup.center G) and verify the properties that this set is suppose to satisfy. We then introduce two maps G_to_syst and G_to_center that associated to every g : G its representatives and its Subgroup.center G parts.

Contents

• system_of_repr_center.set G : the set of representatives of G⧸ (Subgroup.center G).
• G_to_syst G : the map that associated to every g : G its representative.
• G_to_center G : the map that associated to every g : G the elements h : Subgroup.center G such that g = gg*h where gg : system_of_repr_center.set G.
• system_of_repr_center.set_center_iso_G and system_of_repr_center.set_center_iso_G_sigma which are bijections between G and the cartesian product of system_of_repr_center.set G and Subgroup.center G as a cartesian product and as a Sigma type.

theorem center_mul_comm (G : Type u_2) [inst2 : Group G] (g : G) (h : ↥(Subgroup.center G)) : ↑h * g = g * ↑h

An element of type Subgroup.center G commutes with every element of type G.

@[simp]

theorem center_mul (G : Type u_2) [inst2 : Group G] (h : ↥(Subgroup.center G)) (a b : G) (h1 : ↑h = a * b) : ↑h = b * a

simp lemma associated to center_mul_comm.

@[reducible, inline]

abbrev system_of_repr_center.set (G : Type u_2) [inst2 : Group G] : Set G

Equations

• system_of_repr_center.set G = Set.range Quotient.out

noncomputable instance system_of_repr_center.instFintype_myProject (G : Type u_2) [inst3 : Finite G] : Fintype G

A set of representatives of the classes of G⧸ (Subgroup.center G).

Equations

• system_of_repr_center.instFintype_myProject G = Fintype.ofFinite G

instance system_of_repr_center.instFiniteSubtypeMemSubgroup_myProject (G : Type u_2) [inst2 : Group G] [inst3 : Finite G] (H : Subgroup G) : Finite ↥H

instance system_of_repr_center.finite (G : Type u_2) [inst2 : Group G] (h : Finite G) : Finite ↑(set G)

system_of_rep_center_set is finite.

theorem system_of_repr_center.classes_disjoint (G : Type u_2) [inst2 : Group G] (g g' : G) (hG : g ∈ set G) (hG' : g' ∈ set G) : g ≠ g' → {x : G | (QuotientGroup.con (Subgroup.center G)).toSetoid x g} ∩ {x : G | (QuotientGroup.con (Subgroup.center G)).toSetoid x g'} = ∅

theorem system_of_repr_center.classes_union_eq_univ (G : Type u_2) [inst2 : Group G] : Set.univ = ⋃ g ∈ set G, {x : G | (QuotientGroup.con (Subgroup.center G)).toSetoid x g}

Union of the classes of elements of system_of_repr_center.set is the whole group.

noncomputable def system_of_repr_center.set_bij (G : Type u_2) [inst2 : Group G] [inst3 : Finite G] : ↑(set G) ≃ { x : Quotient (QuotientGroup.con (Subgroup.center G)).toSetoid // x ∈ Finset.image (Quotient.mk (QuotientGroup.con (Subgroup.center G)).toSetoid) Finset.univ }

system_of_repr_center G is equivalent to the image of the application G → G⧸ (Subgroup.center G).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def system_of_repr_center.G_to_syst (G : Type u_2) [inst2 : Group G] : G → ↑(set G)

A function that associates to every element g:G the corresponding representative in system_of_repr_center.set.

Equations

• system_of_repr_center.G_to_syst G g = id ⟨⟦g⟧.out, ⋯⟩

@[simp]

theorem system_of_repr_center.G_to_syst_simp (G : Type u_2) [inst2 : Group G] (g : G) (h : ↥(Subgroup.center G)) : G_to_syst G (g * ↑h) = G_to_syst G g

If h : Subgroup.center G, then G_to_syst G (g*h) = G_to_syst G g for every g:G.

noncomputable def system_of_repr_center.G_to_center (G : Type u_2) [inst2 : Group G] : G → ↥(Subgroup.center G)

A function that associates to every element g:G the corresponding z : Subgroup.center G sucht that Quotient.out ↑g = g * z.

Equations

• system_of_repr_center.G_to_center G u = ⋯.choose⁻¹

theorem system_of_repr_center.G_to_center_simp (G : Type u_2) [inst2 : Group G] (g : G) : g = ⟦g⟧.out * ↑(G_to_center G g)

Decomposition of an element g:G into a product of an element of Subgroup.center G by an element of G.

theorem system_of_repr_center.G_eq_G_to_center_G_to_syst_simp (G : Type u_2) [inst2 : Group G] (g : G) : g = ↑(G_to_syst G g) * ↑(G_to_center G g)

G_to_center_simp written with G_to_syst and G_to_center.

theorem system_of_repr_center.G_to_center_to_syst_comm (G : Type u_2) [inst2 : Group G] (g : G) : ↑(G_to_center G g) * ↑(G_to_syst G g) = ↑(G_to_syst G g) * ↑(G_to_center G g)

Commutativity of the product of G_to_center G g and G_to_syst G g for every g : G.

theorem system_of_repr_center.G_to_center_eq_G_G_to_syst_simp (G : Type u_2) [inst2 : Group G] (g : G) : ↑(G_to_center G g) = g * (↑(G_to_syst G g))⁻¹

G_to_center_to_syst_simp written with G_to_center on the right side of the equality.

@[simp]

theorem system_of_repr_center.G_to_center_syst_apply_simp (G : Type u_2) [inst2 : Group G] (g : ↑(set G)) : G_to_center G ↑g = 1

If g : system_of_repr_center.set G then G_to_center G g.1 is equal to the neutral of the group.

@[simp]

theorem system_of_repr_center.G_to_syst_simp_id (G : Type u_2) [inst2 : Group G] (g : ↑(set G)) : G_to_syst G ↑g = g

If g : system_of_repr_center.set G then G_to_syst G g is equal to g.

@[simp]

theorem system_of_repr_center.G_to_center_mul_simp (G : Type u_2) [inst2 : Group G] (g : G) (h : ↥(Subgroup.center G)) : G_to_center G (g * ↑h) = h * G_to_center G g

For every g:G and h : Subgroup.center G, we have the following identity : G_to_center G (g*h) = h * G_to_center G g.

theorem system_of_repr_center.G_to_syst_mul (G : Type u_2) [inst2 : Group G] (g : G) (gbar : ↑(set G)) : G_to_syst G (g * ↑gbar) = G_to_syst G (↑(G_to_syst G g) * ↑gbar)

noncomputable def system_of_repr_center.set_center_iso_G (G : Type u_2) [inst2 : Group G] : G ≃ ↥(Subgroup.center G) × ↑(set G)

G is equivalent to the cartesian product of its center and system_of_repr_center.set G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def system_of_repr_center.set_center_iso_G_sigma (G : Type u_2) [inst2 : Group G] : (_ : ↥(Subgroup.center G)) × ↑(set G) ≃ G

system_of_repr_center.set_center_iso_G written for Sigma types instead of cartesian product.

Equations

• One or more equations did not get rendered due to their size.

theorem system_of_repr_center.set_center_eq_G (G : Type u_2) [inst2 : Group G] : Set.univ = {x : G | ∃ (g : ↑(set G)) (h : ↥(Subgroup.center G)), ↑g * ↑h = x}

system_of_repr_center.set_center_iso_G written as sets.

noncomputable def system_of_repr_center.equiv_perm_fun (G : Type u_2) [inst2 : Group G] (g : G) : ↑(set G) → ↑(set G)

Equations

• system_of_repr_center.equiv_perm_fun G g gi = system_of_repr_center.G_to_syst G (g * ↑gi)

theorem system_of_repr_center.equiv_perm_fun_apply (G : Type u_2) [inst2 : Group G] (g : G) (gi : ↑(set G)) : g * ↑gi = ↑(equiv_perm_fun G g gi) * ↑(G_to_center G (g * ↑gi))

noncomputable def system_of_repr_center.equiv_perm (G : Type u_2) [inst2 : Group G] (g : G) : Equiv.Perm ↑(set G)

Equations

• One or more equations did not get rendered due to their size.

theorem system_of_repr_center.equiv_perm_exists (G : Type u_2) [inst2 : Group G] [inst3 : Finite G] (g : G) : ∃ (σ : Equiv.Perm ↑(set G)), ∀ (gbar : ↑(set G)), g * ↑gbar = ↑(σ gbar) * ↑(G_to_center G (g * ↑gbar))