faithful — Mathlib

English

The inclusion functor of a subgroupoid is faithful on arrows: if two arrows become equal after applying the inclusion map, then they were equal to begin with.

Русский

Включение подгруппоида удовлетворяет условию сохранения различимости морфизмов: если два стрелки в S совпали после применения включения, то они изначально равны.

LaTeX

$$For any S ≤ T, the inclusion functor is faithful on arrows: if f,g ∈ S.Hom(X,Y) and (inclusion h).map f = (inclusion h).map g, then f=g.$$

Lean4

theorem faithful : ∀ c d, Function.Injective fun f : c ⟶ d => (hom S).map f := by
  rintro ⟨c, hc⟩ ⟨d, hd⟩ ⟨f, hf⟩ ⟨g, hg⟩ hfg; exact Subtype.eq hfg

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