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.

structure LightProfinite : Type (u + 1)

LightProfinite is the category of second countable profinite spaces.

• toCompHaus : CompHaus

  The underlying compact Hausdorff space of a light profinite space.

• isTotallyDisconnected : TotallyDisconnectedSpace ↑self.toCompHaus.toTop

  A light profinite space is totally disconnected

• secondCountable : SecondCountableTopology ↑self.toCompHaus.toTop

  A light profinite space is second countable

theorem LightProfinite.isTotallyDisconnected (self : LightProfinite) : TotallyDisconnectedSpace ↑self.toCompHaus.toTop

A light profinite space is totally disconnected

theorem LightProfinite.secondCountable (self : LightProfinite) : SecondCountableTopology ↑self.toCompHaus.toTop

A light profinite space is second countable

def 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 = LightProfinite.mk (CompHausLike.mk { α := X, str := inferInstance } trivial)

instance LightProfinite.instInhabited : Inhabited LightProfinite

Equations

• LightProfinite.instInhabited = { default := LightProfinite.of PEmpty.{u_1 + 1} }

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

Equations

• LightProfinite.category = CategoryTheory.InducedCategory.category LightProfinite.toCompHaus

instance LightProfinite.concreteCategory : CategoryTheory.ConcreteCategory LightProfinite

Equations

• LightProfinite.concreteCategory = CategoryTheory.InducedCategory.concreteCategory LightProfinite.toCompHaus

instance LightProfinite.hasForget₂ : CategoryTheory.HasForget₂ LightProfinite TopCat

Equations

• LightProfinite.hasForget₂ = CategoryTheory.InducedCategory.hasForget₂ fun (X : CategoryTheory.InducedCategory CompHaus LightProfinite.toCompHaus) => X.toCompHaus.toTop

instance LightProfinite.instCoeSortType : CoeSort LightProfinite (Type u_1)

Equations

• LightProfinite.instCoeSortType = { coe := fun (X : LightProfinite) => ↑X.toCompHaus.toTop }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem LightProfinite.coe_id (X : LightProfinite) : CategoryTheory.CategoryStruct.id ((CategoryTheory.forget LightProfinite).obj X) = id

@[simp]

theorem LightProfinite.coe_comp {X : LightProfinite} {Y : LightProfinite} {Z : LightProfinite} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget LightProfinite).map f) ((CategoryTheory.forget LightProfinite).map g) = ⇑g ∘ ⇑f

@[simp]

theorem lightToProfinite_obj (X : LightProfinite) : lightToProfinite.obj X = Profinite.of ↑X.toCompHaus.toTop

@[simp]

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

def lightToProfinite : CategoryTheory.Functor LightProfinite Profinite

The fully faithful embedding of LightProfinite in Profinite.

Equations

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

def lightToProfiniteFullyFaithful : lightToProfinite.FullyFaithful

lightToProfinite is fully faithful.

Equations

• lightToProfiniteFullyFaithful = CategoryTheory.fullyFaithfulInducedFunctor fun (X : LightProfinite) => Profinite.of ↑X.toCompHaus.toTop

instance instFaithfulLightProfiniteProfiniteLightToProfinite : lightToProfinite.Faithful

Equations

• instFaithfulLightProfiniteProfiniteLightToProfinite = ⋯

instance instFullLightProfiniteProfiniteLightToProfinite : lightToProfinite.Full

Equations

• instFullLightProfiniteProfiniteLightToProfinite = ⋯

@[simp]

theorem lightProfiniteToCompHaus_obj (self : LightProfinite) : lightProfiniteToCompHaus.obj self = self.toCompHaus

@[simp]

theorem lightProfiniteToCompHaus_map : ∀ {X Y : CategoryTheory.InducedCategory CompHaus LightProfinite.toCompHaus} (f : X ⟶ Y), lightProfiniteToCompHaus.map f = f

def lightProfiniteToCompHaus : CategoryTheory.Functor LightProfinite CompHaus

The fully faithful embedding of LightProfinite in CompHaus.

Equations

