mapHomologicalComplex_reflects_iso

English

If F reflects isomorphisms, then F.mapHomologicalComplex c also reflects isomorphisms.

Русский

Если F отражает изоморфизмы, то F.mapHomologicalComplex c тоже отражает изоморфизмы.

LaTeX

$$$\text{instance } mapHomologicalComplex_reflects_iso (F : W_{1} \to W_{2}) [F.PreservesZeroMorphisms] [F.ReflectsIsomorphisms] (c : ComplexShape ι) :\; ReflectsIsomorphisms (F.mapHomologicalComplex c)$$$

Lean4

instance mapHomologicalComplex_reflects_iso (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] [ReflectsIsomorphisms F]
    (c : ComplexShape ι) : ReflectsIsomorphisms (F.mapHomologicalComplex c) :=
  ⟨fun f => by
    intro
    haveI : ∀ n : ι, IsIso (F.map (f.f n)) := fun n =>
      ((HomologicalComplex.eval W₂ c n).mapIso (asIso ((F.mapHomologicalComplex c).map f))).isIso_hom
    haveI := fun n => isIso_of_reflects_iso (f.f n) F
    exact HomologicalComplex.Hom.isIso_of_components f⟩

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