postcomp — Mathlib

English

Given β in Ext^n(Y,Z) and a,b with a+n=b, postcomposition with β induces a homomorphism Ext^a(X,Y) → Ext^b(X,Z); this map is built from bilinearComp by flipping β.

Русский

Пост-композиция с элементом β ∈ Ext^n(Y,Z) (при условии a+n=b) задаёт гомоморфизм Ext^a(X,Y) → Ext^b(X,Z); этот пример следует из билинейного композиционирования.

LaTeX

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

Lean4

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

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