Profinite sets as limits of finite sets.

We show that any profinite set is isomorphic to the limit of its discrete (hence finite) quotients.

Definitions

There are a handful of definitions in this file, given X : Profinite:

1. X.fintypeDiagram is the functor DiscreteQuotient X ⥤ FintypeCat whose limit is isomorphic to X (the limit taking place in Profinite via FintypeCat.toProfinite, see 2).
2. X.diagram is an abbreviation for X.fintypeDiagram ⋙ FintypeCat.toProfinite.
3. X.asLimitCone is the cone over X.diagram whose cone point is X.
4. X.isoAsLimitConeLift is the isomorphism X ≅ (Profinite.limitCone X.diagram).X induced by lifting X.asLimitCone.
5. X.asLimitConeIso is the isomorphism X.asLimitCone ≅ (Profinite.limitCone X.diagram) induced by X.isoAsLimitConeLift.
6. X.asLimit is a term of type IsLimit X.asLimitCone.
7. X.lim : CategoryTheory.Limits.LimitCone X.asLimitCone is a bundled combination of 3 and 6.

def Profinite.fintypeDiagram (X : Profinite) : CategoryTheory.Functor (DiscreteQuotient ↑X.toCompHaus.toTop) FintypeCat

The functor DiscreteQuotient X ⥤ Fintype whose limit is isomorphic to X.

Equations

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

@[inline, reducible]

abbrev Profinite.diagram (X : Profinite) : CategoryTheory.Functor (DiscreteQuotient ↑X.toCompHaus.toTop) Profinite

An abbreviation for X.fintypeDiagram ⋙ FintypeCat.toProfinite.

Equations

• Profinite.diagram X = CategoryTheory.Functor.comp (Profinite.fintypeDiagram X) FintypeCat.toProfinite

def Profinite.asLimitCone (X : Profinite) : CategoryTheory.Limits.Cone (Profinite.diagram X)

A cone over X.diagram whose cone point is X.

Equations

• Profinite.asLimitCone X = { pt := X, π := CategoryTheory.NatTrans.mk fun (S : DiscreteQuotient ↑X.toCompHaus.toTop) => ContinuousMap.mk (DiscreteQuotient.proj S) }

instance Profinite.isIso_asLimitCone_lift (X : Profinite) : CategoryTheory.IsIso ((Profinite.limitConeIsLimit (Profinite.diagram X)).lift (Profinite.asLimitCone X))

Equations

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

def Profinite.isoAsLimitConeLift (X : Profinite) : X ≅ (Profinite.limitCone (Profinite.diagram X)).pt

The isomorphism between X and the explicit limit of X.diagram, induced by lifting X.asLimitCone.

Equations

• Profinite.isoAsLimitConeLift X = CategoryTheory.asIso ((Profinite.limitConeIsLimit (Profinite.diagram X)).lift (Profinite.asLimitCone X))

def Profinite.asLimitConeIso (X : Profinite) : Profinite.asLimitCone X ≅ Profinite.limitCone (Profinite.diagram X)

The isomorphism of cones X.asLimitCone and Profinite.limitCone X.diagram. The underlying isomorphism is defeq to X.isoAsLimitConeLift.

Equations

• Profinite.asLimitConeIso X = CategoryTheory.Limits.Cones.ext (Profinite.isoAsLimitConeLift (Profinite.asLimitCone X).pt)

def Profinite.asLimit (X : Profinite) : CategoryTheory.Limits.IsLimit (Profinite.asLimitCone X)

X.asLimitCone is indeed a limit cone.

Equations

• Profinite.asLimit X = CategoryTheory.Limits.IsLimit.ofIsoLimit (Profinite.limitConeIsLimit (Profinite.diagram X)) (Profinite.asLimitConeIso X).symm

def Profinite.lim (X : Profinite) : CategoryTheory.Limits.LimitCone (Profinite.diagram X)

A bundled version of X.asLimitCone and X.asLimit.

Equations

• Profinite.lim X = { cone := Profinite.asLimitCone X, isLimit := Profinite.asLimit X }