Left translation on a coset space

A group G acts on the quotient G ⧸ H by translation. This file records the stabilizer of a coset for that action, and, for the trivial subgroup, the compatibility of the identification QuotientGroup.quotientBot : G ⧸ ⊥ ≃* G with translation.

The stabilizer of the coset sH is the conjugate subgroup sHs⁻¹ (TauCeti.stabilizer_quotientGroup_mk); this is Mathlib's MulAction.stabilizer_quotient, which covers the trivial coset, transported along MulAction.stabilizer_smul_eq_stabilizer_map_conj. Read on elements, it says that g fixes sH exactly when s⁻¹ g s lies in H (TauCeti.smul_quotientGroup_mk_eq_self_iff), which is the form a fixed-coset count is checked in. Reading that criterion over all of G counts the elements x with x⁻¹ g x ∈ H: they form the preimage of the g-fixed cosets, a union of |(G ⧸ H)^g| cosets of H, hence there are |H| * |(G ⧸ H)^g| of them (Subgroup.natCard_mul_natCard_fixedBy).

The cosets of ⊥ in a group G are the elements of G, and Mathlib's QuotientGroup.quotientBot is that identification. The identification is equivariant for left translation, and the only element of G fixing a coset of ⊥ is the identity.

For a finite group, a sum can also be split over the left or right cosets of a subgroup by using Quotient.out as a transversal.

Main statements

• TauCeti.stabilizer_quotientGroup_mk: the stabilizer of sH in G is sHs⁻¹.
• TauCeti.smul_quotientGroup_mk_eq_self_iff: g fixes the coset sH exactly when s⁻¹ g s lies in H.
• Subgroup.natCard_mul_natCard_fixedBy: the elements conjugating g into H number |H| * |(G ⧸ H)^g|.
• TauCeti.smul_quotient_eq_self_of_mem: an element of a normal subgroup fixes every coset.
• TauCeti.quotientBot_equivariant: QuotientGroup.quotientBot intertwines left translation on G ⧸ ⊥ with left translation in G.
• TauCeti.quotientBot_smul_eq_self_iff: a group element fixes a coset of the trivial subgroup only when it is the identity.
• Subgroup.sum_eq_sum_leftCosets and Subgroup.sum_eq_sum_rightCosets: split a finite sum along the left or right cosets of a subgroup.
• QuotientGroup.eq_subgroupOf: two elements of a subgroup H lie in the same left coset of N.subgroupOf H exactly when they lie in the same left coset of N.
• QuotientGroup.out_mul_out_mul_inv_mem: the defect of the representatives chosen by Quotient.out from preserving multiplication lies in the subgroup.

@[simp]

theorem TauCeti.smul_quotient_eq_self_of_mem {G : Type u_1} [Group G] {N : Subgroup G} [N.Normal] {γ : G} (hγ : γ ∈ N) (u : G ⧸ N) : γ • u = u

An element of a normal subgroup N fixes every coset of N.

@[simp]

theorem TauCeti.stabilizer_quotientGroup_mk {G : Type u_1} [Group G] (H : Subgroup G) (s : G) : MulAction.stabilizer G ↑s = MulAut.conj s • H

The stabilizer of the coset sH, for the translation action of G on G ⧸ H, is the conjugate subgroup sHs⁻¹. This is Mathlib's MulAction.stabilizer_quotient transported off the trivial coset along MulAction.stabilizer_smul_eq_stabilizer_map_conj.

theorem TauCeti.smul_quotientGroup_mk_eq_self_iff {G : Type u_1} [Group G] (H : Subgroup G) (g s : G) : g • ↑s = ↑s ↔ s⁻¹ * g * s ∈ H

A group element fixes the coset sH exactly when its conjugate s⁻¹gs lies in H. This is TauCeti.stabilizer_quotientGroup_mk read on elements.

Not a simp lemma: MulAction.Quotient.smul_coe rewrites the translation inside the left-hand side first, so the left-hand side is not in simp-normal form.

theorem Subgroup.natCard_mul_natCard_fixedBy {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : Nat.card ↥H * Nat.card ↑(MulAction.fixedBy (G ⧸ H) g) = Nat.card { x : G // x⁻¹ * g * x ∈ H }

The elements x of G with x⁻¹ g x ∈ H are the preimage of the g-fixed points of G ⧸ H, a union of |(G ⧸ H)^g| cosets of H.

theorem TauCeti.quotientBot_smul {G : Type u_1} [Group G] (g x : G) : QuotientGroup.quotientBot (g • ↑x) = g * QuotientGroup.quotientBot ↑x

Left translation on the cosets of the trivial subgroup is left translation in the group.

Not a simp lemma: simp rewrites the left-hand side further, to QuotientGroup.quotientBot (↑g * ↑x).

theorem TauCeti.quotientBot_equivariant {G : Type u_1} [Group G] (g : G) (q : G ⧸ ⊥) : QuotientGroup.quotientBot.toEquiv (g • q) = g • QuotientGroup.quotientBot.toEquiv q

Identifying the cosets of the trivial subgroup with the group is equivariant for left translation.

Not a simp lemma: simp rewrites MulEquiv.toEquiv away in the left-hand side.

@[simp]

theorem TauCeti.quotientBot_smul_eq_self_iff {G : Type u_1} [Group G] (g : G) (q : G ⧸ ⊥) : g • q = q ↔ g = 1

A group element fixes a coset of the trivial subgroup exactly when it is the identity.

theorem QuotientGroup.eq_subgroupOf {G : Type u_1} [Group G] {H N : Subgroup G} {x y : ↥H} : ↑x = ↑y ↔ ↑↑x = ↑↑y

Two elements of a subgroup H lie in the same left coset of N.subgroupOf H exactly when they lie in the same left coset of N.

theorem QuotientGroup.out_mul_out_mul_inv_mem {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (q r : G ⧸ N) : Quotient.out q * Quotient.out r * (Quotient.out (q * r))⁻¹ ∈ N

The representatives chosen by Quotient.out preserve multiplication up to an element of the normal subgroup: q.out * r.out * (q * r).out⁻¹ ∈ N.

theorem Subgroup.sum_eq_sum_leftCosets {G : Type u_1} [Group G] {M : Type u_2} [AddCommMonoid M] [Fintype G] (H : Subgroup G) (f : G → M) : ∑ g : G, f g = ∑ q : G ⧸ H, ∑ h : ↥H, f (Quotient.out q * ↑h)

Every element of a finite group G is uniquely the product of the Quotient.out representative of a left coset of H and an element of H.

theorem Subgroup.sum_eq_sum_rightCosets {G : Type u_1} [Group G] {M : Type u_2} [AddCommMonoid M] [Fintype G] (H : Subgroup G) (f : G → M) : ∑ g : G, f g = ∑ q : G ⧸ H, ∑ h : ↥H, f (↑h * (Quotient.out q)⁻¹)

The right-coset form of Subgroup.sum_eq_sum_leftCosets.