map_injective — Mathlib

English

Let φ be a Prefunctor with IsCovering. Then for arrows f,g in any Hom-unit, φ.map is injective: φ.map f = φ.map g implies f = g.

Русский

Пусть φ — префунктор с условием IsCovering. Тогда отображение стрел φ.map инъективно: если φ.map f = φ.map g, то f = g.

LaTeX

$$$ (h_\\varphi : φ.IsCovering) \\rightarrow \\forall {u v}, Injective (\\lambda f : u \\to v, φ.map f) $$$

Lean4

@[simp]
theorem map_injective (hφ : φ.IsCovering) {u v : U} : Injective fun f : u ⟶ v => φ.map f :=
  by
  rintro f g he
  have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he
  simpa using (hφ.star_bijective u).left this

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