Evaluating the decomposition of a group into cosets and a subgroup

For a subgroup s of a group α, Mathlib's Subgroup.groupEquivQuotientProdSubgroup identifies α with (α ⧸ s) × s, using the chosen representatives Quotient.out of the left cosets. It is built as a composite of equivalences through a Sigma type, one step of which is a cast along the equality of a coset with the fibre of the quotient map, so its values are not available by unfolding. This file records them:

• Subgroup.groupEquivQuotientProdSubgroup_symm_apply: the pair (q, x) goes to q.out * x;
• Subgroup.groupEquivQuotientProdSubgroup_apply: an element g goes to its coset ⟦g⟧ and the element ⟦g⟧.out⁻¹ * g of s, with the projections groupEquivQuotientProdSubgroup_apply_fst and groupEquivQuotientProdSubgroup_apply_snd_coe.

The additive versions are generated for AddSubgroup.addGroupEquivQuotientProdAddSubgroup.

The file also records how the chosen representatives behave along a tower of subgroups, along an isomorphism of groups, and under translation:

• Subgroup.mk_out_mul_out_bijective: for K ≤ H, the products p.out * k.out of chosen representatives of G ⧸ H and of H ⧸ K.subgroupOf H form a transversal of K in G;
• Subgroup.mk_mulEquiv_out_bijective: an isomorphism e : G ≃* G' carrying H onto H' carries the chosen representatives of G ⧸ H to a transversal of H' in G';
• QuotientGroup.mk_out_smul and QuotientGroup.mk_mul_out_smul: the representative of a translated coset g • q lies in the coset of g * q.out.

All of these have additive versions. Finally, Subgroup.sum_out_smul_eq_relIndex_nsmul sums an orbit map along a tower: for K ≤ H and an element m of an additive G-module fixed by H, the sum of q.out • m over the cosets of K is [H : K] times the sum over the cosets of H.

@[simp]

theorem Subgroup.groupEquivQuotientProdSubgroup_symm_apply {α : Type u_1} [Group α] {s : Subgroup α} (q : α ⧸ s) (x : ↥s) : groupEquivQuotientProdSubgroup.symm (q, x) = Quotient.out q * ↑x

The decomposition of a group into cosets and a subgroup, read backwards: the pair of a left coset q and an element x of the subgroup is the element q.out * x.

@[simp]

theorem AddSubgroup.addGroupEquivQuotientSumAddSubgroup_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (q : α ⧸ s) (x : ↥s) : addGroupEquivQuotientProdAddSubgroup.symm (q, x) = Quotient.out q + ↑x

theorem Subgroup.groupEquivQuotientProdSubgroup_apply {α : Type u_1} [Group α] {s : Subgroup α} (g : α) : groupEquivQuotientProdSubgroup g = (↑g, ⟨(Quotient.out ↑g)⁻¹ * g, ⋯⟩)

The decomposition of a group into cosets and a subgroup: an element g goes to its left coset ⟦g⟧ and the element ⟦g⟧.out⁻¹ * g of the subgroup.

theorem AddSubgroup.addGroupEquivQuotientSumAddSubgroup_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : addGroupEquivQuotientProdAddSubgroup g = (↑g, ⟨-Quotient.out ↑g + g, ⋯⟩)

@[simp]

theorem Subgroup.groupEquivQuotientProdSubgroup_apply_fst {α : Type u_1} [Group α] {s : Subgroup α} (g : α) : (groupEquivQuotientProdSubgroup g).1 = ↑g

The coset component of the decomposition of g is the coset of g.

@[simp]

