The condensed set given by left Kan extension from FintypeCat to Profinite.

This file provides the necessary API to prove that a condensed set X is discrete if and only if for every profinite set S = limᵢSᵢ, X(S) ≅ colimᵢX(Sᵢ), and the analogous result for light condensed sets.

@[reducible, inline]

abbrev Condensed.locallyConstantPresheaf (X : Type (u + 1)) : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))

The presheaf on Profinite of locally constant functions to X.

noncomputable def Condensed.isColimitLocallyConstantPresheaf {I : Type u} [CategoryTheory.Category.{u, u} I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (X : Type (u + 1)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] : CategoryTheory.Limits.IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

The functor locallyConstantPresheaf takes cofiltered limits of finite sets with surjective projection maps to colimits.

@[simp]

theorem Condensed.isColimitLocallyConstantPresheaf_desc_apply {I : Type u} [CategoryTheory.Category.{u, u} I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (X : Type (u + 1)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toProfinite).op.comp (locallyConstantPresheaf X))) (i : I) (f : LocallyConstant (↑(FintypeCat.toProfinite.obj (F.obj i)).toTop) X) : (isColimitLocallyConstantPresheaf c X hc).desc s (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) f) = s.ι.app (Opposite.op i) f

noncomputable def Condensed.isColimitLocallyConstantPresheafDiagram (X : Type (u + 1)) (S : Profinite) : CategoryTheory.Limits.IsColimit ((locallyConstantPresheaf X).mapCocone S.asLimitCone.op)

isColimitLocallyConstantPresheaf in the case of S.asLimit.

@[simp]

theorem Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply (X : Type (u + 1)) (S : Profinite) (s : CategoryTheory.Limits.Cocone (S.diagram.op.comp (locallyConstantPresheaf X))) (i : DiscreteQuotient ↑S.toTop) (f : LocallyConstant (↑(S.diagram.obj i).toTop) X) : (isColimitLocallyConstantPresheafDiagram X S).desc s (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app i).hom) f) = s.ι.app (Opposite.op i) f

@[reducible, inline]

noncomputable abbrev Condensed.lanPresheaf (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))

Given a presheaf F on Profinite, lanPresheaf F is the left Kan extension of its restriction to finite sets along the inclusion functor of finite sets into Profinite.

noncomputable def Condensed.lanPresheafExt {F G : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (i : FintypeCat.toProfinite.op.comp F ≅ FintypeCat.toProfinite.op.comp G) : lanPresheaf F ≅ lanPresheaf G

To presheaves on Profinite whose restrictions to finite sets are isomorphic have isomorphic left Kan extensions.

@[simp]

theorem Condensed.lanPresheafExt_hom {F G : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (S : Profiniteᵒᵖ) (i : FintypeCat.toProfinite.op.comp F ≅ FintypeCat.toProfinite.op.comp G) : (lanPresheafExt i).hom.app S = CategoryTheory.Limits.colimMap ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op S).whiskerLeft i.hom)

@[simp]

theorem Condensed.lanPresheafExt_inv {F G : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (S : Profiniteᵒᵖ) (i : FintypeCat.toProfinite.op.comp F ≅ FintypeCat.toProfinite.op.comp G) : (lanPresheafExt i).inv.app S = CategoryTheory.Limits.colimMap ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op S).whiskerLeft i.inv)

instance Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp {S : Profinite} : (Profinite.Extend.functorOp S.asLimitCone).Final

noncomputable def Condensed.lanPresheafIso {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : (lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S)

A presheaf, which takes a profinite set written as a cofiltered limit to the corresponding colimit, agrees with the left Kan extension of its restriction.

@[simp]

theorem Condensed.lanPresheafIso_hom {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : (lanPresheafIso hF).hom = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op S)).comp (FintypeCat.toProfinite.op.comp F)) (Profinite.Extend.cocone F S)

noncomputable def Condensed.lanPresheafNatIso {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : lanPresheaf F ≅ F

lanPresheafIso is natural in S.

@[simp]

theorem Condensed.lanPresheafNatIso_hom_app {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) (S : Profiniteᵒᵖ) : (lanPresheafNatIso hF).hom.app S = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op (Opposite.unop S))).comp (FintypeCat.toProfinite.op.comp F)) (Profinite.Extend.cocone F (Opposite.unop S))

