Light profinite spaces

We construct the category LightProfinite of light profinite topological spaces. These are implemented as totally disconnected second countable compact Hausdorff spaces.

This file also defines the category LightDiagram, which consists of those spaces that can be written as a sequential limit (in Profinite) of finite sets.

We define an equivalence of categories LightProfinite ≌ LightDiagram and prove that these are essentially small categories.

Implementation

The category LightProfinite is defined using the structure CompHausLike. See the file CompHausLike.Basic for more information.

@[reducible, inline]

abbrev LightProfinite : Type (u_1 + 1)

LightProfinite is the category of second countable profinite spaces.

instance LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology (X : Type u_1) [TopologicalSpace X] [TotallyDisconnectedSpace X] [SecondCountableTopology X] : CompHausLike.HasProp (fun (Y : TopCat) => TotallyDisconnectedSpace ↑Y ∧ SecondCountableTopology ↑Y) X

@[reducible, inline]

abbrev LightProfinite.of (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [SecondCountableTopology X] : LightProfinite

Construct a term of LightProfinite from a type endowed with the structure of a compact, Hausdorff, totally disconnected and second countable topological space.

@[implicit_reducible]

instance LightProfinite.instInhabited : Inhabited LightProfinite

instance LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology {X : LightProfinite} : TotallyDisconnectedSpace ↑X.toTop

instance LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace {X : LightProfinite} : SecondCountableTopology ↑X.toTop

@[reducible, inline]

abbrev lightToProfinite : CategoryTheory.Functor LightProfinite Profinite

The fully faithful embedding of LightProfinite in Profinite.

@[reducible, inline]

abbrev lightToProfiniteFullyFaithful : lightToProfinite.FullyFaithful

lightToProfinite is fully faithful.

@[reducible, inline]

abbrev lightProfiniteToCompHaus : CategoryTheory.Functor LightProfinite CompHaus

The fully faithful embedding of LightProfinite in CompHaus.

@[reducible, inline]

abbrev LightProfinite.toTopCat : CategoryTheory.Functor LightProfinite TopCat

The fully faithful embedding of LightProfinite in TopCat. This is definitionally the same as the obvious composite.

def FintypeCat.toLightProfinite : CategoryTheory.Functor FintypeCat LightProfinite

The natural functor from Fintype to LightProfinite, endowing a finite type with the discrete topology.

theorem FintypeCat.toLightProfinite_map_hom_hom_apply {X✝ Y✝ : FintypeCat} (f : X✝ ⟶ Y✝) (a : X✝.obj) : (TopCat.Hom.hom (toLightProfinite.map f).hom) a = (CategoryTheory.ConcreteCategory.hom f) a

def FintypeCat.toLightProfiniteFullyFaithful : toLightProfinite.FullyFaithful

FintypeCat.toLightProfinite is fully faithful.

instance instFaithfulFintypeCatLightProfiniteToLightProfinite : FintypeCat.toLightProfinite.Faithful

instance instFullFintypeCatLightProfiniteToLightProfinite : FintypeCat.toLightProfinite.Full

instance instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite (X : FintypeCat) : Finite ↑(FintypeCat.toLightProfinite.obj X).toTop

instance instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj (X : FintypeCat) : Finite ↑(LightProfinite.of X.obj).toTop

instance LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J LightProfinite) : TotallyDisconnectedSpace ↑(CompHaus.limitCone (F.comp lightProfiniteToCompHaus)).pt.toTop

def LightProfinite.limitCone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J] (F : CategoryTheory.Functor J LightProfinite) : CategoryTheory.Limits.Cone F

An explicit limit cone for a functor F : J ⥤ LightProfinite, for a countable category J defined in terms of CompHaus.limitCone, which is defined in terms of TopCat.limitCone.

def LightProfinite.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J] (F : CategoryTheory.Functor J LightProfinite) : CategoryTheory.Limits.IsLimit (limitCone F)

The limit cone LightProfinite.limitCone F is indeed a limit cone.

@[implicit_reducible]

noncomputable instance LightProfinite.createsCountableLimits {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J] : CategoryTheory.CreatesLimitsOfShape J lightToProfinite

instance LightProfinite.instHasCountableLimits : CategoryTheory.Limits.HasCountableLimits LightProfinite

instance LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology : CategoryTheory.Limits.PreservesLimitsOfShape ℕᵒᵖ (CategoryTheory.forget LightProfinite)

theorem LightProfinite.isClosedMap {X Y : LightProfinite} (f : X ⟶ Y) : IsClosedMap ⇑(CategoryTheory.ConcreteCategory.hom f)

Any morphism of light profinite spaces is a closed map.

theorem LightProfinite.isIso_of_bijective {X Y : LightProfinite} (f : X ⟶ Y) (bij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.IsIso f

Any continuous bijection of light profinite spaces induces an isomorphism.

noncomputable def LightProfinite.isoOfBijective {X Y : LightProfinite} (f : X ⟶ Y) (bij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) : X ≅ Y

Any continuous bijection of light profinite spaces induces an isomorphism.

instance LightProfinite.forget_reflectsIsomorphisms : (CategoryTheory.forget LightProfinite).ReflectsIsomorphisms

theorem LightProfinite.epi_iff_surjective {X Y : LightProfinite} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

instance LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite : lightToProfinite.PreservesEpimorphisms

structure LightDiagram : Type (u + 1)

A structure containing the data of sequential limit in Profinite of finite sets.

• diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat

  The indexing diagram.

• cone : CategoryTheory.Limits.Cone (self.diagram.comp FintypeCat.toProfinite)

  The limit cone.

• isLimit : CategoryTheory.Limits.IsLimit self.cone

  The limit cone is limiting.

def LightDiagram.toProfinite (S : LightDiagram) : Profinite

The underlying Profinite of a LightDiagram.

@[implicit_reducible]

instance LightDiagram.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} LightDiagram

