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.

source
@[reducible, inline]
abbrev LightProfinite.fintypeDiagram (S : LightProfinite) :
CategoryTheory.Functor ℕᵒᵖ FintypeCat

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

Equations
  • S.fintypeDiagram = S.toLightDiagram.diagram
source
@[reducible, inline]
abbrev LightProfinite.diagram (S : LightProfinite) :
CategoryTheory.Functor ℕᵒᵖ LightProfinite

An abbreviation for S.fintypeDiagram ⋙ FintypeCat.toProfinite.

Equations
source
def LightProfinite.asLimitConeAux (S : LightProfinite) :
CategoryTheory.Limits.Cone S.diagram

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

Equations
source
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
source
def LightProfinite.asLimitAux (S : LightProfinite) :
CategoryTheory.Limits.IsLimit S.asLimitConeAux

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

Equations
source
def LightProfinite.asLimitCone (S : LightProfinite) :
CategoryTheory.Limits.Cone S.diagram

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

Equations
  • One or more equations did not get rendered due to their size.
source
def LightProfinite.asLimit (S : LightProfinite) :
CategoryTheory.Limits.IsLimit S.asLimitCone

S.asLimitCone is indeed a limit cone.

Equations
  • One or more equations did not get rendered due to their size.
source
def LightProfinite.lim (S : LightProfinite) :
CategoryTheory.Limits.LimitCone S.diagram

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

Equations
  • S.lim = { cone := S.asLimitCone, isLimit := S.asLimit }
source
@[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
source
theorem LightProfinite.lightToProfinite_map_proj_eq (S : LightProfinite) (n : ℕ) :
lightToProfinite.map (S.proj n) = (lightToProfinite.obj S).asLimitCone.π.app ((CategoryTheory.Limits.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))
source
theorem LightProfinite.proj_surjective (S : LightProfinite) (n : ℕ) :
Function.Surjective ⇑(S.proj n)
source
@[reducible, inline]
abbrev LightProfinite.component (S : LightProfinite) (n : ℕ) :
LightProfinite

An abbreviation for the nth component of S.diagram.

Equations
source
@[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
source
@[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
source
theorem LightProfinite.proj_comp_transitionMap (S : LightProfinite) (n : ℕ) :
CategoryTheory.CategoryStruct.comp (S.proj (n + 1)) (S.diagram.map (Opposite.op (CategoryTheory.homOfLE ⋯))) = S.proj n
source
theorem LightProfinite.proj_comp_transitionMap' (S : LightProfinite) (n : ℕ) :
⇑(S.transitionMap n) ∘ ⇑(S.proj (n + 1)) = ⇑(S.proj n)
source
theorem LightProfinite.proj_comp_transitionMapLE (S : LightProfinite) {n m : ℕ} (h : n ≤ m) :
CategoryTheory.CategoryStruct.comp (S.proj m) (S.diagram.map (Opposite.op (CategoryTheory.homOfLE h))) = S.proj n
source
theorem LightProfinite.proj_comp_transitionMapLE' (S : LightProfinite) {n m : ℕ} (h : n ≤ m) :
⇑(S.transitionMapLE h) ∘ ⇑(S.proj m) = ⇑(S.proj n)
source
theorem LightProfinite.surjective_transitionMap (S : LightProfinite) (n : ℕ) :
Function.Surjective ⇑(S.transitionMap n)
source
theorem LightProfinite.surjective_transitionMapLE (S : LightProfinite) {n m : ℕ} (h : n ≤ m) :
Function.Surjective ⇑(S.transitionMapLE h)