N₁Γ₀_hom_app_f_f — Mathlib

English

The f-component of the N₁Γ₀.app at level n coincides with the inverse splitting component applied to the f-component of Γ₀NondegComplexIso.

Русский

Компонента f в N₁Γ₀.app на уровне n совпадает с обратной частью разложения, применённой к компоненте f Γ₀NondegComplexIso.

LaTeX

$$$\big( N_1Γ_0\text{ app } K \big).f.f_n = \big( Γ_0.splitting_K \big)^{\,-1}.f.f_n$$$

Lean4

@[simp]
theorem N₁Γ₀_hom_app_f_f (K : ChainComplex C ℕ) (n : ℕ) :
    (N₁Γ₀.hom.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n :=
  by
  rw [N₁Γ₀_hom_app]
  apply comp_id

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