Extending cones in Profinite

Let (Sᵢ)_{i : I} be a family of finite sets indexed by a cofiltered category I and let S be its limit in Profinite. Let G be a functor from Profinite 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 i. Then G.obj S is isomorphic to a limit indexed by StructuredArrow S toProfinite (see Profinite.Extend.isLimitCone).

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

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

theorem Profinite.exists_hom {I : Type u} [CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (hc : CategoryTheory.Limits.IsLimit c) {X : FintypeCat} (f : c.pt ⟶ FintypeCat.toProfinite.obj X) : ∃ (i : I) (g : F.obj i ⟶ X), f = CategoryTheory.CategoryStruct.comp (c.π.app i) (FintypeCat.toProfinite.map g)

A continuous map from a profinite set to a finite set factors through one of the components of the profinite set when written as a cofiltered limit of finite sets.

def Profinite.Extend.functor {I : Type u} [CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) : CategoryTheory.Functor I (CategoryTheory.StructuredArrow c.pt FintypeCat.toProfinite)

Given a cone in Profinite, consisting of finite sets and indexed by a cofiltered category, we obtain a functor from the indexing category to StructuredArrow c.pt toProfinite.

@[simp]

theorem Profinite.Extend.functor_map {I : Type u} [CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) {X✝ Y✝ : I} (f : X✝ ⟶ Y✝) : (functor c).map f = CategoryTheory.StructuredArrow.homMk (F.map f) ⋯

@[simp]

theorem Profinite.Extend.functor_obj {I : Type u} [CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (i : I) : (functor c).obj i = CategoryTheory.StructuredArrow.mk (c.π.app i)

def Profinite.Extend.functorOp {I : Type u} [CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) : CategoryTheory.Functor Iᵒᵖ (CategoryTheory.CostructuredArrow FintypeCat.toProfinite.op (Opposite.op c.pt))

Given a cone in Profinite, consisting of finite sets and indexed by a cofiltered category, we obtain a functor from the opposite of the indexing category to CostructuredArrow toProfinite.op ⟨c.pt⟩.

@[simp]

theorem Profinite.Extend.functorOp_map {I : Type u} [CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) {X✝ Y✝ : Iᵒᵖ} (f : X✝ ⟶ Y✝) : (functorOp c).map f = CategoryTheory.CostructuredArrow.homMk (F.map f.unop).op ⋯

@[simp]

theorem Profinite.Extend.functorOp_obj {I : Type u} [CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (X : Iᵒᵖ) : (functorOp c).obj X = CategoryTheory.CostructuredArrow.mk (c.π.app (Opposite.unop X)).op

theorem Profinite.Extend.functor_initial {I : Type u} [CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] : (functor c).Initial

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

TODO: investigate how to weaken the assumption ∀ i, Epi (c.π.app i) to ∀ i, ∃ j (_ : j ⟶ i), Epi (c.π.app j).

theorem Profinite.Extend.functorOp_final {I : Type u} [CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] : (functorOp c).Final

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

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

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

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

@[simp]

theorem Profinite.Extend.cone_pt {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (S : Profinite) : (cone G S).pt = G.obj S

@[simp]

theorem Profinite.Extend.cone_π_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (S : Profinite) (i : CategoryTheory.StructuredArrow S FintypeCat.toProfinite) : (cone G S).π.app i = G.map i.hom

noncomputable def Profinite.Extend.isLimitCone {I : Type u} [CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : 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 Profinite.Extend.cocone {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profiniteᵒᵖ C) (S : Profinite) : CategoryTheory.Limits.Cocone ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op S)).comp (FintypeCat.toProfinite.op.comp G))

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

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

@[simp]

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

@[simp]

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

noncomputable def Profinite.Extend.isColimitCocone {I : Type u} [CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profiniteᵒᵖ C) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : 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 Profinite.fintypeDiagram' (S : Profinite) : CategoryTheory.Functor (CategoryTheory.StructuredArrow S FintypeCat.toProfinite) FintypeCat

A functor StructuredArrow S toProfinite ⥤ FintypeCat whose limit in Profinite is isomorphic to S.

@[reducible, inline]

abbrev Profinite.diagram' (S : Profinite) : CategoryTheory.Functor (CategoryTheory.StructuredArrow S FintypeCat.toProfinite) Profinite

An abbreviation for S.fintypeDiagram' ⋙ toProfinite.

@[reducible, inline]

abbrev Profinite.asLimitCone' (S : Profinite) : CategoryTheory.Limits.Cone S.diagram'

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

instance Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone (S : Profinite) (i : DiscreteQuotient ↑S.toTop) : CategoryTheory.Epi (S.asLimitCone.π.app i)

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

S.asLimitCone' is a limit cone.

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

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