mk' — Mathlib

English

A constructive principle: if a property holds for all isomorphic copies of a diagram, then the diagram is triangulated.

Русский

Если свойство выполняется для всех изоморфных копий диаграммы, то диаграмма треугольна.

LaTeX

$$$\\text{mk'} (h)$: a criterion that reduces checking triangulated property via isomorphisms$$

Lean4

/-- Constructor for `IsTriangulated C` which shows that it suffices to obtain an octahedron
for a suitable isomorphic diagram instead of the given diagram. -/
theorem mk'
    (h :
      ∀ ⦃X₁' X₂' X₃' : C⦄ (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃'),
        ∃ (X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C) (u₁₂ : X₁ ⟶ X₂) (u₂₃ : X₂ ⟶ X₃) (e₁ : X₁' ≅ X₁) (e₂ : X₂' ≅ X₂) (e₃ : X₃' ≅ X₃) (_
          : u₁₂' ≫ e₂.hom = e₁.hom ≫ u₁₂) (_ : u₂₃' ≫ e₃.hom = e₂.hom ≫ u₂₃) (v₁₂ : X₂ ⟶ Z₁₂) (w₁₂ : Z₁₂ ⟶ X₁⟦1⟧) (h₁₂ :
          Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distTriang C) (v₂₃ : X₃ ⟶ Z₂₃) (w₂₃ : Z₂₃ ⟶ X₂⟦1⟧) (h₂₃ :
          Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distTriang C) (v₁₃ : X₃ ⟶ Z₁₃) (w₁₃ : Z₁₃ ⟶ X₁⟦1⟧) (h₁₃ :
          Triangle.mk (u₁₂ ≫ u₂₃) v₁₃ w₁₃ ∈ distTriang C), Nonempty (Octahedron rfl h₁₂ h₂₃ h₁₃)) :
    IsTriangulated C where
  octahedron_axiom {X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' u₁₂' u₂₃' u₁₃'} comm' {v₁₂' w₁₂'} h₁₂' {v₂₃' w₂₃'} h₂₃' {v₁₃' w₁₃'}
    h₁₃' :=
    by
    obtain
      ⟨X₁, X₂, X₃, Z₁₂, Z₂₃, Z₁₃, u₁₂, u₂₃, e₁, e₂, e₃, comm₁₂, comm₂₃, v₁₂, w₁₂, h₁₂, v₂₃, w₂₃, h₂₃, v₁₃, w₁₃, h₁₃,
        H⟩ :=
      h u₁₂' u₂₃'
    exact
      ⟨Octahedron.ofIso u₁₂' u₂₃' u₁₃' comm' h₁₂' h₂₃' h₁₃' u₁₂ u₂₃ _ rfl e₁ e₂ e₃ comm₁₂ comm₂₃ v₁₂ w₁₂ h₁₂ v₂₃ w₂₃ h₂₃
          v₁₃ w₁₃ h₁₃ H.some⟩

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