ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K L : CochainComplex C ℕ<VAR>φ : K ⟶ L<VAR>HomologicalComplex.HasHomology K 0<VAR>HomologicalComplex.HasHomology L 0<GOAL>HomologicalComplex.homologyMap φ 0 ≫ L.isoHomologyπ₀.inv = K.isoHomologyπ₀.inv ≫ HomologicalComplex.cyclesMap φ 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.homologyMap (-φ) i = -HomologicalComplex.homologyMap φ i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>φ ψ : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.homologyMap (φ + ψ) i = HomologicalComplex.homologyMap φ i + HomologicalComplex.homologyMap ψ i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>φ ψ : K ⟶ L<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.homologyMap (φ - ψ) i = HomologicalComplex.homologyMap φ i - HomologicalComplex.homologyMap ψ i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>K : CochainComplex C ℕ<VAR>X : C<VAR>φ : X ⟶ K.X 0<VAR>HomologicalComplex.HasHomology K 0<VAR>hφ : φ ≫ K.d 0 1 = 0<GOAL>CategoryTheory.IsIso (HomologicalComplex.liftCycles K φ 1 ⋯ hφ) ↔ (CategoryTheory.ShortComplex.mk φ (K.d 0 1) hφ).Exact ∧ CategoryTheory.Mono φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>K : ChainComplex C ℕ<VAR>X : C<VAR>φ : K.X 0 ⟶ X<VAR>HomologicalComplex.HasHomology K 0<VAR>hφ : K.d 1 0 ≫ φ = 0<GOAL>CategoryTheory.IsIso (HomologicalComplex.descOpcycles K φ 1 ⋯ hφ) ↔ (CategoryTheory.ShortComplex.mk (K.d 1 0) φ hφ).Exact ∧ CategoryTheory.Epi φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>(K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).iCycles = K.iCycles j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>(K.cyclesIsoSc' i j k hi hk).inv ≫ K.iCycles j = (K.sc' i j k).iCycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>K.toCycles i j ≫ (K.cyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).toCycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>(K.sc' i j k).pOpcycles ≫ (K.opcyclesIsoSc' i j k hi hk).inv = K.pOpcycles j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>K.pOpcycles j ≫ (K.opcyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).pOpcycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>(K.opcyclesIsoSc' i j k hi hk).inv ≫ K.fromOpcycles j k = (K.sc' i j k).fromOpcycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>K.homologyπ j ≫ (K.homologyIsoSc' i j k hi hk).hom = (K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyπ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>(K.sc' i j k).homologyπ ≫ (K.homologyIsoSc' i j k hi hk).inv = (K.cyclesIsoSc' i j k hi hk).inv ≫ K.homologyπ j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>(K.homologyIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyι = K.homologyι j ≫ (K.opcyclesIsoSc' i j k hi hk).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>K.HasHomology j<VAR>(K.sc' i j k).HasHomology<GOAL>(K.homologyIsoSc' i j k hi hk).inv ≫ K.homologyι j = (K.sc' i j k).homologyι ≫ (K.opcyclesIsoSc' i j k hi hk).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<GOAL>∀ (x x_1 : ι), (K.restriction e).d x x_1 = K.d (e.f x) (e.f x_1)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>i : ι<GOAL>(K.restriction e).X i = K.X (e.f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>i j : ι<VAR>i' j' : ι'<VAR>hi : e.f i = i'<VAR>hj : e.f j = j'<GOAL>(K.restriction e).d i j = (K.restrictionXIso e hi).hom ≫ K.d i' j' ≫ (K.restrictionXIso e hj).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K L : HomologicalComplex C c'<VAR>φ : K ⟶ L<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>i : ι<GOAL>(HomologicalComplex.restrictionMap φ e).f i = φ.f (e.f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K L : HomologicalComplex C c'<VAR>φ : K ⟶ L<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>i : ι<VAR>i' : ι'<VAR>hi : e.f i = i'<GOAL>(HomologicalComplex.restrictionMap φ e).f i = (K.restrictionXIso e hi).hom ≫ φ.f i' ≫ (L.restrictionXIso e hi).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<GOAL>HomologicalComplex.restrictionMap (𝟙 K) e = 𝟙 (K.restriction e)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>L : HomologicalComplex C c'<VAR>M : HomologicalComplex C c'<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>e : c.Embedding c'<VAR>e.IsRelIff<GOAL>HomologicalComplex.restrictionMap (φ ≫ φ') e = HomologicalComplex.restrictionMap φ e ≫ HomologicalComplex.restrictionMap φ' e
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>e.IsRelIff<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<GOAL>(e.restrictionFunctor C).obj K = K.restriction e
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>e.IsRelIff<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : HomologicalComplex C c'} (φ : X ⟶ Y), (e.restrictionFunctor C).map φ = HomologicalComplex.restrictionMap φ e
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>a : R<VAR>φ : S₁ ⟶ S₂<GOAL>(a • φ).τ₁ = a • φ.τ₁
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>a : R<VAR>φ : S₁ ⟶ S₂<GOAL>(a • φ).τ₂ = a • φ.τ₂
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>a : R<VAR>φ : S₁ ⟶ S₂<GOAL>(a • φ).τ₃ = a • φ.τ₃
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>a : R<GOAL>(γ.smul a).φH = a • γ.φH
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>a : R<GOAL>(γ.smul a).φK = a • γ.φK
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>a : R<GOAL>CategoryTheory.ShortComplex.leftHomologyMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>a : R<GOAL>CategoryTheory.ShortComplex.cyclesMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>a : R<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.leftHomologyMap (a • φ) = a • CategoryTheory.ShortComplex.leftHomologyMap φ
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>a : R<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.cyclesMap (a • φ) = a • CategoryTheory.ShortComplex.cyclesMap φ
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>a : R<GOAL>(γ.smul a).φH = a • γ.φH
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>a : R<GOAL>(γ.smul a).φQ = a • γ.φQ
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>a : R<GOAL>CategoryTheory.ShortComplex.rightHomologyMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>a : R<GOAL>CategoryTheory.ShortComplex.opcyclesMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>a : R<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.rightHomologyMap (a • φ) = a • CategoryTheory.ShortComplex.rightHomologyMap φ
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>a : R<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.opcyclesMap (a • φ) = a • CategoryTheory.ShortComplex.opcyclesMap φ
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>a : R<GOAL>(γ.smul a).left = γ.left.smul a
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>a : R<GOAL>(γ.smul a).right = γ.right.smul a
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>a : R<GOAL>CategoryTheory.ShortComplex.homologyMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>a : R<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.ShortComplex.homologyMap (a • φ) = a • CategoryTheory.ShortComplex.homologyMap φ
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>a : R<GOAL>(h.smul a).h₃ = a • h.h₃
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>a : R<GOAL>(h.smul a).h₀ = a • h.h₀
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>a : R<GOAL>(h.smul a).h₁ = a • h.h₁
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>a : R<GOAL>(h.smul a).h₂ = a • h.h₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>e.IsTruncGE<VAR>∀ (i' : ι'), K.HasHomology i'<VAR>i j k : ι<GOAL>HomologicalComplex.truncGE'.d K e i j ≫ HomologicalComplex.truncGE'.d K e j k = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>e.IsTruncGE<VAR>∀ (i' : ι'), K.HasHomology i'<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>i' j' : ι'<VAR>hi' : e.f i = i'<VAR>hj' : e.f j = j'<VAR>hi : ¬e.BoundaryGE i<GOAL>(K.truncGE' e).d i j = (K.truncGE'XIso e hi' hi).hom ≫ K.d i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>e.IsTruncGE<VAR>∀ (i' : ι'), K.HasHomology i'<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>i' j' : ι'<VAR>hi' : e.f i = i'<VAR>hj' : e.f j = j'<VAR>hi : e.BoundaryGE i<GOAL>(K.truncGE' e).d i j = (K.truncGE'XIsoOpcycles e hi' hi).hom ≫ K.fromOpcycles i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>i' : ι'<VAR>j : ι<VAR>hj : c'.Rel i' (e.f j)<VAR>hi' : ∀ (i : ι), e.f i ≠ i'<GOAL>e.BoundaryGE j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>j k : ι<VAR>hk : c.Rel j k<GOAL>¬e.BoundaryGE k
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>j k : ι<VAR>hj : ¬e.BoundaryGE j<VAR>hk : c.next j = k<GOAL>¬e.BoundaryGE k
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>j : ι<VAR>hj : e.BoundaryGE j<VAR>i' : ι'<VAR>hi' : c'.Rel i' (e.f j)<VAR>a : ι<GOAL>e.f a ≠ i'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>i j : ι<VAR>hij : c.prev j = i<VAR>hj : ¬e.BoundaryGE j<GOAL>c'.prev (e.f j) = e.f i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>j : ι<VAR>hj : e.BoundaryGE j<VAR>e.IsTruncLE<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>k' : ι'<VAR>j : ι<VAR>hj : c'.Rel (e.f j) k'<VAR>hk' : ∀ (i : ι), e.f i ≠ k'<GOAL>e.BoundaryLE j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>i j : ι<VAR>hi : c.Rel i j<GOAL>¬e.BoundaryLE i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>i j : ι<VAR>hj : ¬e.BoundaryLE j<VAR>hk : c.prev j = i<GOAL>¬e.BoundaryLE i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>j : ι<VAR>hj : e.BoundaryLE j<VAR>k' : ι'<VAR>hk' : c'.Rel (e.f j) k'<VAR>a : ι<GOAL>e.f a ≠ k'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>e.IsRelIff<VAR>j k : ι<VAR>hjk : c.next j = k<VAR>hj : ¬e.BoundaryLE j<GOAL>c'.next (e.f j) = e.f k
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>j : ι<VAR>hj : e.BoundaryLE j<VAR>e.IsTruncGE<GOAL>False
<VAR>p : ℤ<VAR>n : ℕ<GOAL>(ComplexShape.embeddingUpIntGE p).BoundaryGE n ↔ n = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>self : K.IsStrictlySupported e<VAR>i' : ι'<VAR>hi' : ∀ (i : ι), e.f i ≠ i'<GOAL>CategoryTheory.Limits.IsZero (K.X i')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>K.IsStrictlySupported e<VAR>i' : ι'<VAR>hi' : ∀ (i : ι), e.f i ≠ i'<GOAL>CategoryTheory.Limits.IsZero (K.X i')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K L : HomologicalComplex C c'<VAR>e' : K ≅ L<VAR>e : c.Embedding c'<VAR>K.IsStrictlySupported e<GOAL>L.IsStrictlySupported e
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>self : K.IsSupported e<VAR>i' : ι'<VAR>hi' : ∀ (i : ι), e.f i ≠ i'<GOAL>K.ExactAt i'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>K.IsSupported e<VAR>i' : ι'<VAR>hi' : ∀ (i : ι), e.f i ≠ i'<GOAL>K.ExactAt i'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K L : HomologicalComplex C c'<VAR>e' : K ≅ L<VAR>e : c.Embedding c'<VAR>K.IsSupported e<GOAL>L.IsSupported e
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>self : K.IsStrictlySupportedOutside e<VAR>i : ι<GOAL>CategoryTheory.Limits.IsZero (K.X (e.f i))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>self : K.IsSupportedOutside e<VAR>i : ι<GOAL>K.ExactAt (e.f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<VAR>h : K.IsStrictlySupportedOutside e<GOAL>K.IsSupportedOutside e
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c'<VAR>e : c.Embedding c'<GOAL>CategoryTheory.Limits.IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e