ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets

6 Theorems | 2 Definitions | 2 Abbreviations | 7 Instances

This module packages the finite permutation image of the coset action of an open subgroup, proves continuity of the action homomorphism, and transfers finite-group-class membership to the image.

import

ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices

Imported by

Abbreviation ReidemeisterSchreier.Profinite.openSubgroupIndexActionImage

abbrev openSubgroupIndexActionImage
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) : Type :=
  (ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom
      (G := G) (H : Subgroup G) H.isOpen'
      (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn).range

The actual permutation image of the finite coset action, before any universe lift.

Theorem ReidemeisterSchreier.Profinite.openSubgroupIndexContinuousHom_range_mem_class

theorem openSubgroupIndexContinuousHom_range_mem_class
    {C : ProCGroups.FiniteGroupClass.{u}}
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G)
    (H : OpenSubgroup G) {n : ℕ}
    (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    C.MemAcrossUniverses (openSubgroupIndexActionImage (G := G) H hn)

The actual finite permutation image belongs to the class across universes.

Show Lean proof

Abbreviation ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange

abbrev openSubgroupIndexActionRange
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) : Type u :=
  ULift.{u} (openSubgroupIndexActionImage (G := G) H hn)

Universe-lifted permutation image of the finite coset action attached to an open subgroup.

Instance ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_topologicalSpace

instance openSubgroupIndexActionRange_topologicalSpace
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    TopologicalSpace (openSubgroupIndexActionRange (G := G) H hn) :=
  inferInstance

The finite permutation image is equipped with the discrete topology inherited from the finite permutation target.

Instance ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_discreteTopology

instance openSubgroupIndexActionRange_discreteTopology
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    DiscreteTopology (openSubgroupIndexActionRange (G := G) H hn) :=
  inferInstance

The finite permutation image carries the discrete topology.

Instance ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_isTopologicalGroup

instance openSubgroupIndexActionRange_isTopologicalGroup
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    IsTopologicalGroup (openSubgroupIndexActionRange (G := G) H hn) :=
  inferInstance

The finite permutation image is a topological group with its discrete topology.

Instance ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_finite

instance openSubgroupIndexActionRange_finite
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    Finite (openSubgroupIndexActionRange (G := G) H hn) :=
  inferInstance

The permutation image of the open-subgroup coset action is finite.

Definition ReidemeisterSchreier.Profinite.openSubgroupIndexActionRangeContinuousHom

noncomputable def openSubgroupIndexActionRangeContinuousHom
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    G →ₜ* openSubgroupIndexActionRange (G := G) H hn := by
  let φ : G →ₜ* Equiv.Perm (Fin n) :=
    ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom (G := G) (H : Subgroup G)
      H.isOpen' (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
  refine
    { toMonoidHom :=
        { toFun := fun g => ⟨⟨φ g, ⟨g, rfl⟩⟩⟩
          map_one' := by
            apply ULift.ext
            apply Subtype.ext
            simp only [map_one, ContinuousMonoidHom.coe_toMonoidHom, ULift.one_down,
                OneMemClass.coe_one, φ]
          map_mul' := by
            intro g h
            apply ULift.ext
            apply Subtype.ext
            change φ (g * h) = φ g * φ h
            exact map_mul φ g h }
      continuous_toFun := ?_ }
  exact continuous_uliftUp.comp <|
    Continuous.subtype_mk φ.continuous_toFun _

The finite coset-action homomorphism lifted to its universe-lifted permutation image.

Instance ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_mulAction

instance openSubgroupIndexActionRange_mulAction
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    MulAction (openSubgroupIndexActionRange (G := G) H hn) (Fin n) where
  smul g i := g.down.1 i
  one_smul i := by
    rfl
  mul_smul g h i := by
    rfl

The lifted permutation image acts on the finite coset index set through its underlying permutation.

Theorem ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_smul_apply

@[simp] theorem openSubgroupIndexActionRange_smul_apply
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n)
    (g : openSubgroupIndexActionRange (G := G) H hn) (i : Fin n) :
    g • i = g.down.1 i

The lifted permutation image acts on a finite coset by applying the represented permutation.

Show Lean proof

Definition ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_leftQuotient_smul

