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_closedEmbedding {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : ClosedEmbedding ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F)

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

• ⋯ = ⋯