isDiscrete_tfae — Mathlib

English

For a LightCondSet X, seven equivalent statements describe discreteness, matching the corresponding tfae structure with counits and essImage under condensed settings.

Русский

Для LightCondSet X восемь эквивалентных утверждений описывают дискретность, согласуя структуру TFAE в конденсированном окружении.

LaTeX

$$$\\mathrm{TFAE}\\left[ \\mathrm{IsDiscrete}(X), \\mathrm{IsIso}(\\mathrm{LightCondensed.discreteUnderlyingAdj}.counit.app X), \\mathrm{essImage}(\\mathrm{LightCondensed.discrete}, X), \\mathrm{LightCondSet.LocallyConstant.functor.essImage}(X), \\mathrm{IsIso}(\\mathrm{LightCondSet.LocallyConstant.adjunction}.counit.app X), \\forall S, \\mathrm{Nonempty}(\\mathrm{IsColimit}(X.val.mapCocone (coconeRightOpOfCone S.asLimitCone))) \\right]$$$

Lean4

theorem isDiscrete_tfae (X : LightCondSet.{u}) :
    TFAE
      [X.IsDiscrete, IsIso ((LightCondensed.discreteUnderlyingAdj _).counit.app X),
        (LightCondensed.discrete _).essImage X, LightCondSet.LocallyConstant.functor.essImage X,
        IsIso (LightCondSet.LocallyConstant.adjunction.counit.app X),
        ∀ S : LightProfinite.{u}, Nonempty (IsColimit <| X.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 X
  tfae_have 1 ↔ 5 :=
    have : functor.Faithful := inferInstance
    have : functor.Full := inferInstance
    Sheaf.isConstant_iff_isIso_counit_app' _ LightProfinite.isTerminalPUnit adjunction X
  tfae_have 6 → 4 := fun h ↦ mem_locallyConstant_essImage_of_isColimit_mapCocone X (fun S ↦ (h S).some)
  tfae_have 4 → 6 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv ((sheafToPresheaf _ _).mapIso i)
        (LightCondensed.isColimitLocallyConstantPresheafDiagram Y S)⟩
  tfae_finish

Похожие утверждения