noncomputable def Condensed.lanSheafProfinite (X : Type (u + 1)) : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) (Type (u + 1))

lanPresheaf (locallyConstantPresheaf X) is a sheaf for the coherent topology on Profinite.

noncomputable def Condensed.lanCondensedSet (X : Type (u + 1)) : CondensedSet

lanPresheaf (locallyConstantPresheaf X) as a condensed set.

def Condensed.finYoneda (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) : CategoryTheory.Functor FintypeCatᵒᵖ (Type (u + 1))

The functor which takes a finite set to the set of maps into F(*) for a presheaf F on Profinite.

@[simp]

theorem Condensed.finYoneda_obj (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) (X : FintypeCatᵒᵖ) : (finYoneda F).obj X = ((Opposite.unop X).obj → F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))

@[simp]

theorem Condensed.finYoneda_map (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) {X✝ Y✝ : FintypeCatᵒᵖ} (f : X✝ ⟶ Y✝) (g : (Opposite.unop X✝).obj → F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1})))) (a✝ : (Opposite.unop Y✝).obj) : (finYoneda F).map f g a✝ = (g ∘ ⇑(CategoryTheory.ConcreteCategory.hom f.unop)) a✝

def Condensed.locallyConstantIsoFinYoneda (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) : FintypeCat.toProfinite.op.comp (locallyConstantPresheaf (F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))) ≅ finYoneda F

locallyConstantPresheaf restricted to finite sets is isomorphic to finYoneda F.

@[simp]

theorem Condensed.locallyConstantIsoFinYoneda_hom_app (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) (X : FintypeCatᵒᵖ) (a✝ : (FintypeCat.toProfinite.op.comp (locallyConstantPresheaf (F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1})))))).obj X) : (locallyConstantIsoFinYoneda F).hom.app X a✝ = ⇑a✝

def Condensed.fintypeCatAsCofan (X : Profinite) : CategoryTheory.Limits.Cofan fun (x : ↑X.toTop) => Profinite.of PUnit.{u + 1}

A finite set as a coproduct cocone in Profinite over itself.

def Condensed.fintypeCatAsCofanIsColimit (X : Profinite) [Finite ↑X.toTop] : CategoryTheory.Limits.IsColimit (fintypeCatAsCofan X)

A finite set is the coproduct of its points in Profinite.

instance Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Finite ↑X.toTop] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ↑X.toTop) F

noncomputable def Condensed.isoFinYonedaComponents (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Finite ↑X.toTop] : F.obj (Opposite.op X) ≅ ↑X.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))

Auxiliary definition for isoFinYoneda.

theorem Condensed.isoFinYonedaComponents_hom_apply (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Finite ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop) : (isoFinYonedaComponents F X).hom y x = F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op y

theorem Condensed.isoFinYonedaComponents_inv_comp (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] {X Y : Profinite} [Finite ↑X.toTop] [Finite ↑Y.toTop] (f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) (g : X ⟶ Y) : (isoFinYonedaComponents F X).inv (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom g)) = F.map g.op ((isoFinYonedaComponents F Y).inv f)

noncomputable def Condensed.isoFinYoneda (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] : FintypeCat.toProfinite.op.comp F ≅ finYoneda F

The restriction of a finite-product-preserving presheaf F on Profinite to the category of finite sets is isomorphic to finYoneda F.

@[simp]

theorem Condensed.isoFinYoneda_hom_app (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (FintypeCat.toProfinite.op.comp F).obj X) : (isoFinYoneda F).hom.app X a✝ = (isoFinYonedaComponents F (FintypeCat.toProfinite.obj (Opposite.unop X))).hom a✝

@[simp]

theorem Condensed.isoFinYoneda_inv_app (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (finYoneda F).obj X) : (isoFinYoneda F).inv.app X a✝ = (isoFinYonedaComponents F (FintypeCat.toProfinite.obj (Opposite.unop X))).inv a✝

noncomputable def Condensed.isoLocallyConstantOfIsColimit (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : F ≅ locallyConstantPresheaf (F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))

