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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : CategoryTheory.Aut F →* (X : C) → CategoryTheory.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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (σ : CategoryTheory.Aut F) (X : C) : (CategoryTheory.PreGaloisCategory.autEmbedding F) σ X = CategoryTheory.Iso.app σ X

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

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

def CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFintypeCatObj {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : TopologicalSpace (CategoryTheory.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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : DiscreteTopology (CategoryTheory.Aut (F.obj X))

instance CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFunctorFintypeCat {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : TopologicalSpace (CategoryTheory.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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : Set.range ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F) = ⋂ (f : CategoryTheory.Arrow C), {a : (X : C) → CategoryTheory.Aut (F.obj X) | CategoryTheory.CategoryStruct.comp (F.map f.hom) (a f.right).hom = CategoryTheory.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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : IsClosed (Set.range ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F))

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

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

@[deprecated CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding]

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

Alias of CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance CategoryTheory.PreGaloisCategory.instSMulAutFintypeCatObjαFintype {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : SMul (CategoryTheory.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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : ContinuousSMul (CategoryTheory.Aut (F.obj X)) ↑(F.obj X)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {H : Set (CategoryTheory.Aut F)} (h1 : 1 ∈ H) (h : IsOpen H) : ∃ (I : Set C) (x : Fintype ↑I), (∀ X ∈ I, CategoryTheory.PreGaloisCategory.IsConnected X) ∧ ∀ (σ : CategoryTheory.Aut F), (∀ (X : ↑I), σ.hom.app ↑X = CategoryTheory.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₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (nhds 1).HasBasis (fun (x : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) => True) fun (X : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) => ↑(MulAction.stabilizer (CategoryTheory.Aut F) X.pt)

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