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.

Equations

• Condensed.locallyConstantPresheaf X = CompHausLike.LocallyConstant.functorToPresheaves.obj 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 ((Condensed.locallyConstantPresheaf X).mapCocone c.op)

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

Equations

• One or more equations did not get rendered due to their size.

@[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 (Condensed.locallyConstantPresheaf X))) (i : I) (f : LocallyConstant (↑(FintypeCat.toProfinite.obj (F.obj i)).toTop) X) : (Condensed.isColimitLocallyConstantPresheaf c X hc).desc s (LocallyConstant.comap (c.π.app i) f) = s.ι.app (Opposite.op i) f

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

isColimitLocallyConstantPresheaf in the case of S.asLimit.

Equations

• Condensed.isColimitLocallyConstantPresheafDiagram X S = Condensed.isColimitLocallyConstantPresheaf S.asLimitCone X S.asLimit

@[simp]

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

@[reducible, inline]

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.

Equations

• Condensed.lanPresheaf F = FintypeCat.toProfinite.op.pointwiseLeftKanExtension (FintypeCat.toProfinite.op.comp F)

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

instance Condensed.instFinalOppositeDiscreteQuotientαTopologicalSpaceToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp {S : Profinite} : (Profinite.Extend.functorOp S.asLimitCone).Final

Equations

• ⋯ = ⋯

def Condensed.lanPresheafIso {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : (Condensed.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Condensed.lanPresheafIso_hom {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : (Condensed.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)

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

lanPresheafIso is natural in S.

Equations

• Condensed.lanPresheafNatIso hF = CategoryTheory.NatIso.ofComponents (fun (x : Profiniteᵒᵖ) => match x with | Opposite.op S => Condensed.lanPresheafIso (hF 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ᵒᵖ) : (Condensed.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))

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.

Equations

• Condensed.lanSheafProfinite X = { val := Condensed.lanPresheaf (Condensed.locallyConstantPresheaf X), cond := ⋯ }

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

lanPresheaf (locallyConstantPresheaf X) as a condensed set.

Equations

• Condensed.lanCondensedSet X = (Condensed.ProfiniteCompHaus.equivalence (Type (?u.11 + 1))).functor.obj (Condensed.lanSheafProfinite X)

@[simp]

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

@[simp]

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

locallyConstantPresheaf restricted to finite sets is isomorphic to finYoneda F.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Condensed.fintypeCatAsCofan X = CategoryTheory.Limits.Cofan.mk X fun (x : ↑X.toTop) => ContinuousMap.const (↑(Profinite.of PUnit.{?u.24 + 1} ).toTop) x

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

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteαTopologicalSpaceToTopTotallyDisconnectedSpaceOfFintype (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Fintype ↑X.toTop] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ↑X.toTop) F

Equations

• One or more equations did not get rendered due to their size.

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

Auxiliary definition for isoFinYoneda.

Equations

• One or more equations did not get rendered due to their size.

theorem Condensed.isoFinYonedaComponents_hom_apply (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Fintype ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop) : (Condensed.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 : Profinite} {Y : Profinite} [Fintype ↑X.toTop] [Fintype ↑Y.toTop] (f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1} ))) (g : X ⟶ Y) : (Condensed.isoFinYonedaComponents F X).inv (f ∘ ⇑g) = F.map g.op ((Condensed.isoFinYonedaComponents F Y).inv f)

@[simp]

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

@[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), (Condensed.isoFinYoneda F).hom.app X a = (Condensed.isoFinYonedaComponents F (FintypeCat.toProfinite.obj (Opposite.unop X))).hom a

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

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

Equations

• Condensed.isoFinYoneda F = CategoryTheory.NatIso.ofComponents (fun (X : FintypeCatᵒᵖ) => Condensed.isoFinYonedaComponents F (FintypeCat.toProfinite.obj (Opposite.unop X))) ⋯

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 ≅ Condensed.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(*).

Equations

