isConstant_iff_isIso_counit_app' — Mathlib

English

For a general left adjoint to evaluation at a terminal object, F is constant if and only if the corresponding counit at F is an isomorphism.

Русский

Для общего левого сопоставителя к вычислению в терминальном объекте, F константен тогда и только тогда, когда соответствующий counit на F является изоморфизмом.

LaTeX

$$$\mathrm{IsConstant}(J,F) \;\iff\; \mathrm{IsIso}\big(adj.\text{counit.app }F\big)$$$

Lean4

/-- A variant of `isConstant_iff_isIso_counit_app` for a general left adjoint to evaluation at a
terminal object.
-/
theorem isConstant_iff_isIso_counit_app' {L : D ⥤ Sheaf J D} {T : C} (hT : IsTerminal T)
    (adj : L ⊣ (sheafSections J D).obj ⟨T⟩) [L.Faithful] [L.Full] (F : Sheaf J D) :
    IsConstant J F ↔ IsIso (adj.counit.app F) :=
  (isConstant_iff_mem_essImage J hT adj F).trans (isIso_counit_app_iff_mem_essImage adj).symm

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