N₁Γ₀_app — Mathlib

English

The f-component of the homomorphism part of the isomorphism N₂Γ₂ToKaroubiIso, applied to a chain complex X, equals PInfty.

Русский

Компонента f отображения гомоморфизма из изоморфизма N₂Γ₂ToKaroubiIso равна PInfty.

LaTeX

$$$\big( N_2\Gamma_2^{\mathrm{ToKaroubiIso}}.hom\big).app X.f = PInfty$$$

Lean4

theorem N₁Γ₀_app (K : ChainComplex C ℕ) :
    N₁Γ₀.app K = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫ (toKaroubi _).mapIso (Γ₀NondegComplexIso K) :=
  by
  ext1
  dsimp [N₁Γ₀]
  erw [id_comp, comp_id, comp_id]
  rfl

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