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.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.
source
def Profinite.fintypeDiagram (X : Profinite) :
CategoryTheory.Functor (DiscreteQuotient ↑X.toCompHaus.toTop) FintypeCat

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

Instances For
    source
    @[inline, reducible]
    abbrev Profinite.diagram (X : Profinite) :
    CategoryTheory.Functor (DiscreteQuotient ↑X.toCompHaus.toTop) Profinite

    An abbreviation for X.fintypeDiagram ⋙ FintypeCat.toProfinite.

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

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

      Instances For
        source
        instance Profinite.isIso_asLimitCone_lift (X : Profinite) :
        CategoryTheory.IsIso (CategoryTheory.Limits.IsLimit.lift (Profinite.limitConeIsLimit (Profinite.diagram X)) (Profinite.asLimitCone X))
        source
        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.

        Instances For
          source
          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.

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

            X.asLimitCone is indeed a limit cone.

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

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

              Instances For