N₁Γ₀_inv_app_f_f — Mathlib

English

The inv-component of the N₁Γ₀.app evaluated at K equals the map obtained by composing the Karoubi preimage with the Γ₀NondegComplexIso inverse.

Русский

Компонента inv в N₁Γ₀.app на K равна композиции предобраза Karoubi с обратной Γ₀NondegComplexIso.

LaTeX

$$$\big( N_1Γ_0\text{ app } K \big).inv = (toKaroubi _).map (Γ_0^{\mathrm{Nondeg}}(K))^{-1} \circ (Γ_0.splitting K)^{\mathrm{toKaroubiNondegComplexIsoN_1}.hom$$$

Lean4

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

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