@[simp]

theorem LightDiagram.comp_hom_hom_hom_apply {X Y Z : LightDiagram} (a✝ : X ⟶ Y) (a✝¹ : Y ⟶ Z) (a✝² : ↑X.toProfinite.toTop) : (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp a✝ a✝¹).hom.hom) a✝² = a✝¹.hom.hom.hom' (a✝.hom.hom.hom' a✝²)

@[simp]

theorem LightDiagram.id_hom_hom_hom_apply (X : LightDiagram) (a : ↑X.toProfinite.toTop) : (TopCat.Hom.hom (CategoryTheory.CategoryStruct.id X).hom.hom) a = a

@[implicit_reducible]

instance LightDiagram.hasForget : CategoryTheory.ConcreteCategory LightDiagram fun (X Y : LightDiagram) => C(↑X.toProfinite.toTop, ↑Y.toProfinite.toTop)

def lightDiagramToProfinite : CategoryTheory.Functor LightDiagram Profinite

The fully faithful embedding LightDiagram ⥤ Profinite

@[simp]

theorem lightDiagramToProfinite_obj (S : LightDiagram) : lightDiagramToProfinite.obj S = S.toProfinite

@[simp]

theorem lightDiagramToProfinite_map {X✝ Y✝ : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite} (f : X✝ ⟶ Y✝) : lightDiagramToProfinite.map f = f.hom

instance instFaithfulLightDiagramProfiniteLightDiagramToProfinite : lightDiagramToProfinite.Faithful

instance instFullLightDiagramProfiniteLightDiagramToProfinite : lightDiagramToProfinite.Full

instance LightProfinite.instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology (S : LightProfinite) : Countable (TopologicalSpace.Clopens ↑S.toTop)

instance LightProfinite.instCountableDiscreteQuotient (S : LightProfinite) : Countable (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)

noncomputable def LightProfinite.toLightDiagram (S : LightProfinite) : LightDiagram

A profinite space which is light gives rise to a light profinite space.

noncomputable def lightProfiniteToLightDiagram : CategoryTheory.Functor LightProfinite LightDiagram

The functor part of the equivalence LightProfinite ≌ LightDiagram

@[simp]

theorem lightProfiniteToLightDiagram_map {X✝ Y✝ : LightProfinite} (f : X✝ ⟶ Y✝) : lightProfiniteToLightDiagram.map f = CategoryTheory.InducedCategory.homMk (CategoryTheory.InducedCategory.homMk f.hom)

@[simp]

theorem lightProfiniteToLightDiagram_obj (X : LightProfinite) : lightProfiniteToLightDiagram.obj X = X.toLightDiagram

instance instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone (S : LightDiagram) : SecondCountableTopology ↑S.cone.pt.toTop

def lightDiagramToLightProfinite : CategoryTheory.Functor LightDiagram LightProfinite

The inverse part of the equivalence LightProfinite ≌ LightDiagram

@[simp]

theorem lightDiagramToLightProfinite_obj (X : LightDiagram) : lightDiagramToLightProfinite.obj X = LightProfinite.of ↑X.cone.pt.toTop

@[simp]

theorem lightDiagramToLightProfinite_map {X✝ Y✝ : LightDiagram} (f : X✝ ⟶ Y✝) : lightDiagramToLightProfinite.map f = CategoryTheory.InducedCategory.homMk f.hom.hom

noncomputable def LightProfinite.equivDiagram : LightProfinite ≌ LightDiagram

The equivalence of categories LightProfinite ≌ LightDiagram

instance instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram : lightProfiniteToLightDiagram.IsEquivalence

instance instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite : lightDiagramToLightProfinite.IsEquivalence

structure LightDiagram' : Type u

This is an auxiliary definition used to show that LightDiagram is essentially small.

Note that below we put a category instance on this structure which is completely different from the category instance on ℕᵒᵖ ⥤ FintypeCat.Skeleton.{u}. Neither the morphisms nor the objects are the same.

• diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat.Skeleton

  The diagram takes values in a small category equivalent to FintypeCat.

noncomputable def LightDiagram'.toProfinite (S : LightDiagram') : Profinite

A LightDiagram' yields a Profinite.

@[implicit_reducible]

noncomputable instance instCategoryLightDiagram' : CategoryTheory.Category.{u_1, u_1} LightDiagram'

noncomputable def LightDiagram'.toLightFunctor : CategoryTheory.Functor LightDiagram' LightDiagram

The functor part of the equivalence of categories LightDiagram' ≌ LightDiagram.

instance instFaithfulLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.Faithful

instance instFullLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.Full

instance instEssSurjLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.EssSurj

instance instIsEquivalenceLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.IsEquivalence

noncomputable def LightDiagram.equivSmall : LightDiagram ≌ LightDiagram'

The equivalence between LightDiagram and a small category.

instance instEssentiallySmallLightDiagram : CategoryTheory.EssentiallySmall.{u, u, u + 1} LightDiagram

instance instEssentiallySmallLightProfinite : CategoryTheory.EssentiallySmall.{u, u, u + 1} LightProfinite