Being light is a property of profinite spaces #

We define a class Profinite.IsLight which says that a profinite space S has countably many clopen subsets. We prove that a profinite space which IsLight gives rise to a LightProfinite and that the underlying profinite space of a LightProfinite is light.

Main results #

IsLight is preserved under taking cartesian products
Given a monomorphism whose target IsLight, its sourse is also light: Profinite.isLight_of_mono

Project #

Prove the Stone duality theorem that Profinite is equivalent to the opposite category of boolean algebras. Then the property of being light says precisely that the corresponding boolean algebra is countable. Maybe constructions of limits and colimits in LightProfinite become easier when transporting over this equivalence.

source

class Profinite.IsLight (S : Profinite) :

Prop

A profinite space is light if it has countably many clopen subsets.

countable_clopens : Countable (TopologicalSpace.Clopens ↑S.toCompHaus.toTop)
The set of clopens is countable

Instances

source

instance Profinite.instIsLightProd (X : Profinite) (Y : Profinite) [Profinite.IsLight X] [Profinite.IsLight Y] :

Profinite.IsLight (Profinite.of (↑X.toCompHaus.toTop × ↑Y.toCompHaus.toTop))

Equations

⋯ = ⋯

source

instance Profinite.instCountableDiscreteQuotientOfIsLight (S : Profinite) [Profinite.IsLight S] :

Countable (DiscreteQuotient ↑S.toCompHaus.toTop)

Equations

⋯ = ⋯

source

noncomputable def LightProfinite.ofIsLight (S : Profinite) [Profinite.IsLight S] :

LightProfinite

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.

Instances For

source

instance LightProfinite.instIsLightToProfinite (S : LightProfinite) :

Profinite.IsLight (LightProfinite.toProfinite S)

Equations

⋯ = ⋯

source

instance LightProfinite.instIsLightObjLightProfiniteToQuiverToCategoryStructInstCategoryLightProfiniteProfiniteCategoryToPrefunctorLightToProfinite (S : LightProfinite) :

Profinite.IsLight (LightProfinite.lightToProfinite.obj S)

Equations

⋯ = ⋯

Given a monomorphism f : X ⟶ Y in Profinite, such that Y.IsLight, we want to prove that X.IsLight. We do this by regarding Y as a LightProfinite, and constructing a LightProfinite with X as its underlying Profinite. The diagram is just the image of f in the diagram of Y.

source

noncomputable def Profinite.lightProfiniteDiagramOfHom {X : Profinite} {Y : LightProfinite} (f : X ⟶ LightProfinite.toProfinite Y) :

CategoryTheory.Functor ℕ ᵒᵖ FintypeCat

The image of f in the diagram of Y

Equations

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

Instances For

source

def Profinite.lightProfiniteConeOfHom_π_app' {X : Profinite} {Y : LightProfinite} (f : X ⟶ LightProfinite.toProfinite Y) (n : ℕ ᵒᵖ) :

C(↑X.toCompHaus.toTop, ↑(Set.range ⇑(CategoryTheory.CategoryStruct.comp f (Y.cone.π.app n))))

An auxiliary definition to prove continuity in lightProfiniteConeOfHom_π_app.

Equations

Profinite.lightProfiniteConeOfHom_π_app' f n = { toFun := fun (x : ↑X.toCompHaus.toTop) => { val := (Y.cone.π.app n) (f x), property := ⋯ }, continuous_toFun := ⋯ }

Instances For

source

def Profinite.lightProfiniteConeOfHom_π_app {X : Profinite} {Y : LightProfinite} (f : X ⟶ LightProfinite.toProfinite Y) (n : ℕ ᵒᵖ) :

X ⟶ (CategoryTheory.Functor.comp (Profinite.lightProfiniteDiagramOfHom f) FintypeCat.toProfinite).obj n

An auxiliary definition for lightProfiniteConeOfHom.

Equations

Profinite.lightProfiniteConeOfHom_π_app f n = { toFun := fun (x : ↑X.toCompHaus.toTop) => { val := (Y.cone.π.app n) (f x), property := ⋯ }, continuous_toFun := ⋯ }