mono_iff_injective — Mathlib

English

In TopCat, a morphism is mono if and only if it is injective on the underlying map.

Русский

В TopCat мононеморфизм эквивалентен инъективности соответствующего отображения.

LaTeX

$$$\\text{Mono}(f) \\iff \\text{Function.Injective}(f)$$$

Lean4

theorem mono_iff_injective {X Y : TopCat.{u}} (f : X ⟶ Y) : Mono f ↔ Function.Injective f :=
  by
  suffices Mono f ↔ Mono ((forget TopCat).map f)
    by
    rw [this, CategoryTheory.mono_iff_injective]
    rfl
  constructor
  · intro
    infer_instance
  · apply Functor.mono_of_mono_map

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