Profinite completion and finite group actions

The action of an abstract group G on a finite set extends uniquely and continuously to the profinite completion of G. These extensions are natural in the finite G-set, and together exhibit the profinite completion as the fundamental group of the forgetful fibre functor from finite G-sets.

Main declarations

• TauCeti.ProfiniteCompletion.actionHom: the continuous permutation representation extending a finite G-action.
• TauCeti.ProfiniteCompletion.etaFn_smul: the extended action restricts to the original action along the canonical map from G.
• TauCeti.ProfiniteCompletion.instIsFundamentalGroup: the profinite completion is a fundamental group of the forgetful functor on finite G-sets. Consequently CategoryTheory.PreGaloisCategory.toAutMulEquiv identifies the profinite completion with the automorphism group of that functor.

The construction uses Mathlib's profinite completion and its universal property.

noncomputable def TauCeti.ProfiniteCompletion.actionHom (G : Type u) [Group G] (A : Action FintypeCat G) : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop →* Equiv.Perm A.V.obj

The permutation representation of the profinite completion extending a finite G-action.

Equations

• TauCeti.ProfiniteCompletion.actionHom G A = id (have f := (ProfiniteGrp.Hom.hom (TauCeti.ProfiniteCompletion.continuousActionHom✝ G A)).toMonoidHom; f)

@[instance_reducible]

noncomputable instance TauCeti.ProfiniteCompletion.instMulAction (G : Type u) [Group G] (A : Action FintypeCat G) : MulAction (↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop) A.V.obj

The profinite completion acts on every finite G-set.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.ProfiniteCompletion.instMulActionForgetObj (G : Type u) [Group G] (A : Action FintypeCat G) : MulAction (↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop) ((Action.forget FintypeCat G).obj A).obj

Specialize instMulAction to assist typeclass inference: Action.forget is not reducible, so instance synthesis does not see (Action.forget FintypeCat G).obj A as A.V.

Equations

• TauCeti.ProfiniteCompletion.instMulActionForgetObj G A = TauCeti.ProfiniteCompletion.instMulAction G A

@[simp]

theorem TauCeti.ProfiniteCompletion.actionHom_etaFn (G : Type u) [Group G] (A : Action FintypeCat G) (g : G) : (actionHom G A) (ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) g) = (MulAction.toPermHom G A.V.obj) g

The extended permutation representation restricts along G → Ĝ to the original one.

@[simp]

theorem TauCeti.ProfiniteCompletion.etaFn_smul (G : Type u) [Group G] (A : Action FintypeCat G) (g : G) (x : A.V.obj) : ProfiniteGrp.ProfiniteCompletion.etaFn (↧G) g • x = g • x

The extended action restricts along the canonical map G → Ĝ to the original action.

theorem TauCeti.ProfiniteCompletion.continuous_actionHom (G : Type u) [Group G] (A : Action FintypeCat G) : Continuous ⇑(actionHom G A)

The extended permutation representation is continuous, the finite permutation group carrying the discrete topology.

theorem TauCeti.ProfiniteCompletion.continuousSMul (G : Type u) [Group G] (A : Action FintypeCat G) : ContinuousSMul (↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop) A.V.obj

The extended action on a finite G-set is continuous when the set has the discrete topology.

instance TauCeti.ProfiniteCompletion.instIsNaturalSMul (G : Type u) [Group G] : CategoryTheory.PreGaloisCategory.IsNaturalSMul (Action.forget FintypeCat G) ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop

The profinite-completion actions on finite G-sets are natural in equivariant maps.

theorem TauCeti.ProfiniteCompletion.isPretransitive_of_isConnected (G : Type u) [Group G] (A : Action FintypeCat G) [CategoryTheory.PreGaloisCategory.IsConnected A] : MulAction.IsPretransitive (↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop) A.V.obj

On a connected finite G-set, the profinite-completion action is transitive.

theorem TauCeti.ProfiniteCompletion.actionHom_one_quotient (G : Type u) [Group G] (H : FiniteIndexNormalSubgroup G) (g : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop) : let A := Action.FintypeCat.ofMulAction G ↧(G ⧸ H.toSubgroup); ((actionHom G A) g) 1 = (coordinateHom G H) g

On the finite quotient by H, acting on the identity coset reads the H-coordinate of an element of the profinite completion.

theorem TauCeti.ProfiniteCompletion.eq_one_of_forall_smul_eq (G : Type u) [Group G] (g : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop) (h : ∀ (A : Action FintypeCat G) (x : ((Action.forget FintypeCat G).obj A).obj), g • x = x) : g = 1

An element of the profinite completion acting trivially on every finite G-set is the identity. The regular actions on the finite quotients detect all coordinates of the limit.

instance TauCeti.ProfiniteCompletion.instIsFundamentalGroup (G : Type u) [Group G] : CategoryTheory.PreGaloisCategory.IsFundamentalGroup (Action.forget FintypeCat G) ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧G).toProfinite.toTop

The profinite completion of G is a fundamental group of the forgetful fibre functor on finite G-sets.