Definitions: Mathlib.Algebra, part 11 of 17

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then the colimit cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then $\operatorname{isColimitColimitCocone}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_isColimitOfIsColimit\_u3c0\_}$ applied to the colimit cocone of $F$, $\mathrm{CategoryTheory\_\_ShortComplex\_\_isColimit\_u3c0\_\_u2081\_MapCoconeColimitCocone}$ applied to $F$, $\mathrm{CategoryTheory\_\_ShortComplex\_\_isColimit\_u3c0\_\_u2082\_MapCoconeColimitCocone}$ applied to $F$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_isColimit\_u3c0\_\_u2083\_MapCoconeColimitCocone}$ applied to $F$.

Let $c$ be a cocone of $F$. Let $x_{3}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of the first projection functor and $c$. Let $x_{4}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of the second projection functor and $c$. Let $x_{5}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of the third projection functor and $c$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_isColimitOfIsColimit\_u3c0\_}$ applied to $c$, $x_{3}$, $x_{4}$ and $x_{5}$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_isColimit\_u3c0\_\_u2081\_MapCoconeColimitCocone}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of the first projection functor and the colimit cocone of $F$.

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_isColimit\_u3c0\_\_u2082\_MapCoconeColimitCocone}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of the second projection functor and the colimit cocone of $F$.

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_isColimit\_u3c0\_\_u2083\_MapCoconeColimitCocone}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of the third projection functor and the colimit cocone of $F$.

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then $\operatorname{isLimitLimitCone}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_isLimitOfIsLimit\_u3c0\_}$ applied to the limit cone of $F$, $\mathrm{CategoryTheory\_\_ShortComplex\_\_isLimit\_u3c0\_\_u2081\_MapConeLimitCone}$ applied to $F$, $\mathrm{CategoryTheory\_\_ShortComplex\_\_isLimit\_u3c0\_\_u2082\_MapConeLimitCone}$ applied to $F$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_isLimit\_u3c0\_\_u2083\_MapConeLimitCone}$ applied to $F$.

Let $c$ be a cone of $F$. Let $x_{3}$ be an element of $\operatorname{IsLimit}$ applied to the map cone of the first projection functor and $c$. Let $x_{4}$ be an element of $\operatorname{IsLimit}$ applied to the map cone of the second projection functor and $c$. Let $x_{5}$ be an element of $\operatorname{IsLimit}$ applied to the map cone of the third projection functor and $c$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_isLimitOfIsLimit\_u3c0\_}$ applied to $c$, $x_{3}$, $x_{4}$ and $x_{5}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_isLimit\_u3c0\_\_u2081\_MapConeLimitCone}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the map cone of the first projection functor and the limit cone of $F$.

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_isLimit\_u3c0\_\_u2082\_MapConeLimitCone}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the map cone of the second projection functor and the limit cone of $F$.

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_isLimit\_u3c0\_\_u2083\_MapConeLimitCone}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the map cone of the third projection functor and the limit cone of $F$.

the limit cone of F (from the name)

Let $F$ be a functor of $J$ and the set of short complexes of $C$. Then the limit cone of $F$ is a cone of $F$.

the scalar multiple of x9 and a (from the name)

Let $x_{9}$ be a homology map data of $x_{7}$ and $x_{8}$. Let $a$ be an element of $R$. Then the scalar multiple of $x_{9}$ and $a$ is a homology map data of $x_{7}$ and $x_{8}$ defined as $\operatorname{mk}$ applied to the scalar multiple of the left of $x_{9}$ and $a$ and the scalar multiple of the right of $x_{9}$ and $a$.

the scalar multiple of h and a (from the name)

Let $h$ be a homotopy of $x_{6}$ and $x_{7}$. Let $a$ be an element of $R$. Then the scalar multiple of $h$ and $a$ is a homotopy of $\HSMulhSMulMACRoAL {a}{x_{6}}$ and $\HSMulhSMulMACRoAL {a}{x_{7}}$.

the scalar multiple of x9 and a (from the name)

Let $x_{9}$ be a left homology map data of $x_{7}$ and $x_{8}$. Let $a$ be an element of $R$. Then the scalar multiple of $x_{9}$ and $a$ is a left homology map data of $x_{7}$ and $x_{8}$.

the scalar multiple of x9 and a (from the name)

Let $x_{9}$ be a right homology map data of $x_{7}$ and $x_{8}$. Let $a$ be an element of $R$. Then the scalar multiple of $x_{9}$ and $a$ is a right homology map data of $x_{7}$ and $x_{8}$.

the module category cycle isomorphism of S (from the name)

Let $S$ be a short complex of the set of module categories of $R$. Then the module category cycle isomorphism of $S$ is an isomorphism of the cycle of $S$ and $\operatorname{K}$ applied to the explicit left homology data of $S$ defined as the isomorphism of the explicit left homology data of $S$.

the module category homology isomorphism of S (from the name)

Let $S$ be a short complex of the set of module categories of $R$. Then the module category homology isomorphism of $S$ is an isomorphism of the homology of $S$ and $\operatorname{H}$ applied to the explicit left homology data of $S$ defined as the homology isomorphism of the explicit left homology data of $S$.

the explicit left homology data of S (from the docstring)

Let $S$ be a short complex of the set of module categories of $R$. Then the explicit left homology data of $S$ is a left homology data of $S$.

the module category of f and g (from the name)

Let $f$ be a linear map of $x_{1}$ and $x_{2}$. Let $g$ be a linear map of $x_{2}$ and $x_{3}$ such that the composition of $g$ and $f$ is equal to $0$. Then the module category of $f$ and $g$ is a short complex of the set of module categories of $R$.

the module category of f and g (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{2}$ and $x_{3}$ such that the range of the homomorphism of $f$ is less than or equal to the kernel of the homomorphism of $g$. Then the module category of $f$ and $g$ is a short complex of the set of module categories of $R$.

Let $S$ be a short complex of the set of module categories of $R$. Then $\operatorname{moduleCatOpcyclesIso}$ applied to $S$ is an isomorphism of $\operatorname{opcycles}$ applied to $S$ and $\operatorname{of}$ applied to $R$ and the set of quotients of the set of carriers of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and the range of the homomorphism of $\operatorname{f}$ applied to $S$ defined as the composition of the canonical isomorphism of $S$ and the categorical cokernel in $\operatorname{f}$ applied to $S$.

the module category to cycle of S (from the name)

Let $S$ be a short complex of the set of module categories of $R$. Then the module category to cycle of $S$ is a linear map of the set of carriers of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{hom} (\operatorname{g} (S)))}{x_{1}})}$ defined as $\operatorname{codRestrict}$ applied to the kernel of the homomorphism of $\operatorname{g}$ applied to $S$, the homomorphism of $\operatorname{f}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_moduleCat\_zero\_apply}$ applied to $S$.

the short complex kernel of f (from the name)

Let $f$ be a linear map of $M$ and $N$. Then the short complex kernel of $f$ is a short complex of the set of module categories of $R$.

the short complex in f (from the docstring)

Let $f$ be a linear map of $M$ and $N$. Let $g$ be a linear map of $N$ and $L$ such that the composition of $g$ and $f$ is equal to $0$. Then the short complex in $f$ is a short complex of the set of module categories of $R$.

the short complex of f and g (from the name)