A presheaf F, which takes a profinite set written as a cofiltered limit to the corresponding colimit, is isomorphic to the presheaf LocallyConstant - F(*).

theorem Condensed.isoLocallyConstantOfIsColimit_inv (X : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts X] (hX : (S : Profinite) → CategoryTheory.Limits.IsColimit (X.mapCocone S.asLimitCone.op)) : (isoLocallyConstantOfIsColimit X hX).inv = CompHausLike.LocallyConstant.counitApp X

@[reducible, inline]

abbrev LightCondensed.locallyConstantPresheaf (X : Type u) : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)

The presheaf on LightProfinite of locally constant functions to X.

noncomputable def LightCondensed.isColimitLocallyConstantPresheaf {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (X : Type u) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] : CategoryTheory.Limits.IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

The functor locallyConstantPresheaf takes sequential limits of finite sets with surjective projection maps to colimits.

@[simp]

theorem LightCondensed.isColimitLocallyConstantPresheaf_desc_apply {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (X : Type u) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toLightProfinite).op.comp (locallyConstantPresheaf X))) (n : ℕᵒᵖ) (f : LocallyConstant (↑(FintypeCat.toLightProfinite.obj (F.obj n)).toTop) X) : (isColimitLocallyConstantPresheaf c X hc).desc s (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n).hom) f) = s.ι.app (Opposite.op n) f

noncomputable def LightCondensed.isColimitLocallyConstantPresheafDiagram (X : Type u) (S : LightProfinite) : CategoryTheory.Limits.IsColimit ((locallyConstantPresheaf X).mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))

isColimitLocallyConstantPresheaf in the case of S.asLimit.

@[simp]

theorem LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply (X : Type u) (S : LightProfinite) (s : CategoryTheory.Limits.Cocone (S.diagram.rightOp.comp (locallyConstantPresheaf X))) (n : ℕ) (f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X) : (isColimitLocallyConstantPresheafDiagram X S).desc s (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n)).hom) f) = s.ι.app n f

instance LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType (S : LightProfiniteᵒᵖ) : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.CostructuredArrow FintypeCat.toLightProfinite.op S) (Type u)

@[reducible, inline]

noncomputable abbrev LightCondensed.lanPresheaf (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)

Given a presheaf F on LightProfinite, lanPresheaf F is the left Kan extension of its restriction to finite sets along the inclusion functor of finite sets into Profinite.

noncomputable def LightCondensed.lanPresheafExt {F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (i : FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G) : lanPresheaf F ≅ lanPresheaf G

To presheaves on LightProfinite whose restrictions to finite sets are isomorphic have isomorphic left Kan extensions.

@[simp]

theorem LightCondensed.lanPresheafExt_hom {F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (S : LightProfiniteᵒᵖ) (i : FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G) : (lanPresheafExt i).hom.app S = CategoryTheory.Limits.colimMap ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op S).whiskerLeft i.hom)

@[simp]

theorem LightCondensed.lanPresheafExt_inv {F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (S : LightProfiniteᵒᵖ) (i : FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G) : (lanPresheafExt i).inv.app S = CategoryTheory.Limits.colimMap ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op S).whiskerLeft i.inv)

instance LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp {S : LightProfinite} : (LightProfinite.Extend.functorOp S.asLimitCone).Final

noncomputable def LightCondensed.lanPresheafIso {S : LightProfinite} {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : (lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S)

A presheaf, which takes a light profinite set written as a sequential limit to the corresponding colimit, agrees with the left Kan extension of its restriction.

@[simp]

theorem LightCondensed.lanPresheafIso_hom {S : LightProfinite} {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : (lanPresheafIso hF).hom = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op S)).comp (FintypeCat.toLightProfinite.op.comp F)) (LightProfinite.Extend.cocone F S)

noncomputable def LightCondensed.lanPresheafNatIso {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : lanPresheaf F ≅ F

lanPresheafIso is natural in S.

@[simp]

theorem LightCondensed.lanPresheafNatIso_hom_app {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) (S : LightProfiniteᵒᵖ) : (lanPresheafNatIso hF).hom.app S = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op (Opposite.unop S))).comp (FintypeCat.toLightProfinite.op.comp F)) (LightProfinite.Extend.cocone F (Opposite.unop S))

