Topology of fundamental group

In this file we define a natural topology on the automorphism group of a functor F : C ⥤ FintypeCat: It is defined as the subspace topology induced by the natural embedding of Aut F into ∀ X, Aut (F.obj X) where Aut (F.obj X) carries the discrete topology.

References

• Stacks 0BMQ

def CategoryTheory.PreGaloisCategory.autEmbedding {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : Aut F →* (X : C) → Aut (F.obj X)

For a functor F : C ⥤ FintypeCat, the canonical embedding of Aut F into the product over Aut (F.obj X) for all objects X.

Equations

• CategoryTheory.PreGaloisCategory.autEmbedding F = MonoidHom.mk' (fun (σ : CategoryTheory.Aut F) (X : C) => CategoryTheory.Iso.app σ X) ⋯

@[simp]

theorem CategoryTheory.PreGaloisCategory.autEmbedding_apply {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (σ : Aut F) (X : C) : (autEmbedding F) σ X = Iso.app σ X

theorem CategoryTheory.PreGaloisCategory.autEmbedding_injective {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : Function.Injective ⇑(autEmbedding F)

def CategoryTheory.PreGaloisCategory.instTopologicalSpaceCarrierObjFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : TopologicalSpace (F.obj X).carrier

We put the discrete topology on F.obj X.

Equations

• CategoryTheory.PreGaloisCategory.instTopologicalSpaceCarrierObjFintypeCat F X = ⊥

theorem CategoryTheory.PreGaloisCategory.obj_discreteTopology {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : DiscreteTopology (F.obj X).carrier

def CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFintypeCatObj {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : TopologicalSpace (Aut (F.obj X))

We put the discrete topology on Aut (F.obj X).

Equations

• CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFintypeCatObj F X = ⊥

theorem CategoryTheory.PreGaloisCategory.aut_discreteTopology {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : DiscreteTopology (Aut (F.obj X))

instance CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFunctorFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : TopologicalSpace (Aut F)

Aut F is equipped with the by the embedding into ∀ X, Aut (F.obj X) induced embedding.

Equations

• CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFunctorFintypeCat F = TopologicalSpace.induced (⇑(CategoryTheory.PreGaloisCategory.autEmbedding F)) inferInstance

theorem CategoryTheory.PreGaloisCategory.autEmbedding_range {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : Set.range ⇑(autEmbedding F) = ⋂ (f : Arrow C), {a : (X : C) → Aut (F.obj X) | CategoryStruct.comp (F.map f.hom) (a f.right).hom = CategoryStruct.comp (a f.left).hom (F.map f.hom)}

The image of Aut F in ∀ X, Aut (F.obj X) are precisely the compatible families of automorphisms.

theorem CategoryTheory.PreGaloisCategory.autEmbedding_range_isClosed {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : IsClosed (Set.range ⇑(autEmbedding F))

The image of Aut F in ∀ X, Aut (F.obj X) is closed.

theorem CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : Topology.IsClosedEmbedding ⇑(autEmbedding F)

instance CategoryTheory.PreGaloisCategory.instCompactSpaceAutFunctorFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : CompactSpace (Aut F)

instance CategoryTheory.PreGaloisCategory.instT2SpaceAutFunctorFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : T2Space (Aut F)

instance CategoryTheory.PreGaloisCategory.instTotallyDisconnectedSpaceAutFunctorFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : TotallyDisconnectedSpace (Aut F)

instance CategoryTheory.PreGaloisCategory.instContinuousMulAutFunctorFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : ContinuousMul (Aut F)

instance CategoryTheory.PreGaloisCategory.instContinuousInvAutFunctorFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : ContinuousInv (Aut F)

instance CategoryTheory.PreGaloisCategory.instIsTopologicalGroupAutFunctorFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : IsTopologicalGroup (Aut F)

instance CategoryTheory.PreGaloisCategory.instSMulAutFintypeCatObjCarrier {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : SMul (Aut (F.obj X)) (F.obj X).carrier

Equations

• CategoryTheory.PreGaloisCategory.instSMulAutFintypeCatObjCarrier F X = { smul := fun (σ : CategoryTheory.Aut (F.obj X)) (a : (F.obj X).carrier) => σ.hom a }

instance CategoryTheory.PreGaloisCategory.instContinuousSMulAutFintypeCatObjCarrier {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : ContinuousSMul (Aut (F.obj X)) (F.obj X).carrier

instance CategoryTheory.PreGaloisCategory.continuousSMul_aut_fiber {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : ContinuousSMul (Aut F) (F.obj X).carrier

theorem CategoryTheory.PreGaloisCategory.continuous_mapAut_whiskeringRight {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (G : Functor FintypeCat FintypeCat) : Continuous ⇑(Functor.mapAut F ((whiskeringRight C FintypeCat FintypeCat).obj G))

If G is a functor of categories of finite types, the induced map Aut F → Aut (F ⋙ G) is continuous.

noncomputable def CategoryTheory.PreGaloisCategory.autEquivAutWhiskerRight {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) {G : Functor FintypeCat FintypeCat} (h : G.FullyFaithful) : Aut F ≃ₜ* Aut (F.comp G)

If G is a fully faithful functor of categories finite types, this is the automorphism of topological groups Aut F ≃ Aut (F ⋙ G).

Equations

• CategoryTheory.PreGaloisCategory.autEquivAutWhiskerRight F h = { toMulEquiv := (h.whiskeringRight C).autMulEquivOfFullyFaithful F, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] {H : Set (Aut F)} (h1 : 1 ∈ H) (h : IsOpen H) : ∃ (I : Set C) (x : Fintype ↑I), (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = CategoryStruct.id (F.obj ↑X)) → σ ∈ H

If H is an open subset of Aut F such that 1 ∈ H, there exists a finite set I of connected objects of C such that every σ : Aut F that induces the identity on F.obj X for all X ∈ I is contained in H. In other words: The kernel of the evaluation map Aut F →* ∏ X : I ↦ Aut (F.obj X) is contained in H.

theorem CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] : (nhds 1).HasBasis (fun (x : PointedGaloisObject F) => True) fun (X : PointedGaloisObject F) => ↑(MulAction.stabilizer (Aut F) X.pt)

The stabilizers of points in the fibers of Galois objects form a neighbourhood basis of the identity in Aut F.