Let $\mathrm{eM}$ be a linear equivalence of $M$ and $\mathrm{M'}$. Let $\mathrm{eN}$ be a linear equivalence of $N$ and $\mathrm{N'}$. Let $\mathrm{eL}$ be a linear equivalence of $L$ and $\mathrm{L'}$. Let $f$ be a linear map of $\mathrm{M'}$ and $\mathrm{N'}$. Let $g$ be a linear map of $\mathrm{N'}$ and $\mathrm{L'}$ such that the composition of $g$ and $f$ is equal to $0$. Then the short complex of $f$ and $g$ is a short complex of the set of module categories of $R$.

the sum of x8 and x9 (from the name)

Let $x_{8}$ and $x_{9}$ be homology map data of $x_{6}$ and $x_{7}$. Then the sum of $x_{8}$ and $x_{9}$ is a homology map data of $x_{6}$ and $x_{7}$ defined as $\operatorname{mk}$ applied to the sum of the left of $x_{8}$ and the left of $x_{9}$ and the sum of the right of $x_{8}$ and the right of $x_{9}$.

the negation of x7 (from the name)

Let $x_{7}$ be a homology map data of $x_{5}$ and $x_{6}$. Then the negation of $x_{7}$ is a homology map data of $x_{5}$ and $x_{6}$ defined as $\operatorname{mk}$ applied to the negation of the left of $x_{7}$ and the negation of the right of $x_{7}$.

homotopy of x4 and x5 (from the name)

Let $x_{4}$ and $x_{5}$ be homomorphisms of $x_{2}$ and $x_{3}$. Then the homotopies of $x_{4}$ and $x_{5}$ are a basic type.

the sum of h and #2 (from the name)

Let $h$ be a homotopy of $x_{4}$ and $x_{5}$. Let $\mathrm{h'}$ be a homotopy of $x_{6}$ and $x_{7}$. Then the sum of $h$ and $\mathrm{h'}$ is a homotopy of $x_{4} + x_{6}$ and $x_{5} + x_{7}$.

the composition of h and #2 (from the name)

Let $h$ be a homotopy of $x_{5}$ and $x_{6}$. Let $\mathrm{h'}$ be a homotopy of $x_{7}$ and $x_{8}$. Then the composition of $h$ and $\mathrm{h'}$ is a homotopy of the composition of $x_{5}$ and $x_{7}$ and the composition of $x_{6}$ and $x_{8}$ defined as the composition of the right composition of $h$ and $x_{7}$ and the left composition of $\mathrm{h'}$ and $x_{6}$.

the left composition of h and x7 (from the name)

Let $h$ be a homotopy of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{2}$. Then the left composition of $h$ and $x_{7}$ is a homotopy of the composition of $x_{7}$ and $x_{5}$ and the composition of $x_{7}$ and $x_{6}$.

the right composition of h and x7 (from the name)

Let $h$ be a homotopy of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the right composition of $h$ and $x_{7}$ is a homotopy of the composition of $x_{5}$ and $x_{7}$ and the composition of $x_{6}$ and $x_{7}$.

the equivalence difference zero of x4 and x5 (from the name)

Let $x_{4}$ and $x_{5}$ be homomorphisms of $x_{2}$ and $x_{3}$. Then the equivalence difference zero of $x_{4}$ and $x_{5}$ is an equivalence from the set of homotopies of $x_{4}$ and $x_{5}$ to the set of homotopies of $x_{4} - x_{5}$ and $0$.

Let $\mathrm{self}$ be a homotopy of $x_{4}$ and $x_{5}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_Homotopy\_\_h\_u2080\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homotopy of $x_{4}$ and $x_{5}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_Homotopy\_\_h\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homotopy of $x_{4}$ and $x_{5}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_Homotopy\_\_h\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{3}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homotopy of $x_{4}$ and $x_{5}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_Homotopy\_\_h\_u2083\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{3}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the negation of h (from the name)

Let $h$ be a homotopy of $x_{4}$ and $x_{5}$. Then the negation of $h$ is a homotopy of $\operatorname{neg}$ applied to $x_{4}$ and $\operatorname{neg}$ applied to $x_{5}$.

the homotopy of h (from the name)

Assume that $\EqtMACRoH {x_{4}}{x_{5}}$. Then the homotopy of $h$ is a homotopy of $x_{4}$ and $x_{5}$.

the homotopy of x6 and x7 (from the name)

Let $x_{2}$ and $x_{3}$ be short complexes of $C$. Let $x_{4}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$ such that the composition of $x_{4}$ and $\operatorname{f}$ applied to $x_{3}$ is equal to $0$. Let $x_{5}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$. Let $x_{6}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{3}$. Let $x_{7}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{3}$ such that the composition of $\operatorname{g}$ applied to $x_{2}$ and $x_{7}$ is equal to $0$. Then the homotopy of $x_{6}$ and $x_{7}$ is a homotopy of $\operatorname{nullHomotopic}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $h$, $x_{5}$, $x_{6}$, $x_{7}$ and $h_{1}$ and $0$.

the opposite of h (from the name)

Let $h$ be a homotopy of $x_{4}$ and $x_{5}$. Then the opposite of $h$ is a homotopy of the opposite morphism in $x_{4}$ and the opposite morphism in $x_{5}$.

the identity of x4 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the identity of $x_{4}$ is a homotopy of $x_{4}$ and $x_{4}$.

the difference of h and #2 (from the name)

Let $h$ be a homotopy of $x_{4}$ and $x_{5}$. Let $\mathrm{h'}$ be a homotopy of $x_{6}$ and $x_{7}$. Then the difference of $h$ and $\mathrm{h'}$ is a homotopy of $x_{4} - x_{6}$ and $x_{5} - x_{7}$.

the inverse of h (from the name)

Let $h$ be a homotopy of $x_{4}$ and $x_{5}$. Then the inverse of $h$ is a homotopy of $x_{5}$ and $x_{4}$.

the composition of x7 and x8 (from the name)

Let $x_{7}$ be a homotopy of $x_{4}$ and $x_{5}$. Let $x_{8}$ be a homotopy of $x_{5}$ and $x_{6}$. Then the composition of $x_{7}$ and $x_{8}$ is a homotopy of $x_{4}$ and $x_{6}$.

the opposite of h (from the name)

Let $h$ be a homotopy of $x_{4}$ and $x_{5}$. Then the opposite of $h$ is a homotopy of the opposite map of $x_{4}$ and the opposite map of $x_{5}$.

homotopy equivalence of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be short complexes of $C$. Then the homotopy equivalences of $x_{2}$ and $x_{3}$ are a basic type.

the forward direction of self (from the docstring)

Let $\mathrm{self}$ be a homotopy equivalence of $x_{2}$ and $x_{3}$. Then the forward direction of $\mathrm{self}$ is a homomorphism of $x_{2}$ and $x_{3}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the homotopy homomorphism inverse identity of self (from the name)

Let $\mathrm{self}$ be a homotopy equivalence of $x_{2}$ and $x_{3}$. Then the homotopy homomorphism inverse identity of $\mathrm{self}$ is a homotopy of the composition of the forward direction of $\mathrm{self}$ and the inverse of $\mathrm{self}$ and the identity morphism of $x_{2}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the homotopy inverse homomorphism identity of self (from the name)

Let $\mathrm{self}$ be a homotopy equivalence of $x_{2}$ and $x_{3}$. Then the homotopy inverse homomorphism identity of $\mathrm{self}$ is a homotopy of the composition of the inverse of $\mathrm{self}$ and the forward direction of $\mathrm{self}$ and the identity morphism of $x_{3}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the inverse of self (from the name)

Let $\mathrm{self}$ be a homotopy equivalence of $x_{2}$ and $x_{3}$. Then the inverse of $\mathrm{self}$ is a homomorphism of $x_{3}$ and $x_{2}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the identity of S (from the name)

Let $S$ be a short complex of $C$. Then the identity of $S$ is a homotopy equivalence of $S$ and $S$.

the inverse of e (from the docstring)

Let $e$ be a homotopy equivalence of $x_{2}$ and $x_{3}$. Then the inverse of $e$ is a homotopy equivalence of $x_{3}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the inverse of $e$, the forward direction of $e$, the homotopy inverse homomorphism identity of $e$ and the homotopy homomorphism inverse identity of $e$.

the composition of e and #2 (from the name)

Let $e$ be a homotopy equivalence of $x_{2}$ and $x_{3}$. Let $\mathrm{e'}$ be a homotopy equivalence of $x_{3}$ and $x_{4}$. Then the composition of $e$ and $\mathrm{e'}$ is a homotopy equivalence of $x_{2}$ and $x_{4}$.

the sum of x8 and x9 (from the name)

Let $x_{8}$ and $x_{9}$ be left homology map data of $x_{6}$ and $x_{7}$. Then the sum of $x_{8}$ and $x_{9}$ is a left homology map data of $x_{6}$ and $x_{7}$.

the negation of x7 (from the name)

Let $x_{7}$ be a left homology map data of $x_{5}$ and $x_{6}$. Then the negation of $x_{7}$ is a left homology map data of $x_{5}$ and $x_{6}$.

the left homology map data of x8 and x9 (from the name)

Let $x_{4}$ be a left homology data of $x_{2}$. Let $x_{5}$ be a left homology data of $x_{3}$. Let $x_{6}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$ such that the composition of $x_{6}$ and $\operatorname{f}$ applied to $x_{3}$ is equal to $0$. Let $x_{7}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$. Let $x_{8}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{3}$. Let $x_{9}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{3}$ such that the composition of $\operatorname{g}$ applied to $x_{2}$ and $x_{9}$ is equal to $0$. Then the left homology map data of $x_{8}$ and $x_{9}$ is a left homology map data of $x_{4}$ and $x_{5}$.

the sum of x8 and x9 (from the name)

Let $x_{8}$ and $x_{9}$ be right homology map data of $x_{6}$ and $x_{7}$. Then the sum of $x_{8}$ and $x_{9}$ is a right homology map data of $x_{6}$ and $x_{7}$.

the negation of x7 (from the name)

Let $x_{7}$ be a right homology map data of $x_{5}$ and $x_{6}$. Then the negation of $x_{7}$ is a right homology map data of $x_{5}$ and $x_{6}$.

the right homology map data of x8 and x9 (from the name)

Let $x_{4}$ be a right homology data of $x_{2}$. Let $x_{5}$ be a right homology data of $x_{3}$. Let $x_{6}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$ such that the composition of $x_{6}$ and $\operatorname{f}$ applied to $x_{3}$ is equal to $0$. Let $x_{7}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$. Let $x_{8}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{3}$. Let $x_{9}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{3}$ such that the composition of $\operatorname{g}$ applied to $x_{2}$ and $x_{9}$ is equal to $0$. Then the right homology map data of $x_{8}$ and $x_{9}$ is a right homology map data of $x_{4}$ and $x_{5}$.

Let $x_{2}$ and $x_{3}$ be short complexes of $C$. Let $x_{4}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$ such that the composition of $x_{4}$ and $\operatorname{f}$ applied to $x_{3}$ is equal to $0$. Let $x_{5}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$. Let $x_{6}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{3}$. Let $x_{7}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{3}$ such that the composition of $\operatorname{g}$ applied to $x_{2}$ and $x_{7}$ is equal to $0$. Then $\operatorname{nullHomotopic}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $h$, $x_{5}$, $x_{6}$, $x_{7}$ and $h_{1}$ is a homomorphism of $x_{2}$ and $x_{3}$.

F preserves a homology (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ preserves a homology.

Let $F$ be a functor of $C$ and $D$. Let $S$ be a short complex of $C$. Then we can say that $\operatorname{PreservesLeftHomologyOf}$ holds for $F$ and $S$.

Let $F$ be a functor of $C$ and $D$. Let $S$ be a short complex of $C$. Then we can say that $\operatorname{PreservesRightHomologyOf}$ holds for $F$ and $S$.

the map of h and F (from the name)

Let $h$ be a homology data of $S$. Let $F$ be a functor of $C$ and $D$. Then the map of $h$ and $F$ is a homology data of the map of $S$ and $F$.

the map of x9 and F (from the name)

Let $x_{9}$ be a homology map data of $x_{7}$ and $x_{8}$. Let $F$ be a functor of $C$ and $D$. Then the map of $x_{9}$ and $F$ is a homology map data of the map of $x_{7}$ and $F$ and the map of $x_{8}$ and $F$ defined as $\operatorname{mk}$ applied to the map of the left of $x_{9}$ and $F$ and the map of the right of $x_{9}$ and $F$.

the natural transformation application of h6 and x4 (from the name)

Let $h_{6}$ be a homology data of $S$. Let $x_{4}$ be a homomorphism of $F$ and $G$. Then the natural transformation application of $h_{6}$ and $x_{4}$ is a homology map data of the map of $h_{6}$ and $F$ and the map of $h_{6}$ and $G$ defined as $\operatorname{mk}$ applied to the natural transformation application of the left of $h_{6}$ and $x_{4}$ and the natural transformation application of the right of $h_{6}$ and $x_{4}$.

Let $h$ be a left homology data of $S$. Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{IsPreservedBy}$ holds for $h$ and $F$.

the map of h and F (from the name)

Let $h$ be a left homology data of $S$. Let $F$ be a functor of $C$ and $D$. Then the map of $h$ and $F$ is a left homology data of the map of $S$ and $F$.

the map of x9 and F (from the name)

Let $x_{9}$ be a left homology map data of $x_{7}$ and $x_{8}$. Let $F$ be a functor of $C$ and $D$. Then the map of $x_{9}$ and $F$ is a left homology map data of the map of $x_{7}$ and $F$ and the map of $x_{8}$ and $F$.

the natural transformation application of h4 and x4 (from the name)

Let $h_{4}$ be a left homology data of $S$. Let $x_{4}$ be a homomorphism of $F$ and $G$. Then the natural transformation application of $h_{4}$ and $x_{4}$ is a left homology map data of the map of $h_{4}$ and $F$ and the map of $h_{4}$ and $G$.

Let $h$ be a right homology data of $S$. Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{IsPreservedBy}$ holds for $h$ and $F$.

the map of h and F (from the name)

Let $h$ be a right homology data of $S$. Let $F$ be a functor of $C$ and $D$. Then the map of $h$ and $F$ is a right homology data of the map of $S$ and $F$.

the map of x9 and F (from the name)

Let $x_{9}$ be a right homology map data of $x_{7}$ and $x_{8}$. Let $F$ be a functor of $C$ and $D$. Then the map of $x_{9}$ and $F$ is a right homology map data of the map of $x_{7}$ and $F$ and the map of $x_{8}$ and $F$.

the natural transformation application of h4 and x4 (from the name)

Let $h_{4}$ be a right homology data of $S$. Let $x_{4}$ be a homomorphism of $F$ and $G$. Then the natural transformation application of $h_{4}$ and $x_{4}$ is a right homology map data of the map of $h_{4}$ and $F$ and the map of $h_{4}$ and $G$.

the natural isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the natural isomorphism of $F$ is an isomorphism of the composition of the map short complex of $F$ and the cycle functor of $D$ and the composition of the cycle functor of $C$ and $F$.

the natural isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the natural isomorphism of $F$ is an isomorphism of the composition of the map short complex of $F$ and the homology functor of $D$ and the composition of the homology functor of $C$ and $F$.

the natural isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the natural isomorphism of $F$ is an isomorphism of the composition of the map short complex of $F$ and the left homology functor of $D$ and the composition of the left homology functor of $C$ and $F$.

the map cycle isomorphism of S and F (from the name)

Let $S$ be a short complex of $C$. Let $F$ be a functor of $C$ and $D$. Then the map cycle isomorphism of $S$ and $F$ is an isomorphism of the cycle of the map of $S$ and $F$ and the action of $F$ and the cycle of $S$ defined as the isomorphism of the map of the left homology data of $S$ and $F$.

the map homology isomorphism of S and F (from the name)

Let $S$ be a short complex of $C$. Let $F$ be a functor of $C$ and $D$. Then the map homology isomorphism of $S$ and $F$ is an isomorphism of the homology of the map of $S$ and $F$ and the action of $F$ and the homology of $S$ defined as the homology isomorphism of the map of the left of the homology data of $S$ and $F$.

the map homology isomorphism of S and F (from the name)

Let $S$ be a short complex of $C$. Let $F$ be a functor of $C$ and $D$. Then the map homology isomorphism of $S$ and $F$ is an isomorphism of the homology of the map of $S$ and $F$ and the action of $F$ and the homology of $S$ defined as the composition of the homology isomorphism of the map of the right of the homology data of $S$ and $F$ and the map isomorphism of $F$ and the inverse of the homology isomorphism of the right of the homology data of $S$.

the map left homology isomorphism of S and F (from the name)

Let $S$ be a short complex of $C$. Let $F$ be a functor of $C$ and $D$. Then the map left homology isomorphism of $S$ and $F$ is an isomorphism of the left homology of the map of $S$ and $F$ and the action of $F$ and the left homology of $S$ defined as the isomorphism of the map of the left homology data of $S$ and $F$.

Let $S$ be a short complex of $C$. Let $F$ be a functor of $C$ and $D$. Then $\operatorname{mapOpcyclesIso}$ applied to $S$ and $F$ is an isomorphism of $\operatorname{opcycles}$ applied to the map of $S$ and $F$ and the action of $F$ and $\operatorname{opcycles}$ applied to $S$ defined as the isomorphism of the map of the right homology data of $S$ and $F$.

the map right homology isomorphism of S and F (from the name)

Let $S$ be a short complex of $C$. Let $F$ be a functor of $C$ and $D$. Then the map right homology isomorphism of $S$ and $F$ is an isomorphism of the right homology of the map of $S$ and $F$ and the action of $F$ and the right homology of $S$ defined as the isomorphism of the map of the right homology data of $S$ and $F$.

the natural isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the natural isomorphism of $F$ is an isomorphism of the composition of the map short complex of $F$ and $\operatorname{opcyclesFunctor}$ applied to $D$ and the composition of $\operatorname{opcyclesFunctor}$ applied to $C$ and $F$.

the natural isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the natural isomorphism of $F$ is an isomorphism of the composition of the map short complex of $F$ and the right homology functor of $D$ and the composition of the right homology functor of $C$ and $F$.

the pullback of S and f (from the docstring)

Let $S$ be a short complex of $C$. Let $f$ be a homomorphism of $Y$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$. Then the pullback of $S$ and $f$ is a short complex of $C$.

the pushout of S and f (from the docstring)

Let $S$ be a short complex of $C$. Let $f$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $Y$. Then the pushout of $S$ and $f$ is a short complex of $C$.

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then we can say that $\operatorname{QuasiIso}$ holds for $x_{4}$.

S has a right homology (from the name)

Let $S$ be a short complex of $C$. Then we can say that $S$ has a right homology.

the opposite of h (from the name)

Let $h$ be a left homology data of $S$. Then the opposite of $h$ is a right homology data of the opposite of $S$.

the opposite of h (from the name)

Let $h$ be a left homology data of $S$. Then the opposite of $h$ is a right homology data of the opposite of $S$.

the opposite of x7 (from the name)

Let $x_{7}$ be a left homology map data of $x_{5}$ and $x_{6}$. Then the opposite of $x_{7}$ is a right homology map data of the opposite of $x_{6}$ and the opposite of $x_{5}$.

the opposite of x7 (from the name)

Let $x_{7}$ be a left homology map data of $x_{5}$ and $x_{6}$. Then the opposite of $x_{7}$ is a right homology map data of the opposite of $x_{6}$ and the opposite of $x_{5}$.

right homology data of S (from the name)

Let $S$ be a short complex of $C$. Then the right homology data of $S$ are a basic type.

Let $\mathrm{self}$ be a right homology data of $S$. Then $\operatorname{H}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a right homology data of $S$. Then $\operatorname{Q}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the copy of eQ and eH (from the name)

Let $h$ be a right homology data of $S$. Let $\mathrm{eQ}$ be an isomorphism of $\mathrm{Q'}$ and $\operatorname{Q}$ applied to $h$. Let $\mathrm{eH}$ be an isomorphism of $\mathrm{H'}$ and $\operatorname{H}$ applied to $h$. Then the copy of $\mathrm{eQ}$ and $\mathrm{eH}$ is a right homology data of $S$.

Let $h$ be a right homology data of $S$. Let $k$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $A$ such that the composition of $\operatorname{f}$ applied to $S$ and $k$ is equal to $0$. Then $\operatorname{descH}$ applied to $h$, $k$ and $\mathrm{hk}$ is a homomorphism of $\operatorname{H}$ applied to $h$ and $A$ defined as the composition of the inclusion of $h$ and $\operatorname{descQ}$ applied to $h$, $k$ and $\mathrm{hk}$.

Let $h$ be a right homology data of $S$. Let $k$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $A$ such that the composition of $\operatorname{f}$ applied to $S$ and $k$ is equal to $0$. Then $\operatorname{descQ}$ applied to $h$, $k$ and $\mathrm{hk}$ is a homomorphism of $\operatorname{Q}$ applied to $h$ and $A$ defined as $\operatorname{desc}$ applied to $\operatorname{hp}$ applied to $h$ and the projection of $k$ and $\mathrm{hk}$.

Let $h$ be a right homology data of $S$. Then $\operatorname{g'}$ applied to $h$ is a homomorphism of $\operatorname{Q}$ applied to $h$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ defined as $\operatorname{descQ}$ applied to $h$, $\operatorname{g}$ applied to $S$ and $\operatorname{zero}$ applied to $S$.

Let $\mathrm{self}$ be a right homology data of $S$. Then $\operatorname{hp}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\operatorname{p}$ applied to $\mathrm{self}$ and $\operatorname{wp}$ applied to $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

the inclusion of self (from the name)

Let $\mathrm{self}$ be a right homology data of $S$. Then the inclusion of $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_RightHomologyData\_\_w\_u3b9\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$.

the inclusion of h (from the name)

Let $h$ be a right homology data of $S$. Then the inclusion of $h$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $h$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_RightHomologyData\_\_\_u3b9\_\_g'}$ applied to $h$ defined as the inclusion of $h$.

the lift of h and k (from the name)

Let $h$ be a right homology data of $S$. Let $k$ be a homomorphism of $A$ and $\operatorname{Q}$ applied to $h$ such that the composition of $k$ and $\operatorname{g'}$ applied to $h$ is equal to $0$. Then the lift of $h$ and $k$ is a homomorphism of $A$ and $\operatorname{H}$ applied to $h$ defined as the lift of the inclusion of $h$ and the inclusion of $k$ and $\mathrm{hk}$.

the right homology data of x4 and h (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $h$ be a right homology data of $x_{2}$. Then the right homology data of $x_{4}$ and $h$ is a right homology data of $x_{3}$ defined as the opposite of the left homology data of the opposite morphism in $x_{4}$ and the opposite of $h$.

the right homology data of x4 and h (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $h$ be a right homology data of $x_{3}$. Then the right homology data of $x_{4}$ and $h$ is a right homology data of $x_{2}$ defined as the opposite of the left homology data of the opposite morphism in $x_{4}$ and the opposite of $h$.

the right homology data of S and hg (from the name)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{g} (S)}{0}$. Then the right homology data of $S$ and $\mathrm{hg}$ is a right homology data of $S$.

the right homology data of S (from the name)

Let $S$ be a short complex of $C$. Then the right homology data of $S$ is a right homology data of $S$.

the right homology data of S and hf (from the name)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{f} (S)}{0}$. Then the right homology data of $S$ and $\mathrm{hf}$ is a right homology data of $S$.

the right homology data of c and hc (from the name)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{g} (S)}{0}$. Let $c$ be a cokernel cofork of $\operatorname{f}$ applied to $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the right homology data of $c$ and $\mathrm{hc}$ is a right homology data of $S$.

the right homology data of c and hc (from the name)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{f} (S)}{0}$. Let $c$ be a kernel fork of $\operatorname{g}$ applied to $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the right homology data of $c$ and $\mathrm{hc}$ is a right homology data of $S$.

the right homology data of e and x4 (from the name)

Let $e$ be an isomorphism of $x_{2}$ and $x_{3}$. Let $x_{4}$ be a right homology data of $x_{2}$. Then the right homology data of $e$ and $x_{4}$ is a right homology data of $x_{3}$ defined as the right homology data of the homomorphism of $e$ and $x_{4}$.

the right homology data of S (from the name)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{f} (S)}{0}$ and $\EqtMACRoH {\operatorname{g} (S)}{0}$. Then the right homology data of $S$ is a right homology data of $S$.

the opposite of h (from the name)

Let $h$ be a right homology data of $S$. Then the opposite of $h$ is a left homology data of the opposite of $S$.

the isomorphism of h (from the docstring)

Let $h$ be a right homology data of $S$. Then the isomorphism of $h$ is an isomorphism of $\operatorname{opcycles}$ applied to $S$ and $\operatorname{Q}$ applied to $h$ defined as $\operatorname{opcyclesMapIso'}$ applied to the identity of $S$, the right homology data of $S$ and $h$.

Let $\mathrm{self}$ be a right homology data of $S$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $\operatorname{Q}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the isomorphism of h (from the docstring)

Let $h$ be a right homology data of $S$. Then the isomorphism of $h$ is an isomorphism of the right homology of $S$ and $\operatorname{H}$ applied to $h$ defined as the right homology map isomorphism of the right homology data of $S$ and $h$.

the opposite of h (from the name)

Let $h$ be a right homology data of $S$. Then the opposite of $h$ is a left homology data of the opposite of $S$.

the inclusion of self (from the name)

Let $\mathrm{self}$ be a right homology data of $S$. Then the inclusion of $\mathrm{self}$ is a homomorphism of $\operatorname{H}$ applied to $\mathrm{self}$ and $\operatorname{Q}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

right homology map data of x5 and x6 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a right homology data of $x_{2}$. Let $x_{6}$ be a right homology data of $x_{3}$. Then the right homology map data of $x_{5}$ and $x_{6}$ are a basic type.

the composition of right homology map data of x10 and x11 (from the docstring)

Let $x_{10}$ be a right homology map data of $x_{7}$ and $x_{8}$. Let $x_{11}$ be a right homology map data of $x_{8}$ and $x_{9}$. Then the composition of right homology map data of $x_{10}$ and $x_{11}$ is a right homology map data of $x_{7}$ and $x_{9}$.

the compatibility of c and hc (from the name)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{f} (S)}{0}$ and $\EqtMACRoH {\operatorname{g} (S)}{0}$. Let $c$ be a cokernel cofork of $\operatorname{f}$ applied to $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the compatibility of $c$ and $\mathrm{hc}$ is a right homology map data of the right homology data of $S$ and the right homology data of $c$ and $\mathrm{hc}$.

the compatibility of c and hc (from the name)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{f} (S)}{0}$ and $\EqtMACRoH {\operatorname{g} (S)}{0}$. Let $c$ be a kernel fork of $\operatorname{g}$ applied to $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the compatibility of $c$ and $\mathrm{hc}$ is a right homology map data of the right homology data of $c$ and $\mathrm{hc}$ and the right homology data of $S$.

the identity of h (from the name)

Let $h$ be a right homology data of $S$. Then the identity of $h$ is a right homology map data of $h$ and $h$.

the right homology map data of x4 and h (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $h$ be a right homology data of $x_{2}$. Then the right homology map data of $x_{4}$ and $h$ is a right homology map data of $h$ and the right homology data of $x_{4}$ and $h$.

the right homology map data of x4 and h (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $h$ be a right homology data of $x_{3}$. Then the right homology map data of $x_{4}$ and $h$ is a right homology map data of the right homology data of $x_{4}$ and $h$ and $h$.

the right homology map data of x8 and f (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Assume that $\EqtMACRoH {\operatorname{g} (x_{2})}{0}$. Let $x_{5}$ be a cokernel cofork of $\operatorname{f}$ applied to $x_{2}$. Let $x_{6}$ be an element of $\operatorname{IsColimit}$ applied to $x_{5}$. Assume that $\EqtMACRoH {\operatorname{g} (x_{3})}{0}$. Let $x_{7}$ be a cokernel cofork of $\operatorname{f}$ applied to $x_{3}$. Let $x_{8}$ be an element of $\operatorname{IsColimit}$ applied to $x_{7}$. Let $f$ be a homomorphism of $\operatorname{pt}$ applied to $x_{5}$ and $\operatorname{pt}$ applied to $x_{7}$ such that the composition of $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2082\_}$ applied to $x_{4}$ and the projection of $x_{7}$ is equal to the composition of the projection of $x_{5}$ and $f$. Then the right homology map data of $x_{8}$ and $f$ is a right homology map data of the right homology data of $x_{5}$ and $x_{6}$ and the right homology data of $x_{7}$ and $x_{8}$.

the right homology map data of x8 and f (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Assume that $\EqtMACRoH {\operatorname{f} (x_{2})}{0}$. Let $x_{5}$ be a kernel fork of $\operatorname{g}$ applied to $x_{2}$. Let $x_{6}$ be an element of $\operatorname{IsLimit}$ applied to $x_{5}$. Assume that $\EqtMACRoH {\operatorname{f} (x_{3})}{0}$. Let $x_{7}$ be a kernel fork of $\operatorname{g}$ applied to $x_{3}$. Let $x_{8}$ be an element of $\operatorname{IsLimit}$ applied to $x_{7}$. Let $f$ be a homomorphism of $\operatorname{pt}$ applied to $x_{5}$ and $\operatorname{pt}$ applied to $x_{7}$ such that the composition of the inclusion of $x_{5}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2082\_}$ applied to $x_{4}$ is equal to the composition of $f$ and the inclusion of $x_{7}$. Then the right homology map data of $x_{8}$ and $f$ is a right homology map data of the right homology data of $x_{5}$ and $x_{6}$ and the right homology data of $x_{7}$ and $x_{8}$.

the right homology map data of x4 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Assume that $\EqtMACRoH {\operatorname{f} (x_{2})}{0}$. Assume that $\EqtMACRoH {\operatorname{g} (x_{2})}{0}$. Assume that $\EqtMACRoH {\operatorname{f} (x_{3})}{0}$. Assume that $\EqtMACRoH {\operatorname{g} (x_{3})}{0}$. Then the right homology map data of $x_{4}$ is a right homology map data of the right homology data of $x_{2}$ and the right homology data of $x_{3}$.

the opposite of x7 (from the name)

Let $x_{7}$ be a right homology map data of $x_{5}$ and $x_{6}$. Then the opposite of $x_{7}$ is a left homology map data of the opposite of $x_{6}$ and the opposite of $x_{5}$.

the opposite of x7 (from the name)

Let $x_{7}$ be a right homology map data of $x_{5}$ and $x_{6}$. Then the opposite of $x_{7}$ is a left homology map data of the opposite of $x_{6}$ and the opposite of $x_{5}$.

the zero of x4 and x5 (from the name)

Let $x_{4}$ be a right homology data of $x_{2}$. Let $x_{5}$ be a right homology data of $x_{3}$. Then the zero of $x_{4}$ and $x_{5}$ is a right homology map data of $x_{4}$ and $x_{5}$.

Let $\mathrm{self}$ be a right homology map data of $x_{5}$ and $x_{6}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_RightHomologyMapData\_\_\_u3c6\_H}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{H}$ applied to $x_{5}$ and $\operatorname{H}$ applied to $x_{6}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a right homology map data of $x_{5}$ and $x_{6}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_RightHomologyMapData\_\_\_u3c6\_Q}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{Q}$ applied to $x_{5}$ and $\operatorname{Q}$ applied to $x_{6}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the cycle opposite isomorphism of S (from the name)

Let $S$ be a short complex of $C$. Then the cycle opposite isomorphism of $S$ is an isomorphism of the cycle of the opposite of $S$ and $\operatorname{op}$ applied to $\operatorname{opcycles}$ applied to $S$ defined as the isomorphism of the opposite of the right homology data of $S$.

Let $S$ be a short complex of $C$. Let $k$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $A$ such that the composition of $\operatorname{f}$ applied to $S$ and $k$ is equal to $0$. Then $\operatorname{descOpcycles}$ applied to $S$, $k$ and $\mathrm{hk}$ is a homomorphism of $\operatorname{opcycles}$ applied to $S$ and $A$ defined as $\operatorname{descQ}$ applied to the right homology data of $S$, $k$ and $\mathrm{hk}$.

Let $S$ be a short complex of $C$. Let $k$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $A$ such that the composition of $\operatorname{f}$ applied to $S$ and $k$ is equal to $0$. Then $\operatorname{descRightHomology}$ applied to $S$, $k$ and $\mathrm{hk}$ is a homomorphism of the right homology of $S$ and $A$ defined as the composition of the right homology inclusion of $S$ and $\operatorname{descOpcycles}$ applied to $S$, $k$ and $\mathrm{hk}$.

Let $S$ be a short complex of $C$. Then $\operatorname{fromOpcycles}$ applied to $S$ is a homomorphism of $\operatorname{opcycles}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ defined as $\operatorname{g'}$ applied to the right homology data of $S$.

the natural transformation of C (from the docstring)

Let $C$ be a set. Then the natural transformation of $C$ is a homomorphism of $\operatorname{opcyclesFunctor}$ applied to $C$ and the third projection functor.

the isomorphism from the point of S and hcc (from the docstring)

Let $S$ be a short complex of $C$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Then the isomorphism from the point of $S$ and $\mathrm{hcc}$ is an isomorphism of $\operatorname{pt}$ applied to $\mathrm{cc}$ and $\operatorname{opcycles}$ applied to $S$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\mathrm{hcc}$ and $\operatorname{opcyclesIsCokernel}$ applied to $S$.

the opposite of the left homology functor of C (from the docstring)

Let $C$ be a set. Then the opposite of the left homology functor of $C$ is an isomorphism of the opposite of the left homology functor of $C$ and the composition of the obvious functor of $C$ and the right homology functor of the set of opposites of $C$.

the left homology in the opposite category of the opposite of S (from the docstring)

Let $S$ be a short complex of $C$. Then the left homology in the opposite category of the opposite of $S$ is an isomorphism of the left homology of the opposite of $S$ and $\operatorname{op}$ applied to the right homology of $S$ defined as the isomorphism of the opposite of the right homology data of $S$.

Let $S$ be a short complex of $C$. Then $\operatorname{opcycles}$ applied to $S$ is an element of $C$ defined as $\operatorname{Q}$ applied to the right homology data of $S$.

Let $C$ be a set. Then $\operatorname{opcyclesFunctor}$ applied to $C$ is a functor of the set of short complexes of $C$ and $C$.

Let $S$ be a short complex of $C$. Then $\operatorname{opcyclesIsCokernel}$ applied to $S$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\operatorname{pOpcycles}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_f\_pOpcycles}$ applied to $S$ defined as $\operatorname{hp}$ applied to the right homology data of $S$.

the canonical isomorphism of S (from the docstring)

Let $S$ be a short complex of $C$. Then the canonical isomorphism of $S$ is an isomorphism of $\operatorname{opcycles}$ applied to $S$ and the cokernel of $\operatorname{f}$ applied to $S$.

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{g} (S)}{0}$. Then $\operatorname{opcyclesIsoRightHomology}$ applied to $S$ and $\mathrm{hg}$ is an isomorphism of $\operatorname{opcycles}$ applied to $S$ and the right homology of $S$ defined as the inverse of $\operatorname{asIso}$ applied to the right homology inclusion of $S$.

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{f} (S)}{0}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_opcyclesIsoX\_u2082\_}$ applied to $S$ and $\mathrm{hf}$ is an isomorphism of $\operatorname{opcycles}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ defined as the inverse of $\operatorname{asIso}$ applied to $\operatorname{pOpcycles}$ applied to $S$.

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then $\operatorname{opcyclesMap}$ applied to $x_{4}$ is a homomorphism of $\operatorname{opcycles}$ applied to $x_{2}$ and $\operatorname{opcycles}$ applied to $x_{3}$ defined as $\operatorname{opcyclesMap'}$ applied to $x_{4}$, the right homology data of $x_{2}$ and the right homology data of $x_{3}$.

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a right homology data of $x_{2}$. Let $x_{6}$ be a right homology data of $x_{3}$. Then $\operatorname{opcyclesMap'}$ applied to $x_{4}$, $x_{5}$ and $x_{6}$ is a homomorphism of $\operatorname{Q}$ applied to $x_{5}$ and $\operatorname{Q}$ applied to $x_{6}$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_RightHomologyMapData\_\_\_u3c6\_Q}$ applied to the right homology map data of $x_{5}$ and $x_{6}$.

the isomorphism of e (from the docstring)

Let $e$ be an isomorphism of $x_{2}$ and $x_{3}$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{opcycles}$ applied to $x_{2}$ and $\operatorname{opcycles}$ applied to $x_{3}$.

Let $e$ be an isomorphism of $x_{2}$ and $x_{3}$. Let $x_{4}$ be a right homology data of $x_{2}$. Let $x_{5}$ be a right homology data of $x_{3}$. Then $\operatorname{opcyclesMapIso'}$ applied to $e$, $x_{4}$ and $x_{5}$ is an isomorphism of $\operatorname{Q}$ applied to $x_{4}$ and $\operatorname{Q}$ applied to $x_{5}$.

Let $S$ be a short complex of $C$. Then $\operatorname{opcyclesOpIso}$ applied to $S$ is an isomorphism of $\operatorname{opcycles}$ applied to the opposite of $S$ and $\operatorname{op}$ applied to the cycle of $S$ defined as the isomorphism of the opposite of the left homology data of $S$.

Let $S$ be a short complex of $C$. Then $\operatorname{pOpcycles}$ applied to $S$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $\operatorname{opcycles}$ applied to $S$ defined as $\operatorname{p}$ applied to the right homology data of $S$.

the natural transformation of C (from the docstring)

Let $C$ be a set. Then the natural transformation of $C$ is a homomorphism of the second projection functor and $\operatorname{opcyclesFunctor}$ applied to $C$.

the right homology of S (from the docstring)

Let $S$ be a short complex of $C$. Then the right homology of $S$ is an element of $C$ defined as $\operatorname{H}$ applied to the right homology data of $S$.

the right homology data of S (from the name)

Let $S$ be a short complex of $C$. Then the right homology data of $S$ is a right homology data of $S$ defined as $\operatorname{some}$ applied to $\operatorname{condition}$.

the right homology functor of C (from the docstring)

Let $C$ be a set. Then the right homology functor of $C$ is a functor of the set of short complexes of $C$ and $C$.

the opposite of the right homology functor of C (from the docstring)

Let $C$ be a set. Then the opposite of the right homology functor of $C$ is an isomorphism of the opposite of the right homology functor of $C$ and the composition of the obvious functor of $C$ and the left homology functor of the set of opposites of $C$.

Let $S$ be a short complex of $C$. Then $\operatorname{rightHomologyIsKernel}$ applied to $S$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the right homology inclusion of $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_rightHomology\_u3b9\_\_comp\_fromOpcycles}$ applied to $S$ defined as the inclusion of the right homology data of $S$.

the right homology of S (from the docstring)

Let $S$ be a short complex of $C$. Then the right homology of $S$ is an isomorphism of the right homology of $S$ and the kernel of $\operatorname{desc}$ applied to $\operatorname{f}$ applied to $S$, $\operatorname{g}$ applied to $S$ and $\operatorname{zero}$ applied to $S$ defined as the isomorphism of the right homology data of $S$.

the right homology map of x4 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the right homology map of $x_{4}$ is a homomorphism of the right homology of $x_{2}$ and the right homology of $x_{3}$ defined as the right homology map of the right homology data of $x_{2}$ and the right homology data of $x_{3}$.

the right homology map of x5 and x6 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a right homology data of $x_{2}$. Let $x_{6}$ be a right homology data of $x_{3}$. Then the right homology map of $x_{5}$ and $x_{6}$ is a homomorphism of $\operatorname{H}$ applied to $x_{5}$ and $\operatorname{H}$ applied to $x_{6}$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_RightHomologyMapData\_\_\_u3c6\_H}$ applied to the right homology map data of $x_{5}$ and $x_{6}$.

the right homology map data of x5 and x6 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a right homology data of $x_{2}$. Let $x_{6}$ be a right homology data of $x_{3}$. Then the right homology map data of $x_{5}$ and $x_{6}$ is a right homology map data of $x_{5}$ and $x_{6}$ defined as $\operatorname{default}$.

the isomorphism of e (from the docstring)

Let $e$ be an isomorphism of $x_{2}$ and $x_{3}$. Then the isomorphism of $e$ is an isomorphism of the right homology of $x_{2}$ and the right homology of $x_{3}$.

the right homology map isomorphism of x4 and x5 (from the name)

Let $e$ be an isomorphism of $x_{2}$ and $x_{3}$. Let $x_{4}$ be a right homology data of $x_{2}$. Let $x_{5}$ be a right homology data of $x_{3}$. Then the right homology map isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $\operatorname{H}$ applied to $x_{4}$ and $\operatorname{H}$ applied to $x_{5}$.

the right homology in the opposite category of the opposite of S (from the docstring)

Let $S$ be a short complex of $C$. Then the right homology in the opposite category of the opposite of $S$ is an isomorphism of the right homology of the opposite of $S$ and $\operatorname{op}$ applied to the left homology of $S$ defined as the isomorphism of the opposite of the left homology data of $S$.

the right homology inclusion of S (from the name)

Let $S$ be a short complex of $C$. Then the right homology inclusion of $S$ is a homomorphism of the right homology of $S$ and $\operatorname{opcycles}$ applied to $S$ defined as the inclusion of the right homology data of $S$.

the natural transformation of C (from the docstring)

Let $C$ be a set. Then the natural transformation of $C$ is a homomorphism of the right homology functor of $C$ and $\operatorname{opcyclesFunctor}$ applied to $C$.

Let $S$ be a short complex of $C$. Then we can say that $\operatorname{ShortExact}$ holds for $S$.

Assume that $\operatorname{ShortExact}$ holds for $S$. Then $\operatorname{fIsKernel}$ applied to $\mathrm{hS}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $\operatorname{f}$ applied to $S$ and $\operatorname{zero}$ applied to $S$.

Assume that $\operatorname{ShortExact}$ holds for $S$. Then $\operatorname{gIsCokernel}$ applied to $\mathrm{hS}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\operatorname{g}$ applied to $S$ and $\operatorname{zero}$ applied to $S$.

the splitting of hS (from the name)

Assume that $\operatorname{ShortExact}$ holds for $S$. Then the splitting of $\mathrm{hS}$ is a splitting of $S$.

the splitting of hS (from the name)

Assume that $\operatorname{ShortExact}$ holds for $S$. Then the splitting of $\mathrm{hS}$ is a splitting of $S$.

Let $C$ be a set. Then there is an object property of the set of short complexes of $C$. Proof. Let $C$ be arbitrary. By CategoryTheory__ShortComplex__ShortExact.

short exact sequence of C (from the name)

Let $C$ be a set. Then a short exact sequence of $C$ is an element of the function that maps $C$ to the set of full subcategories of $\operatorname{shortExact}$ applied to $C$.

snake input of C (from the name)

Let $C$ be a set. Then the snake inputs of $C$ are a basic type.

homomorphism of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be snake inputs of $C$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the composition of $f$ and $g$ is a homomorphism of $x_{2}$ and $x_{4}$.

Let $\mathrm{self}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_Hom\_\_f\_u2080\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $x_{3}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_Hom\_\_f\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_}$ applied to $x_{3}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_Hom\_\_f\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $x_{3}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_Hom\_\_f\_u2083\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $x_{3}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the identity morphism of S (from the docstring)

