mono_homologyMap_of_mono_opcyclesMap'

English

If opcyclesMap φ is mono, then homologyMap φ is mono.

Русский

Если opcyclesMap φ моно, то homologyMap φ моно.

LaTeX

$$Mono (homologyMap φ)$$

Lean4

theorem mono_homologyMap_of_mono_opcyclesMap' [S₁.HasHomology] [S₂.HasHomology] (h : Mono (opcyclesMap φ)) :
    Mono (homologyMap φ) :=
  by
  have : Mono (homologyMap φ ≫ S₂.homologyι) :=
    by
    rw [homologyι_naturality φ]
    apply mono_comp
  exact mono_of_mono (homologyMap φ) S₂.homologyι

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