complete_distinguished_triangle_morphism

English

The instance CatCommSq for OppositeTriangle map with triangleOpEquivalence is provided, ensuring coherence of the opposite triangle operation with equivalences.

Русский

Дано экземпляр CatCommSq для OppositeTriangle, обеспечивающий когерентность противоположной операции треугольника с эквивалентностями.

LaTeX

$$$instCatCommSqOppositeTriangleOpMapTriangleFunctorTriangleOpEquivalence$$$

Lean4

theorem complete_distinguished_triangle_morphism (T₁ T₂ : Triangle Cᵒᵖ) (hT₁ : T₁ ∈ distinguishedTriangles C)
    (hT₂ : T₂ ∈ distinguishedTriangles C) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂)
    (comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁) :
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ a⟦1⟧' = c ≫ T₂.mor₃ :=
  by
  rw [mem_distinguishedTriangles_iff] at hT₁ hT₂
  obtain ⟨c, hc₁, hc₂⟩ :=
    Pretriangulated.complete_distinguished_triangle_morphism₁ _ _ hT₂ hT₁ b.unop a.unop (Quiver.Hom.op_inj comm.symm)
  dsimp at c hc₁ hc₂
  replace hc₂ := ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫= hc₂
  dsimp at hc₂
  simp only [assoc, Iso.unop_hom_inv_id_app_assoc] at hc₂
  refine ⟨c.op, Quiver.Hom.unop_inj hc₁.symm, Quiver.Hom.unop_inj ?_⟩
  apply (shiftFunctor C (1 : ℤ)).map_injective
  rw [unop_comp, unop_comp, Functor.map_comp, Functor.map_comp, Quiver.Hom.unop_op, hc₂, ← unop_comp_assoc, ←
    unop_comp_assoc, ← opShiftFunctorEquivalence_unitIso_inv_naturality]
  simp

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