Let $S$ be a snake input of $C$. Then the identity morphism of $S$ is a homomorphism of $S$ and $S$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $\mathrm{self}$ is a short complex of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_'}$ applied to $S$ is a short complex of $C$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_X\_u2082\_ToP}$ applied to $S$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $S$ and $\operatorname{P}$ applied to $S$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_}$ applied to $\mathrm{self}$ is a short complex of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_'}$ applied to $S$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{g}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $S$, $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3b4\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_\_g\_\_u3b4\_}$ applied to $S$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $\mathrm{self}$ is a short complex of $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_'}$ applied to $S$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3b4\_}$ applied to $S$, $\operatorname{f}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3b4\_\_L\_u2083\_\_f}$ applied to $S$.

the duality isomorphism of S (from the docstring)

Let $S$ be a snake input of $C$. Then the duality isomorphism of $S$ is an isomorphism of the opposite of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_'}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_'}$ applied to the opposite of $S$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $\mathrm{self}$ is a short complex of $C$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $S$ be a snake input of $C$. Then $\operatorname{P}$ applied to $S$ is an element of $C$ defined as the pullback of $\operatorname{g}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2083\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2080\_\_u2081\_}$ applied to $S$.

Let $S$ be a snake input of $C$. Then $\operatorname{P'}$ applied to $S$ is an element of $C$ defined as the pushout of $\operatorname{f}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2081\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2082\_\_u2083\_}$ applied to $S$.

the duality isomorphism of S (from the docstring)

Let $S$ be a snake input of $C$. Then the duality isomorphism of $S$ is an isomorphism of $\operatorname{P'}$ applied to $S$ and the opposite of $\operatorname{P}$ applied to the opposite of $S$ defined as the pushout isomorphism opposite pullback of $\operatorname{f}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2081\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2082\_\_u2083\_}$ applied to $S$.

the duality isomorphism of S (from the docstring)

Let $S$ be a snake input of $C$. Then the duality isomorphism of $S$ is an isomorphism of $\operatorname{P}$ applied to $S$ and the opposite of $\operatorname{P'}$ applied to the opposite of $S$ defined as the pullback isomorphism opposite pushout of $\operatorname{g}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2083\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2080\_\_u2081\_}$ applied to $S$.

the composable arrow of S (from the name)

Let $S$ be a snake input of $C$. Then the composable arrow of $S$ is a composable arrow of $C$ and $5$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2085\_}$ applied to $\operatorname{f}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $S$, $\operatorname{g}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $S$, $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3b4\_}$ applied to $S$, $\operatorname{f}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $S$ and $\operatorname{g}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $S$.

the composable arrow functor (from the name)

The composable arrow functor is a functor of the set of snake inputs of $C$ and the set of composable arrows of $C$ and $5$.

the functor (from the name)

The functor is a functor of the set of snake inputs of $C$ and the set of short complexes of $C$.

the functor (from the name)

The functor is a functor of the set of snake inputs of $C$ and the set of short complexes of $C$.

the functor (from the name)

The functor is a functor of the set of snake inputs of $C$ and the set of short complexes of $C$.

the functor (from the name)

The functor is a functor of the set of snake inputs of $C$ and the set of short complexes of $C$.

the functor (from the name)

The functor is a functor of the set of snake inputs of $C$ and the set of short complexes of $C$.

the functor (from the name)

The functor is a functor of the set of snake inputs of $C$ and the set of short complexes of $C$.

the functor (from the name)

The functor is a functor of the set of snake inputs of $C$ and $C$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2080\_}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2080\_\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2080\_\_u2082\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj9}$ applied to $\mathrm{self}$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2080\_\_u3c4\_\_u2081\_}$ applied to $S$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2081\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2080\_\_u2081\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2080\_\_u2082\_\_\_u3c4\_\_u2081\_}$ applied to $S$ defined as $\operatorname{isLimitForkMapOfIsLimit'}$ applied to the first projection functor, $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2080\_\_u2082\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2080\_}$ applied to $S$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2080\_\_u3c4\_\_u2082\_}$ applied to $S$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2082\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2080\_\_u2081\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2080\_\_u2082\_\_\_u3c4\_\_u2082\_}$ applied to $S$ defined as $\operatorname{isLimitForkMapOfIsLimit'}$ applied to the second projection functor, $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2080\_\_u2082\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2080\_}$ applied to $S$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2080\_\_u3c4\_\_u2083\_}$ applied to $S$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2083\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2080\_\_u2081\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2080\_\_u2082\_\_\_u3c4\_\_u2083\_}$ applied to $S$ defined as $\operatorname{isLimitForkMapOfIsLimit'}$ applied to the third projection functor, $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2080\_\_u2082\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2080\_}$ applied to $S$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2083\_}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2082\_\_u2083\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2081\_\_u2083\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj10}$ applied to $\mathrm{self}$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2083\_\_u3c4\_\_u2081\_}$ applied to $S$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2081\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2082\_\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2081\_\_u2083\_\_\_u3c4\_\_u2081\_}$ applied to $S$ defined as $\operatorname{isColimitCoforkMapOfIsColimit'}$ applied to the first projection functor, $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2081\_\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2083\_}$ applied to $S$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2083\_\_u3c4\_\_u2082\_}$ applied to $S$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2082\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2082\_\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2081\_\_u2083\_\_\_u3c4\_\_u2082\_}$ applied to $S$ defined as $\operatorname{isColimitCoforkMapOfIsColimit'}$ applied to the second projection functor, $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2081\_\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2083\_}$ applied to $S$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2083\_\_u3c4\_\_u2083\_}$ applied to $S$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2083\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2082\_\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2081\_\_u2083\_\_\_u3c4\_\_u2083\_}$ applied to $S$ defined as $\operatorname{isColimitCoforkMapOfIsColimit'}$ applied to the third projection functor, $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_w\_u2081\_\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_h\_u2083\_}$ applied to $S$.

