mk₀_comp_mk₀_assoc — Mathlib

English

For any Ext object α: Ext Z T n and morphisms f: X → Y, g: Y → Z, the associativity of mk₀ composition with α holds: (mk₀ f) . ( (mk₀ g) . α ) = mk₀ (f ≫ g) . α.

Русский

Для расширения α: Ext Z T n и стрелок f: X → Y, g: Y → Z выполняется ассоциативность композиции mk₀: (mk₀ f) · ((mk₀ g) · α) = mk₀ (f ≫ g) · α.

LaTeX

$$$ (mk_0 f).\\mathrm{comp}((mk_0 g).\\mathrm{comp} \\alpha) = (mk_0 (f\\gg g)).\\mathrm{comp} \\alpha $$$

Lean4

@[simp]
theorem mk₀_comp_mk₀_assoc (f : X ⟶ Y) (g : Y ⟶ Z) {n : ℕ} (α : Ext Z T n) :
    (mk₀ f).comp ((mk₀ g).comp α (zero_add n)) (zero_add n) = (mk₀ (f ≫ g)).comp α (zero_add n) :=
  by
  rw [← mk₀_comp_mk₀, comp_assoc]
  cutsat

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