Module

ClosedNormalClosure.lean

Nyll.EtaleFundamentalGroups.ContinuousActions.ClosedNormalClosure

2 declarations indexed from sourceView source ↗

Module documentation

Detecting closed normal closures by finite continuous actions

An element belongs to the closed normal subgroup generated by a set exactly when every finite continuous action on which the generators act trivially also makes that element act trivially.

Imports7

Nyll.ProCGroups.Presentations.Profinite
Mathlib.CategoryTheory.Action.Continuous
Mathlib.CategoryTheory.Action.Concrete
Mathlib.GroupTheory.GroupAction.Quotient
Mathlib.Topology.Algebra.ClopenNhdofOne
Mathlib.Topology.Algebra.OpenSubgroup
Mathlib.Topology.Category.FinTopCat

Imported by2

lemma

isClosed_ker_toPermHom

L33 ↗

ProCGroups.Presentations.isClosed_ker_toPermHom

Source context 5 commands

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

noncomputable section
universe u w
open CategoryTheory
open scoped FintypeCatDiscrete
namespace ProCGroups.Presentations

Lean source · statement

lemma isClosed_ker_toPermHom
    {G : Type u} {A : Type w}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [TopologicalSpace A] [DiscreteTopology A]
    [MulAction G A] [ContinuousSMul G A] :
    IsClosed ((MulAction.toPermHom G A).ker : Set G)

theorem

mem_closedNormalClosure_iff_fixedBy_finite_continuous_actions

L62 ↗

ProCGroups.Presentations.Subgroup.mem_closedNormalClosure_iff_fixedBy_finite_continuous_actions

Documentation

Membership in the closed normal closure of R is detected by finite continuous G-actions: if every element of R fixes every point, then so does g.

Source context 8 commands