Definitions: Mathlib.Algebra, part 10 of 17

K has cylinders (from the name)

Let $K$ be a homological complex of $C$ and $c$. Then $K$ has cylinders, if the lift of the identity morphism of $K$ and $\operatorname{neg}$ applied to the identity morphism of $K$ has homotopy cofibers.

x3 has homotopy cofibers (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Then we can say that $x_{3}$ has homotopy cofibers.

the cylinder object of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the cylinder object of $K$ is a homological complex of $C$ and $c$ defined as the homotopy cofiber of the lift of the identity morphism of $K$ and $\operatorname{neg}$ applied to the identity morphism of $K$.

Let $x_{4}$ and $x_{5}$ be homomorphisms of $K$ and $F$. Let $h_{2}$ be a homotopy of $x_{4}$ and $x_{5}$. Then $\operatorname{desc}$ applied to $x_{4}$, $x_{5}$ and $h_{2}$ is a homomorphism of the cylinder object of $K$ and $F$.

the homotopy equivalence of K and hc (from the name)

Let $K$ be a homological complex of $C$ and $c$. Assume that for all elements $j$ of $x_{2}$, there exists an element $i$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the homotopy equivalence of $K$ and $\mathrm{hc}$ is a homotopy equivalence of the cylinder object of $K$ and $K$.

the homotopy of K and hc (from the name)

Let $K$ be a homological complex of $C$ and $c$. Assume that for all elements $j$ of $x_{2}$, there exists an element $i$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the homotopy of $K$ and $\mathrm{hc}$ is a homotopy of the left inclusion of $K$ and the right inclusion of $K$.

the left injection of i and j (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\operatorname{Rel}$ holds for $c$, $j$ and $i$. Then the left injection of $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to $K$ and $i$ and $\operatorname{X}$ applied to the cylinder object of $K$ and $j$ defined as the left injection of $i$ and $j$.

the right inclusion of K and i (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then the right inclusion of $K$ and $i$ is a homomorphism of $\operatorname{X}$ applied to the biproduct of $K$ and $K$ and $i$ and $\operatorname{X}$ applied to the cylinder object of $K$ and $i$ defined as the right inclusion of the lift of the identity morphism of $K$ and $\operatorname{neg}$ applied to the identity morphism of $K$ and $i$.

the map homological complex object isomorphism of F and H (from the name)

Let $F$ be a homological complex of $C$ and $c$. Let $H$ be a functor of $C$ and $D$. Assume that for all elements $j$ of $x_{2}$, there exists an element $i$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the map homological complex object isomorphism of $F$ and $H$ is an isomorphism of the action of the map homological complex of $H$ and $c$ and the cylinder object of $F$ and the cylinder object of the action of the map homological complex of $H$ and $c$ and $F$.

the left inclusion of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the left inclusion of $K$ is a homomorphism of $K$ and the cylinder object of $K$ defined as the composition of the left injection and the right inclusion of the lift of the identity morphism of $K$ and $\operatorname{neg}$ applied to the identity morphism of $K$.

the right inclusion of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the right inclusion of $K$ is a homomorphism of $K$ and the cylinder object of $K$ defined as the composition of the right injection and the right inclusion of the lift of the identity morphism of $K$ and $\operatorname{neg}$ applied to the identity morphism of $K$.

the projection of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the projection of $K$ is a homomorphism of the cylinder object of $K$ and $K$ defined as $\operatorname{desc}$ applied to the identity morphism of $K$, the identity morphism of $K$ and the identity of the identity morphism of $K$.

the projection composition inclusion homotopy of K and hc (from the name)

Let $K$ be a homological complex of $C$ and $c$. Assume that for all elements $j$ of $x_{2}$, there exists an element $i$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the projection composition inclusion homotopy of $K$ and $\mathrm{hc}$ is a homotopy of the composition of the projection of $K$ and the left inclusion of $K$ and the identity morphism of the cylinder object of $K$.

the null homotopic map of K (from the name)

Let $K$ be a homological complex of $C$ and $c$. Then the null homotopic map of $K$ is a homomorphism of the cylinder object of $K$ and the cylinder object of $K$ defined as the null homotopic map of the function that maps $i$, $j$ and $\mathrm{hij}$ to the composition of the second projection of the lift of the identity morphism of $K$ and $\operatorname{neg}$ applied to the identity morphism of $K$ and $i$ and the composition of $\operatorname{f}$ applied to the projection onto the second summand and $i$ and the left injection of $i$ and $j$.

the null homotopy of K (from the name)

Let $K$ be a homological complex of $C$ and $c$. Then the null homotopy of $K$ is a homotopy of the null homotopic map of $K$ and $0$ defined as the null homotopy of the function that maps $i$, $j$ and $\mathrm{hij}$ to the composition of the second projection of the lift of the identity morphism of $K$ and $\operatorname{neg}$ applied to the identity morphism of $K$ and $i$ and the composition of $\operatorname{f}$ applied to the projection onto the second summand and $i$ and the left injection of $i$ and $j$.

the homotopy cofiber of x3 (from the docstring)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Then the homotopy cofiber of $x_{3}$ is a homological complex of $C$ and $c$.

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $i$ be an element of $x_{2}$. Then $\operatorname{X}$ applied to $x_{3}$ and $i$ is an element of $C$ defined as $\mathrm{dite}$ applied to $\operatorname{Rel}$ applied to $c$, $i$ and $\operatorname{next}$ applied to $c$ and $i$, the function that maps $\mathrm{hi}$ to the biproduct of $\operatorname{X}$ applied to $F$ and $\operatorname{next}$ applied to $c$ and $i$ and $\operatorname{X}$ applied to $G$ and $i$ and the function that maps $\mathrm{hi1}$ to $\operatorname{X}$ applied to $G$ and $i$.

the isomorphism of x3 and i (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $i$ be an element of $x_{2}$ such that it is not the case that $\operatorname{Rel}$ holds for $c$, $i$ and $\operatorname{next}$ applied to $c$ and $i$. Then the isomorphism of $x_{3}$ and $i$ is an isomorphism of $\operatorname{X}$ applied to $x_{3}$ and $i$ and $\operatorname{X}$ applied to $G$ and $i$.

the isomorphism biproduct of i and j (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $i$ and $j$ be elements of $x_{2}$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the isomorphism biproduct of $i$ and $j$ is an isomorphism of $\operatorname{X}$ applied to $x_{3}$ and $i$ and the biproduct of $\operatorname{X}$ applied to $F$ and $j$ and $\operatorname{X}$ applied to $G$ and $i$.

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $i$ and $j$ be elements of $x_{2}$. Then $\operatorname{d}$ applied to $x_{3}$, $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to $x_{3}$ and $i$ and $\operatorname{X}$ applied to $x_{3}$ and $j$ defined as $\mathrm{dite}$ applied to $\operatorname{Rel}$ applied to $c$, $i$ and $j$, the function that maps $\mathrm{hij}$ to the sum of $\mathrm{dite}$ applied to $\operatorname{Rel}$ applied to $c$, $j$ and $\operatorname{next}$ applied to $c$ and $j$, the function that maps $\mathrm{hj}$ to $\operatorname{neg}$ applied to the composition of the first component of $i$ and $j$ and the composition of $\operatorname{d}$ applied to $F$, $j$ and $\operatorname{next}$ applied to $c$ and $j$ and the left injection of $\operatorname{next}$ applied to $c$ and $j$ and $j$ and the function that maps $\mathrm{hj1}$ to $0$, the composition of the first component of $i$ and $j$ and the composition of $\operatorname{f}$ applied to $x_{3}$ and $j$ and the right inclusion of $x_{3}$ and $j$ and the composition of the second projection of $x_{3}$ and $i$ and the composition of $\operatorname{d}$ applied to $G$, $i$ and $j$ and the right inclusion of $x_{3}$ and $j$ and the function that maps $\mathrm{hij1}$ to $0$.

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $G$ and $K$. Let $x_{6}$ be a homotopy of the composition of $x_{3}$ and $x_{5}$ and $0$. Then $\operatorname{desc}$ applied to $x_{3}$, $x_{5}$ and $x_{6}$ is a homomorphism of the homotopy cofiber of $x_{3}$ and $K$.

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $K$ be a homological complex of $C$ and $c$. Assume that for all elements $j$ of $x_{2}$, there exists an element $i$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then $\operatorname{descEquiv}$ applied to $x_{3}$, $K$ and $\mathrm{hc}$ is an equivalence from $\Sigma$ applied to the function that maps $x_{5}$ to the set of homotopies of the composition of $x_{3}$ and $x_{5}$ and $0$ to the set of homomorphisms of the homotopy cofiber of $x_{3}$ and $K$.

the first component of i and j (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $i$ and $j$ be elements of $x_{2}$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the first component of $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to $x_{3}$ and $i$ and $\operatorname{X}$ applied to $F$ and $j$ defined as the composition of the homomorphism of the isomorphism biproduct of $i$ and $j$ and the projection onto the first summand.

the left injection of i and j (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $i$ and $j$ be elements of $x_{2}$ such that $\operatorname{Rel}$ holds for $c$, $j$ and $i$. Then the left injection of $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to $F$ and $i$ and $\operatorname{X}$ applied to $x_{3}$ and $j$ defined as the composition of the left injection and the inverse of the isomorphism biproduct of $j$ and $i$.

the right inclusion of x3 (from the docstring)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Then the right inclusion of $x_{3}$ is a homomorphism of $G$ and the homotopy cofiber of $x_{3}$.

the composition of x3 and hc (from the docstring)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Assume that for all elements $j$ of $x_{2}$, there exists an element $i$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the composition of $x_{3}$ and $\mathrm{hc}$ is a homotopy of the composition of $x_{3}$ and the right inclusion of $x_{3}$ and $0$.

the right inclusion of x3 and i (from the docstring)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $i$ be an element of $x_{2}$. Then the right inclusion of $x_{3}$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $G$ and $i$ and $\operatorname{X}$ applied to $x_{3}$ and $i$ defined as $\mathrm{dite}$ applied to $\operatorname{Rel}$ applied to $c$, $i$ and $\operatorname{next}$ applied to $c$ and $i$, the function that maps $\mathrm{hi}$ to the composition of the right injection and the inverse of the isomorphism biproduct of $i$ and $\operatorname{next}$ applied to $c$ and $i$ and the function that maps $\mathrm{hi1}$ to the inverse of the isomorphism of $x_{3}$ and $i$.

the map arrow homomorphism of x5 and x6 (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $\mathrm{F'}$ and $\mathrm{G'}$. Assume that for all elements $j$ of $x_{2}$, there exists an element $i$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Let $x_{6}$ be a homomorphism of $\operatorname{mk}$ applied to $x_{3}$ and $\operatorname{mk}$ applied to $x_{5}$. Then the map arrow homomorphism of $x_{5}$ and $x_{6}$ is a homomorphism of the homotopy cofiber of $x_{3}$ and the homotopy cofiber of $x_{5}$.

the map arrow isomorphism of x5 and x6 (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $\mathrm{F'}$ and $\mathrm{G'}$. Assume that for all elements $j$ of $x_{2}$, there exists an element $i$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Let $x_{6}$ be an isomorphism of $\operatorname{mk}$ applied to $x_{3}$ and $\operatorname{mk}$ applied to $x_{5}$. Then the map arrow isomorphism of $x_{5}$ and $x_{6}$ is an isomorphism of the homotopy cofiber of $x_{3}$ and the homotopy cofiber of $x_{5}$.

the map homological complex object isomorphism of x3 and H (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $H$ be a functor of $C$ and $D$. Then the map homological complex object isomorphism of $x_{3}$ and $H$ is an isomorphism of the action of the map homological complex of $H$ and $c$ and the homotopy cofiber of $x_{3}$ and the homotopy cofiber of the map of the map homological complex of $H$ and $c$ and $x_{3}$.

the second projection of x3 and i (from the docstring)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $i$ be an element of $x_{2}$. Then the second projection of $x_{3}$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $x_{3}$ and $i$ and $\operatorname{X}$ applied to $G$ and $i$ defined as $\mathrm{dite}$ applied to $\operatorname{Rel}$ applied to $c$, $i$ and $\operatorname{next}$ applied to $c$ and $i$, the function that maps $\mathrm{hi}$ to the composition of the homomorphism of the isomorphism biproduct of $i$ and $\operatorname{next}$ applied to $c$ and $i$ and the projection onto the second summand and the function that maps $\mathrm{hi1}$ to the homomorphism of the isomorphism of $x_{3}$ and $i$.

x3 has homotopy fibers (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Then we can say that $x_{3}$ has homotopy fibers.

K has path objects (from the name)

Let $K$ be a homological complex of $C$ and $c$. Then $K$ has path objects, if $\operatorname{desc}$ applied to the identity morphism of $K$ and $\operatorname{neg}$ applied to the identity morphism of $K$ has homotopy fibers.

the homotopy fiber of x3 (from the docstring)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Then the homotopy fiber of $x_{3}$ is a homological complex of $C$ and $c$ defined as the action of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $c$ and $\operatorname{op}$ applied to the homotopy cofiber of the map of $\operatorname{opFunctor}$ applied to $C$ and $c$ and the opposite in $x_{3}$.

the path object of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the path object of $K$ is a homological complex of $C$ and the inverse of the inverse of $c$ defined as the action of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $c$ and $\operatorname{op}$ applied to the cylinder object of the opposite of $K$.

the homotopy equivalence of K and hc (from the name)

Let $K$ be a homological complex of $C$ and $c$. Assume that for all elements $i$ of $x_{2}$, there exists an element $j$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the homotopy equivalence of $K$ and $\mathrm{hc}$ is a homotopy equivalence of $K$ and the path object of $K$.

the homotopy of K and hc (from the name)

Let $K$ be a homological complex of $C$ and $c$. Assume that for all elements $i$ of $x_{2}$, there exists an element $j$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the homotopy of $K$ and $\mathrm{hc}$ is a homotopy of the first projection of $K$ and the second projection of $K$ defined as the opposite of the homotopy of the opposite of $K$ and $\mathrm{hc}$.

the lift of x5 and h2 (from the name)

Let $x_{4}$ and $x_{5}$ be homomorphisms of $F$ and $K$. Let $h_{2}$ be a homotopy of $x_{4}$ and $x_{5}$. Then the lift of $x_{5}$ and $h_{2}$ is a homomorphism of $F$ and the path object of $K$ defined as the map of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $c$ and the opposite in $\operatorname{desc}$ applied to the map of $\operatorname{opFunctor}$ applied to $C$ and $c$ and the opposite in $x_{4}$, the map of $\operatorname{opFunctor}$ applied to $C$ and $c$ and the opposite in $x_{5}$ and the opposite of $h_{2}$.

the map homological complex object isomorphism of K and H (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $H$ be a functor of $C$ and $D$. Assume that for all elements $i$ of $x_{2}$, there exists an element $j$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the map homological complex object isomorphism of $K$ and $H$ is an isomorphism of the action of the map homological complex of $H$ and $c$ and the path object of $K$ and the path object of the action of the map homological complex of $H$ and $c$ and $K$ defined as the map isomorphism of $\operatorname{unopFunctor}$ applied to $D$ and the inverse of $c$ and the inverse of the opposite isomorphism of the map homological complex object isomorphism of the opposite of $K$ and the opposite of $H$.

the inclusion of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the inclusion of $K$ is a homomorphism of $K$ and the path object of $K$ defined as the map of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $c$ and the opposite in the projection of the opposite of $K$.

the first projection of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the first projection of $K$ is a homomorphism of the path object of $K$ and $K$ defined as the map of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $c$ and the opposite in the left inclusion of the opposite of $K$.

the projection composition inclusion homotopy of K and hc (from the name)

Let $K$ be a homological complex of $C$ and $c$. Assume that for all elements $i$ of $x_{2}$, there exists an element $j$ of $x_{2}$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the projection composition inclusion homotopy of $K$ and $\mathrm{hc}$ is a homotopy of the composition of the first projection of $K$ and the inclusion of $K$ and the identity morphism of the path object of $K$ defined as the opposite of the projection composition inclusion homotopy of the opposite of $K$ and $\mathrm{hc}$.

the second projection of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the second projection of $K$ is a homomorphism of the path object of $K$ and $K$ defined as the map of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $c$ and the opposite in the right inclusion of the opposite of $K$.

the image to kernel of f and g (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Let $g$ be a homomorphism of $B$ and $C$ such that the composition of $f$ and $g$ is equal to $0$. Then the image to kernel of $f$ and $g$ is a homomorphism of the action of $\operatorname{underlying}$ and the image of $f$ and the action of $\operatorname{underlying}$ and the kernel of $g$ defined as the subobject of the image of $f$ and the kernel of $g$.

the image to kernel of f and g (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Let $g$ be a homomorphism of $B$ and $C$ such that the composition of $f$ and $g$ is equal to $0$. Then the image to kernel of $f$ and $g$ is a homomorphism of the categorical image of $f$ and the kernel of $g$.

left resolution of x2 (from the name)

Let $x_{2}$ be a functor of $C$ and $A$. Then the left resolutions of $x_{2}$ are a basic type.

Let $\mathrm{self}$ be a left resolution of $x_{2}$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is a functor of $A$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the chain complex of x3 and X (from the name)

Let $x_{3}$ be a left resolution of $x_{2}$. Let $X$ be an element of $A$. Then the chain complex of $x_{3}$ and $X$ is a chain complex of $C$ and $\Natural$.

the chain complex functor of x3 (from the name)

Let $x_{3}$ be a left resolution of $x_{2}$. Then the chain complex functor of $x_{3}$ is a functor of $A$ and the set of chain complexes of $C$ and $\Natural$.

the chain complex map of x3 and f (from the name)

Let $x_{3}$ be a left resolution of $x_{2}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the chain complex map of $x_{3}$ and $f$ is a homomorphism of the chain complex of $x_{3}$ and $X$ and the chain complex of $x_{3}$ and $Y$.

the chain complex isomorphism of X and n (from the name)

Let $x_{3}$ be a left resolution of $x_{2}$. Let $X$ be an element of $A$. Let $n$ be a natural number. Then the chain complex isomorphism of $X$ and $n$ is an isomorphism of $\operatorname{X}$ applied to the chain complex of $x_{3}$ and $X$ and $n + 2$ and the action of $\operatorname{F}$ applied to $x_{3}$ and the kernel of the map of $x_{2}$ and $\operatorname{d}$ applied to the chain complex of $x_{3}$ and $X$, $n + 1$ and $n$.

the chain complex one isomorphism of x3 and X (from the name)

Let $x_{3}$ be a left resolution of $x_{2}$. Let $X$ be an element of $A$. Then the chain complex one isomorphism of $x_{3}$ and $X$ is an isomorphism of $\operatorname{X}$ applied to the chain complex of $x_{3}$ and $X$ and $1$ and the action of $\operatorname{F}$ applied to $x_{3}$ and the kernel of the component of the projection of $x_{3}$ and $X$ defined as the identity of $\operatorname{X}$ applied to the chain complex of $x_{3}$ and $X$ and $1$.

the chain complex zero isomorphism of x3 and X (from the name)

Let $x_{3}$ be a left resolution of $x_{2}$. Let $X$ be an element of $A$. Then the chain complex zero isomorphism of $x_{3}$ and $X$ is an isomorphism of $\operatorname{X}$ applied to the chain complex of $x_{3}$ and $X$ and $0$ and the action of $\operatorname{F}$ applied to $x_{3}$ and $X$ defined as the identity of $\operatorname{X}$ applied to the chain complex of $x_{3}$ and $X$ and $0$.

the projection of self (from the name)

Let $\mathrm{self}$ be a left resolution of $x_{2}$. Then the projection of $\mathrm{self}$ is a homomorphism of the composition of $\operatorname{F}$ applied to $\mathrm{self}$ and $x_{2}$ and the identity of $A$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $x_{3}$ be a left resolution of $x_{2}$. Then $\operatorname{karoubi}$ applied to $x_{3}$ is a left resolution of the action of the canonical functor of $C$ and $A$ and $x_{2}$.

the retract arrow of x3 and X (from the name)

Let $x_{3}$ be a left resolution of $x_{2}$. Let $X$ be an element of $A$. Then the retract arrow of $x_{3}$ and $X$ is a retract arrow of the component of $\mathrm{CategoryTheory\_\_Abelian\_\_LeftResolution\_\_karoubi\_\_\_u3c0\_'}$ applied to $x_{3}$ and $X$ and the map of $\operatorname{toKaroubi}$ applied to $A$ and the component of the projection of $x_{3}$ and $X$.

Let $x_{3}$ be a left resolution of $x_{2}$. Then $\operatorname{reduced}$ applied to $x_{3}$ is a left resolution of $x_{2}$.

the left resolution of x4 and e (from the name)

Let $x_{4}$ be a left resolution of $x_{3}$. Let $e$ be an isomorphism of the composition of $G$ and $x_{5}$ and $x_{3}$. Then the left resolution of $x_{4}$ and $e$ is a left resolution of $x_{5}$.

the transport of eC and e (from the name)

Let $x_{5}$ be a left resolution of $x_{4}$. Let $\mathrm{eA}$ be an equivalence of $\mathrm{A'}$ and $A$. Let $\mathrm{eC}$ be an equivalence of $\mathrm{C'}$ and $C$. Let $e$ be an isomorphism of the composition of $x_{6}$ and the functor of $\mathrm{eA}$ and the composition of the functor of $\mathrm{eC}$ and $x_{4}$. Then the transport of $\mathrm{eC}$ and $e$ is a left resolution of $x_{6}$.

the local cohomology of J and i (from the name)

Let $J$ be an ideal of $R$. Let $i$ be a natural number. Then the local cohomology of $J$ and $i$ is a functor of the set of module categories of $R$ and the set of module categories of $R$ defined as the local cohomology of the ideal power diagram of $J$ and $i$.

Let $J$ be an ideal of $R$. Then an element of $\operatorname{SelfLERadical}$ applied to $J$ is an element of the function that maps $J$ to the set of full subcategories of the function that maps $\mathrm{J'}$ to the proposition that $J$ is less than or equal to the radical of $\mathrm{J'}$.

the cast of hJK (from the name)

Assume that the radical of $J$ is equal to the radical of $K$. Then the cast of $\mathrm{hJK}$ is a functor of $\operatorname{SelfLERadical}$ applied to $J$ and $\operatorname{SelfLERadical}$ applied to $K$.

the cast equivalence of hJK (from the name)

Assume that the radical of $J$ is equal to the radical of $K$. Then the cast equivalence of $\mathrm{hJK}$ is an equivalence of $\operatorname{SelfLERadical}$ applied to $J$ and $\operatorname{SelfLERadical}$ applied to $K$.

the isomorphism of hJK and i (from the name)

Assume that the radical of $J$ is equal to the radical of $K$. Let $i$ be a natural number. Then the isomorphism of $\mathrm{hJK}$ and $i$ is an isomorphism of the local cohomology of $J$ and $i$ and the local cohomology of $K$ and $i$.

the diagram of I and i (from the name)

Let $I$ be a functor of $D$ and the set of ideals of $R$. Let $i$ be a natural number. Then the diagram of $I$ and $i$ is a functor of the set of opposites of $D$ and the set of functors of the set of module categories of $R$ and the set of module categories of $R$ defined as the composition of the opposite of $\operatorname{ringModIdeals}$ applied to $I$ and the extension of $i$.

the diagram composition of i and #3 (from the name)

Let $\mathrm{I'}$ be a functor of $E$ and $D$. Let $I$ be a functor of $D$ and the set of ideals of $R$. Let $i$ be a natural number. Then the diagram composition of $I$ and $i$ is an isomorphism of the diagram of the composition of $\mathrm{I'}$ and $I$ and $i$ and the composition of the opposite of $\mathrm{I'}$ and the diagram of $I$ and $i$.

the ideal power diagram of J (from the name)

Let $J$ be an ideal of $R$. Then the ideal power diagram of $J$ is a functor of the set of opposites of $\Natural$ and the set of ideals of $R$.

Let $J$ be an ideal of $R$. Then $\operatorname{idealPowersToSelfLERadical}$ applied to $J$ is a functor of the set of opposites of $\Natural$ and $\operatorname{SelfLERadical}$ applied to $J$.

the isomorphism of i and #3 (from the name)

Let $\mathrm{I'}$ be a functor of $E$ and $D$. Let $I$ be a functor of $D$ and the set of ideals of $R$. Let $i$ be a natural number. Then the isomorphism of $I$ and $i$ is an isomorphism of the local cohomology of the composition of $\mathrm{I'}$ and $I$ and $i$ and the local cohomology of $I$ and $i$ defined as the composition of the isomorphism of the diagram composition of $I$ and $i$ and the colimit isomorphism of the opposite of $\mathrm{I'}$ and the diagram of $I$ and $i$.

the isomorphism of hJK and i (from the name)

Assume that the radical of $J$ is equal to the radical of $K$. Let $i$ be a natural number. Then the isomorphism of $\mathrm{hJK}$ and $i$ is an isomorphism of the local cohomology of $J$ and $i$ and the local cohomology of $K$ and $i$ defined as the composition of the inverse of $\operatorname{isoSelfLERadical}$ applied to $J$ and $i$ and the composition of the isomorphism of $\mathrm{hJK}$ and $i$ and $\operatorname{isoSelfLERadical}$ applied to $K$ and $i$.

Let $J$ be an ideal of $R$. Let $i$ be a natural number. Then $\operatorname{isoSelfLERadical}$ applied to $J$ and $i$ is an isomorphism of the local cohomology of $J$ and $i$ and the local cohomology of $J$ and $i$ defined as the composition of the inverse of the isomorphism of $\operatorname{selfLERadicalDiagram}$ applied to $J$ and $i$ and the isomorphism of the identity of the diagram of the composition of $\operatorname{idealPowersToSelfLERadical}$ applied to $J$ and $\operatorname{selfLERadicalDiagram}$ applied to $J$ and $i$.

the local cohomology of I and i (from the name)

Let $I$ be a functor of $D$ and the set of ideals of $R$. Let $i$ be a natural number. Then the local cohomology of $I$ and $i$ is a functor of the set of module categories of $R$ and the set of module categories of $R$ defined as the colimit of the diagram of $I$ and $i$.

the local cohomology of J and i (from the name)

Let $J$ be an ideal of $R$. Let $i$ be a natural number. Then the local cohomology of $J$ and $i$ is a functor of the set of module categories of $R$ and the set of module categories of $R$ defined as the local cohomology of $\operatorname{selfLERadicalDiagram}$ applied to $J$ and $i$.

Let $\mathrm{I'}$ be a functor of $E$ and $D$. Let $I$ be a functor of $D$ and the set of ideals of $R$. Then $\operatorname{ringModIdealComp}$ applied to $\mathrm{I'}$ and $I$ is an isomorphism of $\operatorname{ringModIdeals}$ applied to the composition of $\mathrm{I'}$ and $I$ and the composition of $\mathrm{I'}$ and $\operatorname{ringModIdeals}$ applied to $I$.

Let $I$ be a functor of $D$ and the set of ideals of $R$. Then $\operatorname{ringModIdeals}$ applied to $I$ is a functor of $D$ and the set of module categories of $R$.

Let $J$ be an ideal of $R$. Then $\operatorname{selfLERadicalDiagram}$ applied to $J$ is a functor of $\operatorname{SelfLERadical}$ applied to $J$ and the set of ideals of $R$ defined as the inclusion of the function that maps $\mathrm{J'}$ to the proposition that $J$ is less than or equal to the radical of $\mathrm{J'}$.

Let $F$ be a functor of $C$ and $D$. Let $c$ be a complex shape of $x_{2}$. Then $\operatorname{mapHomologicalComplexUpToQuasiIso}$ applied to $F$ and $c$ is a functor of $\mathrm{HomologicalComplexUpToQuasiIso}$ applied to $C$ and $c$ and $\mathrm{HomologicalComplexUpToQuasiIso}$ applied to $D$ and $c$ defined as the localized functor of $\operatorname{Q}$ and $\operatorname{Q}$.

Let $F$ be a functor of $C$ and $D$. Let $c$ be a complex shape of $x_{2}$. Then $\operatorname{mapHomologicalComplexUpToQuasiIsoFactors}$ applied to $F$ and $c$ is an isomorphism of the composition of $\operatorname{Q}$ and $\operatorname{mapHomologicalComplexUpToQuasiIso}$ applied to $F$ and $c$ and the composition of the map homological complex of $F$ and $c$ and $\operatorname{Q}$ defined as the isomorphism of the composition of the map homological complex of $F$ and $c$ and $\operatorname{Q}$ and $\operatorname{mapHomologicalComplexUpToQuasiIso}$ applied to $F$ and $c$.

Let $F$ be a functor of $C$ and $D$. Let $c$ be a complex shape of $x_{2}$. Then $\operatorname{mapHomologicalComplexUpToQuasiIsoFactorsh}$ applied to $F$ and $c$ is an isomorphism of the composition of $\operatorname{Qh}$ and $\operatorname{mapHomologicalComplexUpToQuasiIso}$ applied to $F$ and $c$ and the composition of the map homotopy category of $F$ and $c$ and $\operatorname{Qh}$ defined as the lift natural isomorphism of the composition of the map homotopy category of $F$ and $c$ and $\operatorname{Qh}$ and $\operatorname{mapHomologicalComplexUpToQuasiIsoFactors}$ applied to $F$ and $c$.

Let $F$ be a functor of $C$ and $D$. Let $c$ be a complex shape of $x_{2}$. Then $\operatorname{mapHomologicalComplexUpToQuasiIsoLocalizerMorphism}$ applied to $F$ and $c$ is a localizer morphism of $\operatorname{quasiIso}$ applied to $C$ and $c$ and $\operatorname{quasiIso}$ applied to $D$ and $c$.

Let $c$ be a complex shape of $x$. Let $C$ be a set. Then we can say that $\operatorname{QFactorsThroughHomotopy}$ holds for $c$ and $C$.

the strict universal property fixed target quotient of c (from the name)

Let $c$ be a complex shape of $x$ such that for all elements $j$ of $x$, there exists an element $i$ of $x$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Let $C$ and $E$ be sets. Then the strict universal property fixed target quotient of $c$ is a strict universal property fixed target of the homotopy equivalence of $C$ and $c$ and $E$.

Let $C$ be a set. Let $c$ be a complex shape of $x_{1}$. Then an element of $\mathrm{HomologicalComplexUpToQuasiIso}$ applied to $C$ and $c$ is an element of the function that maps $C$ and $c$ to the set of localizations of $\operatorname{quasiIso}$ applied to $C$ and $c$.

$\operatorname{Q}$ is a functor of the set of homological complexes of $C$ and $c$ and $\mathrm{HomologicalComplexUpToQuasiIso}$ applied to $C$ and $c$ defined as $\operatorname{Q'}$ applied to $\operatorname{quasiIso}$ applied to $C$ and $c$.

$\operatorname{Qh}$ is a functor of the set of homotopy categories of $C$ and $c$ and $\mathrm{HomologicalComplexUpToQuasiIso}$ applied to $C$ and $c$.

the homology functor of c and i (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{1}$. Let $i$ be an element of $x_{1}$. Then the homology functor of $c$ and $i$ is a functor of $\mathrm{HomologicalComplexUpToQuasiIso}$ applied to $C$ and $c$ and $C$ defined as the lift of the homology functor of $c$ and $i$ and $\operatorname{Q}$.

the homology functor factor of c and i (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{1}$. Let $i$ be an element of $x_{1}$. Then the homology functor factor of $c$ and $i$ is an isomorphism of the composition of $\operatorname{Q}$ and the homology functor of $c$ and $i$ and the homology functor of $c$ and $i$ defined as the factor of the homology functor of $c$ and $i$ and $\operatorname{Q}$.

Let $C$ be a set. Let $c$ be a complex shape of $x_{1}$. Let $i$ be an element of $x_{1}$. Then $\operatorname{homologyFunctorFactorsh}$ applied to $C$, $c$ and $i$ is an isomorphism of the composition of $\operatorname{Qh}$ and the homology functor of $c$ and $i$ and the homology functor of $c$ and $i$ defined as the natural isomorphism lift of $\mathrm{homotopic}$ applied to $C$ and $c$ and the composition of the inverse of the associator of $\operatorname{Qh}$ and the homology functor of $c$ and $i$ and the composition of the right isomorphism whisker of the canonical isomorphism of $C$ and $c$ and the homology functor of $c$ and $i$ and the composition of the homology functor factor of $c$ and $i$ and the inverse of the homology functor factor of $c$ and $i$.

the canonical isomorphism of C and c (from the docstring)

Let $C$ be a set. Let $c$ be a complex shape of $x_{1}$. Then the canonical isomorphism of $C$ and $c$ is an isomorphism of the composition of the quotient of $C$ and $c$ and $\operatorname{Qh}$ and $\operatorname{Q}$.

Let $C$ be a set. Let $c$ be a complex shape of $x_{1}$. Then there is a morphism property of the set of homotopy categories of $C$ and $c$. Proof. Let $C$ be arbitrary. Let $c$ be arbitrary. Let $x_{3}$ be arbitrary. Let $x_{4}$ be arbitrary. Let $f$ be arbitrary. By x1. Let $i$ be arbitrary. By c. By i. By HomotopyCategory__homologyFunctor. By f. By CategoryTheory__Functor__map. By CategoryTheory__IsIso. By forall.

the cochain of sq and hsq (from the name)

Assume that $\operatorname{CommSq}$ holds for $t$, $i$, $p$ and $b$. Let $\mathrm{hsq}$ be a function from integers $n$ to elements of $\operatorname{LiftStruct}$ applied to $\operatorname{map}$ applied to the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$ and $\mathrm{sq}$. Then the cochain of $\mathrm{sq}$ and $n$ is a cochain of $X$ and $0$ defined as the function that maps $\mathrm{hsq}$ to the cochain of the function that maps $n$ to $\operatorname{l}$ applied to $n$ applied to $n$.

the cochain of n and hQ (from the name)

Assume that $\operatorname{CommSq}$ holds for $t$, $i$, $p$ and $b$. Let $\mathrm{hsq}$ be a function from integers $n$ to elements of $\operatorname{LiftStruct}$ applied to $\operatorname{map}$ applied to the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$ and $\mathrm{sq}$. Let $\mathrm{hQ}$ be an element of $\operatorname{IsColimit}$ applied to the projection of $x_{2}$ and $h$. Let $\mathrm{hK}$ be an element of $\operatorname{IsLimit}$ applied to the inclusion of $x_{3}$ and $h_{1}$. Then the cochain of $\mathrm{hsq}$ and $\mathrm{hQ}$ is a cochain of $K$ and $1$ defined as the function that maps $\mathrm{hK}$ to $\operatorname{mk}$ applied to the function that maps $n$, $m$ and $\mathrm{hnm}$ to $\operatorname{choose}$ applied to $\mathrm{CochainComplex\_\_Lifting\_\_exists\_hom}$ applied to $\mathrm{sq}$, $n$, $\mathrm{hsq}$, $\mathrm{hQ}$, $n$, $m$ and $\mathrm{hnm}$ and $\mathrm{hK}$.

the cocycle of n and hQ (from the name)

Assume that $\operatorname{CommSq}$ holds for $t$, $i$, $p$ and $b$. Let $\mathrm{hsq}$ be a function from integers $n$ to elements of $\operatorname{LiftStruct}$ applied to $\operatorname{map}$ applied to the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$ and $\mathrm{sq}$. Let $\mathrm{hQ}$ be an element of $\operatorname{IsColimit}$ applied to the projection of $x_{2}$ and $h$. Let $\mathrm{hK}$ be an element of $\operatorname{IsLimit}$ applied to the inclusion of $x_{3}$ and $h_{1}$. Then the cocycle of $\mathrm{hsq}$ and $\mathrm{hQ}$ is a cocycle of $K$ and $1$.

the cocycle of sq and hsq (from the name)

Assume that $\operatorname{CommSq}$ holds for $t$, $i$, $p$ and $b$. Let $\mathrm{hsq}$ be a function from integers $n$ to elements of $\operatorname{LiftStruct}$ applied to $\operatorname{map}$ applied to the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$ and $\mathrm{sq}$. Then the cocycle of $\mathrm{sq}$ and $n$ is a cocycle of $X$ and $1$.

Let $x_{5}$, $x_{6}$ and $x_{7}$ be homological complexes of $C$ and $c$. Then $\mathrm{HomologicalComplex\_\_HasGoodTensor\_u2081\_\_u2082\_}$ holds for $x_{5}$, $x_{6}$ and $x_{7}$, if $\mathrm{HomologicalComplex\_\_HasGoodTrifunctor\_u2081\_\_u2082\_Obj}$ holds for the tensor product bifunctor of $C$, the tensor product bifunctor of $C$, $x_{5}$, $x_{6}$, $x_{7}$, $c$ and $c$.

Let $x_{5}$, $x_{6}$ and $x_{7}$ be homological complexes of $C$ and $c$. Then $\mathrm{HomologicalComplex\_\_HasGoodTensor\_u2082\_\_u2083\_}$ holds for $x_{5}$, $x_{6}$ and $x_{7}$, if $\mathrm{HomologicalComplex\_\_HasGoodTrifunctor\_u2082\_\_u2083\_Obj}$ holds for the tensor product bifunctor of $C$, the tensor product bifunctor of $C$, $x_{5}$, $x_{6}$, $x_{7}$, $c$, $c$ and $c$.

Let $x_{5}$ and $x_{6}$ be homological complexes of $C$ and $c$. Then $\operatorname{HasTensor}$ holds for $x_{5}$ and $x_{6}$, if $\operatorname{HasMapBifunctor}$ holds for $x_{5}$, $x_{6}$, the tensor product bifunctor of $C$ and $c$.

Let $C$ be a set. Let $c$ be a complex shape of $I$. Then $\operatorname{inducingFunctorData}$ applied to $C$ and $c$ is an element of $\operatorname{InducingFunctorData}$ applied to $\operatorname{forget}$ applied to $C$ and $c$.

the associator of x7 and x8 (from the name)

Let $x_{6}$, $x_{7}$ and $x_{8}$ be homological complexes of $C$ and $c$. Then the associator of $x_{7}$ and $x_{8}$ is an isomorphism of the tensor object of the tensor object of $x_{6}$ and $x_{7}$ and $x_{8}$ and the tensor object of $x_{6}$ and the tensor object of $x_{7}$ and $x_{8}$ defined as the map bifunctor associator of $c$ and $c$.

the left unitor of K (from the name)

Let $K$ be a homological complex of $C$ and $c$. Then the left unitor of $K$ is an isomorphism of the tensor object of the tensor unit of $C$ and $c$ and $K$ and $K$ defined as the inverse of the isomorphism of the function that maps $i$ to the map isomorphism of the evaluation of $i$ and the inverse of $\operatorname{leftUnitor'}$ applied to $K$ and the function that maps $x_{6}$, $x_{7}$ and $h_{4}$ to $\mathrm{HomologicalComplex\_\_leftUnitor'\_inv\_comm}$ applied to $K$, $x_{6}$ and $x_{7}$.

the right unitor of K (from the name)

Let $K$ be a homological complex of $C$ and $c$. Then the right unitor of $K$ is an isomorphism of the tensor object of $K$ and the tensor unit of $C$ and $c$ and $K$ defined as the inverse of the isomorphism of the function that maps $i$ to the map isomorphism of the evaluation of $i$ and the inverse of $\operatorname{rightUnitor'}$ applied to $K$ and the function that maps $x_{6}$, $x_{7}$ and $h_{4}$ to $\mathrm{HomologicalComplex\_\_rightUnitor'\_inv\_comm}$ applied to $K$, $x_{6}$ and $x_{7}$.

the tensor homomorphism of f and g (from the name)

Let $f$ be a homomorphism of $x_{6}$ and $x_{8}$. Let $g$ be a homomorphism of $x_{7}$ and $x_{9}$. Then the tensor homomorphism of $f$ and $g$ is a homomorphism of the tensor object of $x_{6}$ and $x_{7}$ and the tensor object of $x_{8}$ and $x_{9}$ defined as the map bifunctor map of the tensor product bifunctor of $C$ and $c$.

the tensor object of x6 and x7 (from the name)

Let $x_{6}$ and $x_{7}$ be homological complexes of $C$ and $c$. Then the tensor object of $x_{6}$ and $x_{7}$ is a homological complex of $C$ and $c$ defined as the map bifunctor of the tensor product bifunctor of $C$ and $c$.

the tensor unit of C and c (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $I$. Then the tensor unit of $C$ and $c$ is a homological complex of $C$ and $c$ defined as the action of $\operatorname{single}$ applied to $C$, $c$ and $0$ and the tensor unity in the monoidal structure of $C$.

the tensor unit isomorphism of C and c (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $I$. Then the tensor unit isomorphism of $C$ and $c$ is an isomorphism of the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and the tensor unity in the monoidal structure of $C$ and $\operatorname{X}$ applied to the tensor unit of $C$ and $c$.

the inclusion tensor object of x9 and j (from the name)

Let $x_{6}$ and $x_{7}$ be homological complexes of $C$ and $c$. Let $x_{8}$, $x_{9}$ and $j$ be elements of $I$ such that $\EqtMACRoH {x_{8} + x_{9}}{j}$. Then the inclusion tensor object of $x_{9}$ and $j$ is a homomorphism of the tensor object of $\operatorname{X}$ applied to $x_{6}$ and $x_{8}$ and $\operatorname{X}$ applied to $x_{7}$ and $x_{9}$ and $\operatorname{X}$ applied to the tensor object of $x_{6}$ and $x_{7}$ and $j$ defined as the inclusion of $x_{6}$.

the canonical isomorphism of K and i (from the docstring)

Let $K$ be a homological complex of $V$ and $c$. Let $i$ be an element of $x$. Then the canonical isomorphism of $K$ and $i$ is an isomorphism of the cycle of the opposite of $K$ and $i$ and $\operatorname{op}$ applied to $\operatorname{opcycles}$ applied to $K$ and $i$ defined as the cycle opposite isomorphism of $\operatorname{sc}$ applied to $K$ and $i$.

the cycle opposite natural isomorphism of c and i (from the name)

Let $V$ be a set. Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then the cycle opposite natural isomorphism of $c$ and $i$ is an isomorphism of the composition of $\operatorname{opFunctor}$ applied to $V$ and $c$ and the cycle functor of the inverse of $c$ and $i$ and the opposite of $\operatorname{opcyclesFunctor}$ applied to $V$, $c$ and $i$.

the homology opposite of K and i (from the name)

Let $K$ be a homological complex of $V$ and $c$. Let $i$ be an element of $x$. Then the homology opposite of $K$ and $i$ is an isomorphism of the homology of the opposite of $K$ and $i$ and $\operatorname{op}$ applied to the homology of $K$ and $i$ defined as the canonical isomorphism of $\operatorname{sc}$ applied to $K$ and $i$.

the homology opposite natural isomorphism of c and i (from the name)

Let $V$ be a set. Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then the homology opposite natural isomorphism of $c$ and $i$ is an isomorphism of the composition of $\operatorname{opFunctor}$ applied to $V$ and $c$ and the homology functor of the inverse of $c$ and $i$ and the opposite of the homology functor of $c$ and $i$.

the homology opposite of K and i (from the name)

Let $K$ be a homological complex of the set of opposites of $V$ and $c$. Let $i$ be an element of $x$. Then the homology opposite of $K$ and $i$ is an isomorphism of the homology of the opposite of $K$ and $i$ and the opposite of the homology of $K$ and $i$ defined as the opposite of the homology opposite of the opposite of $K$ and $i$.

the opposite of X (from the name)

Let $X$ be a homological complex of $V$ and $c$. Then the opposite of $X$ is a homological complex of the set of opposites of $V$ and the inverse of $c$.

the opposite equivalence of V and c (from the name)

Let $V$ be a set. Let $c$ be a complex shape of $x$. Then the opposite equivalence of $V$ and $c$ is an equivalence of the set of opposites of the set of homological complexes of $V$ and $c$ and the set of homological complexes of the set of opposites of $V$ and the inverse of $c$.

the opposite inverse of X (from the name)

Let $X$ be a homological complex of $V$ and the inverse of $c$. Then the opposite inverse of $X$ is a homological complex of the set of opposites of $V$ and $c$.

the canonical isomorphism of K and i (from the docstring)

Let $K$ be a homological complex of $V$ and $c$. Let $i$ be an element of $x$. Then the canonical isomorphism of $K$ and $i$ is an isomorphism of $\operatorname{opcycles}$ applied to the opposite of $K$ and $i$ and $\operatorname{op}$ applied to the cycle of $K$ and $i$ defined as $\operatorname{opcyclesOpIso}$ applied to $\operatorname{sc}$ applied to $K$ and $i$.

Let $V$ be a set. Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then $\operatorname{opcyclesOpNatIso}$ applied to $V$, $c$ and $i$ is an isomorphism of the composition of $\operatorname{opFunctor}$ applied to $V$ and $c$ and $\operatorname{opcyclesFunctor}$ applied to the set of opposites of $V$, the inverse of $c$ and $i$ and the opposite of the cycle functor of $c$ and $i$.

the opposite of X (from the name)

Let $X$ be a homological complex of the set of opposites of $V$ and $c$. Then the opposite of $X$ is a homological complex of $V$ and the inverse of $c$.

the opposite equivalence of V and c (from the name)

Let $V$ be a set. Let $c$ be a complex shape of $x$. Then the opposite equivalence of $V$ and $c$ is an equivalence of the set of opposites of the set of homological complexes of the set of opposites of $V$ and $c$ and the set of homological complexes of $V$ and the inverse of $c$.

the opposite inverse of X (from the name)

Let $X$ be a homological complex of the set of opposites of $V$ and the inverse of $c$. Then the opposite inverse of $X$ is a homological complex of $V$ and $c$.

the opposite of h (from the docstring)

Let $h$ be a homotopy of $x_{3}$ and $x_{4}$. Then the opposite of $h$ is a homotopy of the map of $\operatorname{opFunctor}$ applied to $V$ and $c$ and the opposite in $x_{3}$ and the map of $\operatorname{opFunctor}$ applied to $V$ and $c$ and the opposite in $x_{4}$.

the opposite of h (from the name)

Let $h$ be a homotopy of $x_{3}$ and $x_{4}$. Then the opposite of $h$ is a homotopy of the map of $\operatorname{unopFunctor}$ applied to $V$ and $c$ and the opposite in $x_{3}$ and the map of $\operatorname{unopFunctor}$ applied to $V$ and $c$ and the opposite in $x_{4}$.

the precylinder object of K (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Then the precylinder object of $K$ is a precylinder of $K$.

Let $K$ be a homological complex of $C$ and $c$. Then $\operatorname{prepathObject}$ applied to $K$ is an element of $\operatorname{PrepathObject}$ applied to $K$.

Let $C$ be a set. Let $c$ be a complex shape of $x$. Then there is a morphism property of the set of homological complexes of $C$ and $c$. Proof. Let $C$ be arbitrary. Let $c$ be arbitrary. Let $x_{3}$ be arbitrary. Let $x_{4}$ be arbitrary. Let $f$ be arbitrary. By f. By QuasiIso.

Let $f$ be a homomorphism of $K$ and $L$. Then we can say that $\mathrm{QuasiIso}$ holds for $f$.

Let $f$ be a homomorphism of $K$ and $L$. Let $i$ be an element of $x$. Then we can say that $\mathrm{QuasiIsoAt}$ holds for $f$ and $i$.

the isomorphism of f and i (from the docstring)

Let $f$ be a homomorphism of $K$ and $L$. Let $i$ be an element of $x$. Then the isomorphism of $f$ and $i$ is an isomorphism of the homology of $K$ and $i$ and the homology of $L$ and $i$ defined as $\operatorname{asIso}$ applied to the map of $f$ and $i$.

the abelian group cycle isomorphism of S (from the name)

Let $S$ be a short complex of the set of abelian groups. Then the abelian group cycle isomorphism of $S$ is an isomorphism of the cycle of $S$ and $\operatorname{of}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{hom} (\operatorname{g} (S)))}{x})}$ defined as the isomorphism of the explicit left homology data of $S$.

the abelian group homology isomorphism of S (from the name)

Let $S$ be a short complex of the set of abelian groups. Then the abelian group homology isomorphism of $S$ is an isomorphism of the homology of $S$ and $\operatorname{of}$ applied to the set of quotients of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{hom} (\operatorname{g} (S)))}{x})}$ and the range of the abelian group to cycle 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 abelian groups. Then the explicit left homology data of $S$ is a left homology data of $S$.

the abelian group to cycle of S (from the name)

Let $S$ be a short complex of the set of abelian groups. Then the abelian group to cycle of $S$ is an additive monoid homomorphism of the set of carriers of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{hom} (\operatorname{g} (S)))}{x})}$.

the homology data of S (from the name)

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

the homology data of hkf and hcc (from the name)

Let $S$ be a short complex of $C$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Assume that the composition of the inclusion of $\mathrm{kf}$ and the projection of $\mathrm{cc}$ is equal to the composition of $x_{2}$ and $x_{3}$. Then the homology data of $\mathrm{hkf}$ and $\mathrm{hcc}$ is a homology data of $S$.

the isomorphism homology of hkf and hcc (from the name)

Let $S$ be a short complex of $C$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Assume that the composition of the inclusion of $\mathrm{kf}$ and the projection of $\mathrm{cc}$ is equal to the composition of $x_{2}$ and $x_{3}$. Then the isomorphism homology of $\mathrm{hkf}$ and $\mathrm{hcc}$ is an isomorphism of $H$ and the homology of $S$ defined as the composition of the isomorphism image of $\mathrm{hkf}$ and $\mathrm{hcc}$ and the inverse of the homology of $S$.

the isomorphism image of hkf and hcc (from the name)

Let $S$ be a short complex of $C$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Assume that the composition of the inclusion of $\mathrm{kf}$ and the projection of $\mathrm{cc}$ is equal to the composition of $x_{2}$ and $x_{3}$. Then the isomorphism image of $\mathrm{hkf}$ and $\mathrm{hcc}$ is an isomorphism of $H$ and the categorical image of the composition of the cycle of $S$ and $\operatorname{pOpcycles}$ applied to $S$.

the left homology data of hkf and hcc (from the name)

Let $S$ be a short complex of $C$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Assume that the composition of the inclusion of $\mathrm{kf}$ and the projection of $\mathrm{cc}$ is equal to the composition of $x_{2}$ and $x_{3}$. Then the left homology data of $\mathrm{hkf}$ and $\mathrm{hcc}$ is a left homology data of $S$.

the right homology data of hkf and hcc (from the name)

Let $S$ be a short complex of $C$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Assume that the composition of the inclusion of $\mathrm{kf}$ and the projection of $\mathrm{cc}$ is equal to the composition of $x_{2}$ and $x_{3}$. Then the right homology data of $\mathrm{hkf}$ and $\mathrm{hcc}$ is a right homology data of $S$.

the left homology data of S (from the name)

Let $S$ be a short complex of $C$. Then the left homology data of $S$ is a left 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 Abelian image to kernel of S (from the name)

Let $S$ be a short complex of $C$. Then the Abelian image to kernel of $S$ is a homomorphism of the image of $\operatorname{f}$ applied to $S$ and the kernel of $\operatorname{g}$ applied to $S$.

Let $S$ be a short complex of $C$. Then $\operatorname{abelianImageToKernelIsKernel}$ applied to $S$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the Abelian image to kernel of $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_abelianImageToKernel\_comp\_kernel\_\_u3b9\_\_comp\_cokernel\_\_u3c0\_}$ applied to $S$.

the cokernel to Abelian coimage of S (from the name)

Let $S$ be a short complex of $C$. Then the cokernel to Abelian coimage of $S$ is a homomorphism of the cokernel of $\operatorname{f}$ applied to $S$ and the coimage of $\operatorname{g}$ applied to $S$.

Let $S$ be a short complex of $C$. Then $\operatorname{cokernelToAbelianCoimageIsCokernel}$ applied to $S$ is an element of $\operatorname{IsColimit}$ applied to the projection of the cokernel to Abelian coimage of $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_kernel\_\_u3b9\_\_comp\_cokernel\_\_u3c0\_\_comp\_cokernelToAbelianCoimage}$ applied to $S$.

the homology of S (from the docstring)

Let $S$ be a short complex of $C$. Then the homology of $S$ is an isomorphism of the homology of $S$ and the categorical image of the composition of the cycle of $S$ and $\operatorname{pOpcycles}$ applied to $S$.

the map short complex of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map short complex of $F$ is a functor of the set of short complexes of $C$ and the set of short complexes of $D$.

short complex of C (from the name)

Let $C$ be a set. Then the short complexes of $C$ are a basic type.

homomorphism of x2 and x3 (from the name)

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

the composition of x5 and x6 (from the name)

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

the identity morphism of S (from the docstring)

Let $S$ be a short complex of $C$. Then the identity morphism of $S$ is a homomorphism of $S$ and $S$.

Let $\mathrm{self}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2081\_}$ 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 homomorphism of $x_{2}$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_Hom\_\_\_u3c4\_\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ 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\_\_Hom\_\_\_u3c4\_\_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{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a short complex of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a short complex of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a short complex of $C$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a short complex of $C$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the functor (from the name)

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

Let $\mathrm{self}$ be a short complex of $C$. Then $\operatorname{g}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the functor (from the name)

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

the homomorphism of x5 and x6 (from the name)

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}$. Let $x_{5}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ 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\_u2083\_}$ applied to $x_{3}$. Assume that the composition of $x_{4}$ and $\operatorname{f}$ applied to $x_{3}$ is equal to the composition of $\operatorname{f}$ applied to $x_{2}$ and $x_{5}$. Assume that the composition of $x_{5}$ and $\operatorname{g}$ applied to $x_{3}$ is equal to the composition of $\operatorname{g}$ applied to $x_{2}$ and $x_{6}$. Then the homomorphism of $x_{5}$ and $x_{6}$ is a homomorphism of $x_{2}$ and $x_{3}$ defined as $\operatorname{mk}$ applied to $x_{4}$, $x_{5}$, $x_{6}$, $h$ and $h_{1}$.

the isomorphism of x5 and x6 (from the name)

Let $x_{4}$ be an isomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $x_{3}$. Let $x_{5}$ be an isomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $x_{3}$. Let $x_{6}$ be an isomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $x_{3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{4}$ and $\operatorname{f}$ applied to $x_{3}$ is equal to the composition of $\operatorname{f}$ applied to $x_{2}$ and the homomorphism of $x_{5}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_isoMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{5}$ and $\operatorname{g}$ applied to $x_{3}$ is equal to the composition of $\operatorname{g}$ applied to $x_{2}$ and the homomorphism of $x_{6}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_isoMk\_\_\_auto\_3}$. Then the isomorphism of $x_{5}$ and $x_{6}$ is an isomorphism of $x_{2}$ and $x_{3}$.

the map 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 of $S$ and $F$ is a short complex of $D$.

the map natural isomorphism of S and x4 (from the name)

Let $S$ be a short complex of $C$. Let $x_{4}$ be an isomorphism of $F$ and $G$. Then the map natural isomorphism of $S$ and $x_{4}$ is an isomorphism of the map of $S$ and $F$ and the map of $S$ and $G$.

the map natural transformation of S and x4 (from the name)

Let $S$ be a short complex of $C$. Let $x_{4}$ be a homomorphism of $F$ and $G$. Then the map natural transformation of $S$ and $x_{4}$ is a homomorphism of the map of $S$ and $F$ and the map of $S$ and $G$.

the opposite of S (from the docstring)

Let $S$ be a short complex of $C$. Then the opposite of $S$ is a short complex of the set of opposites of $C$.

the opposite equivalence of C (from the name)

Let $C$ be a set. Then the opposite equivalence of $C$ is an equivalence of the set of opposites of the set of short complexes of $C$ and the set of short complexes of the set of opposites of $C$.

the obvious functor of C (from the docstring)

Let $C$ be a set. Then the obvious functor of $C$ is a functor of the set of opposites of the set of short complexes of $C$ and the set of short complexes of the set of opposites of $C$.

the opposite morphism in x4 (from the docstring)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the opposite morphism in $x_{4}$ is a homomorphism of the opposite of $x_{3}$ and the opposite of $x_{2}$.

the opposite opposite of S (from the name)

Let $S$ be a short complex of $C$. Then the opposite opposite of $S$ is an isomorphism of the opposite of the opposite of $S$ and $S$ defined as the opposite of the application of the unit isomorphism of the opposite equivalence of $C$ and $\operatorname{op}$ applied to $S$.

the opposite of S (from the name)

Let $S$ be a short complex of the set of opposites of $C$. Then the opposite of $S$ is a short complex of $C$.

the obvious functor of C (from the docstring)

Let $C$ be a set. Then the obvious functor of $C$ is a functor of the set of short complexes of the set of opposites of $C$ and the set of opposites of the set of short complexes of $C$.

the opposite map of x4 (from the name)

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

the opposite opposite of S (from the name)

Let $S$ be a short complex of the set of opposites of $C$. Then the opposite opposite of $S$ is an isomorphism of the opposite of the opposite of $S$ and $S$ defined as the application of the counit isomorphism of the opposite equivalence of $C$ and $S$.

the first projection functor (from the docstring)

The first projection functor is a functor of the set of short complexes of $C$ and $C$.

the projection to projection (from the name)

The projection to projection is a homomorphism of the first projection functor and the second projection functor.

the second projection functor (from the docstring)

The second projection functor is a functor of the set of short complexes of $C$ and $C$.

the projection to projection (from the name)

The projection to projection is a homomorphism of the second projection functor and the third projection functor.

the third projection functor (from the docstring)

The third projection functor is a functor of the set of short complexes of $C$ and $C$.

the cycle of S and x5 (from the name)

Let $S$ be a short complex of $C$. Let $x_{5}$ be a carrier of the action of the forgetful functor of $C$ and the set of abelian groups and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ such that $\operatorname{hom}$ applied to the map of the forgetful functor of $C$ and the set of abelian groups and $\operatorname{g}$ applied to $S$ and $x_{5}$ is equal to $0$. Then the cycle of $S$ and $x_{5}$ is a carrier of the action of the forgetful functor of $C$ and the set of abelian groups and the cycle of $S$ defined as $\operatorname{hom}$ applied to the homomorphism of the map cycle isomorphism of $S$ and the forgetful functor of $C$ and the set of abelian groups and $\operatorname{hom}$ applied to the inverse of the abelian group cycle isomorphism of the map of $S$ and the forgetful functor of $C$ and the set of abelian groups and $x_{5}$.

S is exact (from the name)

Let $S$ be a short complex of $C$. Then we can say that $S$ is exact.

Assume that $S$ is exact. 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{desc}$ applied to $\mathrm{hS}$, $k$ and $\mathrm{hk}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and $A$ defined as $\operatorname{desc}$ applied to $\operatorname{gIsCokernel}$ applied to $\mathrm{hS}$ and the projection of $k$ and $\mathrm{hk}$.

Assume that $S$ is exact. Let $f$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $J$ such that the composition of $\operatorname{f}$ applied to $S$ and $f$ is equal to $0$. Then $\operatorname{descToInjective}$ applied to $\mathrm{hS}$, $f$ and $\mathrm{hf}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and $J$ defined as $\operatorname{factorThru}$ applied to $\operatorname{descOpcycles}$ applied to $S$, $f$ and $\mathrm{hf}$ and $\operatorname{fromOpcycles}$ applied to $S$.

Assume that $S$ is exact. 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 $S$ is exact. 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 left homology data of kf and hkf (from the name)

Assume that $S$ is exact. Let $\mathrm{kf}$ be a kernel fork of $\operatorname{g}$ applied to $S$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Then the left homology data of $\mathrm{kf}$ and $\mathrm{hkf}$ is a left homology data of $S$.

the lift of k (from the name)

Assume that $S$ is exact. Let $k$ be a homomorphism of $A$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ such that the composition of $k$ and $\operatorname{g}$ applied to $S$ is equal to $0$. Then the lift of $k$ is a homomorphism of $A$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ defined as the lift of $\operatorname{fIsKernel}$ applied to $\mathrm{hS}$ and the inclusion of $k$ and $\mathrm{hk}$.

Assume that $S$ is exact. Let $f$ be a homomorphism of $P$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ such that the composition of $f$ and $\operatorname{g}$ applied to $S$ is equal to $0$. Then $\operatorname{liftFromProjective}$ applied to $\mathrm{hS}$, $f$ and $\mathrm{hf}$ is a homomorphism of $P$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ defined as $\operatorname{factorThru}$ applied to the lift cycle of $S$ and $f$ and the cycle of $S$.

the right homology data of cc and hcc (from the name)

Assume that $S$ is exact. Let $\mathrm{cc}$ be a cokernel cofork of $\operatorname{f}$ applied to $S$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Then the right homology data of $\mathrm{cc}$ and $\mathrm{hcc}$ is a right homology data of $S$.

splitting of S (from the name)

Let $S$ be a short complex of $C$. Then the splittings of $S$ are a basic type.

Let $s$ be a splitting of $S$. Then $\operatorname{fIsKernel}$ applied to $s$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $\operatorname{f}$ applied to $S$ and $\operatorname{zero}$ applied to $S$ defined as $\operatorname{hi}$ applied to the left of the homology data of $s$.

Let $s$ be a splitting of $S$. Then $\operatorname{gIsCokernel}$ applied to $s$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\operatorname{g}$ applied to $S$ and $\operatorname{zero}$ applied to $S$ defined as $\operatorname{hp}$ applied to the right of the homology data of $s$.

the homology data of s (from the docstring)

Let $s$ be a splitting of $S$. Then the homology data of $s$ is a homology data of $S$.

the isomorphism of h (from the docstring)

Let $h$ be a splitting of $S$. Then the isomorphism of $h$ is an isomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and the biproduct of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$.

the left homology data of s (from the docstring)

Let $s$ be a splitting of $S$. Then the left homology data of $s$ is a left homology data of $S$.

the map of s and F (from the name)

Let $s$ be a splitting of $S$. Let $F$ be a functor of $C$ and $D$. Then the map of $s$ and $F$ is a splitting of the map of $S$ and $F$.

the splitting of S and r (from the name)

Let $S$ be an exact short complex of $C$. Let $r$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ such that the composition of $\operatorname{f}$ applied to $S$ and $r$ is equal to the identity morphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$. Assume that $\operatorname{g}$ applied to $S$ is an epimorphism. Then the splitting of $S$ and $r$ is a splitting of $S$.

the splitting of S and s (from the name)

Let $S$ be an exact short complex of $C$. Let $s$ be a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ such that the composition of $s$ and $\operatorname{g}$ applied to $S$ is equal to the identity morphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$. Assume that $\operatorname{f}$ applied to $S$ is a monomorphism. Then the splitting of $S$ and $s$ is a splitting of $S$.

the obvious splitting of the short complex of x2 and x3 (from the docstring)

Let $x_{2}$ and $x_{3}$ be elements of $C$. Then the obvious splitting of the short complex of $x_{2}$ and $x_{3}$ is a splitting of $\operatorname{mk}$ applied to the left injection, the projection onto the second summand and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Splitting\_\_ofHasBinaryBiproduct\_\_\_proof\_1}$ applied to $x_{2}$ and $x_{3}$.

the splitting of S (from the name)

Let $S$ be a short complex of $C$ such that $\operatorname{f}$ applied to $S$ is an isomorphism and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ is a zero. Then the splitting of $S$ is a splitting of $S$.

the splitting of S (from the name)

Let $S$ be a short complex of $C$ such that $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ is a zero, $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ is a zero and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ is a zero. Then the splitting of $S$ is a splitting of $S$.

the splitting of S (from the name)

Let $S$ be a short complex of $C$ such that $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ is a zero and $\operatorname{g}$ applied to $S$ is an isomorphism. Then the splitting of $S$ is a splitting of $S$.

the splitting of s and e (from the name)

Let $s$ be a splitting of $x_{2}$. Let $e$ be an isomorphism of $x_{2}$ and $x_{3}$. Then the splitting of $s$ and $e$ is a splitting of $x_{3}$.

the opposite of h (from the name)

Let $h$ be a splitting of $S$. Then the opposite of $h$ is a splitting of the opposite of $S$.

Let $\mathrm{self}$ be a splitting of $S$. Then $\operatorname{r}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the right homology data of s (from the docstring)

Let $s$ be a splitting of $S$. Then the right homology data of $s$ is a right homology data of $S$.

Let $\mathrm{self}$ be a splitting of $S$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the split epimorphism of s (from the name)

Let $s$ be a splitting of $S$. Then the split epimorphism of $s$ is a split epimorphism of $\operatorname{g}$ applied to $S$ defined as $\operatorname{mk}$ applied to $\operatorname{s}$ applied to $s$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Splitting\_\_s\_g}$ applied to $s$.

Let $s$ be a splitting of $S$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_Splitting\_\_splitMono\_f}$ applied to $s$ is a split monomorphism of $\operatorname{f}$ applied to $S$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ applied to $s$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_Splitting\_\_f\_r}$ applied to $s$.

the opposite of h (from the name)

Let $h$ be a splitting of $S$. Then the opposite of $h$ is a splitting of the opposite of $S$.

the cokernel sequence of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the cokernel sequence of $f$ is a short complex of $C$.

the kernel sequence of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the kernel sequence of $f$ is a short complex of $C$.

the counit isomorphism of the equivalence of J and C (from the docstring)

Let $J$ and $C$ be sets. Then the counit isomorphism of the equivalence of $J$ and $C$ is an isomorphism of the composition of the inverse of $J$ and $C$ and the obvious functor of $J$ and $C$ and the identity of the set of functors of $J$ and the set of short complexes of $C$.

the obvious functor of J and C (from the docstring)

Let $J$ and $C$ be sets. Then the obvious functor of $J$ and $C$ is a functor of the set of short complexes of the set of functors of $J$ and $C$ and the set of functors of $J$ and the set of short complexes of $C$.

the inverse of J and C (from the name)

Let $J$ and $C$ be sets. Then the inverse of $J$ and $C$ is a functor of the set of functors of $J$ and the set of short complexes of $C$ and the set of short complexes of the set of functors of $J$ and $C$.

the unit isomorphism of the equivalence of J and C (from the docstring)

Let $J$ and $C$ be sets. Then the unit isomorphism of the equivalence of $J$ and $C$ is an isomorphism of the identity of the set of short complexes of the set of functors of $J$ and $C$ and the composition of the obvious functor of $J$ and $C$ and the inverse of $J$ and $C$.

the obvious equivalence of J and C (from the docstring)

Let $J$ and $C$ be sets. Then the obvious equivalence of $J$ and $C$ is an equivalence of the set of short complexes of the set of functors of $J$ and $C$ and the set of functors of $J$ and the set of short complexes of $C$.

the canonical isomorphism of K (from the docstring)

Let $K$ be a chain complex of $C$ and $\Natural$. Then the canonical isomorphism of $K$ is an isomorphism of the cycle of $K$ and $0$ and $\operatorname{X}$ applied to $K$ and $0$.

the canonical isomorphism of K (from the docstring)

Let $K$ be a chain complex of $C$ and $\Natural$. Then the canonical isomorphism of $K$ is an isomorphism of the homology of $K$ and $0$ and $\operatorname{opcycles}$ applied to $K$ and $0$.

the canonical isomorphism of K (from the docstring)

Let $K$ be a cochain complex of $C$ and $\Natural$. Then the canonical isomorphism of $K$ is an isomorphism of the cycle of $K$ and $0$ and the homology of $K$ and $0$.

the canonical isomorphism of K (from the docstring)

Let $K$ be a cochain complex of $C$ and $\Natural$. Then the canonical isomorphism of $K$ is an isomorphism of $\operatorname{X}$ applied to $K$ and $0$ and $\operatorname{opcycles}$ applied to $K$ and $0$.

K is acyclic (from the name)

Let $K$ be a homological complex of $C$ and $c$. Then $K$ is acyclic, if for all elements $i$ of $x_{2}$, $\operatorname{ExactAt}$ holds for $K$ and $i$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then $\operatorname{ExactAt}$ holds for $K$ and $i$, if $\operatorname{sc}$ applied to $K$ and $i$ is exact.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then $\operatorname{HasHomology}$ holds for $K$ and $i$, if $\operatorname{sc}$ applied to $K$ and $i$ has a homology.

the cycle of K and i (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then the cycle of $K$ and $i$ is an element of $C$ defined as the cycle of $\operatorname{sc}$ applied to $K$ and $i$.

the cycle functor of c and i (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$ be an element of $x_{2}$. Then the cycle functor of $c$ and $i$ is a functor of the set of homological complexes of $C$ and $c$ and $C$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{next} (c , i)}{j}$. Then $\operatorname{cyclesIsKernel}$ applied to $K$, $i$, $j$ and $\mathrm{hj}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of the cycles of $K$ and $i$ and $\mathrm{HomologicalComplex\_\_iCycles\_d}$ applied to $K$, $i$ and $j$ defined as $\operatorname{ndrec}$ applied to $\operatorname{cyclesIsKernel}$ applied to $\operatorname{sc}$ applied to $K$ and $i$ and $\mathrm{hj}$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$, $j$ and $k$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$ and $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Then $\operatorname{cyclesIsoSc'}$ applied to $K$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$ is an isomorphism of the cycle of $K$ and $j$ and the cycle of $\operatorname{sc'}$ applied to $K$, $i$, $j$ and $k$ defined as the isomorphism of $\operatorname{isoSc'}$ applied to $K$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$.

the map of x3 and i (from the docstring)

Let $x_{3}$ be a homomorphism of $K$ and $L$. Let $i$ be an element of $x_{2}$. Then the map of $x_{3}$ and $i$ is a homomorphism of the cycle of $K$ and $i$ and the cycle of $L$ and $i$ defined as the cycle map of the map of the short complex functor of $c$ and $i$ and $x_{3}$.

the isomorphism of iso and i (from the docstring)

Let $\mathrm{iso}$ be an isomorphism of $K$ and $L$. Let $i$ be an element of $x_{2}$. Then the isomorphism of $\mathrm{iso}$ and $i$ is an isomorphism of the cycle of $K$ and $i$ and the cycle of $L$ and $i$.

Let $K$ be a homological complex of $C$ and $c$. Let $k$ be a homomorphism of $\operatorname{X}$ applied to $K$ and $i$ and $A$. Let $j$ be an element of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , i)}{j}$ and the composition of $\operatorname{d}$ applied to $K$, $j$ and $i$ and $k$ is equal to $0$. Then $\operatorname{descOpcycles}$ applied to $K$, $k$, $j$, $\mathrm{hj}$ and $\mathrm{hk}$ is a homomorphism of $\operatorname{opcycles}$ applied to $K$ and $i$ and $A$.

Let $K$ be a homological complex of $C$ and $c$. Let $k$ be a homomorphism of $\operatorname{X}$ applied to $K$ and $i$ and $A$. Let $j$ be an element of $x_{2}$ such that $\operatorname{Rel}$ holds for $c$, $j$ and $i$ and the composition of $\operatorname{d}$ applied to $K$, $j$ and $i$ and $k$ is equal to $0$. Then $\operatorname{descOpcycles'}$ applied to $K$, $k$, $j$, $\mathrm{hj}$ and $\mathrm{hk}$ is a homomorphism of $\operatorname{opcycles}$ applied to $K$ and $i$ and $A$ defined as $\operatorname{descOpcycles}$ applied to $K$, $k$, $j$, $\mathrm{ComplexShape\_\_prev\_eq'}$ applied to $c$ and $\mathrm{hj}$ and $\mathrm{hk}$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$. Then $\operatorname{fromOpcycles}$ applied to $K$, $i$ and $j$ is a homomorphism of $\operatorname{opcycles}$ applied to $K$ and $i$ and $\operatorname{X}$ applied to $K$ and $j$.

the graded homology functor of C and c (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Then the graded homology functor of $C$ and $c$ is a functor of the set of homological complexes of $C$ and $c$ and the set of graded objects of $x_{2}$ and $C$.

the homology of K and i (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then the homology of $K$ and $i$ is an element of $C$ defined as the homology of $\operatorname{sc}$ applied to $K$ and $i$.

the homology functor of c and i (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$ be an element of $x_{2}$. Then the homology functor of $c$ and $i$ is a functor of the set of homological complexes of $C$ and $c$ and $C$.

the homology functor isomorphism of c and i (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$ be an element of $x_{2}$. Then the homology functor isomorphism of $c$ and $i$ is an isomorphism of the homology functor of $c$ and $i$ and the composition of the short complex functor of $c$ and $i$ and the homology functor of $C$ defined as the identity of the homology functor of $c$ and $i$.

the homology functor isomorphism of j and k (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$, $j$ and $k$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$ and $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Then the homology functor isomorphism of $j$ and $k$ is an isomorphism of the homology functor of $c$ and $j$ and the composition of the short complex functor of $j$ and $k$ and the homology functor of $C$ defined as the composition of the homology functor isomorphism of $c$ and $j$ and the right isomorphism whisker of $\operatorname{natIsoSc'}$ applied to $C$, $c$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$ and the homology functor of $C$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$. Then $\operatorname{homologyIsCokernel}$ applied to $K$, $i$, $j$ and $\mathrm{hi}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the homology projection of $K$ and $j$ and $\mathrm{HomologicalComplex\_\_toCycles\_comp\_homology\_u3c0\_}$ applied to $K$, $i$ and $j$ defined as $\operatorname{ndrec}$ applied to the homology of $\operatorname{sc}$ applied to $K$ and $j$ and $\mathrm{hi}$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{next} (c , i)}{j}$. Then $\operatorname{homologyIsKernel}$ applied to $K$, $i$, $j$ and $\mathrm{hi}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion map of the homology of $K$ and $i$ and $\mathrm{HomologicalComplex\_\_homology\_u3b9\_\_comp\_fromOpcycles}$ applied to $K$, $i$ and $j$ defined as $\operatorname{ndrec}$ applied to the homology of $\operatorname{sc}$ applied to $K$ and $i$ and $\mathrm{hi}$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$, $j$ and $k$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$ and $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Then $\operatorname{homologyIsoSc'}$ applied to $K$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$ is an isomorphism of the homology of $K$ and $j$ and the homology of $\operatorname{sc'}$ applied to $K$, $i$, $j$ and $k$ defined as the homology isomorphism of $\operatorname{isoSc'}$ applied to $K$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$.

the map of x3 and i (from the docstring)

Let $x_{3}$ be a homomorphism of $K$ and $L$. Let $i$ be an element of $x_{2}$. Then the map of $x_{3}$ and $i$ is a homomorphism of the homology of $K$ and $i$ and the homology of $L$ and $i$ defined as the homology map of the map of the short complex functor of $c$ and $i$ and $x_{3}$.

the isomorphism of iso and i (from the docstring)

Let $\mathrm{iso}$ be an isomorphism of $K$ and $L$. Let $i$ be an element of $x_{2}$. Then the isomorphism of $\mathrm{iso}$ and $i$ is an isomorphism of the homology of $K$ and $i$ and the homology of $L$ and $i$.

the inclusion map of the homology of K and i (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then the inclusion map of the homology of $K$ and $i$ is a homomorphism of the homology of $K$ and $i$ and $\operatorname{opcycles}$ applied to $K$ and $i$ defined as the homology inclusion of $\operatorname{sc}$ applied to $K$ and $i$.

the homology projection of K and i (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then the homology projection of $K$ and $i$ is a homomorphism of the cycle of $K$ and $i$ and the homology of $K$ and $i$ defined as the homology projection of $\operatorname{sc}$ applied to $K$ and $i$.

the inclusion of the cycles of K and i (from the docstring)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then the inclusion of the cycles of $K$ and $i$ is a homomorphism of the cycle of $K$ and $i$ and $\operatorname{X}$ applied to $K$ and $i$ defined as the cycle of $\operatorname{sc}$ applied to $K$ and $i$.

the cycle isomorphism of i and j (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{next} (c , i)}{j}$ and $\EqtMACRoH {\operatorname{d} (K , i , j)}{0}$. Then the cycle isomorphism of $i$ and $j$ is an isomorphism of the cycle of $K$ and $i$ and $\operatorname{X}$ applied to $K$ and $i$ defined as $\operatorname{asIso}$ applied to the inclusion of the cycles of $K$ and $i$.

the isomorphism homology inclusion of i and j (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{next} (c , i)}{j}$ and $\EqtMACRoH {\operatorname{d} (K , i , j)}{0}$. Then the isomorphism homology inclusion of $i$ and $j$ is an isomorphism of the homology of $K$ and $i$ and $\operatorname{opcycles}$ applied to $K$ and $i$ defined as $\operatorname{asIso}$ applied to the inclusion map of the homology of $K$ and $i$.

the isomorphism homology projection of i and j (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$ and $\EqtMACRoH {\operatorname{d} (K , i , j)}{0}$. Then the isomorphism homology projection of $i$ and $j$ is an isomorphism of the cycle of $K$ and $j$ and the homology of $K$ and $j$ defined as $\operatorname{asIso}$ applied to the homology projection of $K$ and $j$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$, $j$ and $k$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$ and $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Then $\operatorname{isoSc'}$ applied to $K$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$ is an isomorphism of $\operatorname{sc}$ applied to $K$ and $j$ and $\operatorname{sc'}$ applied to $K$, $i$, $j$ and $k$ defined as the application of $\operatorname{natIsoSc'}$ applied to $C$, $c$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$ and $K$.

the lift cycle of k and j (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $k$ be a homomorphism of $A$ and $\operatorname{X}$ applied to $K$ and $i$. Let $j$ be an element of $x_{2}$ such that $\EqtMACRoH {\operatorname{next} (c , i)}{j}$ and the composition of $k$ and $\operatorname{d}$ applied to $K$, $i$ and $j$ is equal to $0$. Then the lift cycle of $k$ and $j$ is a homomorphism of $A$ and the cycle of $K$ and $i$.

the lift cycle of k and j (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $k$ be a homomorphism of $A$ and $\operatorname{X}$ applied to $K$ and $i$. Let $j$ be an element of $x_{2}$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$ and the composition of $k$ and $\operatorname{d}$ applied to $K$, $i$ and $j$ is equal to $0$. Then the lift cycle of $k$ and $j$ is a homomorphism of $A$ and the cycle of $K$ and $i$ defined as the lift cycle of $k$ and $j$.

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$, $j$ and $k$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$ and $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Then $\operatorname{natIsoSc'}$ applied to $C$, $c$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$ is an isomorphism of the short complex functor of $c$ and $j$ and the short complex functor of $j$ and $k$.

the natural transformation homology inclusion of c and i (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$ be an element of $x_{2}$. Then the natural transformation homology inclusion of $c$ and $i$ is a homomorphism of the homology functor of $c$ and $i$ and $\operatorname{opcyclesFunctor}$ applied to $C$, $c$ and $i$.

the natural transformation homology projection of c and i (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$ be an element of $x_{2}$. Then the natural transformation homology projection of $c$ and $i$ is a homomorphism of the cycle functor of $c$ and $i$ and the homology functor of $c$ and $i$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then $\operatorname{opcycles}$ applied to $K$ and $i$ is an element of $C$ defined as $\operatorname{opcycles}$ applied to $\operatorname{sc}$ applied to $K$ and $i$.

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

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$. Then $\operatorname{opcyclesIsCokernel}$ applied to $K$, $i$, $j$ and $\mathrm{hi}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\operatorname{pOpcycles}$ applied to $K$ and $j$ and $\mathrm{HomologicalComplex\_\_d\_pOpcycles}$ applied to $K$, $i$ and $j$ defined as $\operatorname{ndrec}$ applied to the function that maps $h_{2}$ to $\operatorname{opcyclesIsCokernel}$ applied to $\operatorname{sc}$ applied to $K$ and $j$, $\mathrm{hi}$ and $h$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$, $j$ and $k$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$ and $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Then $\operatorname{opcyclesIsoSc'}$ applied to $K$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$ is an isomorphism of $\operatorname{opcycles}$ applied to $K$ and $j$ and $\operatorname{opcycles}$ applied to $\operatorname{sc'}$ applied to $K$, $i$, $j$ and $k$ defined as the isomorphism of $\operatorname{isoSc'}$ applied to $K$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$.

the map of x3 and i (from the docstring)

Let $x_{3}$ be a homomorphism of $K$ and $L$. Let $i$ be an element of $x_{2}$. Then the map of $x_{3}$ and $i$ is a homomorphism of $\operatorname{opcycles}$ applied to $K$ and $i$ and $\operatorname{opcycles}$ applied to $L$ and $i$ defined as $\operatorname{opcyclesMap}$ applied to the map of the short complex functor of $c$ and $i$ and $x_{3}$.

the isomorphism of iso and i (from the docstring)

Let $\mathrm{iso}$ be an isomorphism of $K$ and $L$. Let $i$ be an element of $x_{2}$. Then the isomorphism of $\mathrm{iso}$ and $i$ is an isomorphism of $\operatorname{opcycles}$ applied to $K$ and $i$ and $\operatorname{opcycles}$ applied to $L$ and $i$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then $\operatorname{pOpcycles}$ applied to $K$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $K$ and $i$ and $\operatorname{opcycles}$ applied to $K$ and $i$ defined as $\operatorname{pOpcycles}$ applied to $\operatorname{sc}$ applied to $K$ and $i$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$ and $\EqtMACRoH {\operatorname{d} (K , i , j)}{0}$. Then $\operatorname{pOpcyclesIso}$ applied to $K$, $i$, $j$, $\mathrm{hi}$ and $h$ is an isomorphism of $\operatorname{X}$ applied to $K$ and $j$ and $\operatorname{opcycles}$ applied to $K$ and $j$ defined as $\operatorname{asIso}$ applied to $\operatorname{pOpcycles}$ applied to $K$ and $j$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $x_{2}$. Then $\operatorname{sc}$ applied to $K$ and $i$ is a short complex of $C$ defined as the action of the short complex functor of $c$ and $i$ and $K$.

Let $K$ be a homological complex of $C$ and $c$. Let $i$, $j$ and $k$ be elements of $x_{2}$. Then $\operatorname{sc'}$ applied to $K$, $i$, $j$ and $k$ is a short complex of $C$ defined as the action of the short complex functor of $j$ and $k$ and $K$.

the short complex functor of c and i (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$ be an element of $x_{2}$. Then the short complex functor of $c$ and $i$ is a functor of the set of homological complexes of $C$ and $c$ and the set of short complexes of $C$ defined as the short complex functor of $i$ and $\operatorname{next}$ applied to $c$ and $i$.

the short complex functor of j and k (from the name)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Let $i$, $j$ and $k$ be elements of $x_{2}$. Then the short complex functor of $j$ and $k$ is a functor of the set of homological complexes of $C$ and $c$ and the set of short complexes of $C$.

the cycle of i and j (from the name)

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$. Then the cycle of $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to $K$ and $i$ and the cycle of $K$ and $j$.

C is a category with homology (from the name)

Let $C$ be a set. Then we can say that $C$ is a category with homology.

S has a homology (from the name)

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

homology data of S (from the name)

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

Let $S$ be a short complex of $C$. Then $\operatorname{canonical}$ applied to $S$ is a homology data of $S$.

the isomorphism of self (from the name)

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

the left of self (from the name)

Let $\mathrm{self}$ be a homology data of $S$. Then the left of $\mathrm{self}$ is a left homology data of $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the 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 homology data of $x_{2}$. Then the homology data of $x_{4}$ and $h$ is a homology data of $x_{3}$.

the 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 homology data of $x_{3}$. Then the homology data of $x_{4}$ and $h$ is a homology data of $x_{2}$.

the 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 homology data of $S$ and $\mathrm{hg}$ is a homology data of $S$.

the 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 homology data of $S$ and $\mathrm{hf}$ is a homology data of $S$.

the 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 homology data of $c$ and $\mathrm{hc}$ is a homology data of $S$.

the homology data of x2 and x3 (from the name)

Let $x_{2}$ be a left homology data of $S$. Let $x_{3}$ be a right homology data of $S$. Then the homology data of $x_{2}$ and $x_{3}$ is a homology data of $S$.

the 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 homology data of $c$ and $\mathrm{hc}$ is a homology data of $S$.

the homology data of e and h (from the name)

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

the 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 homology data of $S$ is a homology data of $S$.

the opposite of h (from the name)

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

the right of self (from the name)

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

the opposite of h (from the name)

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

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 homology data of $x_{2}$. Let $x_{6}$ be a homology data of $x_{3}$. Then the homology map data of $x_{5}$ and $x_{6}$ are a basic type.

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

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

the compatibility of c and hc (from the name)

Assume that $\EqtMACRoH {\operatorname{f} (S)}{0}$. Assume 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 compatibility of $c$ and $\mathrm{hc}$ is a homology map data of the homology data of $S$ and the homology data of $c$ and $\mathrm{hc}$ defined as $\operatorname{mk}$ applied to the compatibility of $c$ and $\mathrm{hc}$ and the compatibility of $c$ and $\mathrm{hc}$.

the compatibility of c and hc (from the name)

Assume that $\EqtMACRoH {\operatorname{f} (S)}{0}$. Assume that $\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 homology map data of the homology data of $c$ and $\mathrm{hc}$ and the homology data of $S$ defined as $\operatorname{mk}$ applied to the compatibility of $c$ and $\mathrm{hc}$ and the compatibility of $c$ and $\mathrm{hc}$.

the 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 homology data of $x_{2}$. Let $x_{6}$ be a homology data of $x_{3}$. Then the homology map data of $x_{5}$ and $x_{6}$ is a homology map data of $x_{5}$ and $x_{6}$ defined as $\operatorname{default}$.

the identity of h (from the name)

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

the left of self (from the name)

Let $\mathrm{self}$ be a homology map data of $x_{5}$ and $x_{6}$. Then the left of $\mathrm{self}$ is a left homology map data of the left of $x_{5}$ and the left of $x_{6}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the 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 homology data of $x_{2}$. Then the homology map data of $x_{4}$ and $h$ is a homology map data of $h$ and the homology data of $x_{4}$ and $h$ defined as $\operatorname{mk}$ applied to the left homology map data of $x_{4}$ and the left of $h$ and the right homology map data of $x_{4}$ and the right of $h$.

the 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 homology data of $x_{3}$. Then the homology map data of $x_{4}$ and $h$ is a homology map data of the homology data of $x_{4}$ and $h$ and $h$ defined as $\operatorname{mk}$ applied to the left homology map data of $x_{4}$ and the left of $h$ and the right homology map data of $x_{4}$ and the right of $h$.

the 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 homology map data of $x_{8}$ and $f$ is a homology map data of the homology data of $x_{5}$ and $x_{6}$ and the homology data of $x_{7}$ and $x_{8}$ defined as $\operatorname{mk}$ applied to the left homology map data of $x_{8}$ and $f$ and the right homology map data of $x_{8}$ and $f$.

the 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 homology map data of $x_{8}$ and $f$ is a homology map data of the homology data of $x_{5}$ and $x_{6}$ and the homology data of $x_{7}$ and $x_{8}$ defined as $\operatorname{mk}$ applied to the left homology map data of $x_{8}$ and $f$ and the right homology map data of $x_{8}$ and $f$.

the 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 homology map data of $x_{4}$ is a homology map data of the homology data of $x_{2}$ and the homology data of $x_{3}$ defined as $\operatorname{mk}$ applied to the left homology map data of $x_{4}$ and the right homology map data of $x_{4}$.

the opposite of x7 (from the name)

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

the right of self (from the name)

Let $\mathrm{self}$ be a homology map data of $x_{5}$ and $x_{6}$. Then the right of $\mathrm{self}$ is a right homology map data of the right of $x_{5}$ and the right of $x_{6}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the opposite of x7 (from the name)

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

the zero of x4 and x5 (from the name)

Let $x_{4}$ be a homology data of $x_{2}$. Let $x_{5}$ be a homology data of $x_{3}$. Then the zero of $x_{4}$ and $x_{5}$ is a homology map data of $x_{4}$ and $x_{5}$ defined as $\operatorname{mk}$ applied to the zero of the left of $x_{4}$ and the left of $x_{5}$ and the zero of the right of $x_{4}$ and the right of $x_{5}$.

Let $S$ be a short complex of $C$. Then $\operatorname{canonical}$ applied to $S$ is a left homology data of $S$.

the homology isomorphism of h (from the name)

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

Let $S$ be a short complex of $C$. Then $\operatorname{canonical}$ applied to $S$ is a right homology data of $S$.

the homology isomorphism of h (from the name)

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

the canonical isomorphism of S and hg (from the docstring)

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

the canonical isomorphism of S and hf (from the docstring)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{f} (S)}{0}$. Then the canonical isomorphism of $S$ and $\mathrm{hf}$ is an isomorphism of the cycle of $S$ and the homology of $S$ defined as $\operatorname{asIso}$ applied to the homology projection of $S$.

Let $S$ be a short complex of $C$. Let $k$ be a homomorphism of the cycle of $S$ and $A$ such that the composition of the cycle of $S$ and $k$ is equal to $0$. Then $\operatorname{descHomology}$ applied to $S$, $k$ and $\mathrm{hk}$ is a homomorphism of the homology of $S$ and $A$ defined as $\operatorname{desc}$ applied to the homology of $S$ and the projection of $k$ and $\mathrm{hk}$.

the homology of S (from the docstring)

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

the homology data of S (from the name)

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

the homology functor of C (from the docstring)

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

the natural isomorphism of C (from the docstring)

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

the homology of S (from the docstring)

Let $S$ be a short complex of $C$. Then the homology of $S$ is an element of $\operatorname{IsColimit}$ applied to the projection of the homology projection of $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_toCycles\_comp\_homology\_u3c0\_}$ applied to $S$.

the homology of S (from the docstring)

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

the homology of S (from the docstring)

Let $S$ be a short complex of $C$. Then the homology of $S$ is an isomorphism of the homology of $S$ and the cokernel of the lift of $\operatorname{g}$ applied to $S$ and $\operatorname{f}$ applied to $S$ defined as the composition of the inverse of the left homology isomorphism of $S$ and the left homology.

the homology of S (from the docstring)

Let $S$ be a short complex of $C$. Then the homology of $S$ is an isomorphism of the 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 composition of the inverse of the right homology isomorphism of $S$ and the right homology of $S$.

the homology map of x4 (from the docstring)

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

the 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 homology data of $x_{2}$. Let $x_{6}$ be a homology data of $x_{3}$. Then the homology map of $x_{5}$ and $x_{6}$ is a homomorphism of $\operatorname{H}$ applied to the left of $x_{5}$ and $\operatorname{H}$ applied to the left of $x_{6}$ defined as the left homology map of the left of $x_{5}$ and the left of $x_{6}$.

the homology isomorphism of e (from the docstring)

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

the 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 homology data of $x_{2}$. Let $x_{5}$ be a homology data of $x_{3}$. Then the homology map isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $\operatorname{H}$ applied to the left of $x_{4}$ and $\operatorname{H}$ applied to the left of $x_{5}$.

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 the homology of the opposite of $S$ and $\operatorname{op}$ applied to the homology of $S$ defined as the composition of the inverse of the left homology isomorphism of the opposite of $S$ and the composition of the left homology in the opposite category of the opposite of $S$ and the opposite isomorphism of the inverse of the right homology isomorphism of $S$.

the homology inclusion of S (from the name)

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

the homology projection of S (from the name)

Let $S$ be a short complex of $C$. Then the homology projection of $S$ is a homomorphism of the cycle of $S$ and the homology of $S$ defined as the composition of the left homology projection of $S$ and the homomorphism of the left homology isomorphism of $S$.

the left homology isomorphism of S (from the name)

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

the left right homology comparison of S (from the name)

Let $S$ be a short complex of $C$. Then the left right homology comparison of $S$ is a homomorphism of the left homology of $S$ and the right homology of $S$ defined as the left right homology comparison of the left homology data of $S$ and the right homology data of $S$.

the left right homology comparison of x2 and x3 (from the name)

Let $x_{2}$ be a left homology data of $S$. Let $x_{3}$ be a right homology data of $S$. Then the left right homology comparison of $x_{2}$ and $x_{3}$ is a homomorphism of $\operatorname{H}$ applied to $x_{2}$ and $\operatorname{H}$ applied to $x_{3}$.

the lift homology of S and k (from the name)

Let $S$ be a short complex of $C$. Let $k$ be a homomorphism of $A$ and $\operatorname{opcycles}$ applied to $S$ such that the composition of $k$ and $\operatorname{fromOpcycles}$ applied to $S$ is equal to $0$. Then the lift homology of $S$ and $k$ is a homomorphism of $A$ and the homology of $S$ defined as the lift of the homology of $S$ and the inclusion of $k$ and $\mathrm{hk}$.

the right homology isomorphism of S (from the name)

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

S has a left homology (from the name)

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

left homology data of S (from the name)

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

Let $\mathrm{self}$ be a left 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 left homology data of $S$. Then $\operatorname{K}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the copy of eK and eH (from the name)

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

the isomorphism of h (from the docstring)

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

Let $h$ be a left homology data of $S$. Let $k$ be a homomorphism of $\operatorname{K}$ applied to $h$ and $A$ such that the composition of $\operatorname{f'}$ applied to $h$ 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 $\operatorname{desc}$ applied to the projection of $h$ and the projection of $k$ and $\mathrm{hk}$.

Let $h$ be a left homology data of $S$. Then $\operatorname{f'}$ applied to $h$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $\operatorname{K}$ applied to $h$ defined as the lift of $h$ and $\operatorname{f}$ applied to $S$.

Let $\mathrm{self}$ be a left homology data of $S$. Then $\operatorname{hi}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $\operatorname{i}$ applied to $\mathrm{self}$ and $\operatorname{wi}$ applied to $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

the projection of self (from the name)

Let $\mathrm{self}$ be a left homology data of $S$. Then the projection of $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_LeftHomologyData\_\_w\_u3c0\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$.

the projection of h (from the name)

Let $h$ be a left homology data of $S$. Then the projection of $h$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $h$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_LeftHomologyData\_\_f'\_\_u3c0\_}$ applied to $h$ defined as the projection of $h$.

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

the isomorphism of h (from the docstring)

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

the lift of h and k (from the name)

Let $h$ be a left homology data of $S$. Let $k$ be a homomorphism of $A$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ such that the composition of $k$ and $\operatorname{g}$ applied to $S$ 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 composition of the lift of $h$ and $k$ and the projection of $h$.

the lift of h and k (from the name)

Let $h$ be a left homology data of $S$. Let $k$ be a homomorphism of $A$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ such that the composition of $k$ and $\operatorname{g}$ applied to $S$ is equal to $0$. Then the lift of $h$ and $k$ is a homomorphism of $A$ and $\operatorname{K}$ applied to $h$ defined as the lift of $\operatorname{hi}$ applied to $h$ and the inclusion of $k$ and $\mathrm{hk}$.

the left 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 left homology data of $x_{2}$. Then the left homology data of $x_{4}$ and $h$ is a left homology data of $x_{3}$.

the left 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 left homology data of $x_{3}$. Then the left homology data of $x_{4}$ and $h$ is a left homology data of $x_{2}$.

the left 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 left homology data of $S$ and $\mathrm{hg}$ is a left homology data of $S$.

the left 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 left homology data of $S$ and $\mathrm{hf}$ is a left homology data of $S$.

the left homology data of S (from the name)

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

the left 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 left homology data of $c$ and $\mathrm{hc}$ is a left homology data of $S$.

the left 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 left homology data of $c$ and $\mathrm{hc}$ is a left homology data of $S$.

the left 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 left homology data of $x_{2}$. Then the left homology data of $e$ and $x_{4}$ is a left homology data of $x_{3}$ defined as the left homology data of the homomorphism of $e$ and $x_{4}$.

the left 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 left homology data of $S$ is a left homology data of $S$.

the projection of self (from the name)

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

left 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 left homology data of $x_{2}$. Let $x_{6}$ be a left homology data of $x_{3}$. Then the left homology map data of $x_{5}$ and $x_{6}$ are a basic type.

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

Let $x_{10}$ be a left homology map data of $x_{7}$ and $x_{8}$. Let $x_{11}$ be a left homology map data of $x_{8}$ and $x_{9}$. Then the composition of left homology map data of $x_{10}$ and $x_{11}$ is a left 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 left homology map data of the left homology data of $S$ and the left 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 left homology map data of the left homology data of $c$ and $\mathrm{hc}$ and the left homology data of $S$.

the identity of h (from the name)

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

the left 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 left homology data of $x_{2}$. Then the left homology map data of $x_{4}$ and $h$ is a left homology map data of $h$ and the left homology data of $x_{4}$ and $h$.

the left 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 left homology data of $x_{3}$. Then the left homology map data of $x_{4}$ and $h$ is a left homology map data of the left homology data of $x_{4}$ and $h$ and $h$.

the left 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 left homology map data of $x_{8}$ and $f$ is a left homology map data of the left homology data of $x_{5}$ and $x_{6}$ and the left homology data of $x_{7}$ and $x_{8}$.

the left 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 left homology map data of $x_{8}$ and $f$ is a left homology map data of the left homology data of $x_{5}$ and $x_{6}$ and the left homology data of $x_{7}$ and $x_{8}$.

the left 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 left homology map data of $x_{4}$ is a left homology map data of the left homology data of $x_{2}$ and the left homology data of $x_{3}$.

the zero of x4 and x5 (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}$. Then the zero of $x_{4}$ and $x_{5}$ is a left homology map data of $x_{4}$ and $x_{5}$.

Let $\mathrm{self}$ be a left homology map data of $x_{5}$ and $x_{6}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_LeftHomologyMapData\_\_\_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 left homology map data of $x_{5}$ and $x_{6}$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_LeftHomologyMapData\_\_\_u3c6\_K}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{K}$ applied to $x_{5}$ and $\operatorname{K}$ applied to $x_{6}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the cycle of S (from the name)

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

the cycle functor of C (from the name)

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

Let $S$ be a short complex of $C$. Then $\operatorname{cyclesIsKernel}$ applied to $S$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the cycle of $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_iCycles\_g}$ applied to $S$ defined as $\operatorname{hi}$ applied to the left 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 the cycle of $S$ and the kernel of $\operatorname{g}$ applied to $S$.

the cycle isomorphism left homology of S and hf (from the name)

Let $S$ be a short complex of $C$ such that $\EqtMACRoH {\operatorname{f} (S)}{0}$. Then the cycle isomorphism left homology of $S$ and $\mathrm{hf}$ is an isomorphism of the cycle of $S$ and the left homology of $S$ defined as $\operatorname{asIso}$ applied to the left homology projection of $S$.

the cycle isomorphism of S and hg (from the name)

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

the cycle map of x4 (from the name)

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

the cycle 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 left homology data of $x_{2}$. Let $x_{6}$ be a left homology data of $x_{3}$. Then the cycle map of $x_{5}$ and $x_{6}$ is a homomorphism of $\operatorname{K}$ applied to $x_{5}$ and $\operatorname{K}$ applied to $x_{6}$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_LeftHomologyMapData\_\_\_u3c6\_K}$ applied to the left 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 the cycle of $x_{2}$ and the cycle of $x_{3}$.

the cycle 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 left homology data of $x_{2}$. Let $x_{5}$ be a left homology data of $x_{3}$. Then the cycle map isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $\operatorname{K}$ applied to $x_{4}$ and $\operatorname{K}$ applied to $x_{5}$.

the cycle of S (from the name)

Let $S$ be a short complex of $C$. Then the cycle of $S$ is a homomorphism of the cycle of $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ defined as $\operatorname{i}$ applied to the left 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 cycle functor of $C$ and the second projection functor.

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

Let $S$ be a short complex of $C$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Then the isomorphism from the point of $S$ and $\mathrm{hkf}$ is an isomorphism of $\operatorname{pt}$ applied to $\mathrm{kf}$ and the cycle of $S$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\mathrm{hkf}$ and $\operatorname{cyclesIsKernel}$ applied to $S$.

the left homology of S (from the docstring)

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

the left homology data of S (from the name)

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

the left homology functor of C (from the docstring)

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

Let $S$ be a short complex of $C$. Then $\operatorname{leftHomologyIsCokernel}$ applied to $S$ is an element of $\operatorname{IsColimit}$ applied to the projection of the left homology projection of $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_toCycles\_comp\_leftHomology\_u3c0\_}$ applied to $S$ defined as the projection of the left homology data of $S$.

the left homology (from the docstring)

The left homology is an isomorphism of the left homology of $S$ and the cokernel of the lift of $\operatorname{g}$ applied to $S$ and $\operatorname{f}$ applied to $S$ defined as the isomorphism of the left homology data of $S$.

the left homology map of x4 (from the name)

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

the left 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 left homology data of $x_{2}$. Let $x_{6}$ be a left homology data of $x_{3}$. Then the left 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\_\_LeftHomologyMapData\_\_\_u3c6\_H}$ applied to the left homology map data of $x_{5}$ and $x_{6}$.

the left 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 left homology data of $x_{2}$. Let $x_{6}$ be a left homology data of $x_{3}$. Then the left homology map data of $x_{5}$ and $x_{6}$ is a left 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 left homology of $x_{2}$ and the left homology of $x_{3}$.

the left 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 left homology data of $x_{2}$. Let $x_{5}$ be a left homology data of $x_{3}$. Then the left 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 left homology projection of S (from the name)

Let $S$ be a short complex of $C$. Then the left homology projection of $S$ is a homomorphism of the cycle of $S$ and the left homology of $S$ defined as the projection of the left 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 cycle functor of $C$ and the left homology functor of $C$.

the lift cycle of S and k (from the name)

Let $S$ be a short complex of $C$. Let $k$ be a homomorphism of $A$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ such that the composition of $k$ and $\operatorname{g}$ applied to $S$ is equal to $0$. Then the lift cycle of $S$ and $k$ is a homomorphism of $A$ and the cycle of $S$ defined as the lift of the left homology data of $S$ and $k$.

the lift left homology of S and k (from the name)

Let $S$ be a short complex of $C$. Let $k$ be a homomorphism of $A$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ such that the composition of $k$ and $\operatorname{g}$ applied to $S$ is equal to $0$. Then the lift left homology of $S$ and $k$ is a homomorphism of $A$ and the left homology of $S$ defined as the composition of the lift cycle of $S$ and $k$ and the left homology projection of $S$.

the cycle of S (from the name)

Let $S$ be a short complex of $C$. Then the cycle of $S$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and the cycle of $S$ defined as $\operatorname{f'}$ applied to the left 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 first projection functor and the cycle functor of $C$.