noncomputable def openSubgroupIndexActionRange_leftQuotient_smul
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    openSubgroupIndexActionRange (G := G) H hn →
      (G ⧸ (H : Subgroup G)) → (G ⧸ (H : Subgroup G)) :=
  fun g q =>
    let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv
      (G := G) (H : Subgroup G)
      (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
    e.symm (g.down.1 (e q))

The inverse transported permutation action of the coset-permutation image on the quotient.

Theorem ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_leftQuotientMulAction_apply

@[simp 900] theorem openSubgroupIndexActionRange_leftQuotientMulAction_apply
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n)
    (g : openSubgroupIndexActionRange (G := G) H hn) (q : G ⧸ (H : Subgroup G)) :
    let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv
      (G := G) (H : Subgroup G)
      (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
    e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn g q) = g.down.1 (e q)

The finite permutation action evaluates on a coset by applying the represented group element.

Show Lean proof

Instance ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_leftQuotientMulAction

noncomputable instance openSubgroupIndexActionRange_leftQuotientMulAction
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    MulAction (openSubgroupIndexActionRange (G := G) H hn) (G ⧸ (H : Subgroup G)) where
  smul := openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn
  one_smul q := by
    let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv
      (G := G) (H : Subgroup G)
      (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
    apply e.injective
    change e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn 1 q) = e q
    simp only [openSubgroupIndexActionRange_leftQuotient_smul, ContinuousMonoidHom.coe_toMonoidHom,
  ULift.one_down, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq, Equiv.symm_apply_apply]
  mul_smul g h q := by
    let e := ProCGroups.FiniteGeneration.openSubgroupIndexEquiv
      (G := G) (H : Subgroup G)
      (Subgroup.quotient_finite_of_isOpen (H : Subgroup G) H.isOpen') hn
    apply e.injective
    change
      e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn (g * h) q) =
        e (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn g
          (openSubgroupIndexActionRange_leftQuotient_smul (G := G) H hn h q))
    rw [openSubgroupIndexActionRange_leftQuotientMulAction_apply (G := G) H hn (g * h) q]
    rw [openSubgroupIndexActionRange_leftQuotientMulAction_apply (G := G) H hn g]
    rw [openSubgroupIndexActionRange_leftQuotientMulAction_apply (G := G) H hn h q]
    rfl

The permutation image acts on the quotient by the inverse transported permutation, so that \(\rho(g)\) sends the basepoint coset to the coset of \(g\).

Instance ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_leftQuotientContinuousSMul

instance openSubgroupIndexActionRange_leftQuotientContinuousSMul
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    ContinuousSMul (openSubgroupIndexActionRange (G := G) H hn) (G ⧸ (H : Subgroup G)) := by
  letI : DiscreteTopology (G ⧸ (H : Subgroup G)) := inferInstance
  exact ⟨continuous_of_discreteTopology⟩

The induced action of the finite permutation image on the quotient by the open subgroup is continuous.

Theorem ReidemeisterSchreier.Profinite.openSubgroupIndexActionRangeContinuousHom_smul_basepoint

@[simp 900] theorem openSubgroupIndexActionRangeContinuousHom_smul_basepoint
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) (g : G) :
    openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •
        (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
      QuotientGroup.mk (s := (H : Subgroup G)) g

The lifted finite permutation action sends the basepoint coset to the expected coset.

Show Lean proof

Theorem ReidemeisterSchreier.Profinite.openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem

@[simp] theorem openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : OpenSubgroup G) {n : ℕ} (hn : Nat.card (G ⧸ (H : Subgroup G)) = n)
    {g : G} (hg : g ∈ (H : Subgroup G)) :
    openSubgroupIndexActionRangeContinuousHom (G := G) H hn g •
        (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
      QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)

Under the subgroup-membership condition, the lifted finite permutation action fixes the basepoint coset as prescribed.

Show Lean proof

Theorem ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_mem_class

theorem openSubgroupIndexActionRange_mem_class
    {C : ProCGroups.FiniteGroupClass.{u}}
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G)
    (H : OpenSubgroup G) {n : ℕ}
    (hn : Nat.card (G ⧸ (H : Subgroup G)) = n) :
    C (openSubgroupIndexActionRange (G := G) H hn)

The universe-lifted finite permutation image of an open-subgroup action belongs to the ambient finite-group class.

Show Lean proof

ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets

Declarations