cohomologyPresheafFunctor — Mathlib

English

For fixed n, there is a bifunctor sending an abelian sheaf F and an object U to Ext^n between the free abelian sheaf generated by Yoneda(U) and F.

Русский

Для фиксированного n существует бифунктор, отправляющий абелеву шапку F и объект U в Ext^n между свободной абелевой шапкой, порождённой Yoneda(U), и F.

LaTeX

$$$\operatorname{cohomologyPresheafFunctor}(n)(F)(U) = \operatorname{Ext}^n\big(\mathrm{Free}(\mathrm{yoneda}(U)), F\big)$$$

Lean4

/-- The bifunctor which sends an abelian sheaf `F` and an object `U` to the
`n`th Ext-group from the free abelian sheaf generated by the
presheaf of sets `yoneda.obj U` to `F`. -/
noncomputable def cohomologyPresheafFunctor (n : ℕ) : Sheaf J AddCommGrpCat.{v} ⥤ Cᵒᵖ ⥤ AddCommGrpCat.{w'} :=
  Functor.flip
    (Functor.op (yoneda ⋙ (Functor.whiskeringRight _ _ _).obj AddCommGrpCat.free ⋙ presheafToSheaf _ _) ⋙ extFunctor n)

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