mono_iff_injective — Mathlib

English

For any f: A → B in NonemptyFinLinOrd, f is mono if and only if f is injective.

Русский

Для любого морфизма f: A → B в категории NonemptyFinLinOrd моноэквивалентно тому, что f инъективен.

LaTeX

$$$\mathrm{Mono}(f) \iff \mathrm{Injective}(f)$$$

Lean4

theorem mono_iff_injective {A B : NonemptyFinLinOrd.{u}} (f : A ⟶ B) : Mono f ↔ Function.Injective f :=
  by
  refine ⟨?_, ConcreteCategory.mono_of_injective f⟩
  intro _ a₁ a₂ h
  let X := of (ULift (Fin 1))
  let g₁ : X ⟶ A := ofHom ⟨fun _ => a₁, fun _ _ _ => by rfl⟩
  let g₂ : X ⟶ A := ofHom ⟨fun _ => a₂, fun _ _ _ => by rfl⟩
  change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))
  have eq : g₁ ≫ f = g₂ ≫ f := by
    ext
    exact h
  rw [cancel_mono] at eq
  rw [eq]

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