map_iff — Mathlib

English

For W, F and G, (W.map F).IsInvertedBy G iff W.IsInvertedBy (F ⋙ G).

Русский

Для W, F и G, (W.map F).IsInvertedBy G эквивалентно W.IsInvertedBy (F ⋙ G).

LaTeX

$$$ (W.map F).IsInvertedBy G \iff W.IsInvertedBy (F \cdot G) $$$

Lean4

theorem map_iff {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃] (W : MorphismProperty C₁) (F : C₁ ⥤ C₂)
    (G : C₂ ⥤ C₃) : (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F ⋙ G) := by
  simp only [IsInvertedBy.iff_map_le_isomorphisms, map_map]

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