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 (CategoryTheory.Functor.comp self.diagram 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

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

def LightProfinite.toProfinite (S : LightProfinite) : Profinite

The underlying Profinite of a LightProfinite.

Equations

• LightProfinite.toProfinite S = S.cone.pt

@[simp]

theorem LightProfinite.instCategoryLightProfinite_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)

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

instance LightProfinite.concreteCategory : CategoryTheory.ConcreteCategory LightProfinite

Equations

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

@[simp]

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

@[simp]

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

def LightProfinite.lightToProfinite : CategoryTheory.Functor LightProfinite Profinite

The fully faithful embedding LightProfinite ⥤ Profinite

Equations

• LightProfinite.lightToProfinite = CategoryTheory.inducedFunctor LightProfinite.toProfinite

instance LightProfinite.instFaithfulLightProfiniteInstCategoryLightProfiniteProfiniteCategoryLightToProfinite : CategoryTheory.Faithful LightProfinite.lightToProfinite

Equations

• LightProfinite.instFaithfulLightProfiniteInstCategoryLightProfiniteProfiniteCategoryLightToProfinite = (_ : CategoryTheory.Faithful (CategoryTheory.inducedFunctor LightProfinite.toProfinite))

instance LightProfinite.instFullLightProfiniteInstCategoryLightProfiniteProfiniteCategoryLightToProfinite : CategoryTheory.Full LightProfinite.lightToProfinite

Equations

• LightProfinite.instFullLightProfiniteInstCategoryLightProfiniteProfiniteCategoryLightToProfinite = let_fun this := inferInstance; this

instance LightProfinite.instReflectsEpimorphismsLightProfiniteInstCategoryLightProfiniteProfiniteCategoryLightToProfinite : CategoryTheory.Functor.ReflectsEpimorphisms LightProfinite.lightToProfinite

Equations

• LightProfinite.instReflectsEpimorphismsLightProfiniteInstCategoryLightProfiniteProfiniteCategoryLightToProfinite = (_ : CategoryTheory.Functor.ReflectsEpimorphisms LightProfinite.lightToProfinite)

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

Equations

• LightProfinite.instTopologicalSpaceObjLightProfiniteToQuiverToCategoryStructInstCategoryLightProfiniteTypeTypesToPrefunctorForgetConcreteCategory = inferInstance

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

Equations

• (_ : TotallyDisconnectedSpace ((CategoryTheory.forget LightProfinite).toPrefunctor.obj X)) = (_ : TotallyDisconnectedSpace ↑X.cone.pt.toCompHaus.toTop)

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

Equations

• (_ : CompactSpace ((CategoryTheory.forget LightProfinite).toPrefunctor.obj X)) = (_ : CompactSpace ↑X.cone.pt.toCompHaus.toTop)

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

Equations

• (_ : T2Space ((CategoryTheory.forget LightProfinite).toPrefunctor.obj X)) = (_ : T2Space ↑X.cone.pt.toCompHaus.toTop)

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.

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

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

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'InstCategoryLightProfinite'LightProfiniteInstCategoryLightProfiniteToLightFunctor : CategoryTheory.Faithful LightProfinite'.toLightFunctor

Equations

• instFaithfulLightProfinite'InstCategoryLightProfinite'LightProfiniteInstCategoryLightProfiniteToLightFunctor = (_ : CategoryTheory.Faithful LightProfinite'.toLightFunctor)

instance instFullLightProfinite'InstCategoryLightProfinite'LightProfiniteInstCategoryLightProfiniteToLightFunctor : CategoryTheory.Full LightProfinite'.toLightFunctor

Equations

• instFullLightProfinite'InstCategoryLightProfinite'LightProfiniteInstCategoryLightProfiniteToLightFunctor = CategoryTheory.Full.mk fun {X Y : LightProfinite'} => id

instance instEssSurjLightProfinite'LightProfiniteInstCategoryLightProfinite'InstCategoryLightProfiniteToLightFunctor : CategoryTheory.EssSurj LightProfinite'.toLightFunctor

Equations

• instEssSurjLightProfinite'LightProfiniteInstCategoryLightProfinite'InstCategoryLightProfiniteToLightFunctor = (_ : CategoryTheory.EssSurj LightProfinite'.toLightFunctor)

instance instIsEquivalenceLightProfinite'InstCategoryLightProfinite'LightProfiniteInstCategoryLightProfiniteToLightFunctor : CategoryTheory.IsEquivalence LightProfinite'.toLightFunctor

Equations

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

def LightProfinite.equivSmall : LightProfinite ≌ LightProfinite'

The equivalence beween LightProfinite and a small category.

Equations

• LightProfinite.equivSmall = (CategoryTheory.Functor.asEquivalence LightProfinite'.toLightFunctor).symm

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

Equations

• instEssentiallySmallLightProfiniteInstCategoryLightProfinite = (_ : CategoryTheory.EssentiallySmall.{u, u, u + 1} LightProfinite)