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
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) ⋯
Instances For
We put the discrete topology on F.obj X.
Instances For
We put the discrete topology on Aut (F.obj X).
Instances For
Aut F is equipped with the by the embedding into ∀ X, Aut (F.obj X) induced embedding.
The image of Aut F in ∀ X, Aut (F.obj X) are precisely the compatible families of
automorphisms.
The image of Aut F in ∀ X, Aut (F.obj X) is closed.
Alias of CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding.
Equations
- CategoryTheory.PreGaloisCategory.instSMulAutFintypeCatObjαFintype F X = { smul := fun (σ : CategoryTheory.Aut (F.obj X)) (a : ↑(F.obj X)) => σ.hom a }
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.
The stabilizers of points in the fibers of Galois objects form a neighbourhood basis
of the identity in Aut F.