NYLL
Module

FinitePermutationTargets.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets
17 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Profinite / Open Subgroups / Finite Permutation Targets

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.

Imports1
Imported by2

Declarations

abbrev

openSubgroupIndexActionImage

L30 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionImage
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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
theorem

openSubgroupIndexContinuousHom_range_mem_class

L38 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexContinuousHom_range_mem_class
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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)
abbrev

openSubgroupIndexActionRange

L68 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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
instance

openSubgroupIndexActionRange_topologicalSpace

L77 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_topologicalSpace
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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)
instance

openSubgroupIndexActionRange_discreteTopology

L84 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_discreteTopology
Documentation

The finite permutation image carries the discrete topology.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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)
instance

openSubgroupIndexActionRange_isTopologicalGroup

L91 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_isTopologicalGroup
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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)
instance

openSubgroupIndexActionRange_finite

L98 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_finite
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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)
def

openSubgroupIndexActionRangeContinuousHom

L105 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRangeContinuousHom
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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
instance

openSubgroupIndexActionRange_mulAction

L134 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_mulAction
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · full declaration
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
theorem

openSubgroupIndexActionRange_smul_apply

L145 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_smul_apply
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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
def

openSubgroupIndexActionRange_leftQuotient_smul

L153 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_leftQuotient_smul
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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))
theorem

openSubgroupIndexActionRange_leftQuotientMulAction_apply

L165 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_leftQuotientMulAction_apply
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · full declaration
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) := by
  simp only [openSubgroupIndexActionRange_leftQuotient_smul, ContinuousMonoidHom.coe_toMonoidHom,
  Equiv.apply_symm_apply]
instance

openSubgroupIndexActionRange_leftQuotientMulAction

L180 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_leftQuotientMulAction
Documentation

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\).

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · full declaration
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
instance

openSubgroupIndexActionRange_leftQuotientContinuousSMul

L211 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_leftQuotientContinuousSMul
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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))
theorem

openSubgroupIndexActionRangeContinuousHom_smul_basepoint

L218 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRangeContinuousHom_smul_basepoint
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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
theorem

openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem

L264 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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)
theorem

openSubgroupIndexActionRange_mem_class

L278 ↗
ReidemeisterSchreier.Profinite.openSubgroupIndexActionRange_mem_class
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ReidemeisterSchreier
namespace Profinite
universe u v
section FinitePermutationTargets
open ProCGroups.ProC
Lean source · statement
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)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.