comp_assoc — Mathlib

English

Associativity of Ext composition: (α ∘ β) ∘ γ = α ∘ (β ∘ γ) under appropriate degree matches.

Русский

Ассоциативность композиции Ext: (α ∘ β) ∘ γ = α ∘ (β ∘ γ) при корректных степенях.

LaTeX

$$$\alpha\comp\beta(h_{12})\comp\gamma = \alpha\comp(\beta\comp\gamma(h_{23}))$$$

Lean4

theorem comp_assoc {a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ} (α : Ext X Y a₁) (β : Ext Y Z a₂) (γ : Ext Z T a₃) (h₁₂ : a₁ + a₂ = a₁₂)
    (h₂₃ : a₂ + a₃ = a₂₃) (h : a₁ + a₂ + a₃ = a) :
    (α.comp β h₁₂).comp γ (show a₁₂ + a₃ = a by cutsat) = α.comp (β.comp γ h₂₃) (by cutsat) :=
  SmallShiftedHom.comp_assoc _ _ _ _ _ _ (by cutsat)

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