the opposite of S (from the name)

Let $S$ be a snake input of $C$. Then the opposite of $S$ is a snake input of the set of opposites of $C$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2080\_\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2081\_\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2082\_\_u2083\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3b4\_}$ applied to $S$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $S$.

the isomorphism of S (from the name)

Let $S$ be a snake input of $C$ such that $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $S$ is a zero and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $S$ is a zero. Then the isomorphism of $S$ is an isomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2080\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2083\_}$ applied to $S$ defined as $\operatorname{asIso}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3b4\_}$ applied to $S$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3c6\_\_u2081\_}$ applied to $S$ is a homomorphism of $\operatorname{P}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $S$.

Let $S$ be a snake input of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3c6\_\_u2082\_}$ applied to $S$ is a homomorphism of $\operatorname{P}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_}$ applied to $S$ defined as the composition of the first projection of the pullback of $\operatorname{g}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2081\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2083\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2080\_\_u2081\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2082\_}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_v\_u2081\_\_u2082\_}$ applied to $S$.

Let $C$ be a chain complex of $V$ and $\Natural$. Let $X$ be an element of $V$. Then $\mathrm{ChainComplex\_\_fromSingle\_u2080\_Equiv}$ applied to $C$ and $X$ is an equivalence from the set of homomorphisms of the action of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $V$ and $X$ and $C$ to the set of homomorphisms of $X$ and $\operatorname{X}$ applied to $C$ and $0$.

Let $V$ be a set. Then $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $V$ is a functor of $V$ and the set of chain complexes of $V$ and $\Natural$ defined as $\operatorname{single}$ applied to $V$, $\operatorname{down}$ applied to $\Natural$ and $0$.

the single equivalence of C and X (from the name)

Let $C$ be a chain complex of $V$ and $\Natural$. Let $X$ be an element of $V$. Then the single equivalence of $C$ and $X$ is an element of $\EquivMACRoAE {\operatorname{Hom} (C , \operatorname{obj} (\mathrm{ChainComplex\_\_single\_u2080\_} (V), X))}{(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (\operatorname{d} (C , 1 , 0), f)}{0})})}$.

Let $C$ be a cochain complex of $V$ and $\Natural$. Let $X$ be an element of $V$. Then $\mathrm{CochainComplex\_\_fromSingle\_u2080\_Equiv}$ applied to $C$ and $X$ is an element of $\EquivMACRoAE {\operatorname{Hom} (\operatorname{obj} (\mathrm{CochainComplex\_\_single\_u2080\_} (V), X), C)}{(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (f , \operatorname{d} (C , 0 , 1))}{0})})}$.

Let $V$ be a set. Then $\mathrm{CochainComplex\_\_single\_u2080\_}$ applied to $V$ is a functor of $V$ and the set of cochain complexes of $V$ and $\Natural$ defined as $\operatorname{single}$ applied to $V$, $\operatorname{up}$ applied to $\Natural$ and $0$.

the single equivalence of C and X (from the name)

Let $C$ be a cochain complex of $V$ and $\Natural$. Let $X$ be an element of $V$. Then the single equivalence of $C$ and $X$ is an equivalence from the set of homomorphisms of $C$ and the action of $\mathrm{CochainComplex\_\_single\_u2080\_}$ applied to $V$ and $X$ to the set of homomorphisms of $\operatorname{X}$ applied to $C$ and $0$ and $X$.

Let $x_{4}$ be a homomorphism of $A$ and $\operatorname{X}$ applied to $K$ and $j$ such that for all elements $k$ of $x_{2}$, if $\operatorname{Rel}$ holds for $c$, $j$ and $k$, then the composition of $x_{4}$ and $\operatorname{d}$ applied to $K$, $j$ and $k$ is equal to $0$. Then $\operatorname{mkHomFromSingle}$ applied to $x_{4}$ and $h_{1}$ is a homomorphism of the action of $\operatorname{single}$ applied to $V$, $c$ and $j$ and $A$ and $K$.

Let $x_{4}$ be a homomorphism of $\operatorname{X}$ applied to $K$ and $j$ and $A$ such that for all elements $i$ of $x_{2}$, if $\operatorname{Rel}$ holds for $c$, $i$ and $j$, then the composition of $\operatorname{d}$ applied to $K$, $i$ and $j$ and $x_{4}$ is equal to $0$. Then $\operatorname{mkHomToSingle}$ applied to $x_{4}$ and $h_{1}$ is a homomorphism of $K$ and the action of $\operatorname{single}$ applied to $V$, $c$ and $j$ and $A$.

Let $V$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $j$ be an element of $x_{2}$. Then $\operatorname{single}$ applied to $V$, $c$ and $j$ is a functor of $V$ and the set of homological complexes of $V$ and $c$.

the single composition evaluation isomorphism self of c and j (from the name)

Let $V$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $j$ be an element of $x_{2}$. Then the single composition evaluation isomorphism self of $c$ and $j$ is an isomorphism of the composition of $\operatorname{single}$ applied to $V$, $c$ and $j$ and the evaluation of $c$ and $j$ and the identity of $V$.

the single object isomorphism of A and i (from the name)

Let $c$ be a complex shape of $x_{2}$. Let $j$ and $i$ be elements of $x_{2}$. Let $A$ be an element of $V$. Assume that $\EqtMACRoH {i}{j}$. Then the single object isomorphism of $A$ and $i$ is an isomorphism of $\operatorname{X}$ applied to the action of $\operatorname{single}$ applied to $V$, $c$ and $j$ and $A$ and $i$ and $A$.

the single object self of j and A (from the name)

Let $c$ be a complex shape of $x_{2}$. Let $j$ be an element of $x_{2}$. Let $A$ be an element of $V$. Then the single object self of $j$ and $A$ is an isomorphism of $\operatorname{X}$ applied to the action of $\operatorname{single}$ applied to $V$, $c$ and $j$ and $A$ and $j$ and $A$ defined as the single object isomorphism of $A$ and $j$.

the homology functor single isomorphism of c and j (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $j$ be an element of $x_{2}$. Then the homology functor single isomorphism of $c$ and $j$ is an isomorphism of the composition of $\operatorname{single}$ applied to $C$, $c$ and $j$ and the homology functor of $c$ and $j$ and the identity of $C$ defined as the natural isomorphism of the function that maps $A$ to the single object homology self isomorphism of $j$ and $A$ and the function that maps $x_{4}$, $x_{5}$ and $f$ to $\mathrm{HomologicalComplex\_\_singleObjHomologySelfIso\_hom\_naturality}$ applied to $c$, $j$ and $f$.

the single object cycle self isomorphism of j and A (from the name)

Let $c$ be a complex shape of $x_{2}$. Let $j$ be an element of $x_{2}$. Let $A$ be an element of $C$. Then the single object cycle self isomorphism of $j$ and $A$ is an isomorphism of the cycle of the action of $\operatorname{single}$ applied to $C$, $c$ and $j$ and $A$ and $j$ and $A$.

the single object homology self isomorphism of j and A (from the name)

Let $c$ be a complex shape of $x_{2}$. Let $j$ be an element of $x_{2}$. Let $A$ be an element of $C$. Then the single object homology self isomorphism of $j$ and $A$ is an isomorphism of the homology of the action of $\operatorname{single}$ applied to $C$, $c$ and $j$ and $A$ and $j$ and $A$.

Let $c$ be a complex shape of $x_{2}$. Let $j$ be an element of $x_{2}$. Let $A$ be an element of $C$. Then $\operatorname{singleObjOpcyclesSelfIso}$ applied to $c$, $j$ and $A$ is an isomorphism of $A$ and $\operatorname{opcycles}$ applied to the action of $\operatorname{single}$ applied to $C$, $c$ and $j$ and $A$ and $j$.

spectral object of C and x (from the name)

Let $C$ and $x$ be sets. Then the spectral objects of $C$ and $x$ are a basic type.

Let $\mathrm{self}$ be a spectral object of $C$ and $x$. Let $n$ be an integer. Then $\operatorname{H}$ applied to $\mathrm{self}$ and $n$ is a functor of the set of composable arrows of $x$ and $1$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $n$.

homomorphism of X and #2 (from the name)

Let $X$ and $\mathrm{X'}$ be spectral objects of $C$ and $x$. Then the homomorphisms of $X$ and $\mathrm{X'}$ are a basic type.

the homomorphism of self and n (from the name)

Let $\mathrm{self}$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $n$ be an integer. Then the homomorphism of $\mathrm{self}$ and $n$ is a homomorphism of $\operatorname{H}$ applied to $X$ and $n$ and $\operatorname{H}$ applied to $\mathrm{X'}$ and $n$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $n$.

the composable arrow of x4 and x5 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $x_{4}$ and $x_{5}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{4} + 1 , x_{5})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_composableArrows\_u2085\_\_\_\_auto\_1}$. Then the composable arrow of $x_{4}$ and $x_{5}$ is a composable arrow of $C$ and $5$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2085\_}$ applied to the map of $\operatorname{H}$ applied to $X$ and $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$, the map of $\operatorname{H}$ applied to $X$ and $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$, $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h_{1}$, the map of $\operatorname{H}$ applied to $X$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ and the map of $\operatorname{H}$ applied to $X$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $x_{4}$ and $x_{5}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{4} + 1 , x_{5})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_sc\_u2081\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_sc\_u2081\_}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$, $x_{4}$, $x_{5}$ and $h_{1}$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h_{1}$, the map of $\operatorname{H}$ applied to $X$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_zero\_u2081\_}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$, $x_{4}$, $x_{5}$ and $h_{1}$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $x_{4}$ be an integer. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_sc\_u2082\_}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $x_{4}$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to the map of $\operatorname{H}$ applied to $X$ and $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$, the map of $\operatorname{H}$ applied to $X$ and $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_zero\_u2082\_}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $x_{4}$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $x_{4}$ and $x_{5}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{4} + 1 , x_{5})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_sc\_u2083\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_sc\_u2083\_}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$, $x_{4}$, $x_{5}$ and $h_{1}$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to the map of $\operatorname{H}$ applied to $X$ and $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$, $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h_{1}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_zero\_u2083\_}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$, $x_{4}$, $x_{5}$ and $h_{1}$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $x_{4}$ and $x_{5}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{4} + 1 , x_{5})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h$ is a homomorphism of the action of $\operatorname{H}$ applied to $X$ and $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $g$ and the action of $\operatorname{H}$ applied to $X$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$ defined as the component of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_'}$ applied to $X$, $x_{4}$, $x_{5}$ and $h$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $f$ and $g$.

Let $\mathrm{self}$ be a spectral object of $C$ and $x$. Let $x_{4}$ and $x_{5}$ be integers such that $x_{4} + 1 = x_{5}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_'}$ applied to $\mathrm{self}$, $x_{4}$, $x_{5}$ and $h$ is a homomorphism of the composition of the functor arrow of $2$ and $2$ and $\operatorname{H}$ applied to $\mathrm{self}$ and $x_{4}$ and the composition of the functor arrow of $1$ and $2$ and $\operatorname{H}$ applied to $\mathrm{self}$ and $x_{5}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{4}$, $x_{5}$ and $h$.

the cokernel isomorphism cycle of fg and n (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $n$ be an integer. Then the cokernel isomorphism cycle of $\mathrm{fg}$ and $n$ is an isomorphism of the cokernel of the map of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ and the cycle of $g$ and $n$.

the cokernel sequence cycle of fg and n (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $n$ be an integer. Then the cokernel sequence cycle of $\mathrm{fg}$ and $n$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to the map of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$, the cycle of $\mathrm{fg}$ and $n$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_H\_map\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_toCycles}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $n$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $x_{4}$ and $x_{5}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{4} + 1 , x_{5})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceOpcycles\_\_\_auto\_1}$. Then $\operatorname{cokernelSequenceOpcycles}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h$, $\operatorname{pOpcycles}$ applied to $X$, $f$, $g$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_\_pOpcycles}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h$.

