Change of reference family and double cosets

The coordinatewise identity comparison restrictedProductCongr identifies the ambient restricted products only. It need not carry the everywhere-integral subgroup of one family onto that of the other; the counterexample exists_map_integralSubgroup_ne is recorded alongside the isomorphism in TauCeti.Topology.Algebra.RestrictedProduct.Congr.Basic. For this reason doubleCosetCongr is stated along the transported subgroups rather than along the integral subgroup of the new family.

References

• A. Weil, Basic Number Theory.

def TauCeti.doubleCosetCongr {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (Γ K : Subgroup (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)) : DoubleCoset.Quotient ↑Γ ↑K ≃ DoubleCoset.Quotient ↑(Subgroup.map (↑(restrictedProductCongr U U' h)) Γ) ↑(Subgroup.map (↑(restrictedProductCongr U U' h)) K)

Transport of a double-coset space along a change of reference family. The subgroups on the right are the images of those on the left under restrictedProductCongr, not the integral subgroups of the new family; see exists_map_integralSubgroup_ne.

theorem TauCeti.doubleCosetCongr_apply_mk {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (Γ K : Subgroup (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) : (doubleCosetCongr U U' h Γ K) (DoubleCoset.mk Γ K x) = DoubleCoset.mk (Subgroup.map (↑(restrictedProductCongr U U' h)) Γ) (Subgroup.map (↑(restrictedProductCongr U U' h)) K) ((restrictedProductCongr U U' h) x)

The transported double-coset space sends the double coset of x to the double coset of its image under the change-of-family equivalence.

Not a simp lemma: the type of doubleCosetCongr mentions the coercions ↑(Γ.map e) and ↑(K.map e), which Subgroup.coe_map rewrites, so the left-hand side is not in simp-normal form. Use DoubleCoset.quotientCongr_apply_mk after unfolding, or rewrite with this lemma directly.

theorem TauCeti.doubleCosetCongr_symm_apply_mk {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (Γ K : Subgroup (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)) (y : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U' i)) Filter.cofinite) : (doubleCosetCongr U U' h Γ K).symm (DoubleCoset.mk (Subgroup.map (↑(restrictedProductCongr U U' h)) Γ) (Subgroup.map (↑(restrictedProductCongr U U' h)) K) y) = DoubleCoset.mk Γ K ((restrictedProductCongr U U' h).symm y)

The inverse of the transported double-coset space sends the double coset of y to the double coset of its image under the inverse change-of-family equivalence.

Not a simp lemma, for the same reason as doubleCosetCongr_apply_mk.