instPreservesLimitsOfShapeDiscreteWalkingPair

English

Triangulated functors preserve discrete walking pair limits.

Русский

Триангулированные функторы сохраняют пределы в дискретной walking-паре.

LaTeX

$$$\\text{PreservesLimitsOfShape}(\\mathrm{DiscreteWalkingPair})\\; F$$$

Lean4

noncomputable instance [F.IsTriangulated] : PreservesLimitsOfShape (Discrete WalkingPair) F :=
  by
  suffices ∀ (X₁ X₃ : C), IsIso (prodComparison F X₁ X₃)
    by
    have := fun (X₁ X₃ : C) ↦ PreservesLimitPair.of_iso_prod_comparison F X₁ X₃
    exact ⟨fun {K} ↦ preservesLimit_of_iso_diagram F (diagramIsoPair K).symm⟩
  intro X₁ X₃
  let φ : F.mapTriangle.obj (binaryProductTriangle X₁ X₃) ⟶ binaryProductTriangle (F.obj X₁) (F.obj X₃) :=
    { hom₁ := 𝟙 _
      hom₂ := prodComparison F X₁ X₃
      hom₃ := 𝟙 _
      comm₁ := by
        dsimp
        ext
        ·
          simp only [assoc, prodComparison_fst, prod.comp_lift, comp_id, comp_zero, limit.lift_π, BinaryFan.mk_pt,
            BinaryFan.π_app_left, BinaryFan.mk_fst, ← F.map_comp, F.map_id]
        ·
          simp only [assoc, prodComparison_snd, prod.comp_lift, comp_id, comp_zero, limit.lift_π, BinaryFan.mk_pt,
            BinaryFan.π_app_right, BinaryFan.mk_snd, ← F.map_comp, F.map_zero]
      comm₂ := by simp
      comm₃ := by simp }
  exact
    isIso₂_of_isIso₁₃ φ (F.map_distinguished _ (binaryProductTriangle_distinguished X₁ X₃))
      (binaryProductTriangle_distinguished _ _) (by dsimp [φ]; infer_instance) (by dsimp [φ]; infer_instance)

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