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.fintypeDiagramFintypeCat.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.

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

Instances For
    @[inline, reducible]

    An abbreviation for X.fintypeDiagramFintypeCat.toProfinite.

    Instances For

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

      Instances For

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

        Instances For

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

          Instances For