English
Analogous six-term equivalence for CondensedMod R: the discrete properties, counit iso, essImage, LocallyConstant essImage, adjunction counit iso, and a colimit condition across Profinite.
Русский
Аналогично шестиусловная эквивалентность для CondensedMod R: дискретность, изоморфность counit, essImage, LocallyConstant essImage, counit adjunction, и условие колимита для Profinite.
LaTeX
$$$\\mathrm{TFAE}\\left[ \\mathrm{IsDiscrete}(M), \\mathrm{IsIso}(\\mathrm{Condensed.discreteUnderlyingAdj}.counit.app M), \\mathrm{essImage}(\\mathrm{discrete}, M), \\mathrm{LocallyConstant.essImage}(M), \\mathrm{IsIso}(\\mathrm{LocallyConstant.adjunction}.counit.app M), \\forall S, \\mathrm{Nonempty}(\\mathrm{IsColimit}( (profiniteToCompHaus.op \\circ M.val).mapCocone S.asLimitCone.op)) \\right]$$$
Lean4
theorem isDiscrete_tfae (M : CondensedMod.{u} R) :
TFAE
[M.IsDiscrete, IsIso ((Condensed.discreteUnderlyingAdj _).counit.app M), (Condensed.discrete _).essImage M,
(CondensedMod.LocallyConstant.functor R).essImage M,
IsIso ((CondensedMod.LocallyConstant.adjunction R).counit.app M),
Sheaf.IsConstant (coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence _).inverse.obj M),
∀ S : Profinite.{u}, Nonempty (IsColimit <| (profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op)] :=
by
tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ CompHaus.isTerminalPUnit (adjunction R) _
tfae_have 1 ↔ 5 :=
have : (functor R).Faithful := inferInstance
have : (functor R).Full := inferInstance
Sheaf.isConstant_iff_isIso_counit_app' _ CompHaus.isTerminalPUnit (adjunction R) _
tfae_have 1 ↔ 6 :=
(Sheaf.isConstant_iff_of_equivalence (coherentTopology Profinite) (coherentTopology CompHaus) profiniteToCompHaus
Profinite.isTerminalPUnit CompHaus.isTerminalPUnit _).symm
tfae_have 7 → 1 := by
intro h
rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)]
intro S
letI : PreservesFilteredColimitsOfSize.{u, u} (forget (ModuleCat R)) :=
preservesFilteredColimitsOfSize_shrink.{u, u + 1, u, u + 1} _
exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩
tfae_have 1 → 7 := by
intro h S
rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)] at h
letI : ReflectsFilteredColimitsOfSize.{u, u} (forget (ModuleCat R)) :=
reflectsFilteredColimitsOfSize_shrink.{u, u + 1, u, u + 1} _
exact ⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩
tfae_finish
