Theorems · Theorem · category theory

CategoryTheory.Abelian.SpectralObject.mono_map

∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀' i₀ i₁ i₂ i₃ : ι}
  (f₁ : i₀ ⟶ i₁) (f₁' : i₀' ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂ f₃) (n₀ n₁ n₂ n₃ : ℤ),
  autoParam (α.app 1 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 1))
      CategoryTheory.Abelian.SpectralObject.mono_map._auto_1 →
    autoParam (α.app 2 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 2))
        CategoryTheory.Abelian.SpectralObject.mono_map._auto_3 →
      autoParam (α.app 3 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 3))
          CategoryTheory.Abelian.SpectralObject.mono_map._auto_5 →
        ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mono_map._auto_7)
          (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mono_map._auto_9),
          autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.mono_map._auto_11 →
            CategoryTheory.Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)

Defined in

Mathlib.Algebra.Homology.SpectralObject.EpiMono

Cited by

0 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.Category