mono_of_mono_app — Mathlib

English

If every component α.app X is a monomorphism, then the natural transformation α : F ⟶ G is a monomorphism.

Русский

Если каждый компонент α.app X является монообразованием, то естественное преобразование α : F ⟶ G монообразно.

LaTeX

$$$ (\forall X, \; \operatorname{Mono}(\alpha.app X)) \Rightarrow \operatorname{Mono}(\alpha). $$$

Lean4

/-- A natural transformation is a monomorphism if each component is. -/
theorem mono_of_mono_app (α : F ⟶ G) [∀ X : C, Mono (α.app X)] : Mono α :=
  ⟨fun g h eq => by
    ext X
    rw [← cancel_mono (α.app X), ← comp_app, eq, comp_app]⟩

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