forget₂_preservesMonomorphisms — Mathlib

English

The forget₂ functor preserves monomorphisms functorially, under the given forgetful structure.

Русский

Функтор forget₂ сохраняет моно-морфизмы в рамках данной структуры забывания.

LaTeX

$$$\text{forget₂ C D}.PreservesMonomorphisms$$$

Lean4

instance forget₂_preservesMonomorphisms (C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C] [Category.{v'} D]
    [HasForget.{w} D] [HasForget₂ C D] [(forget C).PreservesMonomorphisms] : (forget₂ C D).PreservesMonomorphisms :=
  have : (forget₂ C D ⋙ forget D).PreservesMonomorphisms :=
    by
    simp only [HasForget₂.forget_comp]
    infer_instance
  Functor.preservesMonomorphisms_of_preserves_of_reflects _ (forget D)

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