NYLL
Module

NormalRange.lean

Nyll.EtaleFundamentalGroups.ContinuousActions.NormalRange
3 declarations indexed from sourceView source ↗

Module documentation

Normal ranges detected by finite continuous actions

The range of a continuous homomorphism of profinite groups is normal exactly when, on every transitive finite continuous action of the target, one point fixed by the range forces every point to be fixed by the range.

This is the group-action statement underlying Stacks Project, Tag 0BTS.

Imports7
Imported by2

Declarations

theorem

fixed_point_implies_trivial_of_range_normal

L44 ↗
CategoryTheory.ContAction.fixed_point_implies_trivial_of_range_normal
Source context 8 commands

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

noncomputable section
universe g'' g' w
open CategoryTheory
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G'' : Type g''} [Group G''] [TopologicalSpace G'']
  [CompactSpace G'']
variable {G' : Type g'} [Group G'] [TopologicalSpace G']
  [IsTopologicalGroup G'] [CompactSpace G'] [T2Space G']
  [TotallyDisconnectedSpace G']
omit [CompactSpace G''] [IsTopologicalGroup G'] [CompactSpace G'] [T2Space G']
  [TotallyDisconnectedSpace G'] in
Lean source · statement
theorem fixed_point_implies_trivial_of_range_normal
    (h : G'' →ₜ* G') (hnormal : h.toMonoidHom.range.Normal)
    (X : ContAction FintypeCat.{w} G')
    (htrans : MulAction.IsPretransitive G' X.obj.V)
    (hfixed : ∃ x : X.obj.V, ∀ a : G'', h a • x = x) :
    ∀ (a : G'') (x : X.obj.V), h a • x = x
theorem

range_normal_of_fixed_point_implies_trivial

L63 ↗
CategoryTheory.ContAction.range_normal_of_fixed_point_implies_trivial
Source context 7 commands

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

noncomputable section
universe g'' g' w
open CategoryTheory
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G'' : Type g''} [Group G''] [TopologicalSpace G'']
  [CompactSpace G'']
variable {G' : Type g'} [Group G'] [TopologicalSpace G']
  [IsTopologicalGroup G'] [CompactSpace G'] [T2Space G']
  [TotallyDisconnectedSpace G']
Lean source · statement
theorem range_normal_of_fixed_point_implies_trivial
    (h : G'' →ₜ* G')
    (hfixed :
      ∀ X : ContAction FintypeCat.{w} G',
        MulAction.IsPretransitive G' X.obj.V →
        (∃ x : X.obj.V, ∀ a : G'', h a • x = x) →
        ∀ (a : G'') (x : X.obj.V), h a • x = x) :
    h.toMonoidHom.range.Normal
theorem

range_normal_iff_fixed_point_implies_trivial

L164 ↗
CategoryTheory.ContAction.range_normal_iff_fixed_point_implies_trivial
Documentation

The range of a continuous homomorphism of profinite groups is normal exactly when one range-fixed point in every transitive finite continuous target action forces the range to fix the whole action.

Source context 7 commands

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

noncomputable section
universe g'' g' w
open CategoryTheory
open scoped FintypeCatDiscrete
namespace CategoryTheory.ContAction
variable {G'' : Type g''} [Group G''] [TopologicalSpace G'']
  [CompactSpace G'']
variable {G' : Type g'} [Group G'] [TopologicalSpace G']
  [IsTopologicalGroup G'] [CompactSpace G'] [T2Space G']
  [TotallyDisconnectedSpace G']
Lean source · statement
theorem range_normal_iff_fixed_point_implies_trivial
    (h : G'' →ₜ* G') :
    h.toMonoidHom.range.Normal ↔
      ∀ X : ContAction FintypeCat.{w} G',
        MulAction.IsPretransitive G' X.obj.V →
        (∃ x : X.obj.V, ∀ a : G'', h a • x = x) →
        ∀ (a : G'') (x : X.obj.V), h a • x = x

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