preservesMonomorphisms_of_adjunction

English

If F ⊣ G is an adjunction, then G preserves monomorphisms.

Русский

Если F ⊣ G — адъюнкция, то G сохраняет мономорфизмы.

LaTeX

$$G.PreservesMonomorphisms$$

Lean4

theorem preservesMonomorphisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : PreservesMonomorphisms G :=
  {
    preserves := fun {X} {Y} f hf =>
      ⟨by
        intro Z g h H
        replace H := congr_arg (adj.homEquiv Z Y).symm H
        rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
          Equiv.apply_eq_iff_eq] at H⟩ }

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