Characterizing discrete condensed sets and R-modules.

This file proves a characterization of discrete condensed sets, discrete condensed R-modules over a ring R, discrete light condensed sets, and discrete light condensed R-modules over a ring R. see CondensedSet.isDiscrete_tfae, CondensedMod.isDiscrete_tfae, LightCondSet.isDiscrete_tfae, and LightCondMod.isDiscrete_tfae.

Informally, we can say: The following conditions characterize a condensed set X as discrete (CondensedSet.isDiscrete_tfae):

1. There exists a set X' and an isomorphism X ≅ cst X', where cst X' denotes the constant sheaf on X'.
2. The counit induces an isomorphism cst X(*) ⟶ X.
3. There exists a set X' and an isomorphism X ≅ LocallyConstant · X'.
4. The counit induces an isomorphism LocallyConstant · X(*) ⟶ X.
5. For every profinite set S = limᵢSᵢ, the canonical map colimᵢX(Sᵢ) ⟶ X(S) is an isomorphism.

The analogues for light condensed sets, condensed R-modules over any ring, and light condensed R-modules are nearly identical (CondensedMod.isDiscrete_tfae, LightCondSet.isDiscrete_tfae, and LightCondMod.isDiscrete_tfae).

@[reducible, inline]

abbrev Condensed.IsDiscrete {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] (X : Condensed C) : Prop

A condensed object is discrete if it is constant as a sheaf, i.e. isomorphic to a constant sheaf.

Equations

• X.IsDiscrete = CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology CompHaus) X

theorem CondensedSet.mem_locallyContant_essImage_of_isColimit_mapCocone (X : CondensedSet) (h : (S : Profinite) → CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.val).mapCocone S.asLimitCone.op)) : X ∈ CondensedSet.LocallyConstant.functor.essImage

@[reducible, inline]

noncomputable abbrev CondensedSet.LocallyConstant.adjunction : CondensedSet.LocallyConstant.functor ⊣ Condensed.underlying (Type (u + 1))

CondensedSet.LocallyConstant.functor is left adjoint to the forgetful functor from condensed sets to sets.

Equations

• CondensedSet.LocallyConstant.adjunction = CompHausLike.LocallyConstant.adjunction (fun (x : TopCat) => True) CondensedSet.LocallyConstant.functor.proof_1

theorem CondensedSet.isDiscrete_tfae (X : CondensedSet) : [Condensed.IsDiscrete X, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (Type (u + 1))).counit.app X), X ∈ (Condensed.discrete (Type (u + 1))).essImage, X ∈ CondensedSet.LocallyConstant.functor.essImage, CategoryTheory.IsIso (CondensedSet.LocallyConstant.adjunction.counit.app X), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.val).mapCocone S.asLimitCone.op))].TFAE

theorem CondensedMod.isDiscrete_iff_isDiscrete_forget (R : Type (u + 1)) [Ring R] (M : CondensedMod R) : Condensed.IsDiscrete M ↔ Condensed.IsDiscrete ((Condensed.forget R).obj M)

instance CondensedMod.instHasLimitsOfSizeModuleCat (R : Type (u + 1)) [Ring R] : CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (ModuleCat R)

theorem CondensedMod.isDiscrete_tfae (R : Type (u + 1)) [Ring R] (M : CondensedMod R) : [Condensed.IsDiscrete M, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), M ∈ (Condensed.discrete (ModuleCat R)).essImage, M ∈ (CondensedMod.LocallyConstant.functor R).essImage, CategoryTheory.IsIso ((CondensedMod.LocallyConstant.adjunction R).counit.app M), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp M.val).mapCocone S.asLimitCone.op))].TFAE

@[reducible, inline]

abbrev LightCondensed.IsDiscrete {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology LightProfinite) C] (X : LightCondensed C) : Prop

A light condensed object is discrete if it is constant as a sheaf, i.e. isomorphic to a constant sheaf.

Equations

• X.IsDiscrete = CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology LightProfinite) X

theorem LightCondSet.mem_locallyContant_essImage_of_isColimit_mapCocone (X : LightCondSet) (h : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (X.val.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : X ∈ LightCondSet.LocallyConstant.functor.essImage

@[reducible, inline]

noncomputable abbrev LightCondSet.LocallyConstant.adjunction : LightCondSet.LocallyConstant.functor ⊣ LightCondensed.underlying (Type u)

LightCondSet.LocallyConstant.functor is left adjoint to the forgetful functor from light condensed sets to sets.

Equations

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

theorem LightCondSet.isDiscrete_tfae (X : LightCondSet) : [LightCondensed.IsDiscrete X, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X), X ∈ (LightCondensed.discrete (Type u)).essImage, X ∈ LightCondSet.LocallyConstant.functor.essImage, CategoryTheory.IsIso (LightCondSet.LocallyConstant.adjunction.counit.app X), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (X.val.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE

theorem LightCondMod.isDiscrete_iff_isDiscrete_forget (R : Type u) [Ring R] (M : LightCondMod R) : LightCondensed.IsDiscrete M ↔ LightCondensed.IsDiscrete ((LightCondensed.forget R).obj M)

theorem LightCondMod.isDiscrete_tfae (R : Type u) [Ring R] (M : LightCondMod R) : [LightCondensed.IsDiscrete M, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), M ∈ (LightCondensed.discrete (ModuleCat R)).essImage, M ∈ (LightCondMod.LocallyConstant.functor R).essImage, CategoryTheory.IsIso ((LightCondMod.LocallyConstant.adjunction R).counit.app M), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (M.val.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE