map_injective_iff — Mathlib

English

For an equivalence F : C ≌ D, Injective (F.obj P) if and only if Injective P for any P ∈ C.

Русский

Для эквивалентности F : C ≌ D справедливо Injective(F(P)) ⇔ Injective(P).

LaTeX

$$$$\\forall {F : C \\simeq D}, \\; \\forall P \\in C, \\; \\text{Injective}(F(P)) \\iff \\text{Injective}(P).$$$$

Lean4

theorem map_injective_iff (P : C) : Injective (F.functor.obj P) ↔ Injective P :=
  ⟨F.symm.toAdjunction.injective_of_map_injective P, F.symm.toAdjunction.map_injective P⟩

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