precomp — Mathlib

English

In the dual situation, precomposition with α ∈ Ext^n(X,Y) defines a map Ext^a(Y,Z) → Ext^b(X,Z) when n+a=b, again arising from bilinearComp.

Русский

В двойственной ситуации прехоу композиция с α ∈ Ext^n(X,Y) задаёт отображение Ext^a(Y,Z) → Ext^b(X,Z) при условии n+a=b, также через билинейную композицию.

LaTeX

$$$\text{precomp}(\alpha:Ext^n(X,Y), Z)\ (h:\ n+a=b): Ext^a(Y,Z) \to^+ Ext^b(X,Z).$$$

Lean4

/-- The precomposition `Ext Y Z a →+ Ext X Z b` with `α : Ext X Y n` when `n + a = b`. -/
noncomputable abbrev precomp (α : Ext X Y n) (Z : C) {a b : ℕ} (h : n + a = b) : Ext Y Z a →+ Ext X Z b :=
  bilinearComp X Y Z n a b h α

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