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]

abbrev LightProfinite.fintypeDiagram (S : LightProfinite) : CategoryTheory.Functor ℕᵒᵖ FintypeCat

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

@[reducible, inline]

abbrev LightProfinite.diagram (S : LightProfinite) : CategoryTheory.Functor ℕᵒᵖ LightProfinite

An abbreviation for S.fintypeDiagram ⋙ FintypeCat.toProfinite.

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.)

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.

def LightProfinite.asLimitAux (S : LightProfinite) : CategoryTheory.Limits.IsLimit S.asLimitConeAux

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

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

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

def LightProfinite.asLimit (S : LightProfinite) : CategoryTheory.Limits.IsLimit S.asLimitCone

S.asLimitCone is indeed a limit cone.

def LightProfinite.lim (S : LightProfinite) : CategoryTheory.Limits.LimitCone S.diagram

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

@[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.

theorem LightProfinite.lightToProfinite_map_proj_eq (S : LightProfinite) (n : ℕ) : lightToProfinite.map (S.proj n) = (lightToProfinite.obj S).asLimitCone.π.app ((CategoryTheory.Limits.IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

theorem LightProfinite.proj_surjective (S : LightProfinite) (n : ℕ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))

@[reducible, inline]

abbrev LightProfinite.component (S : LightProfinite) (n : ℕ) : LightProfinite

An abbreviation for the nth component of S.diagram.

@[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.

@[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.

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

theorem LightProfinite.proj_comp_transitionMap' (S : LightProfinite) (n : ℕ) : ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (S.proj (n + 1))) = ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))

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

theorem LightProfinite.proj_comp_transitionMapLE' (S : LightProfinite) {n m : ℕ} (h : n ≤ m) : ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (S.proj m)) = ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))

theorem LightProfinite.surjective_transitionMap (S : LightProfinite) (n : ℕ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMap n))

theorem LightProfinite.surjective_transitionMapLE (S : LightProfinite) {n m : ℕ} (h : n ≤ m) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMapLE h))