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 Project: Tag 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.instTopologicalSpaceαFintypeObjFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) (X : C) : TopologicalSpace ↑(F.obj X)

We put the discrete topology on F.obj X.

Equations

• CategoryTheory.PreGaloisCategory.instTopologicalSpaceαFintypeObjFintypeCat F X = ⊥

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

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)

@[deprecated CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding (since := "2024-10-20")]

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

Alias of CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding.

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.instTopologicalGroupAutFunctorFintypeCat {C : Type u₁} [Category.{u₂, u₁} C] (F : Functor C FintypeCat) : TopologicalGroup (Aut F)

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

Equations

• CategoryTheory.PreGaloisCategory.instSMulAutFintypeCatObjαFintype F X = { smul := fun (σ : CategoryTheory.Aut (F.obj X)) (a : ↑(F.obj X)) => σ.hom a }

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

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)

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.