the cycle of g and n (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $n$ be an integer. Then the cycle of $g$ and $n$ is an element of $C$.

the cycle map of #6 and #7 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{i'}$ and $\mathrm{j'}$. Let $\mathrm{g'}$ be a homomorphism of $\mathrm{j'}$ and $\mathrm{k'}$. Let $x_{4}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $f$ and $g$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $\mathrm{f'}$ and $\mathrm{g'}$. Let $n$ be an integer. Then the cycle map of $x_{4}$ and $n$ is a homomorphism of the cycle of $g$ and $n$ and the cycle of $\mathrm{g'}$ and $n$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $x_{4}$ be a homomorphism of the action of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $\mathrm{fg}$ and $A$ such that the composition of the map of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ and $x_{4}$ is equal to $0$. Then $\operatorname{descCycles}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$, $x_{4}$ and $\mathrm{hx}$ is a homomorphism of the cycle of $g$ and $n$ and $A$ defined as $\operatorname{desc}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceCycles\_exact}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $n$, $x_{4}$ and $\mathrm{hx}$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $x_{4}$ and $x_{5}$ be integers such that $x_{4} + 1 = x_{5}$. Let $x_{6}$ be a homomorphism of the action of $\operatorname{H}$ applied to $X$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$ and $A$ such that the composition of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h$ and $x_{6}$ is equal to $0$. Then $\operatorname{descOpcycles}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$, $h$, $x_{6}$ and $\mathrm{hx}$ is a homomorphism of $\operatorname{opcycles}$ applied to $X$, $f$, $g$ and $x_{5}$ and $A$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $n$ be an integer. Then $\operatorname{fromOpcycles}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $n$ is a homomorphism of $\operatorname{opcycles}$ applied to $X$, $f$, $g$ and $n$ and the action of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $\mathrm{fg}$.

the cycle of g and n (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $n$ be an integer. Then the cycle of $g$ and $n$ is a homomorphism of the cycle of $g$ and $n$ and the action of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $g$.

the kernel sequence cycle of x4 and x5 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $x_{4}$ and $x_{5}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{4} + 1 , x_{5})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceCycles\_\_\_auto\_1}$. Then the kernel sequence cycle of $x_{4}$ and $x_{5}$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to the cycle of $g$ and $x_{4}$, $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_iCycles\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $n$ be an integer. Then $\operatorname{kernelSequenceOpcycles}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $n$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{fromOpcycles}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $n$, the map of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_fromOpcycles\_H\_map\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $n$.

the lift cycle of x5 and x6 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $x_{4}$ and $x_{5}$ be integers such that $x_{4} + 1 = x_{5}$. Let $x_{6}$ be a homomorphism of $A$ and the action of $\operatorname{H}$ applied to $X$ and $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $g$ such that the composition of $x_{6}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$, $g$, $x_{4}$, $x_{5}$ and $h$ is equal to $0$. Then the lift cycle of $x_{5}$ and $x_{6}$ is a homomorphism of $A$ and the cycle of $g$ and $x_{4}$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $x_{4}$ be a homomorphism of $A$ and the action of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $\mathrm{fg}$ such that the composition of $x_{4}$ and the map of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ is equal to $0$. Then $\operatorname{liftOpcycles}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$, $x_{4}$ and $\mathrm{hx}$ is a homomorphism of $A$ and $\operatorname{opcycles}$ applied to $X$, $f$, $g$ and $n$ defined as the lift of $x_{4}$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $n$ be an integer. Then $\operatorname{opcycles}$ applied to $X$, $f$, $g$ and $n$ is an element of $C$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $n$ be an integer. Then $\operatorname{opcyclesIsoKernel}$ applied to $X$, $f$, $g$, $\mathrm{fg}$, $h$ and $n$ is an isomorphism of $\operatorname{opcycles}$ applied to $X$, $f$, $g$ and $n$ and the kernel of the map of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{i'}$ and $\mathrm{j'}$. Let $\mathrm{g'}$ be a homomorphism of $\mathrm{j'}$ and $\mathrm{k'}$. Let $x_{4}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $f$ and $g$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $\mathrm{f'}$ and $\mathrm{g'}$. Let $n$ be an integer. Then $\operatorname{opcyclesMap}$ applied to $X$, $f$, $g$, $\mathrm{f'}$, $\mathrm{g'}$, $x_{4}$ and $n$ is a homomorphism of $\operatorname{opcycles}$ applied to $X$, $f$, $g$ and $n$ and $\operatorname{opcycles}$ applied to $X$, $\mathrm{f'}$, $\mathrm{g'}$ and $n$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $n$ be an integer. Then $\operatorname{pOpcycles}$ applied to $X$, $f$, $g$ and $n$ is a homomorphism of the action of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$ and $\operatorname{opcycles}$ applied to $X$, $f$, $g$ and $n$.

the cycle of fg and n (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that the composition of $f$ and $g$ is equal to $\mathrm{fg}$. Let $n$ be an integer. Then the cycle of $\mathrm{fg}$ and $n$ is a homomorphism of the action of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $\mathrm{fg}$ and the cycle of $g$ and $n$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ and $x_{8}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_FromOpcycles\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_FromOpcycles}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$ and $h$ is a homomorphism of $\operatorname{opcycles}$ applied to $X$, $x_{5}$, $x_{6}$ and $x_{7}$ and the action of $\operatorname{H}$ applied to $X$ and $x_{8}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $x_{4}$.

the cycle of x7 and x8 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ and $x_{8}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_ToCycles\_\_\_auto\_1}$. Then the cycle of $x_{7}$ and $x_{8}$ is a homomorphism of the action of $\operatorname{H}$ applied to $X$ and $x_{7}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $x_{6}$ and the cycle of $x_{5}$ and $x_{8}$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{10}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{11}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{12}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{13}$ be a homomorphism of $x_{7}$ and $x_{8}$. Let $x_{14}$ be a homomorphism of $x_{8}$ and $x_{9}$. Let $x_{15}$, $x_{16}$, $x_{17}$ and $x_{18}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{15} + 1 , x_{16})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_d\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{16} + 1 , x_{17})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_d\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{17} + 1 , x_{18})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_d\_\_\_auto\_5}$. Then $\operatorname{d}$ applied to $X$, $x_{10}$, $x_{11}$, $x_{12}$, $x_{13}$, $x_{14}$, $x_{15}$, $x_{16}$, $x_{17}$, $x_{18}$, $h$, $h_{1}$ and $h_{2}$ is a homomorphism of $\operatorname{E}$ applied to $X$, $x_{12}$, $x_{13}$, $x_{14}$, $x_{15}$, $x_{16}$, $x_{17}$, $h$ and $h_{1}$ and $\operatorname{E}$ applied to $X$, $x_{10}$, $x_{11}$, $x_{12}$, $x_{16}$, $x_{17}$, $x_{18}$, $h_{1}$ and $h_{2}$.

the sequence of x9 and x10 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ be a homomorphism of $i$ and $k$ such that the composition of $x_{4}$ and $x_{5}$ is equal to $x_{7}$. Let $x_{8}$ be a homomorphism of $j$ and $l$ such that the composition of $x_{5}$ and $x_{6}$ is equal to $x_{8}$. Let $x_{9}$ and $x_{10}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_sequence\_u3a8\_\_\_\_auto\_1}$. Then the sequence of $x_{9}$ and $x_{10}$ is a composable arrow of $C$ and $3$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the cycle map of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $h$ and $x_{9}$, $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3a8\_}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{9}$, $x_{10}$ and $h_{2}$ and $\operatorname{opcyclesMap}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{4}$, $x_{8}$, $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2083\_To\_u3b4\_\_u2082\_}$ applied to $x_{4}$, $x_{5}$, $x_{6}$, $x_{8}$ and $h_{1}$ and $x_{10}$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ and $x_{8}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3a8\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3a8\_}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$ and $h$ is a homomorphism of the cycle of $x_{6}$ and $x_{7}$ and $\operatorname{opcycles}$ applied to $X$, $x_{4}$, $x_{5}$ and $x_{8}$.

Let $\mathrm{X'}$ be a spectral object of $C$ and $x$. Let $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ be elements of $x$ such that $x_{4} \leq x_{5} \leq x_{6} \leq x_{7} \leq x_{8}$. Let $x_{9}$, $x_{10}$ and $x_{11}$ be integers such that the action of $\operatorname{H}$ applied to $\mathrm{X'}$ and $x_{11}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $h$ is a zero, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_isoMapFour\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that $x_{10} + 1$ is equal to $x_{11}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_isoMapFour\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_isoMapFour\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'}$ applied to $\mathrm{X'}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$, $h_{5}$ and $h_{6}$ is an isomorphism of $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$, the homomorphism of $h_{2}$, the homomorphism of $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{5}$ and $h_{6}$ and $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $h_{1}$, the homomorphism of $h_{2}$, the homomorphism of $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{5}$ and $h_{6}$ defined as $\operatorname{asIso}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'}$ applied to $\mathrm{X'}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{5}$ and $h_{6}$.

Let $\mathrm{X'}$ be a spectral object of $C$ and $x$. Let $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ be elements of $x$ such that $x_{4} \leq x_{5} \leq x_{6} \leq x_{7} \leq x_{8}$. Let $x_{9}$, $x_{10}$ and $x_{11}$ be integers such that the action of $\operatorname{H}$ applied to $\mathrm{X'}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $h_{3}$ is a zero, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_isoMapFour\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that $x_{10} + 1$ is equal to $x_{11}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_isoMapFour\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_'\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_isoMapFour\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_'}$ applied to $\mathrm{X'}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$, $h_{5}$ and $h_{6}$ is an isomorphism of $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $h$, the homomorphism of $h_{1}$, the homomorphism of $h_{2}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{5}$ and $h_{6}$ and $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $h$, the homomorphism of $h_{1}$, the homomorphism of $\operatorname{trans}$ applied to $h_{2}$ and $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{5}$ and $h_{6}$ defined as $\operatorname{asIso}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_'}$ applied to $\mathrm{X'}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{5}$ and $h_{6}$.

Let $\mathrm{X'}$ be a spectral object of $C$ and $x$. Let $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ be elements of $x$ such that $x_{4} \leq x_{5} \leq x_{6} \leq x_{7} \leq x_{8}$. Let $x_{9}$, $x_{10}$ and $x_{11}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that $x_{10} + 1$ is equal to $x_{11}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'}$ applied to $\mathrm{X'}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ is a homomorphism of $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$, the homomorphism of $h_{2}$, the homomorphism of $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ and $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $h_{1}$, the homomorphism of $h_{2}$, the homomorphism of $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ defined as the map of $x_{10}$ and $x_{11}$.

Let $\mathrm{X'}$ be a spectral object of $C$ and $x$. Let $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ be elements of $x$ such that $x_{4} \leq x_{5} \leq x_{6} \leq x_{7} \leq x_{8}$. Let $x_{9}$, $x_{10}$ and $x_{11}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that $x_{10} + 1$ is equal to $x_{11}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_'\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_'}$ applied to $\mathrm{X'}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ is a homomorphism of $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $h$, the homomorphism of $\operatorname{trans}$ applied to $h_{1}$ and $h_{2}$, the homomorphism of $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ and $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$, the homomorphism of $h_{2}$, the homomorphism of $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ defined as the map of $x_{10}$ and $x_{11}$.

Let $\mathrm{X'}$ be a spectral object of $C$ and $x$. Let $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ be elements of $x$ such that $x_{4} \leq x_{5} \leq x_{6} \leq x_{7} \leq x_{8}$. Let $x_{9}$, $x_{10}$ and $x_{11}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that $x_{10} + 1$ is equal to $x_{11}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_'\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_mapFour\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_'}$ applied to $\mathrm{X'}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ is a homomorphism of $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $h$, the homomorphism of $h_{1}$, the homomorphism of $h_{2}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ and $\operatorname{E}$ applied to $\mathrm{X'}$, the homomorphism of $h$, the homomorphism of $h_{1}$, the homomorphism of $\operatorname{trans}$ applied to $h_{2}$ and $h_{3}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{4}$ and $h_{5}$ defined as the map of $x_{10}$ and $x_{11}$.

data has first page computations (from the name)

Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{3}$. Then we can say that $\mathrm{data}$ has first page computations.

the spectral sequence first page isomorphism of x7 and n (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $\mathrm{pq}$ be an element of $x_{1}$. Let $x_{6}$ and $x_{7}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq})}$ and $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq})}$. Let $n$ be an integer such that $n$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq}$. Then the spectral sequence first page isomorphism of $x_{7}$ and $n$ is an isomorphism of $\operatorname{X}$ applied to the page of the spectral sequence of $X$ and $\mathrm{data}$ and $x_{5}$ and $\mathrm{pq}$ and the action of $\operatorname{H}$ applied to $X$ and $n$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_le\_u2081\_\_u2082\_'}$ applied to $\mathrm{data}$, $\mathrm{pq}$, $h_{2}$ and $h_{3}$.

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Then we can say that $\operatorname{HasSpectralSequence}$ holds for $X$ and $\mathrm{data}$.

Y is a first quadrant (from the name)

Let $Y$ be a spectral object of $C$ and the set of integers. Then we can say that $Y$ is a first quadrant.

Y is a third quadrant (from the name)

Let $Y$ be a spectral object of $C$ and the set of integers. Then we can say that $Y$ is a third quadrant.

spectral sequence data of c and x3 (from the name)

Let $x$ be a set. Let $c$ be a function from integers to complex shapes of $x_{1}$. Let $x_{3}$ be an integer. Then the spectral sequence data of $c$ and $x_{3}$ are a basic type.

the degree of self and x4 (from the name)

Let $\mathrm{self}$ be a spectral sequence data of $c$ and $x_{3}$. Let $x_{4}$ be an element of $x_{1}$. Then the degree of $\mathrm{self}$ and $x_{4}$ is an integer defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

Let $\mathrm{self}$ be a spectral sequence data of $c$ and $x_{3}$. Let $r$ be an integer. Let $\mathrm{pq}$ be an element of $x_{1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{3} , r)$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_}$ applied to $\mathrm{self}$, $r$, $\mathrm{pq}$ and $\mathrm{hr}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $r$, $\mathrm{pq}$ and $\mathrm{hr}$.

Let $\mathrm{self}$ be a spectral sequence data of $c$ and $x_{3}$. Let $\mathrm{pq}$ be an element of $x_{1}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{pq}$ is an element of $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $\mathrm{pq}$.

Let $\mathrm{self}$ be a spectral sequence data of $c$ and $x_{3}$. Let $\mathrm{pq}$ be an element of $x_{1}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_}$ applied to $\mathrm{self}$ and $\mathrm{pq}$ is an element of $x$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $\mathrm{pq}$.

Let $\mathrm{self}$ be a spectral sequence data of $c$ and $x_{3}$. Let $r$ be an integer. Let $\mathrm{pq}$ be an element of $x_{1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{3} , r)$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_}$ applied to $\mathrm{self}$, $r$, $\mathrm{pq}$ and $\mathrm{hr}$ is an element of $x$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$, $r$, $\mathrm{pq}$ and $\mathrm{hr}$.

$\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_coreE\_u2082\_Cohomological}$ is a spectral sequence data of the function that maps $r$ to $\operatorname{up'}$ applied to $\ProdmkMACRoU {r}{(1 - r)}$ and $2$.

Let $l$ be a natural number. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_coreE\_u2082\_CohomologicalFin}$ applied to $l$ is a spectral sequence data of the function that maps $r$ to $\operatorname{spectralSequenceFin}$ applied to $l$ and $\ProdmkMACRoU {r}{(1 - r)}$ and $2$.

the cohomological natural number (from the name)

The cohomological natural number is a spectral sequence data of the function that maps $r$ to the spectral sequence natural number of $\ProdmkMACRoU {r}{(1 - r)}$ and $2$.

the homological natural number (from the name)

The homological natural number is a spectral sequence data of the function that maps $r$ to the spectral sequence natural number of $\ProdmkMACRoU {\operatorname{neg} (r)}{(r - 1)}$ and $2$.

the cokernel sequence of x18 and x19 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{10}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{11}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{12}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{13}$ be a homomorphism of $x_{7}$ and $x_{8}$. Let $x_{14}$ be a homomorphism of $x_{8}$ and $x_{9}$. Let $x_{15}$ be a homomorphism of $x_{6}$ and $x_{8}$ such that the composition of $x_{12}$ and $x_{13}$ is equal to $x_{15}$. Let $x_{16}$, $x_{17}$, $x_{18}$ and $x_{19}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{16} + 1 , x_{17})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dCokernelSequence\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{17} + 1 , x_{18})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dCokernelSequence\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{18} + 1 , x_{19})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dCokernelSequence\_\_\_auto\_5}$. Then the cokernel sequence of $x_{18}$ and $x_{19}$ is a short complex of $C$.

the homology data of x24 and x25 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{12}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{13}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{14}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{15}$ be a homomorphism of $x_{7}$ and $x_{8}$. Let $x_{16}$ be a homomorphism of $x_{8}$ and $x_{9}$. Let $x_{17}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $x_{18}$ be a homomorphism of $x_{10}$ and $x_{11}$. Let $x_{19}$ be a homomorphism of $x_{5}$ and $x_{7}$ such that the composition of $x_{13}$ and $x_{14}$ is equal to $x_{19}$. Let $x_{20}$ be a homomorphism of $x_{8}$ and $x_{10}$ such that the composition of $x_{16}$ and $x_{17}$ is equal to $x_{20}$. Let $x_{21}$, $x_{22}$, $x_{23}$, $x_{24}$ and $x_{25}$ be elements of $\Integer$ such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{21} + 1 , x_{22})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyData\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{22} + 1 , x_{23})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyData\_\_\_auto\_3}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{23} + 1 , x_{24})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyData\_\_\_auto\_5}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{24} + 1 , x_{25})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyData\_\_\_auto\_7}$. Then the homology data of $x_{24}$ and $x_{25}$ is a homology data of the short complex of $x_{24}$ and $x_{25}$.

