pseudo_injective_of_mono — Mathlib

English

If a morphism is mono, its action on pseudoelements is injective.

Русский

Если морфизм моно, его действие на псевдоэлементах инъективно.

LaTeX

$$$(\\forall a,b),\\; \\mathrm{pseudoApply}(f)(a)=\\mathrm{pseudoApply}(f)(b) \\Rightarrow a=b$ for Mono f$$

Lean4

/-- A monomorphism is injective on pseudoelements. -/
theorem pseudo_injective_of_mono {P Q : C} (f : P ⟶ Q) [Mono f] : Function.Injective f :=
  by
  intro abar abar'
  refine Quotient.inductionOn₂ abar abar' fun a a' ha => ?_
  apply Quotient.sound
  have : (⟦(a.hom ≫ f : Over Q)⟧ : Quotient (setoid Q)) = ⟦↑(a'.hom ≫ f)⟧ := by convert ha
  have ⟨R, p, q, ep, Eq, comm⟩ := Quotient.exact this
  exact
    ⟨R, p, q, ep, Eq,
      (cancel_mono f).1 <| by
        simp only [Category.assoc]
        exact comm⟩

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