functor — Mathlib

English

The counit of the localization adjunction is an isomorphism.

Русский

Единичный морфизм смежности локализации является изоморфизмом.

LaTeX

$$$\operatorname{IsIso}\bigl((\text{counit})\bigr)$$$

Lean4

/-- `CompHausLike.LocallyConstantModule.functorToPresheaves` lands in sheaves. -/
@[simps]
def functor :
    haveI := CompHausLike.preregular hs
    ModuleCat R ⥤ Sheaf (coherentTopology (CompHausLike.{u} P)) (ModuleCat R)
    where
  obj
    X :=
    { val := (functorToPresheaves.{w, u} R).obj X
      cond := by
        have := CompHausLike.preregular hs
        apply Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp (s := CategoryTheory.forget (ModuleCat R))
        exact ((CompHausLike.LocallyConstant.functor P hs).obj _).cond }
  map f := ⟨(functorToPresheaves.{w, u} R).map f⟩

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