the homology isomorphism of x24 and x25 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{12}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{13}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{14}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{15}$ be a homomorphism of $x_{7}$ and $x_{8}$. Let $x_{16}$ be a homomorphism of $x_{8}$ and $x_{9}$. Let $x_{17}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $x_{18}$ be a homomorphism of $x_{10}$ and $x_{11}$. Let $x_{19}$ be a homomorphism of $x_{5}$ and $x_{7}$ such that the composition of $x_{13}$ and $x_{14}$ is equal to $x_{19}$. Let $x_{20}$ be a homomorphism of $x_{8}$ and $x_{10}$ such that the composition of $x_{16}$ and $x_{17}$ is equal to $x_{20}$. Let $x_{21}$, $x_{22}$, $x_{23}$, $x_{24}$ and $x_{25}$ be elements of $\Integer$ such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{21} + 1 , x_{22})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyIso\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{22} + 1 , x_{23})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyIso\_\_\_auto\_3}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{23} + 1 , x_{24})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyIso\_\_\_auto\_5}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{24} + 1 , x_{25})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyIso\_\_\_auto\_7}$. Then the homology isomorphism of $x_{24}$ and $x_{25}$ is an isomorphism of the homology of the short complex of $x_{24}$ and $x_{25}$ and $\operatorname{E}$ applied to $X$, $x_{19}$, $x_{15}$, $x_{20}$, $x_{22}$, $x_{23}$, $x_{24}$, $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyIso\_\_\_proof\_12}$ applied to $x_{22}$, $x_{23}$ and $h_{3}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dHomologyIso\_\_\_proof\_14}$ applied to $x_{23}$, $x_{24}$ and $h_{4}$.

the kernel sequence of x18 and x19 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{10}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{11}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{12}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{13}$ be a homomorphism of $x_{7}$ and $x_{8}$. Let $x_{14}$ be a homomorphism of $x_{8}$ and $x_{9}$. Let $x_{15}$ be a homomorphism of $x_{5}$ and $x_{7}$ such that the composition of $x_{11}$ and $x_{12}$ is equal to $x_{15}$. Let $x_{16}$, $x_{17}$, $x_{18}$ and $x_{19}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{16} + 1 , x_{17})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dKernelSequence\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{17} + 1 , x_{18})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dKernelSequence\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{18} + 1 , x_{19})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dKernelSequence\_\_\_auto\_5}$. Then the kernel sequence of $x_{18}$ and $x_{19}$ is a short complex of $C$.

the short complex of x22 and x23 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{12}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{13}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{14}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{15}$ be a homomorphism of $x_{7}$ and $x_{8}$. Let $x_{16}$ be a homomorphism of $x_{8}$ and $x_{9}$. Let $x_{17}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $x_{18}$ be a homomorphism of $x_{10}$ and $x_{11}$. Let $x_{19}$, $x_{20}$, $x_{21}$, $x_{22}$ and $x_{23}$ be elements of $\Integer$ such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{19} + 1 , x_{20})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dShortComplex\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{20} + 1 , x_{21})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dShortComplex\_\_\_auto\_3}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{21} + 1 , x_{22})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dShortComplex\_\_\_auto\_5}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{22} + 1 , x_{23})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_dShortComplex\_\_\_auto\_7}$. Then the short complex of $x_{22}$ and $x_{23}$ is a short complex of $C$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_E\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_E\_\_\_auto\_3}$. Then $\operatorname{E}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$ is an element of $C$.

the isomorphism of x5 and x6 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $x_{4}$, $x_{5}$ and $x_{6}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{4} + 1 , x_{5})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_EIsoH\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{5} + 1 , x_{6})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_EIsoH\_\_\_auto\_3}$. Then the isomorphism of $x_{5}$ and $x_{6}$ is an isomorphism of $\operatorname{E}$ applied to $X$, the identity morphism of $i$, $f$, the identity morphism of $j$, $x_{4}$, $x_{5}$, $x_{6}$, $h$ and $h_{1}$ and the action of $\operatorname{H}$ applied to $X$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{8}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{10}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{5}$ and $x_{7}$ such that the composition of $x_{9}$ and $x_{10}$ is equal to $x_{11}$. Let $x_{12}$, $x_{13}$ and $x_{14}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_EToCycles\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{13} + 1 , x_{14})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_EToCycles\_\_\_auto\_3}$. Then $\operatorname{EToCycles}$ applied to $X$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $h$, $x_{12}$, $x_{13}$, $x_{14}$, $h_{1}$ and $h_{2}$ is a homomorphism of $\operatorname{E}$ applied to $X$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{12}$, $x_{13}$, $x_{14}$, $h_{1}$ and $h_{2}$ and the cycle of $x_{11}$ and $x_{13}$.

the cokernel sequence cycle of x8 and x9 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceCyclesE\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceCyclesE\_\_\_auto\_3}$. Then the cokernel sequence cycle of $x_{8}$ and $x_{9}$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to the cycle of $x_{7}$ and $x_{8}$, the projection of $x_{8}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_ToCycles\_\_u3c0\_E}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$.

the cokernel sequence cycle isomorphism of x8 and x9 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceCyclesEIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceCyclesEIso\_\_\_auto\_3}$. Then the cokernel sequence cycle isomorphism of $x_{8}$ and $x_{9}$ is an isomorphism of the cokernel sequence cycle of $x_{8}$ and $x_{9}$ and $\operatorname{mk}$ applied to the cycle of the short complex of $x_{8}$ and $x_{9}$, the homology projection of the short complex of $x_{8}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_toCycles\_comp\_homology\_u3c0\_}$ applied to the short complex of $x_{8}$ and $x_{9}$.

the cokernel sequence of x9 and x10 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ be a homomorphism of $i$ and $k$ such that the composition of $x_{4}$ and $x_{5}$ is equal to $x_{7}$. Let $x_{8}$, $x_{9}$ and $x_{10}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceE\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceE\_\_\_auto\_3}$. Then the cokernel sequence of $x_{9}$ and $x_{10}$ is a short complex of $C$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{8}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{10}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{4}$ and $x_{6}$ such that the composition of $x_{8}$ and $x_{9}$ is equal to $x_{11}$. Let $x_{12}$, $x_{13}$ and $x_{14}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceOpcyclesE\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{13} + 1 , x_{14})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cokernelSequenceOpcyclesE\_\_\_auto\_3}$. Then $\operatorname{cokernelSequenceOpcyclesE}$ applied to $X$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $h$, $x_{12}$, $x_{13}$, $x_{14}$, $h_{1}$ and $h_{2}$ is a short complex of $C$.

the cycle isomorphism of x8 and x9 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cyclesIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cyclesIso\_\_\_auto\_3}$. Then the cycle isomorphism of $x_{8}$ and $x_{9}$ is an isomorphism of the cycle of the short complex of $x_{8}$ and $x_{9}$ and the cycle of $x_{5}$ and $x_{8}$.

the cycle isomorphism of x6 and x7 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{6}$ and $x_{7}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{6} + 1 , x_{7})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_cyclesIsoH\_\_\_auto\_1}$. Then the cycle isomorphism of $x_{6}$ and $x_{7}$ is an isomorphism of the cycle of $f$ and $x_{6}$ and the action of $\operatorname{H}$ applied to $X$ and $x_{6}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ be a homomorphism of $i$ and $k$ such that the composition of $x_{4}$ and $x_{5}$ is equal to $x_{7}$. Let $x_{8}$, $x_{9}$ and $x_{10}$ be integers. Let $x_{11}$ be a homomorphism of the action of $\operatorname{H}$ applied to $X$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $x_{7}$ and $A$ such that the composition of the map of $\operatorname{H}$ applied to $X$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $x_{4}$, $x_{5}$, $x_{7}$ and $h$ and $x_{11}$ is equal to $0$. Assume that $x_{8} + 1 = x_{9}$. Assume that the composition of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $x_{7}$, $x_{6}$, $x_{8}$, $x_{9}$ and $h_{2}$ and $x_{11}$ is equal to $0$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_descE\_\_\_auto\_1}$. Then $\operatorname{descE}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $h$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $h_{1}$, $h_{2}$, $\mathrm{h'}$ and $h_{3}$ is a homomorphism of $\operatorname{E}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{8}$, $x_{9}$, $x_{10}$, $h_{2}$ and $h_{3}$ and $A$.

the homology data identity identity of x5 and x6 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $x_{4}$, $x_{5}$ and $x_{6}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{4} + 1 , x_{5})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_homologyDataIdId\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{5} + 1 , x_{6})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_homologyDataIdId\_\_\_auto\_3}$. Then the homology data identity identity of $x_{5}$ and $x_{6}$ is a homology data of the short complex of $x_{5}$ and $x_{6}$.

the kernel sequence cycle of x13 and x14 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{8}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{10}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{5}$ and $x_{7}$ such that the composition of $x_{9}$ and $x_{10}$ is equal to $x_{11}$. Let $x_{12}$, $x_{13}$ and $x_{14}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceCyclesE\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{13} + 1 , x_{14})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceCyclesE\_\_\_auto\_3}$. Then the kernel sequence cycle of $x_{13}$ and $x_{14}$ is a short complex of $C$.

the kernel sequence of x9 and x10 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ be a homomorphism of $j$ and $l$ such that the composition of $x_{5}$ and $x_{6}$ is equal to $x_{7}$. Let $x_{8}$, $x_{9}$ and $x_{10}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceE\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceE\_\_\_auto\_3}$. Then the kernel sequence of $x_{9}$ and $x_{10}$ is a short complex of $C$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceOpcyclesE\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceOpcyclesE\_\_\_auto\_3}$. Then $\operatorname{kernelSequenceOpcyclesE}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to the inclusion of $x_{8}$ and $x_{9}$, $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_FromOpcycles}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{8}$, $x_{9}$ and $h_{1}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b9\_E\_\_u3b4\_FromOpcycles}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceOpcyclesEIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_kernelSequenceOpcyclesEIso\_\_\_auto\_3}$. Then $\operatorname{kernelSequenceOpcyclesEIso}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$ is an isomorphism of $\operatorname{kernelSequenceOpcyclesE}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$ and $\operatorname{mk}$ applied to the homology inclusion of the short complex of $x_{8}$ and $x_{9}$, $\operatorname{fromOpcycles}$ applied to the short complex of $x_{8}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_homology\_u3b9\_\_comp\_fromOpcycles}$ applied to the short complex of $x_{8}$ and $x_{9}$.

the left homology data short complex of x8 and x9 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_leftHomologyDataShortComplex\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_leftHomologyDataShortComplex\_\_\_auto\_3}$. Then the left homology data short complex of $x_{8}$ and $x_{9}$ is a left homology data of the short complex of $x_{8}$ and $x_{9}$.

the lift of x10 and x11 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ be a homomorphism of $j$ and $l$ such that the composition of $x_{5}$ and $x_{6}$ is equal to $x_{7}$. Let $x_{8}$, $x_{9}$ and $x_{10}$ be integers. Let $x_{11}$ be a homomorphism of $A$ and the action of $\operatorname{H}$ applied to $X$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $x_{7}$ such that the composition of $x_{11}$ and the map of $\operatorname{H}$ applied to $X$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $x_{5}$, $x_{6}$, $x_{7}$ and $h$ is equal to $0$. Assume that $x_{9} + 1 = x_{10}$. Assume that the composition of $x_{11}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $x_{4}$, $x_{7}$, $x_{9}$, $x_{10}$ and $h_{2}$ is equal to $0$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_liftE\_\_\_auto\_1}$. Then the lift of $x_{10}$ and $x_{11}$ is a homomorphism of $A$ and $\operatorname{E}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{8}$, $x_{9}$, $x_{10}$, $h_{3}$ and $h_{2}$.

the map of x12 and x13 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ be a homomorphism of $\mathrm{i'}$ and $\mathrm{j'}$. Let $x_{8}$ be a homomorphism of $\mathrm{j'}$ and $\mathrm{k'}$. Let $x_{9}$ be a homomorphism of $\mathrm{k'}$ and $\mathrm{l'}$. Let $x_{10}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{4}$, $x_{5}$ and $x_{6}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{7}$, $x_{8}$ and $x_{9}$. Let $x_{11}$, $x_{12}$ and $x_{13}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_map\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_map\_\_\_auto\_3}$. Then the map of $x_{12}$ and $x_{13}$ is a homomorphism of $\operatorname{E}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{11}$, $x_{12}$, $x_{13}$, $h$ and $h_{1}$ and $\operatorname{E}$ applied to $X$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{11}$, $x_{12}$, $x_{13}$, $h$ and $h_{1}$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_opcyclesIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_opcyclesIso\_\_\_auto\_3}$. Then $\operatorname{opcyclesIso}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$ is an isomorphism of $\operatorname{opcycles}$ applied to the short complex of $x_{8}$ and $x_{9}$ and $\operatorname{opcycles}$ applied to $X$, $x_{5}$, $x_{6}$ and $x_{8}$ defined as the isomorphism of the right homology data short complex of $x_{8}$ and $x_{9}$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{6}$ and $x_{7}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{6} + 1 , x_{7})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_opcyclesIsoH\_\_\_auto\_1}$. Then $\operatorname{opcyclesIsoH}$ applied to $X$, $f$, $x_{6}$, $x_{7}$ and $h$ is an isomorphism of $\operatorname{opcycles}$ applied to $X$, $f$, the identity morphism of $x_{5}$ and $x_{7}$ and the action of $\operatorname{H}$ applied to $X$ and $x_{7}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{8}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{10}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{4}$ and $x_{6}$ such that the composition of $x_{8}$ and $x_{9}$ is equal to $x_{11}$. Let $x_{12}$, $x_{13}$ and $x_{14}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_opcyclesToE\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{13} + 1 , x_{14})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_opcyclesToE\_\_\_auto\_3}$. Then $\operatorname{opcyclesToE}$ applied to $X$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $h$, $x_{12}$, $x_{13}$, $x_{14}$, $h_{1}$ and $h_{2}$ is a homomorphism of $\operatorname{opcycles}$ applied to $X$, $x_{11}$, $x_{10}$ and $x_{13}$ and $\operatorname{E}$ applied to $X$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{12}$, $x_{13}$, $x_{14}$, $h_{1}$ and $h_{2}$.

the right homology data short complex of x8 and x9 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_rightHomologyDataShortComplex\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_rightHomologyDataShortComplex\_\_\_auto\_3}$. Then the right homology data short complex of $x_{8}$ and $x_{9}$ is a right homology data of the short complex of $x_{8}$ and $x_{9}$.

the short complex of x8 and x9 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_shortComplex\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_shortComplex\_\_\_auto\_3}$. Then the short complex of $x_{8}$ and $x_{9}$ is a short complex of $C$.

the short complex map of x12 and x13 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$ be a homomorphism of $\mathrm{i'}$ and $\mathrm{j'}$. Let $x_{8}$ be a homomorphism of $\mathrm{j'}$ and $\mathrm{k'}$. Let $x_{9}$ be a homomorphism of $\mathrm{k'}$ and $\mathrm{l'}$. Let $x_{10}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{4}$, $x_{5}$ and $x_{6}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{7}$, $x_{8}$ and $x_{9}$. Let $x_{11}$, $x_{12}$ and $x_{13}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_shortComplexMap\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_shortComplexMap\_\_\_auto\_3}$. Then the short complex map of $x_{12}$ and $x_{13}$ is a homomorphism of the short complex of $x_{12}$ and $x_{13}$ and the short complex of $x_{12}$ and $x_{13}$.

Let $X$ be a spectral object of $C$ and $x$. Let $x_{8}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{10}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{4}$ and $x_{6}$. Let $x_{12}$ be a homomorphism of $x_{5}$ and $x_{7}$. Assume that the composition of $x_{8}$ and $x_{9}$ is equal to $x_{11}$. Assume that the composition of $x_{9}$ and $x_{10}$ is equal to $x_{12}$. Let $x_{13}$, $x_{14}$ and $x_{15}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{13} + 1 , x_{14})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_shortComplexOpcyclesThree\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{14} + 1 , x_{15})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_shortComplexOpcyclesThree\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_shortComplexOpcyclesThree\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $X$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $x_{12}$, $h$, $h_{1}$, $x_{13}$, $x_{14}$, $x_{15}$, $h_{2}$ and $h_{3}$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{opcyclesMap}$ applied to $X$, $x_{8}$, $x_{12}$, $x_{11}$, $x_{10}$, $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $x_{12}$, $h$ and $h_{1}$ and $x_{14}$, $\operatorname{opcyclesToE}$ applied to $X$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $h$, $x_{13}$, $x_{14}$, $x_{15}$, $h_{2}$ and $h_{3}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_opcyclesMap\_three\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_opcyclesToE}$ applied to $X$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $x_{12}$, $h$, $h_{1}$, $x_{13}$, $x_{14}$, $x_{15}$, $h_{2}$ and $h_{3}$.

the inclusion of x8 and x9 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b9\_E\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3b9\_E\_\_\_auto\_3}$. Then the inclusion of $x_{8}$ and $x_{9}$ is a homomorphism of $\operatorname{E}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$ and $\operatorname{opcycles}$ applied to $X$, $x_{5}$, $x_{6}$ and $x_{8}$ defined as the composition of the homology inclusion of the short complex of $x_{8}$ and $x_{9}$ and the homomorphism of $\operatorname{opcyclesIso}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$.

the projection of x8 and x9 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{4}$ be a homomorphism of $i$ and $j$. Let $x_{5}$ be a homomorphism of $j$ and $k$. Let $x_{6}$ be a homomorphism of $k$ and $l$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3c0\_E\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_\_u3c0\_E\_\_\_auto\_3}$. Then the projection of $x_{8}$ and $x_{9}$ is a homomorphism of the cycle of $x_{5}$ and $x_{8}$ and $\operatorname{E}$ applied to $X$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$.

the homological spectral sequence natural number of Y (from the name)

