The Galois category of finite sets with a continuous action of a topological group

Let G be a topological group. In this file, we show that the category ContAction FintypeCat G is a Galois category. In order to do this, we show that the corresponding property isContinuous FintypeCat G of objects in Action FintypeCat G consists of the union over all open subgroups H of G of the properties trivialOnSet FintypeCat H (which are satisfied by the representations that are trivial on H).

def Action.trivialOnSet (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_4} [Monoid G] (S : Set G) : CategoryTheory.ObjectProperty (Action V G)

The property of objects in Action V G for which the action of the elements of a subset S : Set G is trivial.

Equations

• Action.trivialOnSet V S X = ∀ s ∈ S, X.ρ s = 1

theorem Action.trivialOnSet_antitone {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_4) [Monoid G] : Antitone (trivialOnSet V)

instance Action.instIsClosedUnderLimitsOfShapeTrivialOnSetOfHasLimitsOfShape {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_4} [Monoid G] (J : Type u_5) [CategoryTheory.Category.{v_2, u_5} J] [CategoryTheory.Limits.HasLimitsOfShape J V] (S : Set G) : (trivialOnSet V S).IsClosedUnderLimitsOfShape J

instance Action.instIsClosedUnderColimitsOfShapeTrivialOnSetOfHasColimitsOfShape {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_4} [Monoid G] (J : Type u_5) [CategoryTheory.Category.{v_2, u_5} J] [CategoryTheory.Limits.HasColimitsOfShape J V] (S : Set G) : (trivialOnSet V S).IsClosedUnderColimitsOfShape J

instance Action.instIsClosedUnderFiniteLimitsTrivialOnSetOfHasFiniteLimits {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_4} [Monoid G] [CategoryTheory.Limits.HasFiniteLimits V] (S : Set G) : (trivialOnSet V S).IsClosedUnderFiniteLimits

instance Action.instIsClosedUnderFiniteColimitsTrivialOnSetOfHasFiniteColimits {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_4} [Monoid G] [CategoryTheory.Limits.HasFiniteColimits V] (S : Set G) : (trivialOnSet V S).IsClosedUnderFiniteColimits

instance Action.instIsClosedUnderSubobjectsTrivialOnSetOfHasPullbacks {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_4} [Monoid G] (S : Set G) [CategoryTheory.Limits.HasPullbacks V] : (trivialOnSet V S).IsClosedUnderSubobjects

instance Action.instIsGaloisSubcategoryFintypeCatTrivialOnSet {G : Type u_4} [Monoid G] (S : Set G) : (trivialOnSet FintypeCat S).IsGaloisSubcategory

theorem Action.trivialOnSet_le_isContinuous {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : OpenSubgroup G) : trivialOnSet FintypeCat ↑H ≤ isContinuous FintypeCat G

If an action of a topological group on a finite set is trivial on an open subgroup, then it is continuous.

theorem Action.isContinuous_eq_iSup {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : isContinuous FintypeCat G = ⨆ (H : OpenSubgroup G), trivialOnSet FintypeCat ↑H

An action of a topological group on a finite set is continuous if and only if it is trivial when restricted to some open subgroup.

instance Action.instIsClosedUnderSubobjectsFintypeCatIsContinuousFunObjFinite {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (isContinuous FintypeCat G).IsClosedUnderSubobjects

theorem Action.exists_openSubgroup_of_isContinuous_of_finite {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {J : Type u_5} [Finite J] (obj : J → Action FintypeCat G) (property : ∀ (j : J), isContinuous FintypeCat G (obj j)) : ∃ (H : OpenSubgroup G), ∀ (j : J), trivialOnSet FintypeCat (↑H) (obj j)

An action of a topological group on a finite set is continuous if and only if it is trivial when restricted to some open subgroup.

instance Action.instIsClosedUnderFiniteLimitsFintypeCatIsContinuousFunObjFinite {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (isContinuous FintypeCat G).IsClosedUnderFiniteLimits

instance Action.instIsClosedUnderFiniteColimitsFintypeCatIsContinuousFunObjFinite {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (isContinuous FintypeCat G).IsClosedUnderFiniteColimits

instance Action.instIsGaloisSubcategoryFintypeCatIsContinuousFunObjFinite {G : Type u_4} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (isContinuous FintypeCat G).IsGaloisSubcategory