iso_iff — Mathlib

English

For isomorphic functors F ≅ G, PreservesMonomorphisms F holds iff PreservesMonomorphisms G holds.

Русский

Для изоморфных функторов F ≅ G выполнение PreservesMonomorphisms F эквивалентно PreservesMonomorphisms G.

LaTeX

$$PreservesMonomorphisms F ⇔ PreservesMonomorphisms G$$

Lean4

theorem iso_iff {F G : C ⥤ D} (α : F ≅ G) : PreservesMonomorphisms F ↔ PreservesMonomorphisms G :=
  ⟨fun _ => preservesMonomorphisms.of_iso α, fun _ => preservesMonomorphisms.of_iso α.symm⟩

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