English
For each n, Ext^n is assembled into a bifunctor Ext^n: C^op × C → AddCommGrpCat, natural in both variables and compatible with composition.
Русский
Для каждого n расширение образуется в двуфунктор Ext^n: C^op × C → AddCommGrpCat, натурализованный по обеим переменным и совместимый с композициями.
LaTeX
$$$\Ext^n: \mathbf{C}^{op} \times \mathbf{C} \to AddCommGrpCat$$$
Lean4
/-- The functor `Cᵒᵖ ⥤ C ⥤ AddCommGrpCat` which sends `X : C` and `Y : C`
to `Ext X Y n`. -/
@[simps]
noncomputable def extFunctor (n : ℕ) : Cᵒᵖ ⥤ C ⥤ AddCommGrpCat.{w}
where
obj X := extFunctorObj X.unop n
map {X₁ X₂}
f :=
{ app := fun Y ↦ AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α (zero_add _)) (by simp))
naturality := fun {Y₁ Y₂} g ↦ by
ext α
dsimp
symm
apply Ext.comp_assoc
all_goals omega }
map_comp {X₁ X₂ X₃} f
f' := by
ext Y α
simp
