cancel_right_of_mono — Mathlib

English

If f2 is mono and (f1 ≫ f2) has kernel pair (a,b), then f1 has kernel pair (a,b).

Русский

Если f2 моно и (f1 ≫ f2) имеет KernelPair (a,b), то и f1 имеет KernelPair (a,b).

LaTeX

$$[Mono f2] ∧ IsKernelPair (f1 ≫ f2) a b ⇒ IsKernelPair f1 a b$$

Lean4

/-- If `(a,b)` is a kernel pair for `f₁ ≫ f₂` and `f₂` is mono, then `(a,b)` is a kernel pair for
just `f₁`.
The converse of `comp_of_mono`.
-/
theorem cancel_right_of_mono {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} [Mono f₂] (big_k : IsKernelPair (f₁ ≫ f₂) a b) :
    IsKernelPair f₁ a b :=
  cancel_right (by rw [← cancel_mono f₂, assoc, assoc, big_k.w]) big_k

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