English
There is a compatibility between N₂ and N₁ under Karoubi constructions: N₂ composed with the Karoubi chain-complex equivalence aligns with embedding and the N₁–Γ₂ composition, yielding a commutative diagram of functors.
Русский
Существует совместимость между N₂ и N₁ в рамках каруоби-конструкций: композиция N₂ с эквивалентностью каруоби-последовательности согласуется с включением и композицией N₁–Γ₂, образуя коммутативную диаграмму функторов.
LaTeX
$$$N_2 \circ (karoubiChainComplexEquivalence C \; Nat).functor = (karoubiFunctorCategoryEmbedding (Opposite SimplexCategory) C) \circ N_1 \circ (karoubiChainComplexEquivalence (Karoubi C) \; \mathbb{N}).functor \circ \mathrm{Functor.mapHomologicalComplex} (\mathrm{KaroubiKaroubi.equivalence C).inverse}$$$
Lean4
theorem compatibility_N₂_N₁_karoubi :
N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor =
karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
N₁ ⋙
(karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse _ :=
by
refine CategoryTheory.Functor.ext (fun P => ?_) fun P Q f => ?_
· refine HomologicalComplex.ext ?_ ?_
· ext n
· rfl
· dsimp
simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp]
· rintro _ n (rfl : n + 1 = _)
ext
have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n
dsimp [N₂, karoubiChainComplexEquivalence, KaroubiHomologicalComplexEquivalence.Functor.obj] at h ⊢
simp only [assoc, Karoubi.eqToHom_f, eqToHom_refl, comp_id, karoubi_alternatingFaceMapComplex_d, karoubi_PInfty_f,
← HomologicalComplex.Hom.comm_assoc, ← h, app_idem_assoc]
· ext n
dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]
simp only [karoubi_PInfty_f, HomologicalComplex.eqToHom_f, Karoubi.eqToHom_f, assoc, comp_id, PInfty_f_naturality,
app_p_comp, karoubiChainComplexEquivalence_functor_obj_X_p, N₂_obj_p_f, eqToHom_refl, PInfty_f_naturality_assoc,
app_comp_p, PInfty_f_idem_assoc]
