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) ⋯
Instances For
@[simp]
theorem
CategoryTheory.PreGaloisCategory.autEmbedding_apply
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
(σ : CategoryTheory.Aut F)
(X : C)
:
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
.
Instances For
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)
.
Instances For
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)
:
Aut F
is equipped with the by the embedding into ∀ X, Aut (F.obj X)
induced embedding.
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)
:
The image of Aut F
in ∀ X, Aut (F.obj X)
is closed.
instance
CategoryTheory.PreGaloisCategory.instCompactSpaceAutFunctorFintypeCat
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.PreGaloisCategory.instT2SpaceAutFunctorFintypeCat
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.PreGaloisCategory.instTotallyDisconnectedSpaceAutFunctorFintypeCat
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.PreGaloisCategory.instContinuousMulAutFunctorFintypeCat
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.PreGaloisCategory.instContinuousInvAutFunctorFintypeCat
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.PreGaloisCategory.instTopologicalGroupAutFunctorFintypeCat
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
:
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
- ⋯ = ⋯