sheafificationAdjunction — Mathlib

English

There exists a canonical adjunction between the sheafification functor and the forgetful functor composed with restriction of scalars, under the locally bijective hypothesis.

Русский

Существуют канонические взаимооднозначные функции между оператором шейификации и забыванием с ограничением скалярных, при локально биективном гомоморфизме.

LaTeX

$$$ \text{sheafification}(\alpha) \dashv (\text{forget } R \circ \mathrm{restrictScalars}(\alpha)) $$$

Lean4

/-- Given a locally bijective morphism `α : R₀ ⟶ R.val` where `R₀` is a presheaf of rings
and `R` a sheaf of rings, this is the adjunction
`sheafification.{v} α ⊣ SheafOfModules.forget R ⋙ restrictScalars α`. -/
noncomputable def sheafificationAdjunction : sheafification.{v} α ⊣ SheafOfModules.forget R ⋙ restrictScalars α :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun _ _ ↦ sheafificationHomEquiv α
      homEquiv_naturality_left_symm := fun {P₀ Q₀ N} f g ↦
        by
        apply (SheafOfModules.toSheaf _).map_injective
        rw [Functor.map_comp]
        erw [toSheaf_map_sheafificationHomEquiv_symm, toSheaf_map_sheafificationHomEquiv_symm α g]
        rw [Functor.map_comp]
        apply (CategoryTheory.sheafificationAdjunction J AddCommGrpCat.{v}).homEquiv_naturality_left_symm
      homEquiv_naturality_right := fun {P₀ M N} f g ↦
        by
        apply (toPresheaf _).map_injective
        erw [toPresheaf_map_sheafificationHomEquiv] }

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