hη — Mathlib

English

The compatibility component hη relates the natural isomorphisms in the additive Dold-Kan correspondence.

Русский

Совместимость hη связывает естественные изоморфизмы в аддитивном соответствие Dold-Kan.

LaTeX

$$$$ h\\eta : \\mathsf{Compatibility.} \\tau_0 = \\mathsf{Compatibility.}\\tau_1(\\text{isoN}_1, \\text{isoΓ}_0, (N_1Γ_0)) $$$$

Lean4

/-- The natural isomorphism `NΓ' satisfies the compatibility that is needed
for the construction of our counit isomorphism `η` -/
theorem hη :
    Compatibility.τ₀ =
      Compatibility.τ₁ isoN₁ isoΓ₀ (N₁Γ₀ : Γ ⋙ N₁ ≅ (toKaroubiEquivalence (ChainComplex C ℕ)).functor) :=
  by
  ext K : 3
  simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app]
  exact (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp)

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