Let $Y$ be a spectral object of $C$ and the set of integers. Then the homological spectral sequence natural number of $Y$ is a spectral sequence of the function that maps $r$ to the spectral sequence natural number of $\ProdmkMACRoU {\operatorname{neg} (r)}{(r - 1)}$ and $2$ defined as the spectral sequence of $Y$ and the homological natural number.

the spectral sequence of Y (from the name)

Let $Y$ be a spectral object of $C$ and the set of integers. Then the spectral sequence of $Y$ is a cohomological spectral sequence of $C$ defined as the spectral sequence of $Y$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_coreE\_u2082\_Cohomological}$.

the spectral sequence natural number of Y (from the name)

Let $Y$ be a spectral object of $C$ and the set of integers. Then the spectral sequence natural number of $Y$ is a spectral sequence of the function that maps $r$ to the spectral sequence natural number of $\ProdmkMACRoU {r}{(1 - r)}$ and $2$ defined as the spectral sequence of $Y$ and the cohomological natural number.

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$ and $x_{13}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq}$ and $\mathrm{pq'}$ be elements of $x_{1}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$ and $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Let $x_{11}$ and $x_{12}$ be integers such that $x_{12}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_cc\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_cc\_\_\_auto\_3}$. Then $\operatorname{cc}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq}$, $\mathrm{pq'}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $h_{6}$ and $h_{7}$ is a cokernel cofork of $\operatorname{d}$ applied to the page of $\mathrm{data}$ and $r$, $\mathrm{pq}$ and $\mathrm{pq'}$.

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$ and $x_{13}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq}$ and $\mathrm{pq'}$ be elements of $x_{1}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$ and $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Let $x_{11}$ and $x_{12}$ be integers such that $x_{12}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_ccSc\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_ccSc\_\_\_auto\_3}$. Then $\operatorname{ccSc}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq}$, $\mathrm{pq'}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $h_{6}$ and $h_{7}$ is a short complex of $C$.

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$, $x_{11}$, $x_{12}$ and $x_{13}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq}$ and $\mathrm{pq'}$ be elements of $x_{1}$ such that $\EqtMACRoH {\operatorname{prev} (c (r), \mathrm{pq'})}{\mathrm{pq}}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$ and $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Assume that $x_{12}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_isColimitCc\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_isColimitCc\_\_\_auto\_3}$. Then $\operatorname{isColimitCc}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq}$, $\mathrm{pq'}$, $\mathrm{hpq}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $h_{7}$ and $h_{8}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{cc}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq}$, $\mathrm{pq'}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_isColimitCc\_\_\_proof\_6}$ applied to $x_{11}$, $x_{12}$ and $h_{7}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_isColimitCc\_\_\_proof\_8}$ applied to $x_{12}$, $x_{13}$ and $h_{8}$.

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$, $x_{11}$, $x_{12}$ and $x_{13}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq'}$ and $\mathrm{pq''}$ be elements of $x_{1}$ such that $\EqtMACRoH {\operatorname{next} (c (r), \mathrm{pq'})}{\mathrm{pq''}}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$ and $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Assume that $x_{12}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_isLimitKf\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_isLimitKf\_\_\_auto\_3}$. Then $\operatorname{isLimitKf}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq'}$, $\mathrm{pq''}$, $\mathrm{hpq'}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $h_{7}$ and $h_{8}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{kf}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq'}$, $\mathrm{pq''}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $h_{7}$ and $h_{8}$ defined as $\operatorname{fIsKernel}$ applied to $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_kfSc\_exact}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq'}$, $\mathrm{pq''}$, $\mathrm{hpq'}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $h_{7}$ and $h_{8}$.

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$ and $x_{13}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq'}$ and $\mathrm{pq''}$ be elements of $x_{1}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$ and $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Let $x_{11}$ and $x_{12}$ be integers such that $x_{12}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_kf\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_kf\_\_\_auto\_3}$. Then $\operatorname{kf}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq'}$, $\mathrm{pq''}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $h_{6}$ and $h_{7}$ is a kernel fork of $\operatorname{d}$ applied to the page of $\mathrm{data}$ and $r$, $\mathrm{pq'}$ and $\mathrm{pq''}$.

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$ and $x_{13}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq'}$ and $\mathrm{pq''}$ be elements of $x_{1}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$ and $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Let $x_{11}$ and $x_{12}$ be integers such that $x_{12}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_kfSc\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_HomologyData\_\_kfSc\_\_\_auto\_3}$. Then $\operatorname{kfSc}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{r'}$, $\mathrm{hrr'}$, $\mathrm{hr}$, $\mathrm{pq'}$, $\mathrm{pq''}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$, $x_{11}$, $x_{12}$, $x_{13}$, $h_{5}$, $h_{6}$ and $h_{7}$ is a short complex of $C$.

the homology data of #25 and #26 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$, $x_{12}$, $x_{13}$ and $x_{14}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$ be elements of $x_{1}$ such that $\EqtMACRoH {\operatorname{prev} (c (r), \mathrm{pq'})}{\mathrm{pq}}$ and $\EqtMACRoH {\operatorname{next} (c (r), \mathrm{pq'})}{\mathrm{pq''}}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$ and $x_{11}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$ and $\EqtMACRoH {x_{11}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Assume that $x_{13}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_homologyData\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{13} + 1 , x_{14})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_homologyData\_\_\_auto\_3}$. Then the homology data of $x_{13}$ and $x_{14}$ is a homology data of $\operatorname{sc'}$ applied to the page of $\mathrm{data}$ and $r$, $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$.

the homology isomorphism of hr and #7 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$ and $\mathrm{r'}$ be integers such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq'}$ be an element of $x_{1}$. Then the homology isomorphism of $\mathrm{r'}$ and $\mathrm{pq'}$ is an isomorphism of the homology of the page of $\mathrm{data}$ and $r$ and $\mathrm{pq'}$ and $\operatorname{X}$ applied to the page of $\mathrm{data}$ and $\mathrm{r'}$ and $\mathrm{pq'}$.

the homology isomorphism of #25 and #26 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$, $x_{12}$, $x_{13}$ and $x_{14}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$ be elements of $x_{1}$ such that $\EqtMACRoH {\operatorname{prev} (c (r), \mathrm{pq'})}{\mathrm{pq}}$ and $\EqtMACRoH {\operatorname{next} (c (r), \mathrm{pq'})}{\mathrm{pq''}}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$ and $x_{11}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$ and $\EqtMACRoH {x_{11}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Assume that $x_{13}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_homologyIso'\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{13} + 1 , x_{14})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_homologyIso'\_\_\_auto\_3}$. Then the homology isomorphism of $x_{13}$ and $x_{14}$ is an isomorphism of the homology of $\operatorname{sc'}$ applied to the page of $\mathrm{data}$ and $r$, $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$ and $\operatorname{X}$ applied to the page of $\mathrm{data}$ and $\mathrm{r'}$ and $\mathrm{pq'}$.

the page of data and r (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$ be an integer such that $x_{5} \leq r$. Then the page of $\mathrm{data}$ and $r$ is a homological complex of $C$ and $c$ applied to $r$.

the page of pq and hr (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$ be an integer. Let $\mathrm{pq}$ and $\mathrm{pq'}$ be elements of $x_{1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{5} , r)$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_pageD\_\_\_auto\_1}$. Then the page of $\mathrm{pq}$ and $\mathrm{pq'}$ is a homomorphism of the page of $r$ and $\mathrm{pq}$ and the page of $r$ and $\mathrm{pq'}$.

the page of r and pq (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$ be an integer. Let $\mathrm{pq}$ be an element of $x_{1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{5} , r)$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_pageX\_\_\_auto\_1}$. Then the page of $r$ and $\mathrm{pq}$ is an element of $C$.

the page isomorphism of x11 and x12 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$ and $x_{12}$ be elements of $\Integer$ such that $x_{5} \leq r$. Let $\mathrm{pq}$ be an element of $x_{1}$. Let $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq} , \mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_pageX\_\_\_proof\_2} (r , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq})}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq})}$ and $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq} , \mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_pageX\_\_\_proof\_2} (r , \mathrm{hr}))}$. Let $x_{10}$ and $x_{11}$ be integers such that $x_{11}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{10} + 1 , x_{11})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_pageXIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_pageXIso\_\_\_auto\_3}$. Then the page isomorphism of $x_{11}$ and $x_{12}$ is an isomorphism of the page of $r$ and $\mathrm{pq}$ and $\operatorname{E}$ applied to $X$, the homomorphism of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_le\_u2080\_\_u2081\_'}$ applied to $\mathrm{data}$, $r$, $\mathrm{hr}$, $\mathrm{pq}$, $h$ and $h_{1}$, the homomorphism of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_le\_u2081\_\_u2082\_'}$ applied to $\mathrm{data}$, $\mathrm{pq}$, $h_{1}$ and $h_{2}$, the homomorphism of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_le\_u2082\_\_u2083\_'}$ applied to $\mathrm{data}$, $r$, $\mathrm{hr}$, $\mathrm{pq}$, $h_{2}$ and $h_{3}$, $x_{10}$, $x_{11}$, $x_{12}$, $h_{5}$ and $h_{6}$.

the short complex isomorphism of h1 and h2 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $x_{6}$ and $x_{10}$ be elements of $\Integer$ such that $x_{5} \leq r$. Let $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$ be elements of $x_{1}$ such that $\operatorname{Rel}$ holds for $c$ applied to $r$, $\mathrm{pq}$ and $\mathrm{pq'}$ and $\operatorname{Rel}$ holds for $c$ applied to $r$, $\mathrm{pq'}$ and $\mathrm{pq''}$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $x_{6} + 1 = x_{7}$, $x_{7} + 1 = x_{8}$, $x_{8} + 1 = x_{9}$, $x_{9} + 1 = x_{10}$ and $x_{8}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$. Then the short complex isomorphism of $x_{9}$ and $x_{10}$ is an isomorphism of $\operatorname{sc'}$ applied to the page of $\mathrm{data}$ and $r$, $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$ and the short complex of $x_{9}$ and $x_{10}$.

the spectral sequence of X and data (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Then the spectral sequence of $X$ and $\mathrm{data}$ is a spectral sequence of $c$ and $x_{5}$ defined as $\operatorname{mk}$ applied to $\operatorname{page}$ applied to $\mathrm{data}$ and the function that maps $r$, $\mathrm{r'}$, $\mathrm{pq}$, $\mathrm{hrr'}$ and $\mathrm{hr}$ to the homology isomorphism of $\mathrm{r'}$ and $\mathrm{pq}$.

the spectral sequence homology data of #25 and #26 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $\mathrm{r'}$, $x_{12}$, $x_{13}$ and $x_{14}$ be elements of $\Integer$ such that $r + 1 = \mathrm{r'}$ and $x_{5} \leq r$. Let $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$ be elements of $x_{1}$ such that $\EqtMACRoH {\operatorname{prev} (c (r), \mathrm{pq'})}{\mathrm{pq}}$ and $\EqtMACRoH {\operatorname{next} (c (r), \mathrm{pq'})}{\mathrm{pq''}}$. Let $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$ and $x_{11}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq'})}$, $\EqtMACRoH {x_{10}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_28} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$ and $\EqtMACRoH {x_{11}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , \mathrm{r'} , \mathrm{pq'} , \mathrm{\_private\_\_Mathlib\_\_Algebra\_\_Homology\_\_SpectralObject\_\_SpectralSequence\_\_0\_\_\_proof\_27} (r , \mathrm{r'} , \mathrm{hrr'} , \mathrm{hr}))}$. Assume that $x_{13}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{12} + 1 , x_{13})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequenceHomologyData\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{13} + 1 , x_{14})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequenceHomologyData\_\_\_auto\_3}$. Then the spectral sequence homology data of $x_{13}$ and $x_{14}$ is a homology data of $\operatorname{sc'}$ applied to the page of the spectral sequence of $X$ and $\mathrm{data}$ and $r$, $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$.

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$, $x_{6}$ and $x_{10}$ be elements of $\Integer$ such that $x_{5} \leq r$. Let $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$ be elements of $x_{1}$ such that $\operatorname{Rel}$ holds for $c$ applied to $r$, $\mathrm{pq}$ and $\mathrm{pq'}$ and $\operatorname{Rel}$ holds for $c$ applied to $r$, $\mathrm{pq'}$ and $\mathrm{pq''}$. Let $x_{7}$, $x_{8}$ and $x_{9}$ be integers such that $x_{8}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq'}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{6} + 1 , x_{7})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequencePageSc'Iso\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{7} + 1 , x_{8})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequencePageSc'Iso\_\_\_auto\_3}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{8} + 1 , x_{9})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequencePageSc'Iso\_\_\_auto\_5}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{9} + 1 , x_{10})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequencePageSc'Iso\_\_\_auto\_7}$. Then $\operatorname{spectralSequencePageSc'Iso}$ applied to $X$, $\mathrm{data}$, $r$, $\mathrm{hr}$, $\mathrm{pq}$, $\mathrm{pq'}$, $\mathrm{pq''}$, $\mathrm{hpq}$, $\mathrm{hpq'}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $h_{1}$, $h_{2}$, $h_{3}$, $h_{4}$ and $h_{5}$ is an isomorphism of $\operatorname{sc'}$ applied to the page of the spectral sequence of $X$ and $\mathrm{data}$ and $r$, $\mathrm{pq}$, $\mathrm{pq'}$ and $\mathrm{pq''}$ and the short complex of $x_{9}$ and $x_{10}$.

the spectral sequence page isomorphism of x11 and x12 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $\mathrm{data}$ be a spectral sequence data of $c$ and $x_{5}$. Let $r$ and $x_{12}$ be elements of $\Integer$ such that $x_{5} \leq r$. Let $\mathrm{pq}$ be an element of $x_{1}$. Let $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ be elements of $x$ such that $\EqtMACRoH {x_{6}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2080\_} (\mathrm{data} , r , \mathrm{pq} , \mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_pageX\_\_\_proof\_2} (r , \mathrm{hr}))}$, $\EqtMACRoH {x_{7}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2081\_} (\mathrm{data} , \mathrm{pq})}$, $\EqtMACRoH {x_{8}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2082\_} (\mathrm{data} , \mathrm{pq})}$ and $\EqtMACRoH {x_{9}}{\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_i\_u2083\_} (\mathrm{data} , r , \mathrm{pq} , \mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequence\_\_pageX\_\_\_proof\_2} (r , \mathrm{hr}))}$. Let $x_{10}$ and $x_{11}$ be integers such that $x_{11}$ is equal to the degree of $\mathrm{data}$ and $\mathrm{pq}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{10} + 1 , x_{11})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequencePageXIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{11} + 1 , x_{12})$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequencePageXIso\_\_\_auto\_3}$. Then the spectral sequence page isomorphism of $x_{11}$ and $x_{12}$ is an isomorphism of $\operatorname{X}$ applied to the page of the spectral sequence of $X$ and $\mathrm{data}$ and $r$ and $\mathrm{pq}$ and $\operatorname{E}$ applied to $X$, the homomorphism of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_le\_u2080\_\_u2081\_'}$ applied to $\mathrm{data}$, $r$, $\mathrm{hr}$, $\mathrm{pq}$, $h_{1}$ and $h_{2}$, the homomorphism of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_le\_u2081\_\_u2082\_'}$ applied to $\mathrm{data}$, $\mathrm{pq}$, $h_{2}$ and $h_{3}$, the homomorphism of $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_SpectralSequenceDataCore\_\_le\_u2082\_\_u2083\_'}$ applied to $\mathrm{data}$, $r$, $\mathrm{hr}$, $\mathrm{pq}$, $h_{3}$ and $h_{4}$, $x_{10}$, $x_{11}$, $x_{12}$, $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequencePageXIso\_\_\_proof\_6}$ applied to $x_{10}$, $x_{11}$ and $h_{6}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_SpectralObject\_\_spectralSequencePageXIso\_\_\_proof\_8}$ applied to $x_{11}$, $x_{12}$ and $h_{7}$.

cohomological spectral sequence of C and x2 (from the name)

