iff_comp — Mathlib

English

For any W and isomorphism e: F1 ≅ F2, W.IsInvertedBy F1 iff W.IsInvertedBy F2.

Русский

Для любого W и изоморфизма e: F1 ≅ F2, W разворачивается по F1 тогда и только тогда по F2.

LaTeX

$$$ W.IsInvertedBy F_1 \iff W.IsInvertedBy F_2 \text{ при } F_1 \cong F_2 $$$

Lean4

@[simp]
theorem iff_comp {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃] (W : MorphismProperty C₁) (F : C₁ ⥤ C₂)
    (G : C₂ ⥤ C₃) [G.ReflectsIsomorphisms] : W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F :=
  by
  constructor
  · intro h X Y f hf
    have : IsIso (G.map (F.map f)) := h _ hf
    exact isIso_of_reflects_iso (F.map f) G
  · intro hF
    exact IsInvertedBy.of_comp W F hF G

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