N₁Γ₀_inv_app — Mathlib

English

The morphism N₂Γ₂.hom aligns with the composition N₂Γ₂ToKaroubiIso.hom.app K ≫ N₁Γ₀.hom.app K for any chain complex K.

Русский

Гомоморфизм N₂Γ₂.hom совместим с композицией N₂Γ₂ToKaroubiIso.hom.app K и N₁Γ₀.hom.app K для любого цепного комплекса K.

LaTeX

$$$N_2Γ_2.hom.app K = N_2Γ_2ToKaroubiIso.hom.app K \; \circ\; N_1Γ_0.hom.app K$$$

Lean4

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

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