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.

Equations

• S.fintypeDiagram = S.toLightDiagram.diagram

@[reducible, inline]

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

An abbreviation for S.fintypeDiagram ⋙ FintypeCat.toProfinite.

Equations

• S.diagram = S.fintypeDiagram.comp FintypeCat.toLightProfinite

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

• S.asLimitConeAux = CategoryTheory.liftLimit S.toLightDiagram.isLimit

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

• S.isoMapCone = CategoryTheory.liftedLimitMapsToOriginal S.toLightDiagram.isLimit

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

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

Equations

• S.asLimitAux = CategoryTheory.Limits.isLimitOfReflects lightToProfinite (S.toLightDiagram.isLimit.ofIsoLimit S.isoMapCone.symm)

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.

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.

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 }

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

• S.proj n = S.asLimitCone.π.app (Opposite.op n)

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.

Equations

• S.component n = S.diagram.obj (Opposite.op n)

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

• S.transitionMap n = S.diagram.map (Opposite.op (CategoryTheory.homOfLE ⋯))

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

• S.transitionMapLE h = S.diagram.map (Opposite.op (CategoryTheory.homOfLE h))

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