isComplex_of_iso — Mathlib

English

Let e: S1 ≅ S2 be an isomorphism of composable arrows. Then S1.IsComplex implies S2.IsComplex, i.e., IsComplex is preserved under isomorphism.

Русский

Пусть e: S1 ≅ S2 — изоморфизм композиционных стрелок. Тогда из того, что S1 является комплексом, следует, что S2 тоже является комплексом; т. е. свойство IsComplex сохраняется под изоморфизмом.

LaTeX

$$$\text{If } e: S_1 \cong S_2 \text{ and } S_1 \text{ is a complex, then } S_2 \text{ is a complex.}$$$

Lean4

theorem isComplex_of_iso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) : S₂.IsComplex where
  zero i
    hi := by
    rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero, ← NatTrans.naturality_assoc, ← NatTrans.naturality,
      reassoc_of% (h₁.zero i hi), zero_comp]

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