Module

FiniteOrbits.lean

Nyll.EtaleFundamentalGroups.ContinuousActions.FiniteOrbits

1 declaration indexed from sourceView source ↗

Module documentation

Finite orbits of a discrete continuous action

This file supplies the finite-orbit construction used internally for Stacks Project, Tag 03QR. Every orbit of a discrete continuous action of a compact topological group is finite.

Imports4

Nyll.EtaleFundamentalGroups.ContinuousActions.TopCatCompat
Mathlib.CategoryTheory.Action.Concrete
Mathlib.Topology.Algebra.OpenSubgroup
Mathlib.Topology.Category.FinTopCat

Imported by2

def

orbitContAction

L37 ↗

CategoryTheory.DiscreteContAction.orbitContAction

Documentation

A single orbit of a discrete continuous action, regarded as a finite continuous G-action.

Source context 7 commands

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

@[expose] public section
universe u v
noncomputable section
open CategoryTheory
open scoped FintypeCatDiscrete
namespace CategoryTheory.DiscreteContAction
variable {G : Type v} [Group G] [TopologicalSpace G]

Lean source · statement

def orbitContAction
    [IsTopologicalGroup G] [CompactSpace G]
    (S : DiscreteContAction TopCat.{u} G)
    (ω : MulAction.orbitRel.Quotient G
      ((forget₂ (DiscreteContAction TopCat.{u} G) TopCat).obj S)) :
    ContAction FintypeCat.{u} G

Module documentation

Finite orbits of a discrete continuous action

Declarations

orbitContAction