instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂

English

The natural functor N₁: SimplicialObject(Karoubi C) ⥤ Karoubi(ChainComplex(Karoubi C)) reflects isomorphisms; i.e., a morphism is an isomorphism whenever its image under N₁ is an isomorphism.

Русский

Натуральный функтор N₁: SimplicialObject(Karoubi C) ⥤ Karoubi(ChainComplex(Karoubi C)) отражает изоморфизмы; то есть морфизм является изоморфизмом тогда и тогда, когда его образ под N₁ является изоморфизмом.

LaTeX

$$$N_1 \;:\; \mathrm{SimplicialObject}(\mathrm{Karoubi}(C)) \to \mathrm{Karoubi}(\mathrm{ChainComplex}(\mathrm{Karoubi}(C), \mathbb{N}))$ reflects isomorphisms$$

Lean4

/-- We deduce that `N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ))`
reflects isomorphisms from the fact that
`N₁ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ)` does. -/
instance : (N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)).ReflectsIsomorphisms :=
  ⟨fun f =>
    by
    intro
      -- The following functor `F` reflects isomorphism because it is
          -- a composition of four functors which reflects isomorphisms.
          -- Then, it suffices to show that `F.map f` is an isomorphism.

    let F₁ := karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
    let F₂ : SimplicialObject (Karoubi C) ⥤ _ := N₁
    let F₃ := (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
    let F₄ := Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse (ComplexShape.down ℕ)
    let F := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
    haveI : F₁.ReflectsIsomorphisms := reflectsIsomorphisms_of_full_and_faithful _
    haveI : F₂.ReflectsIsomorphisms := by infer_instance
    have : IsIso (F.map f) := by
      simp only [F, F₁]
      rw [← compatibility_N₂_N₁_karoubi, Functor.comp_map]
      apply Functor.map_isIso
    exact isIso_of_reflects_iso f F⟩

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