N₁Γ₀_hom_app — Mathlib

English

There is a natural equality of whiskered functors relating N₂Γ₂.hom and N₁Γ₀.hom via an appropriate Karoubi whiskering on the left.

Русский

Существует естественное равенство между функторной операцией whiskerLeft, связывающей N₂Γ₂.hom и N₁Γ₀.hom через лево-Whiskering в Karoubi.

LaTeX

$$$\mathrm{whiskerLeft}(\mathrm{toKaroubi}(\mathrm{ChainComplex}\,C\,\mathbb{N}))\; N_2\Gamma_2\; = \; N_2\Gamma_2^{\mathrm{ToKaroubiIso}}.hom \circ N_1\Gamma_0.hom$$$

Lean4

theorem N₁Γ₀_hom_app (K : ChainComplex C ℕ) :
    N₁Γ₀.hom.app K = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi _).map (Γ₀NondegComplexIso K).hom :=
  by
  change (N₁Γ₀.app K).hom = _
  simp only [N₁Γ₀_app]
  rfl

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