Theorems · Theorem · category theory

CochainComplex.injective_opcycles

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) (n₀ n₁ : ℤ) [CategoryTheory.Injective (K.X n₀)] [CategoryTheory.Injective (K.X n₁)]
  [K.IsStrictlyGE n₀],
  HomologicalComplex.ExactAt K n₀ →
    autoParam (n₀ + 1 = n₁) CochainComplex.injective_opcycles._auto_1 →
      CategoryTheory.Injective (HomologicalComplex.opcycles K n₁)

Defined in: Mathlib.Algebra.Homology.Embedding.CochainComplex
Cited by: 1 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Abelian CategoryTheory.Injective CategoryTheory.Injective CochainComplex.IsStrictlyGE

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites34

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.ShortComplexproof · cited by 1,850
HomologicalComplex.Xstatement and proof · cited by 1,839
CategoryTheory.Abelianstatement and proof · cited by 1,753
ComplexShape.upstatement and proof · cited by 1,123
CochainComplexstatement and proof · cited by 1,016
CategoryTheory.Monoproof · cited by 893
CategoryTheory.ShortComplex.gproof · cited by 658
CategoryTheory.ShortComplex.fproof · cited by 653
HomologicalComplex.dproof · cited by 598
CategoryTheory.ShortComplex.Exactproof · cited by 292
CategoryTheory.ShortComplex.ShortExactproof · cited by 232

Cited by1

Results whose statement or proof uses this declaration.

CochainComplex.Plus.modelCategoryQuillen.exists_quasiIso_injectiveproof · cited by 1