• lightProfiniteToCompHaus = CategoryTheory.inducedFunctor LightProfinite.toCompHaus

def lightProfiniteToCompHausFullyFaithful : lightProfiniteToCompHaus.FullyFaithful

lightProfiniteToCompHaus is fully faithful.

Equations

• lightProfiniteToCompHausFullyFaithful = CategoryTheory.fullyFaithfulInducedFunctor LightProfinite.toCompHaus

instance instFullLightProfiniteCompHausLightProfiniteToCompHaus : lightProfiniteToCompHaus.Full

Equations

• instFullLightProfiniteCompHausLightProfiniteToCompHaus = ⋯

instance instFaithfulLightProfiniteCompHausLightProfiniteToCompHaus : lightProfiniteToCompHaus.Faithful

Equations

• instFaithfulLightProfiniteCompHausLightProfiniteToCompHaus = ⋯

instance instTotallyDisconnectedSpaceαTopologicalSpaceToTopTrueObjLightProfiniteCompHausLightProfiniteToCompHaus {X : LightProfinite} : TotallyDisconnectedSpace ↑(lightProfiniteToCompHaus.obj X).toTop

Equations

• ⋯ = ⋯

instance instSecondCountableTopologyαTopologicalSpaceToTopTrueObjLightProfiniteCompHausLightProfiniteToCompHaus {X : LightProfinite} : SecondCountableTopology ↑(lightProfiniteToCompHaus.obj X).toTop

Equations

• ⋯ = ⋯

@[simp]

theorem LightProfinite.toTopCat_map : ∀ {X Y : CategoryTheory.InducedCategory TopCat fun (X : CategoryTheory.InducedCategory CompHaus LightProfinite.toCompHaus) => X.toCompHaus.toTop} (f : X ⟶ Y), LightProfinite.toTopCat.map f = f

@[simp]

theorem LightProfinite.toTopCat_obj (X : CategoryTheory.InducedCategory CompHaus LightProfinite.toCompHaus) : LightProfinite.toTopCat.obj X = X.toCompHaus.toTop

def 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 = CategoryTheory.forget₂ LightProfinite TopCat

def LightProfinite.toTopCatFullyFaithful : LightProfinite.toTopCat.FullyFaithful

LightProfinite.toTopCat is fully faithful.

Equations

• LightProfinite.toTopCatFullyFaithful = CategoryTheory.fullyFaithfulInducedFunctor fun (X : CategoryTheory.InducedCategory CompHaus LightProfinite.toCompHaus) => X.toCompHaus.toTop

instance instFullLightProfiniteTopCatToTopCat : LightProfinite.toTopCat.Full

Equations

• instFullLightProfiniteTopCatToTopCat = ⋯

instance instFaithfulLightProfiniteTopCatToTopCat : LightProfinite.toTopCat.Faithful

Equations

• instFaithfulLightProfiniteTopCatToTopCat = ⋯

@[simp]

theorem LightProfinite.toCompHaus_comp_toTop : lightProfiniteToCompHaus.comp compHausToTop = LightProfinite.toTopCat

