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 = let c := S.toLightDiagram.cone; let hc := S.toLightDiagram.isLimit; CategoryTheory.liftLimit hc

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 = let c := S.toLightDiagram.cone; let hc := S.toLightDiagram.isLimit; CategoryTheory.liftedLimitMapsToOriginal hc

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 = let hc := S.toLightDiagram.isLimit.ofIsoLimit S.isoMapCone.symm; CategoryTheory.Limits.isLimitOfReflects lightToProfinite hc

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.map_liftedLimit {C : Type u_1} {D : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [CategoryTheory.CreatesLimit K F] {c : CategoryTheory.Limits.Cone (K.comp F)} (t : CategoryTheory.Limits.IsLimit c) (n : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.liftedLimitMapsToOriginal t).inv.hom (F.map ((CategoryTheory.liftLimit t).π.app n)) = c.π.app n

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

theorem LightProfinite.proj_surjective (S : LightProfinite) (n : ℕ) : Function.Surjective ⇑(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 : ℕ) : ⇑(S.transitionMap n) ∘ ⇑(S.proj (n + 1)) = ⇑(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) : ⇑(S.transitionMapLE h) ∘ ⇑(S.proj m) = ⇑(S.proj n)

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

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