map_injective — Mathlib

English

If F ⊣ G is an adjunction with F preserving monomorphisms, then for any object I of D that is injective, G(I) is injective in C.

Русский

Если F ⊣ G есть сопряжение и F сохраняет моно morphisms, то если I в D инъективен, то G(I) в C также инъективен.

LaTeX

$$$$\\forall {F : C \\to D}\\;{G : D \\to C}\\;(\\text{adj} : F \\dashv G)\\;[F\\text{PreservesMonomorphisms}]\\; (I \\in D)\\; (\\text{Injective}(I) \\Rightarrow \\text{Injective}(G(I))).$$$$

Lean4

theorem map_injective (adj : F ⊣ G) [F.PreservesMonomorphisms] (I : D) (hI : Injective I) : Injective (G.obj I) :=
  ⟨fun {X} {Y} f g => by
    intro
    rcases hI.factors (F.map f ≫ adj.counit.app _) (F.map g) with ⟨w, h⟩
    use adj.unit.app Y ≫ G.map w
    rw [← unit_naturality_assoc, ← G.map_comp, h]
    simp⟩

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