unitIso — Mathlib

English

The LocallyConstant functor is left adjoint to the forgetful functor into Sheaf over coherent topology, with unit and counit defined by LocallyConstant structures.

Русский

Локально‑константный функтор является левым сопряжённым к забывающему функтору в категорию Sheaf над когерентной топологией; единица и counit заданы структурами LocallyConstant.

LaTeX

$$LocallyConstant.functor ⊣ forgetful functor with unit and counit given by unit P hs and counit P hs$$

Lean4

/-- The unit of the adjunction is an iso. -/
noncomputable def unitIso :
    𝟭 (Type max u w) ≅ functor.{u, w} P hs ⋙ (sheafSections _ _).obj ⟨CompHausLike.of P PUnit.{u + 1}⟩
    where
  hom := unit P hs
  inv := { app := fun _ f ↦ f.toFun PUnit.unit }

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