mono_of_isIso_fst — Mathlib

English

If f is a kernel morphism and a, b form a kernel pair for f, and a is an isomorphism, then f is a monomorphism.

Русский

Если f — морфизм ядра и пара a,b образует пару ядра для f, а сам a изоморфизм, то f моно.

LaTeX

$$$\\forall {C} [\\mathcal{C}], {R,X,Y}\\ f:X\\to Y, \\ a:R\\to X, \\ b:R\\to X,\\ [\\text{Mono}(a)], \\operatorname{IsKernelPair}(f,a,b) \\Rightarrow \\operatorname{Mono}(f).$$$

Lean4

theorem mono_of_isIso_fst (h : IsKernelPair f a b) [IsIso a] : Mono f :=
  by
  obtain ⟨l, h₁, h₂⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit (𝟙 _) (𝟙 _) (by simp)
  rw [IsPullback.cone_fst, ← IsIso.eq_comp_inv, Category.id_comp] at h₁
  rw [h₁, IsIso.inv_comp_eq, Category.comp_id] at h₂
  constructor
  intro Z g₁ g₂ e
  obtain ⟨l', rfl, rfl⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit _ _ e
  rw [IsPullback.cone_fst, h₂]

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