cohomologyPresheaf — Mathlib

English

The presheaf cohomologyPresheaf is defined as the previous functor applied to F, i.e., cohomologyPresheaf(n) = (cohomologyPresheafFunctor(n)).obj F.

Русский

Когомологическая пресейф-объект определяется как применение предыдущего функторa: cohomologyPresheaf(n) = (cohomologyPresheafFunctor(n)).obj F.

LaTeX

$$$\text{cohomologyPresheaf}(F, n) = (\text{cohomologyPresheafFunctor}(n)).\text{obj} F$$$

Lean4

/-- Given an abelian sheaf `F`, this is the presheaf which sends `U`
to the `n`th Ext-group from the free abelian sheaf generated by the
presheaf of sets `yoneda.obj U` to `F`. -/
noncomputable abbrev cohomologyPresheaf (F : Sheaf J AddCommGrpCat.{v}) (n : ℕ) : Cᵒᵖ ⥤ AddCommGrpCat.{w'} :=
  (cohomologyPresheafFunctor J n).obj F

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