noncomputable def LightCondensed.lanLightCondSet (X : Type u) : LightCondSet

lanPresheaf (locallyConstantPresheaf X) as a light condensed set.

def LightCondensed.finYoneda (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) : CategoryTheory.Functor FintypeCatᵒᵖ (Type u)

The functor which takes a finite set to the set of maps into F(*) for a presheaf F on LightProfinite.

@[simp]

theorem LightCondensed.finYoneda_obj (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) (X : FintypeCatᵒᵖ) : (finYoneda F).obj X = ((Opposite.unop X).obj → F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))

@[simp]

theorem LightCondensed.finYoneda_map (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) {X✝ Y✝ : FintypeCatᵒᵖ} (f : X✝ ⟶ Y✝) (g : (Opposite.unop X✝).obj → F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1})))) (a✝ : (Opposite.unop Y✝).obj) : (finYoneda F).map f g a✝ = (g ∘ ⇑(CategoryTheory.ConcreteCategory.hom f.unop)) a✝

def LightCondensed.locallyConstantIsoFinYoneda (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) : FintypeCat.toLightProfinite.op.comp (locallyConstantPresheaf (F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))) ≅ finYoneda F

locallyConstantPresheaf restricted to finite sets is isomorphic to finYoneda F.

def LightCondensed.fintypeCatAsCofan (X : LightProfinite) : CategoryTheory.Limits.Cofan fun (x : ↑X.toTop) => LightProfinite.of PUnit.{u + 1}

A finite set as a coproduct cocone in LightProfinite over itself.

def LightCondensed.fintypeCatAsCofanIsColimit (X : LightProfinite) [Finite ↑X.toTop] : CategoryTheory.Limits.IsColimit (fintypeCatAsCofan X)

A finite set is the coproduct of its points in LightProfinite.

instance LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteObjFinite (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCat) : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete X.obj) F

noncomputable def LightCondensed.isoFinYonedaComponents (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : LightProfinite) [Finite ↑X.toTop] : F.obj (Opposite.op X) ≅ ↑X.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))

Auxiliary definition for isoFinYoneda.

theorem LightCondensed.isoFinYonedaComponents_hom_apply (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : LightProfinite) [Finite ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop) : (isoFinYonedaComponents F X).hom y x = F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op y

theorem LightCondensed.isoFinYonedaComponents_inv_comp (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] {X Y : LightProfinite} [Finite ↑X.toTop] [Finite ↑Y.toTop] (f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) (g : X ⟶ Y) : (isoFinYonedaComponents F X).inv (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom g)) = F.map g.op ((isoFinYonedaComponents F Y).inv f)

noncomputable def LightCondensed.isoFinYoneda (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] : FintypeCat.toLightProfinite.op.comp F ≅ finYoneda F

The restriction of a finite-product-preserving presheaf F on Profinite to the category of finite sets is isomorphic to finYoneda F.

@[simp]

theorem LightCondensed.isoFinYoneda_hom_app (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (FintypeCat.toLightProfinite.op.comp F).obj X) : (isoFinYoneda F).hom.app X a✝ = (isoFinYonedaComponents F (FintypeCat.toLightProfinite.obj (Opposite.unop X))).hom a✝

@[simp]

theorem LightCondensed.isoFinYoneda_inv_app (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (finYoneda F).obj X) : (isoFinYoneda F).inv.app X a✝ = (isoFinYonedaComponents F (FintypeCat.toLightProfinite.obj (Opposite.unop X))).inv a✝

noncomputable def LightCondensed.isoLocallyConstantOfIsColimit (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : F ≅ locallyConstantPresheaf (F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))

A presheaf F, which takes a light profinite set written as a sequential limit to the corresponding colimit, is isomorphic to the presheaf LocallyConstant - F(*).

theorem LightCondensed.isoLocallyConstantOfIsColimit_inv (X : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts X] (hX : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (X.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : (isoLocallyConstantOfIsColimit X hX).inv = CompHausLike.LocallyConstant.counitApp X