Maps between double-coset quotients

Enlarging either subgroup coarsens the double-coset relation. This file packages the resulting surjections, records their values on representatives, and proves their identity and composition laws. It also transports a double-coset space along a group isomorphism, identifies the quotients by conjugate right subgroups by right translation, and carries a single double coset along a multiplicative map: DoubleCoset.image_doubleCoset computes the image, and DoubleCoset.mem_doubleCoset_image_iff transports membership along an injective multiplicative map.

These are the double-coset analogues of Subgroup.quotientMapOfLE and QuotientGroup.congr for ordinary coset spaces.

def DoubleCoset.quotientMapOfLELeft {G : Type u_1} [Group G] {H H' : Subgroup G} (h : H ≤ H') (K : Subgroup G) : Quotient ↑H ↑K → Quotient ↑H' ↑K

The map H \ G / K → H' \ G / K induced by an inclusion H ≤ H'.

@[simp]

theorem DoubleCoset.quotientMapOfLELeft_apply_mk {G : Type u_1} [Group G] {H H' : Subgroup G} (h : H ≤ H') (K : Subgroup G) (g : G) : quotientMapOfLELeft h K (mk H K g) = mk H' K g

The map induced by H ≤ H' sends the double coset of g to the double coset of g.

@[simp]

theorem DoubleCoset.quotientMapOfLELeft_refl {G : Type u_1} [Group G] (H K : Subgroup G) : quotientMapOfLELeft ⋯ K = id

The double-coset quotient map induced by reflexivity is the identity.

theorem DoubleCoset.quotientMapOfLELeft_trans {G : Type u_1} [Group G] {H H' H'' : Subgroup G} (h : H ≤ H') (h' : H' ≤ H'') (K : Subgroup G) : quotientMapOfLELeft ⋯ K = quotientMapOfLELeft h' K ∘ quotientMapOfLELeft h K

Double-coset quotient maps compose along inclusions of left subgroups.

theorem DoubleCoset.quotientMapOfLELeft_surjective {G : Type u_1} [Group G] {H H' : Subgroup G} (h : H ≤ H') (K : Subgroup G) : Function.Surjective (quotientMapOfLELeft h K)

Enlarging the left subgroup gives a surjection on double-coset quotients.

def DoubleCoset.quotientMapOfLERight {G : Type u_1} [Group G] (H : Subgroup G) {K K' : Subgroup G} (h : K ≤ K') : Quotient ↑H ↑K → Quotient ↑H ↑K'

The map H \ G / K → H \ G / K' induced by an inclusion K ≤ K'.

@[simp]

theorem DoubleCoset.quotientMapOfLERight_apply_mk {G : Type u_1} [Group G] (H : Subgroup G) {K K' : Subgroup G} (h : K ≤ K') (g : G) : quotientMapOfLERight H h (mk H K g) = mk H K' g

The map induced by K ≤ K' sends the double coset of g to the double coset of g.

@[simp]

theorem DoubleCoset.quotientMapOfLERight_refl {G : Type u_1} [Group G] (H K : Subgroup G) : quotientMapOfLERight H ⋯ = id

The right double-coset quotient map induced by reflexivity is the identity.

theorem DoubleCoset.quotientMapOfLERight_trans {G : Type u_1} [Group G] {K K' K'' : Subgroup G} (H : Subgroup G) (h : K ≤ K') (h' : K' ≤ K'') : quotientMapOfLERight H ⋯ = quotientMapOfLERight H h' ∘ quotientMapOfLERight H h

Double-coset quotient maps compose along inclusions of right subgroups.

theorem DoubleCoset.quotientMapOfLERight_surjective {G : Type u_1} [Group G] (H : Subgroup G) {K K' : Subgroup G} (h : K ≤ K') : Function.Surjective (quotientMapOfLERight H h)

Enlarging the right subgroup gives a surjection on double-coset quotients.

def DoubleCoset.quotientConjRight {G : Type u_1} [Group G] (H K : Subgroup G) (g : G) : Quotient ↑H ↑K ≃ Quotient ↑H ↑(Subgroup.map (↑(MulEquiv.symm (MulAut.conj g))) K)

Right translation by g identifies quotients by K and by the conjugate g⁻¹Kg.

theorem DoubleCoset.quotientConjRight_apply_mk {G : Type u_1} [Group G] (H K : Subgroup G) (g x : G) : (quotientConjRight H K g) (mk H K x) = mk H (Subgroup.map (↑(MulEquiv.symm (MulAut.conj g))) K) (x * g)

Right translation sends the double coset of x to the double coset of x * g.

Not a simp lemma: the codomain contains a coerced mapped subgroup, which simp rewrites to a set image in the dependent type.

theorem DoubleCoset.quotientConjRight_symm_apply_mk {G : Type u_1} [Group G] (H K : Subgroup G) (g y : G) : (quotientConjRight H K g).symm (mk H (Subgroup.map (↑(MulEquiv.symm (MulAut.conj g))) K) y) = mk H K (y * g⁻¹)

The inverse conjugation equivalence sends the double coset of y to that of y * g⁻¹.

Not a simp lemma, for the same dependent-type reason as quotientConjRight_apply_mk.

def DoubleCoset.quotientCongr {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] (H K : Subgroup G) {H' K' : Subgroup G'} (e : G ≃* G') (hH : Subgroup.map (↑e) H = H') (hK : Subgroup.map (↑e) K = K') : Quotient ↑H ↑K ≃ Quotient ↑H' ↑K'

Transport of a double-coset space along a group isomorphism e : G ≃* G': the equivalence H \ G / K ≃ H' \ G' / K' when H' and K' are the images of H and K under e.

@[simp]

theorem DoubleCoset.quotientCongr_apply_mk {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] (H K : Subgroup G) {H' K' : Subgroup G'} (e : G ≃* G') (hH : Subgroup.map (↑e) H = H') (hK : Subgroup.map (↑e) K = K') (g : G) : (quotientCongr H K e hH hK) (mk H K g) = mk H' K' (e g)

The transported double-coset space sends the double coset of g to that of e g.

@[simp]

theorem DoubleCoset.quotientCongr_symm_apply_mk {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] (H K : Subgroup G) {H' K' : Subgroup G'} (e : G ≃* G') (hH : Subgroup.map (↑e) H = H') (hK : Subgroup.map (↑e) K = K') (g : G') : (quotientCongr H K e hH hK).symm (mk H' K' g) = mk H K (e.symm g)

The inverse of the transported double-coset space sends the double coset of g to that of e.symm g.

theorem DoubleCoset.image_doubleCoset {α : Type u_3} {β : Type u_4} {F : Type u_5} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) (a : α) (s t : Set α) : ⇑f '' doubleCoset a s t = doubleCoset (f a) (⇑f '' s) (⇑f '' t)

A multiplicative map sends the double coset of a by s and t onto the double coset of f a by the images of s and t.

theorem DoubleCoset.mem_doubleCoset_image_iff {α : Type u_3} {β : Type u_4} {F : Type u_5} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] {f : F} (hf : Function.Injective ⇑f) (a : α) (s t : Set α) (x : α) : f x ∈ doubleCoset (f a) (⇑f '' s) (⇑f '' t) ↔ x ∈ doubleCoset a s t

An injective multiplicative map transports membership in a double coset.