mathlib3 documentation

topology.category.Profinite.as_limit

Profinite sets as limits of finite sets. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.fintype_diagram is the functor discrete_quotient X ⥤ Fintype whose limit is isomorphic to X (the limit taking place in Profinite via Fintype_to_Profinite, see 2).
  2. X.diagram is an abbreviation for X.fintype_diagram ⋙ Fintype_to_Profinite.
  3. X.as_limit_cone is the cone over X.diagram whose cone point is X.
  4. X.iso_as_limit_cone_lift is the isomorphism X ≅ (Profinite.limit_cone X.diagram).X induced by lifting X.as_limit_cone.
  5. X.as_limit_cone_iso is the isomorphism X.as_limit_cone ≅ (Profinite.limit_cone X.diagram) induced by X.iso_as_limit_cone_lift.
  6. X.as_limit is a term of type is_limit X.as_limit_cone.
  7. X.lim : category_theory.limits.limit_cone X.as_limit_cone is a bundled combination of 3 and 6.
source
noncomputable def Profinite.fintype_diagram (X : Profinite) :
discrete_quotient ↥X ⥤ Fintype

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

Equations
source
@[reducible]
noncomputable def Profinite.diagram (X : Profinite) :
discrete_quotient ↥X ⥤ Profinite

An abbreviation for X.fintype_diagram ⋙ Fintype_to_Profinite.

source
def Profinite.as_limit_cone (X : Profinite) :
category_theory.limits.cone X.diagram

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

Equations
source
@[protected, instance]
def Profinite.is_iso_as_limit_cone_lift (X : Profinite) :
category_theory.is_iso ((Profinite.limit_cone_is_limit X.diagram).lift X.as_limit_cone)
source
noncomputable def Profinite.iso_as_limit_cone_lift (X : Profinite) :
X ≅ (Profinite.limit_cone X.diagram).X

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

Equations
source
noncomputable def Profinite.as_limit_cone_iso (X : Profinite) :
X.as_limit_cone ≅ Profinite.limit_cone X.diagram

The isomorphism of cones X.as_limit_cone and Profinite.limit_cone X.diagram. The underlying isomorphism is defeq to X.iso_as_limit_cone_lift.

Equations
source
noncomputable def Profinite.as_limit (X : Profinite) :
category_theory.limits.is_limit X.as_limit_cone

X.as_limit_cone is indeed a limit cone.

Equations
source
noncomputable def Profinite.lim (X : Profinite) :
category_theory.limits.limit_cone X.diagram

A bundled version of X.as_limit_cone and X.as_limit.

Equations