injective_of_map_injective — Mathlib

English

If F ⊣ G with G Full and Faithful, and G(I) is injective for some I in D, then I is injective.

Русский

Если у сопряжения G полно и полнота, и G(I) инъективен, то I инъективен.

LaTeX

$$$$\\forall {I \\in D}\\;[G\\text{Full}]\\;[G\\text{Faithful}]\\; (\\text{Injective}(G(I)) \\Rightarrow \\text{Injective}(I)).$$$$

Lean4

theorem injective_of_map_injective (adj : F ⊣ G) [G.Full] [G.Faithful] (I : D) (hI : Injective (G.obj I)) :
    Injective I :=
  ⟨fun {X} {Y} f g => by
    intro
    haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
    rcases hI.factors (G.map f) (G.map g) with ⟨w, h⟩
    use inv (adj.counit.app _) ≫ F.map w ≫ adj.counit.app _
    exact G.map_injective (by simpa)⟩

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