mono_homologyMap_of_mono_of_not_rel

English

If φ: K → L is a morphism with φ.f i epi for all i and the relation Rel(i,j) does not hold for any j, then the homology map is epi at i.

Русский

Если φ: K → L имеет эпиморфизм на каждом компоненте и отсутствуют пары i,j с отношением Rel, то homologyMap φ i является эпиморфизмом.

LaTeX

$$$$ \\text{epi}(\\mathrm{homologyMap}(\\varphi,i)) $$$$

Lean4

theorem mono_homologyMap_of_mono_of_not_rel (φ : K ⟶ L) (j : ι) [K.HasHomology j] [L.HasHomology j] [Mono (φ.f j)]
    (hj : ∀ i, ¬c.Rel i j) : Mono (homologyMap φ j) :=
  ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff
        (Arrow.isoMk (K.isoHomologyπ _ j rfl (shape _ _ _ (by tauto)))
          (L.isoHomologyπ _ j rfl (shape _ _ _ (by tauto))))).1
    (MorphismProperty.monomorphisms.infer_property (cyclesMap φ j))

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