extFunctorObj — Mathlib

English

For each X in C and n in N, the construction Y ↦ Ext^n(X,Y) defines an additive functor from C to AddCommGrpCat; morphisms act by postcomposition with the morphism in the second variable.

Русский

Для каждого X и числа n функция Y ↦ Ext^n(X,Y) образует добавляющийся функтор из C в AddCommGrpCat; морфизмы действуют посредством посткомпозиции во втором аргументе.

LaTeX

$$$\text{extFunctorObj}(X,n): C \to AddCommGrpCat,\quad Y\mapsto Ext^n(X,Y).$$$

Lean4

/-- Auxiliary definition for `extFunctor`. -/
@[simps]
noncomputable def extFunctorObj (X : C) (n : ℕ) : C ⥤ AddCommGrpCat.{w}
    where
  obj Y := AddCommGrpCat.of (Ext X Y n)
  map f := AddCommGrpCat.ofHom ((Ext.mk₀ f).postcomp _ (add_zero n))
  map_comp f
    f' := by
    ext α
    dsimp [AddCommGrpCat.ofHom]
    rw [← Ext.mk₀_comp_mk₀]
    symm
    apply Ext.comp_assoc
    omega

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