injective_eq_monomorphisms_iff — Mathlib

English

Again, injective morphisms correspond to monomorphisms if forgetful preserves monomorphisms.

Русский

Повторно: инъективные морфизмы соответствуют моно-морфизмам, если забывающий сохраняет моно морфизмы.

LaTeX

$$$\text{injective } C = \text{monomorphisms } C \iff (\text{forget } C).PreservesMonomorphisms$$$

Lean4

theorem injective_eq_monomorphisms_iff :
    MorphismProperty.injective C = monomorphisms C ↔ (forget C).PreservesMonomorphisms :=
  by
  constructor
  · intro h
    constructor
    rintro _ _ f (hf : monomorphisms C f)
    rw [mono_iff_injective]
    rw [← h] at hf
    exact hf
  · intro
    apply le_antisymm (injective_le_monomorphisms C)
    intro _ _ f hf
    have : Mono f := hf
    change Function.Injective ((forget C).map f)
    rw [← mono_iff_injective]
    infer_instance

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