comp_exact_iff_exact — Mathlib

English

If i: P → P' is injective, then Exact(f,i ∘ g) iff Exact(f,g).

Русский

Если i: P → P' инъективно, то Exact(f, i ∘ g) эквивалентно Exact(f, g).

LaTeX

$$$$ \\operatorname{Exact}(f, i \\circ g) \\iff \\operatorname{Exact}(f,g) \\quad (i \\text{ injective}). $$$$

Lean4

theorem comp_exact_iff_exact {i : P →ₗ[R] P'} (h : Injective i) : Exact f (i ∘ₗ g) ↔ Exact f g :=
  forall_congr' fun _ => iff_congr (LinearMap.map_eq_zero_iff _ h) Iff.rfl

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