Documentation

Mathlib.Topology.Category.LightProfinite.AsLimit

Light profinite sets as limits of finite sets. #

We show that any light profinite set is isomorphic to a sequential limit of finite sets.

The limit cone for S : LightProfinite is S.asLimitCone, the fact that it's a limit is S.asLimit.

We also prove that the projection and transition maps in this limit are surjective.

@[reducible, inline]

The functor ℕᵒᵖ ⥤ FintypeCat whose limit is isomorphic to S.

Equations
  • S.fintypeDiagram = S.toLightDiagram.diagram
Instances For
    @[reducible, inline]

    An abbreviation for S.fintypeDiagramFintypeCat.toProfinite.

    Equations
    Instances For

      A cone over S.diagram whose cone point is isomorphic to S. (Auxiliary definition, use S.asLimitCone instead.)

      Equations
      Instances For
        def LightProfinite.isoMapCone (S : LightProfinite) :
        lightToProfinite.mapCone S.asLimitConeAux S.toLightDiagram.cone

        An auxiliary isomorphism of cones used to prove that S.asLimitConeAux is a limit cone.

        Equations
        Instances For

          S.asLimitConeAux is indeed a limit cone. (Auxiliary definition, use S.asLimit instead.)

          Equations
          Instances For

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

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

              S.asLimitCone is indeed a limit cone.

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

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

                Equations
                • S.lim = { cone := S.asLimitCone, isLimit := S.asLimit }
                Instances For
                  @[reducible, inline]
                  abbrev LightProfinite.proj (S : LightProfinite) (n : ) :
                  S S.diagram.obj (Opposite.op n)

                  The projection from S to the nth component of S.diagram.

                  Equations
                  Instances For
                    @[reducible, inline]

                    An abbreviation for the nth component of S.diagram.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev LightProfinite.transitionMap (S : LightProfinite) (n : ) :
                      S.component (n + 1) S.component n

                      The transition map from S_{n+1} to S_n in S.diagram.

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev LightProfinite.transitionMapLE (S : LightProfinite) {n : } {m : } (h : n m) :
                        S.component m S.component n

                        The transition map from S_m to S_n in S.diagram, when m ≤ n.

                        Equations
                        Instances For
                          theorem LightProfinite.proj_comp_transitionMap' (S : LightProfinite) (n : ) :
                          (S.transitionMap n) (S.proj (n + 1)) = (S.proj n)
                          theorem LightProfinite.proj_comp_transitionMapLE' (S : LightProfinite) {n : } {m : } (h : n m) :
                          (S.transitionMapLE h) (S.proj m) = (S.proj n)
                          theorem LightProfinite.surjective_transitionMapLE (S : LightProfinite) {n : } {m : } (h : n m) :
                          Function.Surjective (S.transitionMapLE h)