isomorphic_distinguished — Mathlib

English

If F preserves shifts, the constructed isomorphism mapTriangleOpCompTriangleOpEquivalenceFunctorApp exhibits a natural isomorphism between the composite functors F.mapTriangle.op and triangleOpEquivalence composed with F.op.mapTriangle.

Русский

Если F сохраняет сдвиги, построенный изоморфизм mapTriangleOpCompTriangleOpEquivalenceFunctorApp образует естественный изоморфизм между сочетанием F.mapTriangle.op и triangleOpEquivalence ∘ F.op.mapTriangle.

LaTeX

$$$(triangleOpEquivalence D).functor \circ F.mapTriangle \cong F.op.mapTriangle \circ (triangleOpEquivalence C).functor$$$

Lean4

theorem isomorphic_distinguished (T₁ : Triangle Cᵒᵖ) (hT₁ : T₁ ∈ distinguishedTriangles C) (T₂ : Triangle Cᵒᵖ)
    (e : T₂ ≅ T₁) : T₂ ∈ distinguishedTriangles C :=
  by
  simp only [mem_distinguishedTriangles_iff] at hT₁ ⊢
  exact Pretriangulated.isomorphic_distinguished _ hT₁ _ ((triangleOpEquivalence C).inverse.mapIso e).unop.symm

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