• One or more equations did not get rendered due to their size.

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)) : (Condensed.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.

Equations

• LightCondensed.locallyConstantPresheaf X = CompHausLike.LocallyConstant.functorToPresheaves.obj 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 ((LightCondensed.locallyConstantPresheaf X).mapCocone c.op)

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

Equations

• One or more equations did not get rendered due to their size.

@[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 (LightCondensed.locallyConstantPresheaf X))) (n : ℕᵒᵖ) (f : LocallyConstant (↑(FintypeCat.toLightProfinite.obj (F.obj n)).toTop) X) : (LightCondensed.isColimitLocallyConstantPresheaf c X hc).desc s (LocallyConstant.comap (c.π.app n) f) = s.ι.app (Opposite.op n) f

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

isColimitLocallyConstantPresheaf in the case of S.asLimit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• ⋯ = ⋯

@[reducible, inline]

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.

Equations

• LightCondensed.lanPresheaf F = FintypeCat.toLightProfinite.op.pointwiseLeftKanExtension (FintypeCat.toLightProfinite.op.comp F)

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

def LightCondensed.lanPresheafIso {S : LightProfinite} {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : (LightCondensed.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LightCondensed.lanPresheafIso_hom {S : LightProfinite} {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : (LightCondensed.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)

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

lanPresheafIso is natural in S.

Equations

• LightCondensed.lanPresheafNatIso hF = CategoryTheory.NatIso.ofComponents (fun (x : LightProfiniteᵒᵖ) => match x with | Opposite.op S => LightCondensed.lanPresheafIso (hF 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ᵒᵖ) : (LightCondensed.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))

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

lanPresheaf (locallyConstantPresheaf X) as a light condensed set.

Equations

• LightCondensed.lanLightCondSet X = { val := LightCondensed.lanPresheaf (LightCondensed.locallyConstantPresheaf X), cond := ⋯ }

@[simp]

theorem LightCondensed.finYoneda_obj (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) (X : FintypeCatᵒᵖ) : (LightCondensed.finYoneda F).obj X = (↑(Opposite.unop X) → 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) → F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1} )))) (a : ↑(Opposite.unop Y)), (LightCondensed.finYoneda F).map f g a = (g ∘ f.unop) a

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.

Equations

• One or more equations did not get rendered due to their size.

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

locallyConstantPresheaf restricted to finite sets is isomorphic to finYoneda F.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• LightCondensed.fintypeCatAsCofan X = CategoryTheory.Limits.Cofan.mk X fun (x : ↑X.toTop) => ContinuousMap.const (↑(LightProfinite.of PUnit.{?u.13 + 1} ).toTop) x

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

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteαFintype (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCat) : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ↑X) F

Equations

• LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteαFintype F X = CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv (CategoryTheory.Discrete.equivalence ⋯.some.symm) F

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

Auxiliary definition for isoFinYoneda.

Equations

• One or more equations did not get rendered due to their size.

theorem LightCondensed.isoFinYonedaComponents_hom_apply (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : LightProfinite) [Fintype ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop) : (LightCondensed.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 : LightProfinite} {Y : LightProfinite} [Fintype ↑X.toTop] [Fintype ↑Y.toTop] (f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1} ))) (g : X ⟶ Y) : (LightCondensed.isoFinYonedaComponents F X).inv (f ∘ ⇑g) = F.map g.op ((LightCondensed.isoFinYonedaComponents F Y).inv f)

@[simp]

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

@[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), (LightCondensed.isoFinYoneda F).hom.app X a = (LightCondensed.isoFinYonedaComponents F (FintypeCat.toLightProfinite.obj (Opposite.unop X))).hom a

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

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

Equations

• One or more equations did not get rendered due to their size.

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 ≅ LightCondensed.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(*).

Equations

• One or more equations did not get rendered due to their size.

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))) : (LightCondensed.isoLocallyConstantOfIsColimit X hX).inv = CompHausLike.LocallyConstant.counitApp X