map_comp — Mathlib

English

For a morphism f: F ⟶ G and z: G ⟶ K of degree n, δ(n,m)((Cochain.ofHom f).comp z) equals ((Cochain.ofHom f).comp (δ(n,m) z)).

Русский

Для морфизма f: F ⟶ G и z: G ⟶ K степени n, δ(n,m)((Cochain.ofHom f).comp z) = (Cochain.ofHom f).comp (δ(n,m) z).

LaTeX

$$$\\delta(n,m)((\\mathrm{Cochain.ofHom}(f).\\circ z)) = (\\mathrm{Cochain.ofHom}(f).\\circ (\\delta(n,m) z)).$$$

Lean4

@[simp]
theorem map_comp {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (Φ : C ⥤ D)
    [Φ.Additive] : (Cochain.comp z₁ z₂ h).map Φ = Cochain.comp (z₁.map Φ) (z₂.map Φ) h :=
  by
  ext p q hpq
  dsimp
  simp only [map_v, comp_v _ _ h p _ q rfl (by cutsat), Φ.map_comp]

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