theorem AddSubgroup.addGroupEquivQuotientSumAddSubgroup_apply_fst {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : (addGroupEquivQuotientProdAddSubgroup g).1 = ↑g

@[simp]

theorem Subgroup.groupEquivQuotientProdSubgroup_apply_snd_coe {α : Type u_1} [Group α] {s : Subgroup α} (g : α) : ↑(groupEquivQuotientProdSubgroup g).2 = (Quotient.out ↑g)⁻¹ * g

The subgroup component of the decomposition of g is ⟦g⟧.out⁻¹ * g.

@[simp]

theorem AddSubgroup.addGroupEquivQuotientSumAddSubgroup_apply_snd_coe {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ↑(addGroupEquivQuotientProdAddSubgroup g).2 = -Quotient.out ↑g + g

theorem Subgroup.mk_out_mul_out_bijective {G : Type u_2} [Group G] {H K : Subgroup G} (hKH : K ≤ H) : Function.Bijective fun (i : (G ⧸ H) × ↥H ⧸ K.subgroupOf H) => ↑(Quotient.out i.1 * ↑(Quotient.out i.2))

Transversals multiply along a tower. For subgroups K ≤ H of G, the products p.out * k.out of the chosen representatives of the cosets p ∈ G ⧸ H and k ∈ H ⧸ K.subgroupOf H represent each coset of K in G exactly once.

theorem AddSubgroup.mk_out_add_out_bijective {G : Type u_2} [AddGroup G] {H K : AddSubgroup G} (hKH : K ≤ H) : Function.Bijective fun (i : (G ⧸ H) × ↥H ⧸ K.addSubgroupOf H) => ↑(Quotient.out i.1 + ↑(Quotient.out i.2))

theorem Subgroup.sum_out_smul_eq_relIndex_nsmul {G : Type u_2} [Group G] {H K : Subgroup G} [K.FiniteIndex] [H.FiniteIndex] (hKH : K ≤ H) {M : Type u_3} [AddCommMonoid M] [DistribMulAction G M] {m : M} (hm : ∀ h ∈ H, h • m = m) : ∑ q : G ⧸ K, Quotient.out q • m = K.relIndex H • ∑ q : G ⧸ H, Quotient.out q • m

Summing an H-invariant orbit map along a tower. For subgroups K ≤ H of finite index in G and an element m of an additive commutative monoid with distributive G-action that is fixed by H, the sum of q.out • m over the cosets of K is [H : K] times the sum over the cosets of H: each coset of H is the union of [H : K] cosets of K, and q.out • m depends only on the coset of H containing q.out.

theorem Subgroup.mk_mulEquiv_out_bijective {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {H : Subgroup G} {H' : Subgroup G'} (e : G ≃* G') (he : ∀ (g : G), e g ∈ H' ↔ g ∈ H) : Function.Bijective fun (q : G ⧸ H) => ↑(e (Quotient.out q))

An isomorphism carries a transversal to a transversal. If e : G ≃* G' carries H onto H', then the images under e of the chosen representatives of the cosets of H represent each coset of H' exactly once. Neither subgroup need be normal.

theorem AddSubgroup.mk_addEquiv_out_bijective {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {H : AddSubgroup G} {H' : AddSubgroup G'} (e : G ≃+ G') (he : ∀ (g : G), e g ∈ H' ↔ g ∈ H) : Function.Bijective fun (q : G ⧸ H) => ↑(e (Quotient.out q))

theorem QuotientGroup.mk_out_smul {G : Type u_1} [Group G] {H : Subgroup G} (g : G) (q : G ⧸ H) : ↑(Quotient.out (g • q)) = ↑(g * Quotient.out q)

The chosen representative of the translate g • q of a left coset q lies in the same coset as g times the chosen representative of q.

theorem QuotientAddGroup.mk_out_vadd {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (g : G) (q : G ⧸ H) : ↑(Quotient.out (g +ᵥ q)) = ↑(g + Quotient.out q)

theorem QuotientGroup.mk_mul_out_smul {G : Type u_1} [Group G] {H K : Subgroup G} (a : G) (h : ↥H) (k : ↥H ⧸ K.subgroupOf H) : ↑(a * ↑(Quotient.out (h • k))) = ↑(a * ↑h * ↑(Quotient.out k))

For h ∈ H and a coset k ∈ H ⧸ K.subgroupOf H, the elements a * (h • k).out and a * h * k.out of G lie in the same left coset of K, for every a ∈ G. No inclusion K ≤ H is needed.

theorem QuotientAddGroup.mk_add_out_vadd {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (a : G) (h : ↥H) (k : ↥H ⧸ K.addSubgroupOf H) : ↑(a + ↑(Quotient.out (h +ᵥ k))) = ↑(a + ↑h + ↑(Quotient.out k))