Module

RestrictionEssentialImage.lean

Nyll.EtaleFundamentalGroups.ContinuousActions.RestrictionEssentialImage

1 declaration indexed from sourceView source ↗

Module documentation

Essential image of restriction of finite continuous actions

For a surjective continuous group homomorphism, a finite continuous action is obtained by restriction exactly when the kernel acts trivially.

Imports5

Nyll.EtaleFundamentalGroups.ContinuousActions.RestrictionFullyFaithful
Mathlib.CategoryTheory.EssentialImage
Mathlib.Algebra.Group.Subgroup.Basic
Mathlib.Topology.Category.FinTopCat
Mathlib.Topology.Separation.Hausdorff

Imported by4

theorem

essImage_res_iff_ker_le_ker_ρAut

L41 ↗

CategoryTheory.ContAction.essImage_res_iff_ker_le_ker_ρAut

Documentation

A finite continuous G'-action descends along a surjective continuous homomorphism h : G' → G exactly when ker h acts trivially.

Source context 9 commands

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

@[expose] public section
universe g' g w
noncomputable section
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]
variable [IsTopologicalGroup G] [T2Space G]

Lean source · statement

theorem essImage_res_iff_ker_le_ker_ρAut
    (h : G' →ₜ* G) (hs : Function.Surjective h)
    (Y : ContAction FintypeCat.{w} G') :
    (ContAction.res FintypeCat h).essImage Y ↔
      h.toMonoidHom.ker ≤ (Action.ρAut Y.obj).ker

Module documentation

Essential image of restriction of finite continuous actions

Declarations

essImage_res_iff_ker_le_ker_ρAut