Documentation

Mathlib.Topology.Category.Profinite.AsLimit

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[reducible, inline]

    An abbreviation for X.fintypeDiagramFintypeCat.toProfinite.

    Equations
    Instances For

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

      Equations
      • X.asLimitCone = { pt := X, π := { app := fun (S : DiscreteQuotient X.toTop) => { toFun := S.proj, continuous_toFun := }, naturality := } }
      Instances For
        Equations
        • =

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

        Equations
        Instances For
          def Profinite.asLimitConeIso (X : Profinite) :
          X.asLimitCone Profinite.limitCone X.diagram

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

          Equations
          Instances For

            X.asLimitCone is indeed a limit cone.

            Equations
            Instances For

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

              Equations
              • X.lim = { cone := X.asLimitCone, isLimit := X.asLimit }
              Instances For