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.

Equations

• LightProfinite = CompHausLike fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X

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

Equations

• ⋯ = ⋯

@[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.

Equations

• LightProfinite.of X = CompHausLike.of (fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) X

instance LightProfinite.instInhabited : Inhabited LightProfinite

Equations

• LightProfinite.instInhabited = { default := LightProfinite.of PEmpty.{?u.3 + 1} }

instance LightProfinite.instTotallyDisconnectedSpaceαTopologicalSpaceToTopAndSecondCountableTopology {X : LightProfinite} : TotallyDisconnectedSpace ↑X.toTop

Equations

• ⋯ = ⋯

instance LightProfinite.instSecondCountableTopologyαTopologicalSpaceToTopAndTotallyDisconnectedSpace {X : LightProfinite} : SecondCountableTopology ↑X.toTop

Equations

• ⋯ = ⋯

instance LightProfinite.instTotallyDisconnectedSpaceObjForget {X : LightProfinite} : TotallyDisconnectedSpace ((CategoryTheory.forget LightProfinite).obj X)

Equations

• ⋯ = ⋯

instance LightProfinite.instSecondCountableTopologyObjForget {X : LightProfinite} : SecondCountableTopology ((CategoryTheory.forget LightProfinite).obj X)

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev lightToProfinite : CategoryTheory.Functor LightProfinite Profinite

The fully faithful embedding of LightProfinite in Profinite.

Equations

• lightToProfinite = CompHausLike.toCompHausLike lightToProfinite.proof_1

@[reducible, inline]

abbrev lightToProfiniteFullyFaithful : lightToProfinite.FullyFaithful

lightToProfinite is fully faithful.

Equations

• lightToProfiniteFullyFaithful = CompHausLike.fullyFaithfulToCompHausLike lightToProfinite.proof_1

@[reducible, inline]

abbrev lightProfiniteToCompHaus : CategoryTheory.Functor LightProfinite CompHaus

The fully faithful embedding of LightProfinite in CompHaus.

Equations

• lightProfiniteToCompHaus = compHausLikeToCompHaus fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X

@[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.

Equations

• LightProfinite.toTopCat = CompHausLike.compHausLikeToTop fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X

@[simp]

theorem FintypeCat.toLightProfinite_map_apply : ∀ {X Y : FintypeCat} (f : X ⟶ Y) (a : ↑X), (FintypeCat.toLightProfinite.map f) a = f a

@[simp]

theorem FintypeCat.toLightProfinite_obj_toTop_str_IsOpen (A : FintypeCat) (u : Set ↑A) : TopologicalSpace.IsOpen u = (u ∈ ⊤)

@[simp]

theorem FintypeCat.toLightProfinite_obj_toTop_α (A : FintypeCat) : ↑(FintypeCat.toLightProfinite.obj A).toTop = ↑A

def FintypeCat.toLightProfinite : CategoryTheory.Functor FintypeCat LightProfinite

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

Equations

• One or more equations did not get rendered due to their size.

def FintypeCat.toLightProfiniteFullyFaithful : FintypeCat.toLightProfinite.FullyFaithful

FintypeCat.toLightProfinite is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

instance instFaithfulFintypeCatLightProfiniteToLightProfinite : FintypeCat.toLightProfinite.Faithful

Equations

• instFaithfulFintypeCatLightProfiniteToLightProfinite = ⋯

instance instFullFintypeCatLightProfiniteToLightProfinite : FintypeCat.toLightProfinite.Full

Equations

• instFullFintypeCatLightProfiniteToLightProfinite = ⋯

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

Equations

• ⋯ = ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

instance LightProfinite.instHasCountableLimits : CategoryTheory.Limits.HasCountableLimits LightProfinite

Equations

• LightProfinite.instHasCountableLimits = ⋯

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

Equations

• LightProfinite.instPreservesLimitsOfShapeOppositeNatForget = inferInstanceAs (CategoryTheory.Limits.PreservesLimitsOfShape ℕᵒᵖ (lightToProfinite.comp (CategoryTheory.forget Profinite)))

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

Any morphism of light profinite spaces is a closed map.

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

Any continuous bijection of light profinite spaces induces an isomorphism.

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

Any continuous bijection of light profinite spaces induces an isomorphism.

Equations

• LightProfinite.isoOfBijective f bij = CategoryTheory.asIso f

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

Equations

• LightProfinite.forget_reflectsIsomorphisms = ⋯

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

instance LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite : lightToProfinite.PreservesEpimorphisms

Equations

• LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite = ⋯

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.

Equations

• S.toProfinite = S.cone.pt

@[simp]

theorem LightDiagram.instCategory_id_apply (X : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite) (a : ↑(LightDiagram.toProfinite X).toTop) : (CategoryTheory.CategoryStruct.id X) a = a

@[simp]

theorem LightDiagram.instCategory_comp_apply : ∀ {X Y Z : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite} (f : X ⟶ Y) (g : Y ⟶ Z) (a : ↑(LightDiagram.toProfinite X).toTop), (CategoryTheory.CategoryStruct.comp f g) a = g (f a)

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

Equations

• LightDiagram.instCategory = CategoryTheory.InducedCategory.category LightDiagram.toProfinite

instance LightDiagram.concreteCategory : CategoryTheory.ConcreteCategory LightDiagram

Equations

• LightDiagram.concreteCategory = CategoryTheory.InducedCategory.concreteCategory LightDiagram.toProfinite

@[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

def lightDiagramToProfinite : CategoryTheory.Functor LightDiagram Profinite

The fully faithful embedding LightDiagram ⥤ Profinite

Equations

• lightDiagramToProfinite = CategoryTheory.inducedFunctor LightDiagram.toProfinite

instance instFaithfulLightDiagramProfiniteLightDiagramToProfinite : lightDiagramToProfinite.Faithful

Equations

• instFaithfulLightDiagramProfiniteLightDiagramToProfinite = ⋯

instance instFullLightDiagramProfiniteLightDiagramToProfinite : lightDiagramToProfinite.Full

Equations

• instFullLightDiagramProfiniteLightDiagramToProfinite = ⋯

instance instTopologicalSpaceObjLightDiagramForget {X : LightDiagram} : TopologicalSpace ((CategoryTheory.forget LightDiagram).obj X)

Equations

• instTopologicalSpaceObjLightDiagramForget = inferInstance

instance instTotallyDisconnectedSpaceObjLightDiagramForget {X : LightDiagram} : TotallyDisconnectedSpace ((CategoryTheory.forget LightDiagram).obj X)

Equations

• ⋯ = ⋯

instance instCompactSpaceObjLightDiagramForget {X : LightDiagram} : CompactSpace ((CategoryTheory.forget LightDiagram).obj X)

Equations

• ⋯ = ⋯

instance instT2SpaceObjLightDiagramForget {X : LightDiagram} : T2Space ((CategoryTheory.forget LightDiagram).obj X)

Equations

• ⋯ = ⋯

instance LightProfinite.instCountableClopensαTopologicalSpaceToTopAndTotallyDisconnectedSpaceSecondCountableTopology (S : LightProfinite) : Countable (TopologicalSpace.Clopens ↑S.toTop)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem lightProfiniteToLightDiagram_map : ∀ {X Y : LightProfinite} (f : X ⟶ Y), lightProfiniteToLightDiagram.map f = f

noncomputable def lightProfiniteToLightDiagram : CategoryTheory.Functor LightProfinite LightDiagram

The functor part of the equivalence LightProfinite ≌ LightDiagram

Equations

• One or more equations did not get rendered due to their size.

instance instSecondCountableTopologyαTopologicalSpaceToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone (S : LightDiagram) : SecondCountableTopology ↑S.cone.pt.toTop

Equations

• ⋯ = ⋯

@[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 = f

def lightDiagramToLightProfinite : CategoryTheory.Functor LightDiagram LightProfinite

The inverse part of the equivalence LightProfinite ≌ LightDiagram

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LightProfinite.equivDiagram : LightProfinite ≌ LightDiagram

The equivalence of categories LightProfinite ≌ LightDiagram

Equations

• One or more equations did not get rendered due to their size.

instance instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram : lightProfiniteToLightDiagram.IsEquivalence

Equations

• instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram = ⋯

instance instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite : lightDiagramToLightProfinite.IsEquivalence

Equations

• instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite = ⋯

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.

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

A LightDiagram' yields a Profinite.

Equations

• S.toProfinite = CategoryTheory.Limits.limit (S.diagram.comp (FintypeCat.Skeleton.equivalence.functor.comp FintypeCat.toProfinite))

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

Equations

• instCategoryLightDiagram' = CategoryTheory.InducedCategory.category LightDiagram'.toProfinite

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

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

Equations

• One or more equations did not get rendered due to their size.

instance instFaithfulLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.Faithful

Equations

• instFaithfulLightDiagram'LightDiagramToLightFunctor = ⋯

instance instFullLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.Full

Equations

• instFullLightDiagram'LightDiagramToLightFunctor = ⋯

instance instEssSurjLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.EssSurj

Equations

• instEssSurjLightDiagram'LightDiagramToLightFunctor = ⋯

instance instIsEquivalenceLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.IsEquivalence

Equations

• instIsEquivalenceLightDiagram'LightDiagramToLightFunctor = ⋯

def LightDiagram.equivSmall : LightDiagram ≌ LightDiagram'

The equivalence between LightDiagram and a small category.

Equations

• LightDiagram.equivSmall = LightDiagram'.toLightFunctor.asEquivalence.symm

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

Equations

• instEssentiallySmallLightDiagram = ⋯

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

Equations

• instEssentiallySmallLightProfinite = ⋯