mono_iff_injective — Mathlib

English

A morphism in CompHausLike P is mono if and only if its underlying map is injective.

Русский

Морфизм в CompHausLike P является моно, если и только если соответствующая ему функция инъективна.

LaTeX

$$$f\text{ is Mono }\Leftrightarrow \mathrm{Function.Injective}(f)$$$

Lean4

theorem mono_iff_injective {X Y : CompHausLike.{u} P} (f : X ⟶ Y) : Mono f ↔ Function.Injective f :=
  by
  constructor
  · intro hf x₁ x₂ h
    let g₁ : X ⟶ X := ofHom _ ⟨fun _ => x₁, continuous_const⟩
    let g₂ : X ⟶ X := ofHom _ ⟨fun _ => x₂, continuous_const⟩
    have : g₁ ≫ f = g₂ ≫ f := by ext; exact h
    exact CategoryTheory.congr_fun ((cancel_mono _).mp this) x₁
  · rw [← CategoryTheory.mono_iff_injective]
    apply (forget (CompHausLike P)).mono_of_mono_map

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