Extending cones in LightProfinite

Let (Sₙ)_{n : ℕᵒᵖ} be a sequential inverse system of finite sets and let S be its limit in Profinite. Let G be a functor from LightProfinite to a category C and suppose that G preserves the limit described above. Suppose further that the projection maps S ⟶ Sₙ are epimorphic for all n. Then G.obj S is isomorphic to a limit indexed by StructuredArrow S toLightProfinite (see LightProfinite.Extend.isLimitCone).

We also provide the dual result for a functor of the form G : LightProfiniteᵒᵖ ⥤ C.

We apply this to define LightProfinite.diagram', LightProfinite.asLimitCone', and LightProfinite.asLimit', analogues to their unprimed versions in Mathlib/Topology/Category/LightProfinite/AsLimit.lean, in which the indexing category is StructuredArrow S toLightProfinite instead of ℕᵒᵖ.

def LightProfinite.Extend.functor {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.StructuredArrow c.pt FintypeCat.toLightProfinite)

Given a sequential cone in LightProfinite consisting of finite sets, we obtain a functor from the indexing category to StructuredArrow c.pt toLightProfinite.

@[simp]

theorem LightProfinite.Extend.functor_map {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) {X✝ Y✝ : ℕᵒᵖ} (f : X✝ ⟶ Y✝) : (functor c).map f = CategoryTheory.StructuredArrow.homMk (F.map f) ⋯

@[simp]

theorem LightProfinite.Extend.functor_obj {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (i : ℕᵒᵖ) : (functor c).obj i = CategoryTheory.StructuredArrow.mk (c.π.app i)

def LightProfinite.Extend.functorOp {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) : CategoryTheory.Functor ℕ (CategoryTheory.CostructuredArrow FintypeCat.toLightProfinite.op (Opposite.op c.pt))

Given a sequential cone in LightProfinite consisting of finite sets, we obtain a functor from the opposite of the indexing category to CostructuredArrow toProfinite.op ⟨c.pt⟩.

@[simp]

theorem LightProfinite.Extend.functorOp_obj {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (X : ℕ) : (functorOp c).obj X = CategoryTheory.CostructuredArrow.mk (c.π.app (Opposite.op X)).op

@[simp]

theorem LightProfinite.Extend.functorOp_map {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) {X✝ Y✝ : ℕ} (f : X✝ ⟶ Y✝) : (functorOp c).map f = CategoryTheory.CostructuredArrow.homMk (F.map f.op).op ⋯

theorem LightProfinite.Extend.functor_initial {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] : (functor c).Initial

If the projection maps in the cone are epimorphic and the cone is limiting, then LightProfinite.Extend.functor is initial.

theorem LightProfinite.Extend.functorOp_final {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] : (functorOp c).Final

If the projection maps in the cone are epimorphic and the cone is limiting, then LightProfinite.Extend.functorOp is final.

def LightProfinite.Extend.cone {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfinite C) (S : LightProfinite) : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj S FintypeCat.toLightProfinite).comp (FintypeCat.toLightProfinite.comp G))

Given a functor G from LightProfinite and S : LightProfinite, we obtain a cone on (StructuredArrow.proj S toLightProfinite ⋙ toLightProfinite ⋙ G) with cone point G.obj S.

Whiskering this cone with LightProfinite.Extend.functor c gives G.mapCone c as we check in the example below.

noncomputable def LightProfinite.Extend.isLimitCone {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfinite C) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (hc' : CategoryTheory.Limits.IsLimit (G.mapCone c)) : CategoryTheory.Limits.IsLimit (cone G c.pt)

If c and G.mapCone c are limit cones and the projection maps in c are epimorphic, then cone G c.pt is a limit cone.

def LightProfinite.Extend.cocone {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfiniteᵒᵖ C) (S : LightProfinite) : CategoryTheory.Limits.Cocone ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op S)).comp (FintypeCat.toLightProfinite.op.comp G))

Given a functor G from LightProfiniteᵒᵖ and S : LightProfinite, we obtain a cocone on (CostructuredArrow.proj toLightProfinite.op ⟨S⟩ ⋙ toLightProfinite.op ⋙ G) with cocone point G.obj ⟨S⟩.

Whiskering this cocone with LightProfinite.Extend.functorOp c gives G.mapCocone c.op as we check in the example below.

@[simp]

theorem LightProfinite.Extend.cocone_pt {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfiniteᵒᵖ C) (S : LightProfinite) : (cocone G S).pt = G.obj (Opposite.op S)

@[simp]

theorem LightProfinite.Extend.cocone_ι_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfiniteᵒᵖ C) (S : LightProfinite) (i : CategoryTheory.CostructuredArrow FintypeCat.toLightProfinite.op (Opposite.op S)) : (cocone G S).ι.app i = G.map i.hom

noncomputable def LightProfinite.Extend.isColimitCocone {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfiniteᵒᵖ C) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (hc' : CategoryTheory.Limits.IsColimit (G.mapCocone c.op)) : CategoryTheory.Limits.IsColimit (cocone G c.pt)

If c is a limit cone, G.mapCocone c.op is a colimit cone and the projection maps in c are epimorphic, then cocone G c.pt is a colimit cone.

@[reducible, inline]

abbrev LightProfinite.fintypeDiagram' (S : LightProfinite) : CategoryTheory.Functor (CategoryTheory.StructuredArrow S FintypeCat.toLightProfinite) FintypeCat

A functor StructuredArrow S toLightProfinite ⥤ FintypeCat whose limit in LightProfinite is isomorphic to S.

@[reducible, inline]

abbrev LightProfinite.diagram' (S : LightProfinite) : CategoryTheory.Functor (CategoryTheory.StructuredArrow S FintypeCat.toLightProfinite) LightProfinite

An abbreviation for S.fintypeDiagram' ⋙ toLightProfinite.

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

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

instance LightProfinite.instEpiAppOppositeNatπAsLimitCone (S : LightProfinite) (i : ℕᵒᵖ) : CategoryTheory.Epi (S.asLimitCone.π.app i)

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

S.asLimitCone' is a limit cone.

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

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