English
A tfae chain for LightCondMod_R expresses equivalences among discreteness, counit_is_iso, essImage, LocallyConstant essImage, adjunction counit_iso, and a Profinite-colimit condition.
Русский
Для LightCondMod_R цепь TFAE выражает эквивалентности между дискретностью, изоморфией counit, essImage, essImageLocallyConstant, adjunction counit, и условием колимита по Profinite.
LaTeX
$$$\\mathrm{TFAE}\\left[ \\mathrm{IsDiscrete}(M), \\mathrm{IsIso}(\\mathrm{LightCondensed.discreteUnderlyingAdj}.counit.app M), \\mathrm{essImage}(\\mathrm{discrete}, M), \\mathrm{LightCondMod.LocallyConstant.functor.essImage}(M), \\mathrm{IsIso}(\\mathrm{LightCondMod.LocallyConstant.adjunction}.counit.app M), \\forall S, \\mathrm{Nonempty}(\\mathrm{IsColimit}(M.val.mapCocone (coconeRightOpOfCone S.asLimitCone))) \\right]$$$
Lean4
theorem isDiscrete_tfae (M : LightCondMod.{u} R) :
TFAE
[M.IsDiscrete, IsIso ((LightCondensed.discreteUnderlyingAdj _).counit.app M),
(LightCondensed.discrete _).essImage M, (LightCondMod.LocallyConstant.functor R).essImage M,
IsIso ((LightCondMod.LocallyConstant.adjunction R).counit.app M),
∀ S : LightProfinite.{u}, Nonempty (IsColimit <| M.val.mapCocone (coconeRightOpOfCone S.asLimitCone))] :=
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 _ LightProfinite.isTerminalPUnit (adjunction R) _
tfae_have 1 ↔ 5 :=
have : (functor R).Faithful := inferInstance
have : (functor R).Full := inferInstance
Sheaf.isConstant_iff_isIso_counit_app' _ LightProfinite.isTerminalPUnit (adjunction R) _
tfae_have 6 → 1 := by
intro h
rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)]
intro S
letI : PreservesFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
preservesFilteredColimitsOfSize_shrink.{0, u, 0, u} _
exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩
tfae_have 1 → 6 := by
intro h S
rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)] at h
letI : ReflectsFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
reflectsFilteredColimitsOfSize_shrink.{0, u, 0, u} _
exact ⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩
tfae_finish
