Theorems · Theorem · category theory

CategoryTheory.SpectralSequence.Hom.ext

∀ {C : Type u_1} {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Abelian C} {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀} {x y : E.Hom E'},
  @CategoryTheory.SpectralSequence.Hom.hom C inst inst_1 κ c r₀ E E' x =
      @CategoryTheory.SpectralSequence.Hom.hom C inst inst_1 κ c r₀ E E' y →
    x = y

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

2 results in Mathlib

Foundations

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