@[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_toCompHaus_toTop_str_IsOpen (A : FintypeCat) (u : Set ↑A) : TopologicalSpace.IsOpen u = (u ∈ ⊤)

@[simp]

theorem FintypeCat.toLightProfinite_obj_toCompHaus_toTop_α (A : FintypeCat) : ↑(FintypeCat.toLightProfinite.obj A).toCompHaus.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

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

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 = ⋯

@[simp]

theorem LightProfinite.isoOfHomeo_hom {X : LightProfinite} {Y : LightProfinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) : (LightProfinite.isoOfHomeo f).hom = lightProfiniteToCompHausFullyFaithful.preimage (CompHausLike.isoOfHomeo f).hom

@[simp]

theorem LightProfinite.isoOfHomeo_inv {X : LightProfinite} {Y : LightProfinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) : (LightProfinite.isoOfHomeo f).inv = lightProfiniteToCompHausFullyFaithful.preimage (CompHausLike.isoOfHomeo f).inv

noncomputable def LightProfinite.isoOfHomeo {X : LightProfinite} {Y : LightProfinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) : X ≅ Y

Construct an isomorphism from a homeomorphism.

Equations

• LightProfinite.isoOfHomeo f = lightProfiniteToCompHausFullyFaithful.preimageIso (CompHausLike.isoOfHomeo f)

@[simp]

theorem LightProfinite.homeoOfIso_symm_apply {X : LightProfinite} {Y : LightProfinite} (f : X ≅ Y) (a : ↑Y.toCompHaus.toTop) : (LightProfinite.homeoOfIso f).symm a = f.inv a

@[simp]

theorem LightProfinite.homeoOfIso_apply {X : LightProfinite} {Y : LightProfinite} (f : X ≅ Y) (a : ↑X.toCompHaus.toTop) : (LightProfinite.homeoOfIso f) a = f.hom a

def LightProfinite.homeoOfIso {X : LightProfinite} {Y : LightProfinite} (f : X ≅ Y) : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop

Construct a homeomorphism from an isomorphism.

Equations

• LightProfinite.homeoOfIso f = CompHausLike.homeoOfIso (lightProfiniteToCompHaus.mapIso f)

@[simp]

theorem LightProfinite.isoEquivHomeo_apply_apply {X : LightProfinite} {Y : LightProfinite} (f : X ≅ Y) (a : ↑X.toCompHaus.toTop) : (LightProfinite.isoEquivHomeo f) a = f.hom a

@[simp]

theorem LightProfinite.isoEquivHomeo_apply_symm_apply {X : LightProfinite} {Y : LightProfinite} (f : X ≅ Y) (a : ↑Y.toCompHaus.toTop) : (LightProfinite.isoEquivHomeo f).symm a = f.inv a

@[simp]

theorem LightProfinite.isoEquivHomeo_symm_apply_inv_apply {X : LightProfinite} {Y : LightProfinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) (a : ↑((CompHausLike.compHausLikeToTop fun (x : TopCat) => True).obj (lightProfiniteToCompHaus.obj Y))) : (LightProfinite.isoEquivHomeo.symm f).inv a = f.symm a

@[simp]

theorem LightProfinite.isoEquivHomeo_symm_apply_hom_apply {X : LightProfinite} {Y : LightProfinite} (f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop) (a : ↑((CompHausLike.compHausLikeToTop fun (x : TopCat) => True).obj (lightProfiniteToCompHaus.obj X))) : (LightProfinite.isoEquivHomeo.symm f).hom a = f a

noncomputable def LightProfinite.isoEquivHomeo {X : LightProfinite} {Y : LightProfinite} : (X ≅ Y) ≃ (↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop)

The equivalence between isomorphisms in LightProfinite and homeomorphisms of topological spaces.

Equations

• LightProfinite.isoEquivHomeo = { toFun := LightProfinite.homeoOfIso, invFun := LightProfinite.isoOfHomeo, left_inv := ⋯, right_inv := ⋯ }

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

instance LightProfinite.instEpiCompHaus {X : LightProfinite} {Y : LightProfinite} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Epi f

Equations

• ⋯ = ⋯

instance LightProfinite.instEpiOfCompHaus {X : LightProfinite} {Y : LightProfinite} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Epi f

Equations

• ⋯ = ⋯

theorem LightProfinite.mono_iff_injective {X : LightProfinite} {Y : LightProfinite} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑f

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_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)

@[simp]

theorem LightDiagram.instCategory_id_apply (X : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite) (a : ↑(LightDiagram.toProfinite X).toTop) : (CategoryTheory.CategoryStruct.id X) a = 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_map : ∀ {X Y : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite} (f : X ⟶ Y), lightDiagramToProfinite.map f = f

@[simp]

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

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αTopologicalSpaceToTopTrueToCompHaus (S : LightProfinite) : Countable (TopologicalSpace.Clopens ↑S.toCompHaus.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_map : ∀ {X Y : LightProfinite} (f : X ⟶ Y), lightProfiniteToLightDiagram.map f = f

@[simp]

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

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 beween 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 = ⋯