Light profinite sets

This file contains the basic definitions related to light profinite sets.

Main definitions

• LightProfinite is a structure containing the data of a sequential limit (in Profinite) of finite sets.

• lightToProfinite is the fully faithful embedding of LightProfinite in Profinite.

• LightProfinite.equivSmall is an equivalence from LightProfinite to a small category. In other words, LightProfinite is essentially small.

structure LightProfinite : Type (u + 1)

A light profinite set is one which can be written as a sequential limit 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 FintypeCat.toLightProfinite (X : FintypeCat) : LightProfinite

A finite set can be regarded as a light profinite set as the limit of the constant diagram.

Equations

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

theorem LightProfinite.ext {Y : LightProfinite} {a : ↑Y.cone.pt.toCompHaus.toTop} {b : ↑Y.cone.pt.toCompHaus.toTop} (h : ∀ (n : ℕᵒᵖ), (Y.cone.π.app n) a = (Y.cone.π.app n) b) : a = b

noncomputable def LightProfinite.of (F : CategoryTheory.Functor ℕᵒᵖ FintypeCat) : LightProfinite

Given a functor from ℕᵒᵖ to finite sets we can take its limit in Profinite and obtain a light profinite set. 

Equations

• LightProfinite.of F = { diagram := F, cone := CategoryTheory.Limits.limit.cone (F.comp FintypeCat.toProfinite), isLimit := CategoryTheory.Limits.limit.isLimit (F.comp FintypeCat.toProfinite) }

def LightProfinite.toProfinite (S : LightProfinite) : Profinite

The underlying Profinite of a LightProfinite.

Equations

• S.toProfinite = S.cone.pt

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

theorem LightProfinite.concreteCategory_forget_map : ∀ {X Y : CategoryTheory.InducedCategory Profinite LightProfinite.toProfinite} (f : X ⟶ Y) (a : (CategoryTheory.forget Profinite).obj ((CategoryTheory.inducedFunctor LightProfinite.toProfinite).obj X)), CategoryTheory.ConcreteCategory.forget.map f a = (CategoryTheory.forget Profinite).map f a

@[simp]

theorem LightProfinite.concreteCategory_forget_obj (X : CategoryTheory.InducedCategory Profinite LightProfinite.toProfinite) : CategoryTheory.ConcreteCategory.forget.obj X = (CategoryTheory.forget Profinite).obj (LightProfinite.toProfinite X)

instance LightProfinite.concreteCategory : CategoryTheory.ConcreteCategory LightProfinite

Equations

• LightProfinite.concreteCategory = CategoryTheory.InducedCategory.concreteCategory LightProfinite.toProfinite

@[simp]

theorem LightProfinite.lightToProfinite_obj (S : LightProfinite) : LightProfinite.lightToProfinite.obj S = S.toProfinite

@[simp]

theorem LightProfinite.lightToProfinite_map : ∀ {X Y : CategoryTheory.InducedCategory Profinite LightProfinite.toProfinite} (f : X ⟶ Y), LightProfinite.lightToProfinite.map f = f

def LightProfinite.lightToProfinite : CategoryTheory.Functor LightProfinite Profinite

The fully faithful embedding LightProfinite ⥤ Profinite

Equations

• LightProfinite.lightToProfinite = CategoryTheory.inducedFunctor LightProfinite.toProfinite

instance LightProfinite.instFaithfulProfiniteLightToProfinite : LightProfinite.lightToProfinite.Faithful

Equations

• LightProfinite.instFaithfulProfiniteLightToProfinite = ⋯

instance LightProfinite.instFullProfiniteLightToProfinite : LightProfinite.lightToProfinite.Full

Equations

• LightProfinite.instFullProfiniteLightToProfinite = ⋯

instance LightProfinite.instReflectsEpimorphismsProfiniteLightToProfinite : LightProfinite.lightToProfinite.ReflectsEpimorphisms

Equations

• LightProfinite.instReflectsEpimorphismsProfiniteLightToProfinite = ⋯

instance LightProfinite.instTopologicalSpaceObjForget {X : LightProfinite} : TopologicalSpace ((CategoryTheory.forget LightProfinite).obj X)

Equations

• LightProfinite.instTopologicalSpaceObjForget = inferInstance

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

Equations

• ⋯ = ⋯

instance LightProfinite.instCompactSpaceObjForget {X : LightProfinite} : CompactSpace ((CategoryTheory.forget LightProfinite).obj X)

Equations

• ⋯ = ⋯

instance LightProfinite.instT2SpaceObjForget {X : LightProfinite} : T2Space ((CategoryTheory.forget LightProfinite).obj X)

Equations

• ⋯ = ⋯

def LightProfinite.fintypeCatToLightProfinite : CategoryTheory.Functor FintypeCat LightProfinite

The explicit functor FintypeCat ⥤ LightProfinite.

Equations

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

instance LightProfinite.instFaithfulFintypeCatFintypeCatToLightProfinite : LightProfinite.fintypeCatToLightProfinite.Faithful

Equations

• LightProfinite.instFaithfulFintypeCatFintypeCatToLightProfinite = ⋯

instance LightProfinite.instFullFintypeCatFintypeCatToLightProfinite : LightProfinite.fintypeCatToLightProfinite.Full

Equations

• LightProfinite.instFullFintypeCatFintypeCatToLightProfinite = ⋯

structure LightProfinite' : Type u

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

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

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

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

A LightProfinite' yields a Profinite.

Equations

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

instance instCategoryLightProfinite' : CategoryTheory.Category.{u_1, u_1} LightProfinite'

Equations

• instCategoryLightProfinite' = CategoryTheory.InducedCategory.category LightProfinite'.toProfinite

def LightProfinite'.toLightFunctor : CategoryTheory.Functor LightProfinite' LightProfinite

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

Equations

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

instance instFaithfulLightProfinite'LightProfiniteToLightFunctor : LightProfinite'.toLightFunctor.Faithful

Equations

• instFaithfulLightProfinite'LightProfiniteToLightFunctor = ⋯

instance instFullLightProfinite'LightProfiniteToLightFunctor : LightProfinite'.toLightFunctor.Full

Equations

• instFullLightProfinite'LightProfiniteToLightFunctor = ⋯

instance instEssSurjLightProfinite'LightProfiniteToLightFunctor : LightProfinite'.toLightFunctor.EssSurj

Equations

• instEssSurjLightProfinite'LightProfiniteToLightFunctor = ⋯

instance instIsEquivalenceLightProfinite'LightProfiniteToLightFunctor : LightProfinite'.toLightFunctor.IsEquivalence

Equations

• instIsEquivalenceLightProfinite'LightProfiniteToLightFunctor = CategoryTheory.Functor.IsEquivalence.ofFullyFaithfullyEssSurj LightProfinite'.toLightFunctor

def LightProfinite.equivSmall : LightProfinite ≌ LightProfinite'

The equivalence beween LightProfinite and a small category.

Equations

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

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

Equations

• instEssentiallySmallLightProfinite = ⋯