Inverting a double coset

Inversion is an anti-automorphism of a group, so it carries the double coset Γ₁ g Γ₂ to Γ₂ g⁻¹ Γ₁: the flanking subgroups are exchanged and the element is inverted. This file records that, as a set identity and in membership form.

Exchanging the flanking subgroups is what makes inversion useful for comparing the two sides of a double coset: it turns a right-coset decomposition into a left-coset one, which is how a count indexed by right cosets is matched with one indexed by left cosets.

Main results

• DoubleCoset.doubleCoset_inv: as sets, (Γ₁ g Γ₂)⁻¹ = Γ₂ g⁻¹ Γ₁.
• DoubleCoset.inv_mem_doubleCoset_inv_iff: its membership form.

@[simp]

theorem DoubleCoset.doubleCoset_inv {G : Type u_1} [Group G] (Γ₁ Γ₂ : Subgroup G) (g : G) : (doubleCoset g ↑Γ₁ ↑Γ₂)⁻¹ = doubleCoset g⁻¹ ↑Γ₂ ↑Γ₁

Inverting a double coset exchanges its flanking subgroups. As sets, (Γ₁ g Γ₂)⁻¹ = Γ₂ g⁻¹ Γ₁.

theorem DoubleCoset.inv_mem_doubleCoset_inv_iff {G : Type u_1} [Group G] {Γ₁ Γ₂ : Subgroup G} {g x : G} : x⁻¹ ∈ doubleCoset g⁻¹ ↑Γ₂ ↑Γ₁ ↔ x ∈ doubleCoset g ↑Γ₁ ↑Γ₂

Inverting a double coset exchanges its flanking subgroups: x ∈ Γ₁ g Γ₂ if and only if x⁻¹ ∈ Γ₂ g⁻¹ Γ₁. The membership form of doubleCoset_inv.

Not @[simp], unlike doubleCoset_inv: mem_doubleCoset_iff_mk_mem_orbit already rewrites membership in a double coset to membership in a MulAction.orbit, so this left-hand side is not in simp normal form and simpNF rejects it. Apply it by name.