Let $C$ be a set. Let $x_{2}$ be an integer. Then a cohomological spectral sequence of $C$ and $x_{2}$ is an element of the function that maps $C$ and $x_{2}$ to the set of spectral sequences of the function that maps $r$ to $\operatorname{up'}$ applied to $\ProdmkMACRoU {r}{(1 - r)}$ and $x_{2}$.

Let $C$ be a set. Let $l$ be a natural number. Let $x_{2}$ be an integer. Then an element of $\operatorname{CohomologicalSpectralSequenceFin}$ applied to $C$, $l$ and $x_{2}$ is an element of the function that maps $C$, $l$ and $x_{2}$ to the set of spectral sequences of the function that maps $r$ to $\operatorname{spectralSequenceFin}$ applied to $l$ and $\ProdmkMACRoU {r}{(1 - r)}$ and $x_{2}$.

cohomological spectral sequence natural number of C and x2 (from the name)

Let $C$ be a set. Let $x_{2}$ be an integer. Then a cohomological spectral sequence natural number of $C$ and $x_{2}$ is an element of the function that maps $C$ and $x_{2}$ to the set of spectral sequences of the function that maps $r$ to the spectral sequence natural number of $\ProdmkMACRoU {r}{(1 - r)}$ and $x_{2}$.

cohomological spectral sequence of C (from the name)

Let $C$ be a set. Then a cohomological spectral sequence of $C$ is an element of the function that maps $C$ to the set of cohomological spectral sequences of $C$ and $2$.

Let $C$ be a set. Let $l$ be a natural number. Then an element of $\mathrm{CategoryTheory\_\_E\_u2082\_CohomologicalSpectralSequenceFin}$ applied to $C$ and $l$ is an element of the function that maps $C$ and $l$ to $\operatorname{CohomologicalSpectralSequenceFin}$ applied to $C$, $2$ and $l$.

cohomological spectral sequence natural number of C (from the name)

Let $C$ be a set. Then a cohomological spectral sequence natural number of $C$ is an element of the function that maps $C$ to the set of cohomological spectral sequence natural numbers of $C$ and $2$.

spectral sequence of c and x3 (from the name)

Let $C$ be a set. Let $c$ be a function from integers to complex shapes of $x_{2}$. Let $x_{3}$ be an integer. Then the spectral sequences of $c$ and $x_{3}$ are a basic type.

homomorphism of E and #2 (from the name)

Let $E$ and $\mathrm{E'}$ be spectral sequences of $c$ and $x_{3}$. Then the homomorphisms of $E$ and $\mathrm{E'}$ are a basic type.

the homomorphism of self and r (from the name)

Let $\mathrm{self}$ be a homomorphism of $E$ and $\mathrm{E'}$. Let $r$ be an integer such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{3} , r)$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_Hom\_\_\_auto\_1}$. Then the homomorphism of $\mathrm{self}$ and $r$ is a homomorphism of the page of $E$ and $r$ and the page of $\mathrm{E'}$ and $r$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $r$ and $\mathrm{hr}$.

the isomorphism of pq and hr (from the name)

Let $\mathrm{self}$ be a spectral sequence of $c$ and $x_{3}$. Let $r$ and $\mathrm{r'}$ be integers. Let $\mathrm{pq}$ be an element of $x_{2}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (r + 1 , \mathrm{r'})$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{3} , r)$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_\_auto\_5}$. Then the isomorphism of $\mathrm{r'}$ and $\mathrm{pq}$ is an isomorphism of the homology of the page of $\mathrm{self}$ and $r$ and $\mathrm{pq}$ and $\operatorname{X}$ applied to the page of $\mathrm{self}$ and $\mathrm{r'}$ and $\mathrm{pq}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $r$, $\mathrm{r'}$, $\mathrm{pq}$, $\mathrm{hrr'}$ and $\mathrm{hr}$.

the page of self and r (from the name)

Let $\mathrm{self}$ be a spectral sequence of $c$ and $x_{3}$. Let $r$ be an integer such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{3} , r)$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_\_auto\_1}$. Then the page of $\mathrm{self}$ and $r$ is a homological complex of $C$ and $c$ applied to $r$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $r$ and $\mathrm{hr}$.

the page functor of x3 and r (from the name)

Let $C$ be a set. Let $c$ be a function from integers to complex shapes of $x_{2}$. Let $x_{3}$ and $r$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{3} , r)$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_pageFunctor\_\_\_auto\_1}$. Then the page functor of $x_{3}$ and $r$ is a functor of the set of spectral sequences of $c$ and $x_{3}$ and the set of homological complexes of $C$ and $c$ applied to $r$.

the page homology natural isomorphism of pq and hr (from the name)

Let $C$ be a set. Let $c$ be a function from integers to complex shapes of $x_{2}$. Let $x_{3}$, $r$ and $\mathrm{r'}$ be integers. Let $\mathrm{pq}$ be an element of $x_{2}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (r + 1 , \mathrm{r'})$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_pageHomologyNatIso\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{3} , r)$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_pageHomologyNatIso\_\_\_auto\_3}$. Then the page homology natural isomorphism of $\mathrm{r'}$ and $\mathrm{pq}$ is an isomorphism of the composition of the page functor of $x_{3}$ and $r$ and the homology functor of $c$ applied to $r$ and $\mathrm{pq}$ and the composition of the page functor of $x_{3}$ and $\mathrm{r'}$ and the evaluation of $c$ applied to $\mathrm{r'}$ and $\mathrm{pq}$.

the page isomorphism of r and h (from the name)

Let $E$ be a spectral sequence of $c$ and $x_{3}$. Let $\mathrm{pq}$ be an element of $x_{2}$. Let $r$ and $\mathrm{r'}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (r , \mathrm{r'})$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_pageXIsoOfEq\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Leq} (x_{3} , r)$ and $\mathrm{CategoryTheory\_\_SpectralSequence\_\_pageXIsoOfEq\_\_\_auto\_3}$. Then the page isomorphism of $r$ and $\mathrm{r'}$ is an isomorphism of $\operatorname{X}$ applied to the page of $E$ and $r$ and $\mathrm{pq}$ and $\operatorname{X}$ applied to the page of $E$ and $\mathrm{r'}$ and $\mathrm{pq}$.

Let $l$ be a natural number. Let $u$ be an element of $\mathrm{Prod}$ applied to $\Integer$ and $\Integer$. Then $\operatorname{spectralSequenceFin}$ applied to $l$ and $u$ is a complex shape of $\mathrm{Prod}$ applied to $\Integer$ and $\mathrm{Fin}$ applied to $l$.

the spectral sequence natural number of u (from the name)

Let $u$ be an element of $\mathrm{Prod}$ applied to $\Integer$ and $\Integer$. Then the spectral sequence natural number of $u$ is a complex shape of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$.

the limit kernel fork attached to a pullback square of h1 (from the docstring)

Assume that $\mathrm{sq}$ is a pullback. Then the limit kernel fork attached to a pullback square of $h_{1}$ is an element of $\operatorname{IsLimit}$ applied to the kernel fork of $\mathrm{sq}$.

the colimit cokernel cofork attached to a pushout square of h1 (from the docstring)

Assume that $\mathrm{sq}$ is a pushout. Then the colimit cokernel cofork attached to a pushout square of $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork of $\mathrm{sq}$.

the cokernel cofork of sq (from the name)

Let $\mathrm{sq}$ be a square of $C$. Then the cokernel cofork of $\mathrm{sq}$ is a cokernel cofork of the lift of $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\mathrm{sq}$ and $\operatorname{neg}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\mathrm{sq}$.

Let $\mathrm{sq}$ be a square of $C$. Then $\operatorname{isPullbackEquivIsLimitKernelFork}$ applied to $\mathrm{sq}$ is an equivalence from the proposition that $\mathrm{sq}$ is a pullback to $\operatorname{IsLimit}$ applied to the kernel fork of $\mathrm{sq}$.

Let $\mathrm{sq}$ be a square of $C$. Then $\operatorname{isPushoutEquivIsColimitCokernelCofork}$ applied to $\mathrm{sq}$ is an equivalence from the proposition that $\mathrm{sq}$ is a pushout to $\operatorname{IsColimit}$ applied to the cokernel cofork of $\mathrm{sq}$.

the kernel fork of sq (from the name)

Let $\mathrm{sq}$ be a square of $C$. Then the kernel fork of $\mathrm{sq}$ is a kernel fork of $\operatorname{desc}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $\mathrm{sq}$ and $\operatorname{neg}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $\mathrm{sq}$.

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a complex shape of $x_{4}$. Let $x_{10}$ and $x_{11}$ be elements of $x_{4}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_D\_u2081\_}$ applied to $K$, $x_{7}$, $x_{10}$ and $x_{11}$ is a homomorphism of the map object of the graded object of $K$ and $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{7}$ and the map object of the graded object of $K$ and $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{7}$.

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a complex shape of $x_{4}$. Let $x_{10}$ and $x_{11}$ be elements of $x_{4}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_D\_u2082\_}$ applied to $K$, $x_{7}$, $x_{10}$ and $x_{11}$ is a homomorphism of the map object of the graded object of $K$ and $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{7}$ and the map object of the graded object of $K$ and $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{7}$.

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a complex shape of $x_{4}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_HasTotal}$ holds for $K$ and $x_{7}$, if $\operatorname{HasMap}$ holds for the graded object of $K$ and $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{7}$.

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a complex shape of $x_{4}$. Let $x_{10}$ be an element of $x_{2}$. Let $x_{11}$ be an element of $x_{3}$. Let $x_{12}$ be an element of $x_{4}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_d\_u2081\_}$ applied to $K$, $x_{7}$, $x_{10}$, $x_{11}$ and $x_{12}$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $x_{10}$ and $x_{11}$ and the map object of the graded object of $K$ and $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{7}$ defined as $\HSMulhSMulMACRoAL {\mathrm{ComplexShape\_\_\_u3b5\_\_u2081\_} (x_{5} , x_{6} , x_{7} , \ProdmkMACRoU {x_{10}}{x_{11}})}{\operatorname{comp} (\operatorname{f} (\operatorname{d} (K , x_{10} , \operatorname{next} (x_{5} , x_{10})), x_{11}), \mathrm{CategoryTheory\_\_GradedObject\_\_\_u3b9\_MapObjOrZero} (\mathrm{HomologicalComplex\_u2082\_\_\_toGradedObject} (K), \mathrm{ComplexShape\_\_\_u3c0\_} (x_{7}), \ProdmkMACRoU {\operatorname{next} (x_{5} , x_{10})}{x_{11}}, x_{12}))}$.

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a complex shape of $x_{4}$. Let $x_{10}$ be an element of $x_{2}$. Let $x_{11}$ be an element of $x_{3}$. Let $x_{12}$ be an element of $x_{4}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_d\_u2082\_}$ applied to $K$, $x_{7}$, $x_{10}$, $x_{11}$ and $x_{12}$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $x_{10}$ and $x_{11}$ and the map object of the graded object of $K$ and $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{7}$ defined as $\HSMulhSMulMACRoAL {\mathrm{ComplexShape\_\_\_u3b5\_\_u2082\_} (x_{5} , x_{6} , x_{7} , \ProdmkMACRoU {x_{10}}{x_{11}})}{\operatorname{comp} (\operatorname{d} (\operatorname{X} (K , x_{10}), x_{11} , \operatorname{next} (x_{6} , x_{11})), \mathrm{CategoryTheory\_\_GradedObject\_\_\_u3b9\_MapObjOrZero} (\mathrm{HomologicalComplex\_u2082\_\_\_toGradedObject} (K), \mathrm{ComplexShape\_\_\_u3c0\_} (x_{7}), \ProdmkMACRoU {x_{10}}{\operatorname{next} (x_{6} , x_{11})}, x_{12}))}$.

the total complex of K and x7 (from the docstring)

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a complex shape of $x_{4}$. Then the total complex of $K$ and $x_{7}$ is a homological complex of $C$ and $x_{7}$.

the map of x7 and x8 (from the name)

Let $x_{7}$ be a homomorphism of $K$ and $L$. Let $x_{8}$ be a complex shape of $x_{4}$. Then the map of $x_{7}$ and $x_{8}$ is a homomorphism of the total complex of $K$ and $x_{8}$ and the total complex of $L$ and $x_{8}$.

the isomorphism of e and x7 (from the docstring)

Let $e$ be an isomorphism of $K$ and $L$. Let $x_{7}$ be a complex shape of $x_{4}$. Then the isomorphism of $e$ and $x_{7}$ is an isomorphism of the total complex of $K$ and $x_{7}$ and the total complex of $L$ and $x_{7}$.

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $f$ be a function from elements $x_{11}$ of $x_{2}$ and elements $x_{12}$ of $x_{3}$ and elements of $\mathrm{Proof}$ applied to the proposition that the projection of $x_{7}$ and $\ProdmkMACRoU {x_{11}}{x_{12}}$ is equal to $x_{10}$ to homomorphisms of $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $x_{11}$ and $x_{12}$ and $A$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_totalDesc}$ applied to $K$, $x_{11}$, $x_{12}$ and $f$ is a homomorphism of $\operatorname{X}$ applied to the total complex of $K$ and $x_{7}$ and $x_{10}$ and $A$.

the total functor of x6 and x7 (from the name)

Let $C$ be a set. Let $x_{5}$ be a complex shape of $x_{2}$. Let $x_{6}$ be a complex shape of $x_{3}$. Let $x_{7}$ be a complex shape of $x_{4}$. Then the total functor of $x_{6}$ and $x_{7}$ is a functor of the set of homological complexes of $x_{5}$ and $x_{6}$ and the set of homological complexes of $C$ and $x_{7}$.

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a complex shape of $x_{4}$. Let $x_{10}$ be an element of $x_{2}$. Let $x_{11}$ be an element of $x_{3}$. Let $x_{12}$ be an element of $x_{4}$ such that the projection of $x_{7}$ and $\ProdmkMACRoU {x_{10}}{x_{11}}$ is equal to $x_{12}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_\_u3b9\_Total}$ applied to $K$, $x_{7}$, $x_{10}$, $x_{11}$, $x_{12}$ and $h_{1}$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $x_{10}$ and $x_{11}$ and $\operatorname{X}$ applied to the total complex of $K$ and $x_{7}$ and $x_{12}$ defined as the inclusion map object of $\ProdmkMACRoU {x_{10}}{x_{11}}$ and $x_{12}$.

Let $K$ be a homological complex of $x_{5}$ and $x_{6}$. Let $x_{7}$ be a complex shape of $x_{4}$. Let $x_{10}$ be an element of $x_{2}$. Let $x_{11}$ be an element of $x_{3}$. Let $x_{12}$ be an element of $x_{4}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_\_u3b9\_TotalOrZero}$ applied to $K$, $x_{7}$, $x_{10}$, $x_{11}$ and $x_{12}$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $x_{10}$ and $x_{11}$ and $\operatorname{X}$ applied to the total complex of $K$ and $x_{7}$ and $x_{12}$ defined as $\mathrm{CategoryTheory\_\_GradedObject\_\_\_u3b9\_MapObjOrZero}$ applied to the graded object of $K$, $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{7}$, $\ProdmkMACRoU {x_{10}}{x_{11}}$ and $x_{12}$.

the shift functor of C and x2 (from the name)

Let $C$ be a set. Let $x_{2}$ be an integer. Then the shift functor of $C$ and $x_{2}$ is a functor of the set of homological complexes of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$ and the set of homological complexes of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$ defined as the shift functor of the set of homological complexes of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$ and $x_{2}$.

Let $K$ be a homological complex of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$. Let $a$, $x_{2}$, $\mathrm{a'}$ and $b$ be integers such that $\mathrm{a'} = a + x_{2}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_shiftFunctor\_u2081\_XXIso}$ applied to $K$, $a$, $x_{2}$, $\mathrm{a'}$, $h$ and $b$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{X}$ applied to the action of the shift functor of $C$ and $x_{2}$ and $K$ and $a$ and $b$ and $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $\mathrm{a'}$ and $b$.

the shift functor commutative isomorphism of x2 and y (from the name)

Let $C$ be a set. Let $x_{2}$ and $y$ be integers. Then the shift functor commutative isomorphism of $x_{2}$ and $y$ is an isomorphism of the composition of the shift functor of $C$ and $y$ and the shift functor of $C$ and $x_{2}$ and the composition of the shift functor of $C$ and $x_{2}$ and the shift functor of $C$ and $y$ defined as the identity of the composition of the shift functor of $C$ and $y$ and the shift functor of $C$ and $x_{2}$.

the shift functor of C and y (from the name)

Let $C$ be a set. Let $y$ be an integer. Then the shift functor of $C$ and $y$ is a functor of the set of homological complexes of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$ and the set of homological complexes of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$ defined as the map homological complex of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $y$ and $\operatorname{up}$ applied to $\Integer$.

Let $K$ be a homological complex of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$. Let $a$, $b$, $y$ and $\mathrm{b'}$ be integers such that $\mathrm{b'} = b + y$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_shiftFunctor\_u2082\_XXIso}$ applied to $K$, $a$, $b$, $y$, $\mathrm{b'}$ and $h$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{X}$ applied to the action of the shift functor of $C$ and $y$ and $K$ and $a$ and $b$ and $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $a$ and $\mathrm{b'}$.

the isomorphism of K and x2 (from the docstring)

Let $K$ be a homological complex of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$. Let $x_{2}$ be an integer. Then the isomorphism of $K$ and $x_{2}$ is an isomorphism of the total complex of the action of the shift functor of $C$ and $x_{2}$ and $K$ and $\operatorname{up}$ applied to $\Integer$ and the action of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $x_{2}$ and the total complex of $K$ and $\operatorname{up}$ applied to $\Integer$.

the isomorphism of K and y (from the docstring)

Let $K$ be a homological complex of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$. Let $y$ be an integer. Then the isomorphism of $K$ and $y$ is an isomorphism of the total complex of the action of the shift functor of $C$ and $y$ and $K$ and $\operatorname{up}$ applied to $\Integer$ and the action of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $y$ and the total complex of $K$ and $\operatorname{up}$ applied to $\Integer$.

the symmetry isomorphism of K and c (from the docstring)

Let $K$ be a homological complex of $x_{4}$ and $x_{5}$. Let $c$ be a complex shape of $J$. Then the symmetry isomorphism of $K$ and $c$ is an isomorphism of the total complex of the flip of $K$ and $c$ and the total complex of $K$ and $c$.

n is a prime power (by hand)

Let $n$ be an element of $R$. Then $n$ is a prime power, if there exists an element $p$ of $R$, such that there exists a natural number $k$, such that $p$ is prime, $0 < k$ and $\EqtMACRoH {p ^ {k}}{n}$.

Let $A$ be a set. Then we can say that $\mathrm{IsCommJordan}$ holds for $A$.

Let $A$ be a set. Then we can say that $\mathrm{IsJordan}$ holds for $A$.