of_natTrans — Mathlib

English

If F preserves monomorphisms and f: G ⟶ F is a natural transformation with Mono components, then G preserves monomorphisms.

Русский

Если F сохраняет мономорфизмы и f: G ⟶ F — натрансформация с компонентами моно, тогда G сохраняет мономорфизмы.

LaTeX

$$(PreservesMonomorphisms F) ∧ (∀ X, Mono (f.app X)) ⇒ PreservesMonomorphisms G$$

Lean4

theorem of_natTrans {F G : C ⥤ D} [PreservesMonomorphisms F] (f : G ⟶ F) [∀ X, Mono (f.app X)] :
    PreservesMonomorphisms G where
  preserves {X Y} π
    hπ := by
    suffices Mono (G.map π ≫ f.app Y) from mono_of_mono (G.map π) (f.app Y)
    rw [f.naturality π]
    infer_instance

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