Definitions: Mathlib.Algebra, part 9 of 17

ComplexShape.Embedding.HasLiftdefMathlib.Algebra.Homology.Embedding.HomEquiv, predicate

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $x_{4}$ be a homomorphism of the restriction of $K$ and $e$ and $L$. Then $\operatorname{HasLift}$ holds for $e$ and $x_{4}$, if for all elements $j$ of $x$, if $\operatorname{BoundaryGE}$ holds for $e$ and $j$, then for all elements $\mathrm{i'}$ of $x_{1}$, if $\operatorname{Rel}$ holds for $\mathrm{c'}$, $\mathrm{i'}$ and $\operatorname{f}$ applied to $e$ and $j$, then the composition of $\operatorname{d}$ applied to $K$, $\mathrm{i'}$ and $\operatorname{f}$ applied to $e$ and $j$ and $\operatorname{f}$ applied to $x_{4}$ and $j$ is equal to $0$.

ComplexShape.Embedding.homEquivdefMathlib.Algebra.Homology.Embedding.HomEquiv, function or constant

Wording

the homomorphism equivalence of K and L (from the name)

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $L$ be a homological complex of $C$ and $c$. Then the homomorphism equivalence of $K$ and $L$ is an equivalence from the set of homomorphisms of $K$ and $\operatorname{extend}$ applied to $L$ and $e$ to $\SubtypeSet {x_{4}}{\operatorname{HasLift} (e , x_{4})}$.

ComplexShape.Embedding.homRestrictdefMathlib.Algebra.Homology.Embedding.HomEquiv, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $x_{4}$ be a homomorphism of $K$ and $\operatorname{extend}$ applied to $L$ and $e$. Then $\operatorname{homRestrict}$ applied to $e$ and $x_{4}$ is a homomorphism of the restriction of $K$ and $e$ and $L$.

ComplexShape.Embedding.liftExtenddefMathlib.Algebra.Homology.Embedding.HomEquiv, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $x_{4}$ be a homomorphism of the restriction of $K$ and $e$ and $L$ such that $\operatorname{HasLift}$ holds for $e$ and $x_{4}$. Then $\operatorname{liftExtend}$ applied to $e$, $x_{4}$ and $h_{2}$ is a homomorphism of $K$ and $\operatorname{extend}$ applied to $L$ and $e$ defined as $\operatorname{mk}$ applied to the function that maps $\mathrm{i'}$ to $\operatorname{f}$ applied to $x_{4}$ and $\mathrm{i'}$ and the function that maps $x_{5}$, $x_{6}$ and $h_{3}$ to $\operatorname{comm}$ applied to $x_{4}$, $h_{2}$, $x_{5}$ and $x_{6}$.

ComplexShape.Embedding.liftExtendfArrowIsodefMathlib.Algebra.Homology.Embedding.HomEquiv, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $x_{4}$ be a homomorphism of the restriction of $K$ and $e$ and $L$ such that $\operatorname{HasLift}$ holds for $e$ and $x_{4}$. Assume that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$. Then $\operatorname{liftExtendfArrowIso}$ applied to $e$, $x_{4}$, $h_{2}$ and $\mathrm{hi}$ is an isomorphism of $\operatorname{mk}$ applied to $\operatorname{f}$ applied to $\operatorname{liftExtend}$ applied to $e$, $x_{4}$ and $h_{2}$ and $\mathrm{i'}$ and $\operatorname{mk}$ applied to $\operatorname{f}$ applied to $x_{4}$ and $i$.

Mathlib.Algebra.Homology.Embedding.IsSupported

HomologicalComplex.IsStrictlySupportedclassMathlib.Algebra.Homology.Embedding.IsSupported, predicate

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then we can say that $\operatorname{IsStrictlySupported}$ holds for $K$ and $e$.

HomologicalComplex.IsStrictlySupportedOutsidestructureMathlib.Algebra.Homology.Embedding.IsSupported, predicate

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then we can say that $\operatorname{IsStrictlySupportedOutside}$ holds for $K$ and $e$.

HomologicalComplex.IsSupportedclassMathlib.Algebra.Homology.Embedding.IsSupported, predicate

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then we can say that $\operatorname{IsSupported}$ holds for $K$ and $e$.

HomologicalComplex.IsSupportedOutsidestructureMathlib.Algebra.Homology.Embedding.IsSupported, predicate

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then we can say that $\operatorname{IsSupportedOutside}$ holds for $K$ and $e$.

Mathlib.Algebra.Homology.Embedding.Restriction

ComplexShape.Embedding.restrictionFunctordefMathlib.Algebra.Homology.Embedding.Restriction, function or constant

Wording

the restriction functor of e and C (from the name)

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then the restriction functor of $e$ and $C$ is a functor of the set of homological complexes of $C$ and $\mathrm{c'}$ and the set of homological complexes of $C$ and $c$.

HomologicalComplex.restrictiondefMathlib.Algebra.Homology.Embedding.Restriction, function or constant

Wording

the restriction of K and e (from the name)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the restriction of $K$ and $e$ is a homological complex of $C$ and $c$.

HomologicalComplex.restrictionMapdefMathlib.Algebra.Homology.Embedding.Restriction, function or constant

Wording

the restriction map of x4 and e (from the name)

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the restriction map of $x_{4}$ and $e$ is a homomorphism of the restriction of $K$ and $e$ and the restriction of $L$ and $e$.

HomologicalComplex.restrictionXIsodefMathlib.Algebra.Homology.Embedding.Restriction, function or constant

Wording

the restriction isomorphism of K and e (from the name)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$. Then the restriction isomorphism of $K$ and $e$ is an isomorphism of $\operatorname{X}$ applied to the restriction of $K$ and $e$ and $i$ and $\operatorname{X}$ applied to $K$ and $\mathrm{i'}$.

Mathlib.Algebra.Homology.Embedding.RestrictionHomology

HomologicalComplex.restriction.sc'IsodefMathlib.Algebra.Homology.Embedding.RestrictionHomology, function or constant

Wording

no wording

English

HomologicalComplex.restrictionCyclesIsodefMathlib.Algebra.Homology.Embedding.RestrictionHomology, function or constant

Wording

the restriction cycle isomorphism of j and k (from the name)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $j$ and $k$ be elements of $x$ such that $\EqtMACRoH {\operatorname{next} (c , j)}{k}$, $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$ and $\EqtMACRoH {\operatorname{f} (e , k)}{\mathrm{k'}}$. Assume that $\EqtMACRoH {\operatorname{next} (\mathrm{c'} , \mathrm{j'})}{\mathrm{k'}}$. Then the restriction cycle isomorphism of $j$ and $k$ is an isomorphism of the cycle of the restriction of $K$ and $e$ and $j$ and the cycle of $K$ and $\mathrm{j'}$.

HomologicalComplex.restrictionHomologyIsodefMathlib.Algebra.Homology.Embedding.RestrictionHomology, function or constant

Wording

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

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $i$, $j$ and $k$ be elements of $x$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$, $\EqtMACRoH {\operatorname{next} (c , j)}{k}$, $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$, $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$ and $\EqtMACRoH {\operatorname{f} (e , k)}{\mathrm{k'}}$. Assume that $\EqtMACRoH {\operatorname{prev} (\mathrm{c'} , \mathrm{j'})}{\mathrm{i'}}$. Assume that $\EqtMACRoH {\operatorname{next} (\mathrm{c'} , \mathrm{j'})}{\mathrm{k'}}$. Then the restriction homology isomorphism of $j$ and $k$ is an isomorphism of the homology of the restriction of $K$ and $e$ and $j$ and the homology of $K$ and $\mathrm{j'}$ defined as the composition of $\operatorname{homologyIsoSc'}$ applied to the restriction of $K$ and $e$, $i$, $j$, $k$, $\mathrm{hi}$ and $\mathrm{hk}$ and the composition of the homology isomorphism of $\operatorname{sc'Iso}$ applied to $K$, $e$, $i$, $j$, $k$, $\mathrm{hi'}$, $\mathrm{hj'}$, $\mathrm{hk'}$, $\mathrm{hi''}$ and $\mathrm{hk''}$ and the inverse of $\operatorname{homologyIsoSc'}$ applied to $K$, $\mathrm{i'}$, $\mathrm{j'}$, $\mathrm{k'}$, $\mathrm{hi''}$ and $\mathrm{hk''}$.

HomologicalComplex.restrictionOpcyclesIsodefMathlib.Algebra.Homology.Embedding.RestrictionHomology, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $i$ and $j$ be elements of $x$ such that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$, $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$ and $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Assume that $\EqtMACRoH {\operatorname{prev} (\mathrm{c'} , \mathrm{j'})}{\mathrm{i'}}$. Then $\operatorname{restrictionOpcyclesIso}$ applied to $K$, $e$, $i$, $j$, $\mathrm{hi}$, $\mathrm{hi'}$, $\mathrm{hj'}$ and $\mathrm{hi''}$ is an isomorphism of $\operatorname{opcycles}$ applied to the restriction of $K$ and $e$ and $j$ and $\operatorname{opcycles}$ applied to $K$ and $\mathrm{j'}$.

Mathlib.Algebra.Homology.Embedding.Splitting

ComplexShape.Embedding.splittingExtenddefMathlib.Algebra.Homology.Embedding.Splitting, function or constant

Wording

no wording

English

Let $e$ be an embedding of $x_{2}$ and $x_{3}$. Let $x_{6}$ be a function from elements $i$ of $x$ to splittings of the map of $S$ and the evaluation of $x_{2}$ and $i$. Let $x_{7}$ be an element of $x_{1}$. Then $\operatorname{splittingExtend}$ applied to $e$, $i$, $x_{6}$ and $x_{7}$ is a splitting of the map of the map of $S$ and $\operatorname{extendFunctor}$ applied to $e$ and $C$ and the evaluation of $x_{3}$ and $x_{7}$.

Mathlib.Algebra.Homology.Embedding.StupidTrunc

ComplexShape.Embedding.stupidTruncFunctordefMathlib.Algebra.Homology.Embedding.StupidTrunc, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then $\operatorname{stupidTruncFunctor}$ applied to $e$ and $C$ is a functor of the set of homological complexes of $C$ and $\mathrm{c'}$ and the set of homological complexes of $C$ and $\mathrm{c'}$.

HomologicalComplex.stupidTruncdefMathlib.Algebra.Homology.Embedding.StupidTrunc, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{stupidTrunc}$ applied to $K$ and $e$ is a homological complex of $C$ and $\mathrm{c'}$ defined as $\operatorname{extend}$ applied to the restriction of $K$ and $e$ and $e$.

HomologicalComplex.stupidTruncMapdefMathlib.Algebra.Homology.Embedding.StupidTrunc, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{stupidTruncMap}$ applied to $x_{4}$ and $e$ is a homomorphism of $\operatorname{stupidTrunc}$ applied to $K$ and $e$ and $\operatorname{stupidTrunc}$ applied to $L$ and $e$ defined as $\operatorname{extendMap}$ applied to the restriction map of $x_{4}$ and $e$ and $e$.

HomologicalComplex.stupidTruncXIsodefMathlib.Algebra.Homology.Embedding.StupidTrunc, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$. Then $\operatorname{stupidTruncXIso}$ applied to $K$, $e$ and $\mathrm{hi'}$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{stupidTrunc}$ applied to $K$ and $e$ and $\mathrm{i'}$ and $\operatorname{X}$ applied to $K$ and $\mathrm{i'}$.

Mathlib.Algebra.Homology.Embedding.TruncGE

ComplexShape.Embedding.restrictionToTruncGE'NatTransdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

the natural transformation of e and C (from the docstring)

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then the natural transformation of $e$ and $C$ is a homomorphism of the restriction functor of $e$ and $C$ and $\operatorname{truncGE'Functor}$ applied to $e$ and $C$.

ComplexShape.Embedding.truncGE'FunctordefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then $\operatorname{truncGE'Functor}$ applied to $e$ and $C$ is a functor of the set of homological complexes of $C$ and $\mathrm{c'}$ and the set of homological complexes of $C$ and $c$.

ComplexShape.Embedding.truncGEFunctordefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then $\operatorname{truncGEFunctor}$ applied to $e$ and $C$ is a functor of the set of homological complexes of $C$ and $\mathrm{c'}$ and the set of homological complexes of $C$ and $\mathrm{c'}$.

ComplexShape.Embedding.πTruncGENatTransdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

the natural transformation of e and C (from the docstring)

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then the natural transformation of $e$ and $C$ is a homomorphism of the identity of the set of homological complexes of $C$ and $\mathrm{c'}$ and $\operatorname{truncGEFunctor}$ applied to $e$ and $C$.

HomologicalComplex.restrictionToTruncGE'defMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{restrictionToTruncGE'}$ applied to $K$ and $e$ is a homomorphism of the restriction of $K$ and $e$ and the canonical truncation of $K$ and $e$.

HomologicalComplex.truncGEdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

the canonical truncation of K and e (from the docstring)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the canonical truncation of $K$ and $e$ is a homological complex of $C$ and $\mathrm{c'}$ defined as $\operatorname{extend}$ applied to the canonical truncation of $K$ and $e$ and $e$.

HomologicalComplex.truncGE'defMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

the canonical truncation of K and e (from the docstring)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the canonical truncation of $K$ and $e$ is a homological complex of $C$ and $c$.

HomologicalComplex.truncGE'.XdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $i$ be an element of $x$. Then $\operatorname{X}$ applied to $K$, $e$ and $i$ is an element of $C$ defined as $\iteMACRoG {\operatorname{BoundaryGE} (e , i)}{\operatorname{opcycles} (K , \operatorname{f} (e , i))}{\operatorname{X} (K , \operatorname{f} (e , i))}$.

HomologicalComplex.truncGE'.XIsodefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

the isomorphism of K and e (from the name)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that it is not the case that $\operatorname{BoundaryGE}$ holds for $e$ and $i$. Then the isomorphism of $K$ and $e$ is an isomorphism of $\operatorname{X}$ applied to $K$, $e$ and $i$ and $\operatorname{X}$ applied to $K$ and $\operatorname{f}$ applied to $e$ and $i$.

HomologicalComplex.truncGE'.XIsoOpcyclesdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\operatorname{BoundaryGE}$ holds for $e$ and $i$. Then $\operatorname{XIsoOpcycles}$ applied to $K$, $e$ and $\mathrm{hi}$ is an isomorphism of $\operatorname{X}$ applied to $K$, $e$ and $i$ and $\operatorname{opcycles}$ applied to $K$ and $\operatorname{f}$ applied to $e$ and $i$.

HomologicalComplex.truncGE'.ddefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $i$ and $j$ be elements of $x$. Then $\operatorname{d}$ applied to $K$, $e$, $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to $K$, $e$ and $i$ and $\operatorname{X}$ applied to $K$, $e$ and $j$.

HomologicalComplex.truncGE'MapdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{truncGE'Map}$ applied to $x_{4}$ and $e$ is a homomorphism of the canonical truncation of $K$ and $e$ and the canonical truncation of $L$ and $e$.

HomologicalComplex.truncGE'XIsodefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

HomologicalComplex.truncGE'XIsoOpcyclesdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

HomologicalComplex.truncGEMapdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{truncGEMap}$ applied to $x_{4}$ and $e$ is a homomorphism of the canonical truncation of $K$ and $e$ and the canonical truncation of $L$ and $e$ defined as the map of $\operatorname{extendFunctor}$ applied to $e$ and $C$ and $\operatorname{truncGE'Map}$ applied to $x_{4}$ and $e$.

HomologicalComplex.truncGEXIsodefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$ and it is not the case that $\operatorname{BoundaryGE}$ holds for $e$ and $i$. Then $\operatorname{truncGEXIso}$ applied to $K$, $e$, $\mathrm{hi'}$ and $\mathrm{hi}$ is an isomorphism of $\operatorname{X}$ applied to the canonical truncation of $K$ and $e$ and $\mathrm{i'}$ and $\operatorname{X}$ applied to $K$ and $\mathrm{i'}$ defined as the composition of $\operatorname{extendXIso}$ applied to the canonical truncation of $K$ and $e$, $e$ and $\mathrm{hi'}$ and $\operatorname{truncGE'XIso}$ applied to $K$, $e$, $\mathrm{hi'}$ and $\mathrm{hi}$.

HomologicalComplex.truncGEXIsoOpcyclesdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$ and $\operatorname{BoundaryGE}$ holds for $e$ and $i$. Then $\operatorname{truncGEXIsoOpcycles}$ applied to $K$, $e$, $\mathrm{hi'}$ and $\mathrm{hi}$ is an isomorphism of $\operatorname{X}$ applied to the canonical truncation of $K$ and $e$ and $\mathrm{i'}$ and $\operatorname{opcycles}$ applied to $K$ and $\mathrm{i'}$ defined as the composition of $\operatorname{extendXIso}$ applied to the canonical truncation of $K$ and $e$, $e$ and $\mathrm{hi'}$ and $\operatorname{truncGE'XIsoOpcycles}$ applied to $K$, $e$, $\mathrm{hi'}$ and $\mathrm{hi}$.

HomologicalComplex.πTruncGEdefMathlib.Algebra.Homology.Embedding.TruncGE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\mathrm{HomologicalComplex\_\_\_u3c0\_TruncGE}$ applied to $K$ and $e$ is a homomorphism of $K$ and the canonical truncation of $K$ and $e$ defined as $\operatorname{liftExtend}$ applied to $e$, $\operatorname{restrictionToTruncGE'}$ applied to $K$ and $e$ and $\mathrm{HomologicalComplex\_\_restrictionToTruncGE'\_hasLift}$ applied to $K$ and $e$.

Mathlib.Algebra.Homology.Embedding.TruncGEHomology

HomologicalComplex.truncGE'.homologyDatadefMathlib.Algebra.Homology.Embedding.TruncGEHomology, function or constant

Wording

the homology data of j and k (from the name)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $i$, $j$ and $k$ be elements of $x$ such that $\EqtMACRoH {\operatorname{next} (c , j)}{k}$, $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$ and $\operatorname{BoundaryGE}$ holds for $e$ and $j$. Then the homology data of $j$ and $k$ is a homology data of $\operatorname{sc'}$ applied to the canonical truncation of $K$ and $e$, $i$, $j$ and $k$.

HomologicalComplex.truncGE.rightHomologyMapDatadefMathlib.Algebra.Homology.Embedding.TruncGEHomology, function or constant

Wording

the right homology map data of K and e (from the name)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Assume that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$. Assume that $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Assume that $\operatorname{BoundaryGE}$ holds for $e$ and $j$. Then the right homology map data of $K$ and $e$ is a right homology map data of $\operatorname{canonical}$ applied to $\operatorname{sc}$ applied to $K$ and $\mathrm{j'}$ and the right homology data of the canonical truncation of $K$ and $e$.

Mathlib.Algebra.Homology.Embedding.TruncLE

ComplexShape.Embedding.truncLE'FunctordefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then $\operatorname{truncLE'Functor}$ applied to $e$ and $C$ is a functor of the set of homological complexes of $C$ and $\mathrm{c'}$ and the set of homological complexes of $C$ and $c$.

ComplexShape.Embedding.truncLE'ToRestrictionNatTransdefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

the natural transformation of e and C (from the docstring)

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then the natural transformation of $e$ and $C$ is a homomorphism of $\operatorname{truncLE'Functor}$ applied to $e$ and $C$ and the restriction functor of $e$ and $C$.

ComplexShape.Embedding.truncLEFunctordefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then $\operatorname{truncLEFunctor}$ applied to $e$ and $C$ is a functor of the set of homological complexes of $C$ and $\mathrm{c'}$ and the set of homological complexes of $C$ and $\mathrm{c'}$.

ComplexShape.Embedding.ιTruncLENatTransdefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

the natural transformation of e and C (from the docstring)

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then the natural transformation of $e$ and $C$ is a homomorphism of $\operatorname{truncLEFunctor}$ applied to $e$ and $C$ and the identity of the set of homological complexes of $C$ and $\mathrm{c'}$.

HomologicalComplex.truncLEdefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

the canonical truncation of K and e (from the docstring)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the canonical truncation of $K$ and $e$ is a homological complex of $C$ and $\mathrm{c'}$ defined as the opposite of the canonical truncation of the opposite of $K$ and the opposite embedding in $e$.

HomologicalComplex.truncLE'defMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

the canonical truncation of K and e (from the docstring)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the canonical truncation of $K$ and $e$ is a homological complex of $C$ and $c$ defined as the opposite of the canonical truncation of the opposite of $K$ and the opposite embedding in $e$.

HomologicalComplex.truncLE'MapdefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{truncLE'Map}$ applied to $x_{4}$ and $e$ is a homomorphism of the canonical truncation of $K$ and $e$ and the canonical truncation of $L$ and $e$ defined as the map of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $c$ and the opposite in $\operatorname{truncGE'Map}$ applied to the map of $\operatorname{opFunctor}$ applied to $C$ and $\mathrm{c'}$ and the opposite in $x_{4}$ and the opposite embedding in $e$.

HomologicalComplex.truncLE'ToRestrictiondefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{truncLE'ToRestriction}$ applied to $K$ and $e$ is a homomorphism of the canonical truncation of $K$ and $e$ and the restriction of $K$ and $e$ defined as the map of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $c$ and the opposite in $\operatorname{restrictionToTruncGE'}$ applied to the opposite of $K$ and the opposite embedding in $e$.

HomologicalComplex.truncLE'XIsodefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

no wording

English

HomologicalComplex.truncLE'XIsoCyclesdefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

no wording

English

HomologicalComplex.truncLEIsodefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

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

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the canonical isomorphism of $K$ and $e$ is an isomorphism of the canonical truncation of $K$ and $e$ and $\operatorname{extend}$ applied to the canonical truncation of $K$ and $e$ and $e$ defined as the map isomorphism of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $\mathrm{c'}$ and the opposite isomorphism of the inverse of the canonical isomorphism of the canonical truncation of $K$ and $e$ and $e$.

HomologicalComplex.truncLEMapdefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{truncLEMap}$ applied to $x_{4}$ and $e$ is a homomorphism of the canonical truncation of $K$ and $e$ and the canonical truncation of $L$ and $e$ defined as the map of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $\mathrm{c'}$ and the opposite in $\operatorname{truncGEMap}$ applied to the map of $\operatorname{opFunctor}$ applied to $C$ and $\mathrm{c'}$ and the opposite in $x_{4}$ and the opposite embedding in $e$.

HomologicalComplex.truncLEXIsodefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

the truncation lexicographic isomorphism of K and e (from the name)

English

HomologicalComplex.truncLEXIsoCyclesdefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

the truncation lexicographic isomorphism cycle of K and e (from the name)

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$ and $\operatorname{BoundaryLE}$ holds for $e$ and $i$. Then the truncation lexicographic isomorphism cycle of $K$ and $e$ is an isomorphism of $\operatorname{X}$ applied to the canonical truncation of $K$ and $e$ and $\mathrm{i'}$ and the cycle of $K$ and $\mathrm{i'}$.

HomologicalComplex.ιTruncLEdefMathlib.Algebra.Homology.Embedding.TruncLE, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\mathrm{HomologicalComplex\_\_\_u3b9\_TruncLE}$ applied to $K$ and $e$ is a homomorphism of the canonical truncation of $K$ and $e$ and $K$ defined as the map of $\operatorname{unopFunctor}$ applied to $C$ and the inverse of $\mathrm{c'}$ and the opposite in $\mathrm{HomologicalComplex\_\_\_u3c0\_TruncGE}$ applied to the opposite of $K$ and the opposite embedding in $e$.

Mathlib.Algebra.Homology.Embedding.TruncLEHomology

HomologicalComplex.shortComplexTruncLEdefMathlib.Algebra.Homology.Embedding.TruncLEHomology, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $\mathrm{c'}$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{shortComplexTruncLE}$ applied to $K$ and $e$ is a short complex of the set of homological complexes of $C$ and $\mathrm{c'}$.

Mathlib.Algebra.Homology.EulerCharacteristic

ComplexShape.EulerCharSignsclassMathlib.Algebra.Homology.EulerCharacteristic, predicate

Wording

no wording

English

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

ComplexShape.EulerCharSigns.χdefMathlib.Algebra.Homology.EulerCharacteristic, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $x$. Let $x_{1}$ be an element of $x$. Then $\mathrm{ComplexShape\_\_EulerCharSigns\_\_\_u3c7\_}$ applied to $c$ and $x_{1}$ is a unit of $\Integer$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

ComplexShape.χdefMathlib.Algebra.Homology.EulerCharacteristic, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $x$. Let $x_{2}$ be an element of $x$. Then $\mathrm{ComplexShape\_\_\_u3c7\_}$ applied to $c$ and $x_{2}$ is a unit of $\Integer$ defined as $\mathrm{ComplexShape\_\_EulerCharSigns\_\_\_u3c7\_}$ applied to $c$ and $x_{2}$.

GradedObject.eulerChardefMathlib.Algebra.Homology.EulerCharacteristic, function or constant

Wording

the Euler characteristic of c and X (from the docstring)

English

Let $c$ be a complex shape of $x_{1}$. Let $X$ be a graded object of $x_{1}$ and the set of module categories of $R$. Then the Euler characteristic of $c$ and $X$ is an integer defined as the finite sum of the function that maps $i$ to the product of the underlying value in the base of $\mathrm{ComplexShape\_\_\_u3c7\_}$ applied to $c$ and $i$ and the rank of $R$ and the set of carriers of $X$ applied to $i$.

GradedObject.finrankSupportdefMathlib.Algebra.Homology.EulerCharacteristic, function or constant

Wording

the support of X (from the docstring)

English

Let $X$ be a graded object of $x_{1}$ and the set of module categories of $R$. Then the support of $X$ is an element of $\wp x_{1}$ defined as the support of the function that maps $i$ to the rank of $R$ and the set of carriers of $X$ applied to $i$.

HomologicalComplex.eulerChardefMathlib.Algebra.Homology.EulerCharacteristic, function or constant

Wording

the Euler characteristic of C (from the docstring)

English

Let $C$ be a homological complex of the set of module categories of $R$ and $c$. Then the Euler characteristic of $C$ is an integer defined as the Euler characteristic of $c$ and $\operatorname{X}$ applied to $C$.

HomologicalComplex.homologyEulerChardefMathlib.Algebra.Homology.EulerCharacteristic, function or constant

Wording

the homological Euler characteristic of C (from the docstring)

English

Let $C$ be a homological complex of the set of module categories of $R$ and $c$. Then the homological Euler characteristic of $C$ is an integer defined as the Euler characteristic of $c$ and the function that maps $i$ to the homology of $C$ and $i$.

Mathlib.Algebra.Homology.ExactSequence

CategoryTheory.ComposableArrows.ExactstructureMathlib.Algebra.Homology.ExactSequence, predicate

Wording

S is exact (from the docstring)

English

Let $S$ be a composable arrow of $C$ and $n$. Then we can say that $S$ is exact.

CategoryTheory.ComposableArrows.Exact.scdefMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

no wording

English

Assume that $S$ is exact. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i + 2 , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_Exact\_\_sc\_\_\_auto\_1}$. Then $\operatorname{sc}$ applied to $\mathrm{hS}$, $i$ and $\mathrm{hi}$ is a short complex of $C$.

CategoryTheory.ComposableArrows.Exact.sc'defMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

no wording

English

Assume that $S$ is exact. Let $i$, $j$ and $k$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (i + 1 , j)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_Exact\_\_sc'\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (j + 1 , k)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_Exact\_\_sc'\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for $\mathrm{Leq} (k , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_Exact\_\_sc'\_\_\_auto\_5}$. Then $\operatorname{sc'}$ applied to $\mathrm{hS}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$ is a short complex of $C$ defined as $\operatorname{sc'}$ applied to $S$, $\operatorname{toIsComplex}$ applied to $\mathrm{hS}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$.

CategoryTheory.ComposableArrows.IsComplexstructureMathlib.Algebra.Homology.ExactSequence, predicate

Wording

S is a complex (from the docstring)

English

Let $S$ be a composable arrow of $C$ and $n$. Then we can say that $S$ is a complex.

CategoryTheory.ComposableArrows.scdefMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

no wording

English

Let $S$ be a composable arrow of $C$ and $n$ such that $S$ is a complex. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i + 2 , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc\_\_\_auto\_1}$. Then $\operatorname{sc}$ applied to $S$, $\mathrm{hS}$, $i$ and $\mathrm{hi}$ is a short complex of $C$.

CategoryTheory.ComposableArrows.sc'defMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

no wording

English

Let $S$ be a composable arrow of $C$ and $n$ such that $S$ is a complex. Let $i$, $j$ and $k$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (i + 1 , j)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (j + 1 , k)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for $\mathrm{Leq} (k , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'\_\_\_auto\_5}$. Then $\operatorname{sc'}$ applied to $S$, $\mathrm{hS}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$ is a short complex of $C$.

CategoryTheory.ComposableArrows.sc'MapdefMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Assume that $x_{2}$ is a complex. Assume that $x_{3}$ is a complex. Let $i$, $j$ and $k$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (i + 1 , j)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'Map\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (j + 1 , k)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'Map\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for $\mathrm{Leq} (k , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'Map\_\_\_auto\_5}$. Then $\operatorname{sc'Map}$ applied to $x_{4}$, $h$, $h_{1}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$ is a homomorphism of $\operatorname{sc'}$ applied to $x_{2}$, $h$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$ and $\operatorname{sc'}$ applied to $x_{3}$, $h_{1}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$.

CategoryTheory.ComposableArrows.sc'MapIsodefMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

no wording

English

Let $e$ be an isomorphism of $x_{2}$ and $x_{3}$. Assume that $x_{2}$ is a complex. Assume that $x_{3}$ is a complex. Let $i$, $j$ and $k$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (i + 1 , j)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'MapIso\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Eq} (j + 1 , k)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'MapIso\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for $\mathrm{Leq} (k , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_sc'MapIso\_\_\_auto\_5}$. Then $\operatorname{sc'MapIso}$ applied to $e$, $h$, $h_{1}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$ is an isomorphism of $\operatorname{sc'}$ applied to $x_{2}$, $h$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$ and $\operatorname{sc'}$ applied to $x_{3}$, $h_{1}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hjk}$ and $\mathrm{hk}$.

CategoryTheory.ComposableArrows.scMapdefMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Assume that $x_{2}$ is a complex. Assume that $x_{3}$ is a complex. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i + 2 , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_scMap\_\_\_auto\_1}$. Then $\operatorname{scMap}$ applied to $x_{4}$, $h$, $h_{1}$, $i$ and $\mathrm{hi}$ is a homomorphism of $\operatorname{sc}$ applied to $x_{2}$, $h$, $i$ and $\mathrm{hi}$ and $\operatorname{sc}$ applied to $x_{3}$, $h_{1}$, $i$ and $\mathrm{hi}$.

CategoryTheory.ComposableArrows.scMapIsodefMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

no wording

English

Let $e$ be an isomorphism of $x_{2}$ and $x_{3}$. Assume that $x_{2}$ is a complex. Assume that $x_{3}$ is a complex. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i + 2 , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_scMapIso\_\_\_auto\_1}$. Then $\operatorname{scMapIso}$ applied to $e$, $h$, $h_{1}$, $i$ and $\mathrm{hi}$ is an isomorphism of $\operatorname{sc}$ applied to $x_{2}$, $h$, $i$ and $\mathrm{hi}$ and $\operatorname{sc}$ applied to $x_{3}$, $h_{1}$, $i$ and $\mathrm{hi}$.

CategoryTheory.ShortComplex.mapToComposableArrowsdefMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

the map to composable arrow of x4 (from the name)

English

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

CategoryTheory.ShortComplex.toComposableArrowsdefMathlib.Algebra.Homology.ExactSequence, function or constant

Wording

the composable arrow of S (from the name)

English

Let $S$ be a short complex of $C$. Then the composable arrow of $S$ is a composable arrow of $C$ and $2$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $\operatorname{f}$ applied to $S$ and $\operatorname{g}$ applied to $S$.

Mathlib.Algebra.Homology.ExactSequenceFour

CategoryTheory.ComposableArrows.Exact.cokerIsoKerdefMathlib.Algebra.Homology.ExactSequenceFour, function or constant

Wording

the cokernel isomorphism kernel of k (from the name)

English

Assume that $S$ is exact. Let $k$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (k , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_Exact\_\_cokerIsoKer\_\_\_auto\_1}$. Then the cokernel isomorphism kernel of $k$ is an isomorphism of the cokernel of the map of $k$ and $k + 1$ and the kernel of the map of $k + 2$ and $k + 3$.

CategoryTheory.ComposableArrows.Exact.cokerIsoKer'defMathlib.Algebra.Homology.ExactSequenceFour, function or constant

Wording

the cokernel isomorphism kernel of hcc and hkf (from the name)

English

Assume that $S$ is exact. Let $k$ be a natural number such that $k \leq n$. Let $\mathrm{cc}$ be a cokernel cofork of the map of $k$ and $k + 1$. Let $\mathrm{kf}$ be a kernel fork of the map of $k + 2$ and $k + 3$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Then the cokernel isomorphism kernel of $\mathrm{hcc}$ and $\mathrm{hkf}$ is an isomorphism of $\operatorname{pt}$ applied to $\mathrm{cc}$ and $\operatorname{pt}$ applied to $\mathrm{kf}$ defined as $\operatorname{asIso}$ applied to the cokernel to kernel of $\mathrm{hcc}$ and $\mathrm{hkf}$.

CategoryTheory.ComposableArrows.Exact.cokerToKer'defMathlib.Algebra.Homology.ExactSequenceFour, function or constant

Wording

the cokernel to kernel of hcc and hkf (from the name)

English

Assume that $S$ is exact. Let $k$ be a natural number such that $k \leq n$. Let $\mathrm{cc}$ be a cokernel cofork of the map of $k$ and $k + 1$. Let $\mathrm{kf}$ be a kernel fork of the map of $k + 2$ and $k + 3$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Then the cokernel to kernel of $\mathrm{hcc}$ and $\mathrm{hkf}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{cc}$ and $\operatorname{pt}$ applied to $\mathrm{kf}$.

CategoryTheory.ComposableArrows.Exact.opcyclesIsoCyclesdefMathlib.Algebra.Homology.ExactSequenceFour, function or constant

Wording

no wording

English

Assume that $S$ is exact. Let $k$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (k , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_Exact\_\_opcyclesIsoCycles\_\_\_auto\_1}$. Then $\operatorname{opcyclesIsoCycles}$ applied to $\mathrm{hS}$, $k$ and $\mathrm{hk}$ is an isomorphism of $\operatorname{opcycles}$ applied to $\operatorname{sc}$ applied to $\mathrm{hS}$, $k$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_Exact\_\_opcyclesIsoCycles\_\_\_proof\_4}$ applied to $k$ and $\mathrm{hk}$ and the cycle of $\operatorname{sc}$ applied to $\mathrm{hS}$, $k + 1$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_Exact\_\_opcyclesIsoCycles\_\_\_proof\_13}$ applied to $k$ and $\mathrm{hk}$.

CategoryTheory.ComposableArrows.IsComplex.cokerToKerdefMathlib.Algebra.Homology.ExactSequenceFour, function or constant

Wording

the cokernel to kernel of k (from the name)

English

Assume that $S$ is a complex. Let $k$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (k , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_IsComplex\_\_cokerToKer\_\_\_auto\_1}$. Then the cokernel to kernel of $k$ is a homomorphism of the cokernel of the map of $k$ and $k + 1$ and the kernel of the map of $k + 2$ and $k + 3$.

CategoryTheory.ComposableArrows.IsComplex.cokerToKer'defMathlib.Algebra.Homology.ExactSequenceFour, function or constant

Wording

the cokernel to kernel of hcc and hkf (from the name)

English

Assume that $S$ is a complex. Let $k$ be a natural number such that $k \leq n$. Let $\mathrm{cc}$ be a cokernel cofork of the map of $k$ and $k + 1$. Let $\mathrm{kf}$ be a kernel fork of the map of $k + 2$ and $k + 3$. Let $\mathrm{hcc}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Let $\mathrm{hkf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Then the cokernel to kernel of $\mathrm{hcc}$ and $\mathrm{hkf}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{cc}$ and $\operatorname{pt}$ applied to $\mathrm{kf}$.

CategoryTheory.ComposableArrows.IsComplex.opcyclesToCyclesdefMathlib.Algebra.Homology.ExactSequenceFour, function or constant

Wording

no wording

English

Assume that $S$ is a complex. Let $k$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (k , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_IsComplex\_\_opcyclesToCycles\_\_\_auto\_1}$. Then $\operatorname{opcyclesToCycles}$ applied to $\mathrm{hS}$, $k$ and $\mathrm{hk}$ is a homomorphism of $\operatorname{opcycles}$ applied to $\operatorname{sc}$ applied to $S$, $\mathrm{hS}$, $k$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_IsComplex\_\_opcyclesToCycles\_\_\_proof\_4}$ applied to $k$ and $\mathrm{hk}$ and the cycle of $\operatorname{sc}$ applied to $S$, $\mathrm{hS}$, $k + 1$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_IsComplex\_\_opcyclesToCycles\_\_\_proof\_6}$ applied to $k$ and $\mathrm{hk}$.

Mathlib.Algebra.Homology.Factorizations.Basic

CochainComplex.degreewiseEpiWithInjectiveKerneldefMathlib.Algebra.Homology.Factorizations.Basic, function or constant

Wording

the degreewise epimorphism with injective kernel (from the name)

English

The degreewise epimorphism with injective kernel is a morphism property of the set of cochain complexes of $C$ and $\Integer$ defined as the function that maps $x_{2}$, $x_{3}$ and $x_{4}$ to the proposition that for all integers $i$, $\operatorname{epiWithInjectiveKernel}$.

Mathlib.Algebra.Homology.Factorizations.CM5b

CochainComplex.cm5b.IdefMathlib.Algebra.Homology.Factorizations.CM5b, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Then $\operatorname{I}$ applied to $K$ is a cochain complex of $C$ and $\Integer$.

CochainComplex.cm5b.homotopyEquivdefMathlib.Algebra.Homology.Factorizations.CM5b, function or constant

Wording

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

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Then the homotopy equivalence of $K$ and $L$ is a homotopy equivalence of the biproduct of the mapping cone of the identity morphism of $\operatorname{I}$ applied to $K$ and $L$ and $L$.

CochainComplex.cm5b.idefMathlib.Algebra.Homology.Factorizations.CM5b, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $K$ and $L$. Then $\operatorname{i}$ applied to $f$ is a homomorphism of $K$ and the biproduct of the mapping cone of the identity morphism of $\operatorname{I}$ applied to $K$ and $L$.

CochainComplex.cm5b.pdefMathlib.Algebra.Homology.Factorizations.CM5b, function or constant

Wording

no wording

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Then $\operatorname{p}$ applied to $K$ and $L$ is a homomorphism of the biproduct of the mapping cone of the identity morphism of $\operatorname{I}$ applied to $K$ and $L$ and $L$ defined as the projection onto the second summand.

Mathlib.Algebra.Homology.FullSubcategory

HomologicalComplex.liftFunctorObjectPropertydefMathlib.Algebra.Homology.FullSubcategory, function or constant

Wording

the lift functor object property of P and F (from the name)

English

Let $P$ be an object property of $V$. Let $F$ be a functor of $D$ and the set of homological complexes of $V$ and $c$ such that for all elements $X$ of $D$, for all elements $n$ of $x_{1}$, $P$ holds for $\operatorname{X}$ applied to the action of $F$ and $X$ and $n$. Then the lift functor object property of $P$ and $F$ is a functor of $D$ and the set of homological complexes of the set of full subcategories of $P$ and $c$.

HomologicalComplex.liftObjectPropertydefMathlib.Algebra.Homology.FullSubcategory, function or constant

Wording

the lift object property of P and K (from the name)

English

Let $P$ be an object property of $V$. Let $K$ be a homological complex of $V$ and $c$ such that for all elements $n$ of $x$, $P$ holds for $\operatorname{X}$ applied to $K$ and $n$. Then the lift object property of $P$ and $K$ is a homological complex of the set of full subcategories of $P$ and $c$.

Mathlib.Algebra.Homology.Functor

HomologicalComplex.asFunctordefMathlib.Algebra.Homology.Functor, function or constant

Wording

no wording

English

Let $C$ be a homological complex of the set of functors of $T$ and $V$ and $c$. Then $\operatorname{asFunctor}$ applied to $C$ is a functor of $T$ and the set of homological complexes of $V$ and $c$.

HomologicalComplex.complexOfFunctorsToFunctorToComplexdefMathlib.Algebra.Homology.Functor, function or constant

Wording

the complex (from the name)

English

The complex is a functor of the set of homological complexes of the set of functors of $T$ and $V$ and $c$ and the set of functors of $T$ and the set of homological complexes of $V$ and $c$.

Mathlib.Algebra.Homology.HasNoLoop

ComplexShape.HasNoLoopclassMathlib.Algebra.Homology.HasNoLoop, predicate

Wording

no wording

English

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

Mathlib.Algebra.Homology.HomologicalBicomplex

HomologicalComplex₂defMathlib.Algebra.Homology.HomologicalBicomplex, type

Wording

homological complex of x4 and x5 (from the name)

English

Let $C$ be a set. Let $x_{4}$ be a complex shape of $x_{2}$. Let $x_{5}$ be a complex shape of $x_{3}$. Then a homological complex of $x_{4}$ and $x_{5}$ is an element of the function that maps $C$, $x_{4}$ and $x_{5}$ to the set of homological complexes of the set of homological complexes of $C$ and $x_{5}$ and $x_{4}$.

HomologicalComplex₂.XXIsoOfEqdefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

no wording

English

Let $C$ be a set. Let $x_{4}$ be a complex shape of $x_{2}$. Let $x_{5}$ be a complex shape of $x_{3}$. Let $K$ be a homological complex of $x_{4}$ and $x_{5}$. Assume that $\EqtMACRoH {x_{6}}{x_{7}}$. Assume that $\EqtMACRoH {x_{8}}{x_{9}}$. Then $\mathrm{HomologicalComplex\_u2082\_\_\_XXIsoOfEq}$ applied to $C$, $x_{4}$, $x_{5}$, $K$, $h$ and $h_{1}$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $x_{6}$ and $x_{8}$ and $\operatorname{X}$ applied to $\operatorname{X}$ applied to $K$ and $x_{7}$ and $x_{9}$.

HomologicalComplex₂.flipdefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

the flip of K (from the name)

English

Let $K$ be a homological complex of $x_{4}$ and $x_{5}$. Then the flip of $K$ is a homological complex of $x_{5}$ and $x_{4}$.

HomologicalComplex₂.flipEquivalencedefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

the flip equivalence of x4 and x5 (from the name)

English

Let $C$ be a set. Let $x_{4}$ be a complex shape of $x_{2}$. Let $x_{5}$ be a complex shape of $x_{3}$. Then the flip equivalence of $x_{4}$ and $x_{5}$ is an equivalence of the set of homological complexes of $x_{4}$ and $x_{5}$ and the set of homological complexes of $x_{5}$ and $x_{4}$.

HomologicalComplex₂.flipFunctordefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

the flip functor of x4 and x5 (from the name)

English

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

HomologicalComplex₂.homMkdefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of the graded object of $K$ and the graded object of $L$ such that for all elements $x_{9}$ of $x_{2}$, for all elements $x_{10}$ of $x_{2}$, for all elements $x_{11}$ of $x_{3}$, if $\operatorname{Rel}$ holds for $x_{4}$, $x_{9}$ and $x_{10}$, then the composition of $f$ applied to $\ProdmkMACRoU {x_{9}}{x_{11}}$ and $\operatorname{f}$ applied to $\operatorname{d}$ applied to $L$, $x_{9}$ and $x_{10}$ and $x_{11}$ is equal to the composition of $\operatorname{f}$ applied to $\operatorname{d}$ applied to $K$, $x_{9}$ and $x_{10}$ and $x_{11}$ and $f$ applied to $\ProdmkMACRoU {x_{10}}{x_{11}}$ and for all elements $x_{6}$ of $x_{2}$, for all elements $x_{7}$ of $x_{3}$, for all elements $x_{8}$ of $x_{3}$, if $\operatorname{Rel}$ holds for $x_{5}$, $x_{7}$ and $x_{8}$, then the composition of $f$ applied to $\ProdmkMACRoU {x_{6}}{x_{7}}$ and $\operatorname{d}$ applied to $\operatorname{X}$ applied to $L$ and $x_{6}$, $x_{7}$ and $x_{8}$ is equal to the composition of $\operatorname{d}$ applied to $\operatorname{X}$ applied to $K$ and $x_{6}$, $x_{7}$ and $x_{8}$ and $f$ applied to $\ProdmkMACRoU {x_{6}}{x_{8}}$. Then the homomorphism of $f$ is a homomorphism of $K$ and $L$.

HomologicalComplex₂.ofGradedObjectdefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

the homological complex of x6 and x29 (from the name)

English

Let $x_{4}$ be a complex shape of $x_{2}$. Let $x_{5}$ be a complex shape of $x_{3}$. Let $X$ be a graded object of $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$ and $C$. Let $x_{6}$ be a function from elements $x_{29}$ of $x_{2}$ and elements $x_{30}$ of $x_{2}$ and elements $x_{31}$ of $x_{3}$ to homomorphisms of $X$ applied to $\ProdmkMACRoU {x_{29}}{x_{31}}$ and $X$ applied to $\ProdmkMACRoU {x_{30}}{x_{31}}$. Let $x_{7}$ be a function from elements $x_{26}$ of $x_{2}$ and elements $x_{27}$ of $x_{3}$ and elements $x_{28}$ of $x_{3}$ to homomorphisms of $X$ applied to $\ProdmkMACRoU {x_{26}}{x_{27}}$ and $X$ applied to $\ProdmkMACRoU {x_{26}}{x_{28}}$. Assume that for all elements $x_{23}$ and $x_{24}$ of $x_{2}$, if it is not the case that $\operatorname{Rel}$ holds for $x_{4}$, $x_{23}$ and $x_{24}$, then for all elements $x_{25}$ of $x_{3}$, $\EqtMACRoH {x_{6} (x_{23} , x_{24} , x_{25})}{0}$. Assume that for all elements $x_{20}$ of $x_{2}$, for all elements $x_{21}$ and $x_{22}$ of $x_{3}$, if it is not the case that $\operatorname{Rel}$ holds for $x_{5}$, $x_{21}$ and $x_{22}$, then $\EqtMACRoH {x_{7} (x_{20} , x_{21} , x_{22})}{0}$. Assume that for all elements $x_{16}$, $x_{17}$ and $x_{18}$ of $x_{2}$, for all elements $x_{19}$ of $x_{3}$, the composition of $x_{6}$ applied to $x_{16}$, $x_{17}$ and $x_{19}$ and $x_{6}$ applied to $x_{17}$, $x_{18}$ and $x_{19}$ is equal to $0$. Assume that for all elements $x_{12}$ of $x_{2}$, for all elements $x_{13}$, $x_{14}$ and $x_{15}$ of $x_{3}$, the composition of $x_{7}$ applied to $x_{12}$, $x_{13}$ and $x_{14}$ and $x_{7}$ applied to $x_{12}$, $x_{14}$ and $x_{15}$ is equal to $0$. Assume that for all elements $x_{8}$ and $x_{9}$ of $x_{2}$, for all elements $x_{10}$ and $x_{11}$ of $x_{3}$, the composition of $x_{6}$ applied to $x_{8}$, $x_{9}$ and $x_{10}$ and $x_{7}$ applied to $x_{9}$, $x_{10}$ and $x_{11}$ is equal to the composition of $x_{7}$ applied to $x_{8}$, $x_{10}$ and $x_{11}$ and $x_{6}$ applied to $x_{8}$, $x_{9}$ and $x_{11}$. Then the homological complex of $x_{29}$ and $x_{30}$ is a homological complex of $x_{4}$ and $x_{5}$.

HomologicalComplex₂.toGradedObjectdefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

the graded object of K (from the name)

English

Let $K$ be a homological complex of $x_{4}$ and $x_{5}$. Then the graded object of $K$ is a graded object of $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$ and $C$.

HomologicalComplex₂.toGradedObjectFunctordefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

the graded object functor of x4 and x5 (from the name)

English

Let $C$ be a set. Let $x_{4}$ be a complex shape of $x_{2}$. Let $x_{5}$ be a complex shape of $x_{3}$. Then the graded object functor of $x_{4}$ and $x_{5}$ is a functor of the set of homological complexes of $x_{4}$ and $x_{5}$ and the set of graded objects of $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$ and $C$.

HomologicalComplex₂.toGradedObjectMapdefMathlib.Algebra.Homology.HomologicalBicomplex, function or constant

Wording

the graded object map of x6 (from the name)

English

Let $x_{6}$ be a homomorphism of $K$ and $L$. Then the graded object map of $x_{6}$ is a homomorphism of the graded object of $K$ and the graded object of $L$.

Mathlib.Algebra.Homology.HomologicalComplex

ChainComplexdefMathlib.Algebra.Homology.HomologicalComplex, type

Wording

chain complex of V and x2 (from the name)

English

Let $V$ and $x_{2}$ be sets. Then a chain complex of $V$ and $x_{2}$ is an element of the function that maps $V$ and $x_{2}$ to the set of homological complexes of $V$ and $\operatorname{down}$ applied to $x_{2}$.

ChainComplex.mkdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

ChainComplex.mk'defMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $V$. Let $d$ be a homomorphism of $x_{3}$ and $x_{2}$. Let $\mathrm{succ'}$ be a function from elements $x_{4}$ of $V$ and elements $x_{5}$ of $V$ and homomorphisms $f$ of $x_{5}$ and $x_{4}$ to elements of $\mathrm{PSigma}$ applied to the function that maps $x_{6}$ to $\mathrm{PSigma}$ applied to the function that maps $d_{1}$ to the proposition that the composition of $d_{1}$ and $f$ is equal to $0$. Then $\operatorname{mk'}$ applied to $x_{2}$, $x_{3}$, $d$, $x_{4}$, $x_{5}$, $f$ and $\mathrm{succ'}$ is a chain complex of $V$ and $\Natural$.

ChainComplex.mk'XIsodefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the isomorphism of x13 and x14 (from the name)

English

Let $x_{2}$ and $x_{3}$ be elements of $V$. Let $x_{4}$ be a homomorphism of $x_{3}$ and $x_{2}$. Let $\mathrm{succ'}$ be a function from elements $x_{13}$ of $V$ and elements $x_{14}$ of $V$ and homomorphisms $f$ of $x_{14}$ and $x_{13}$ to elements of $\mathrm{PSigma}$ applied to the function that maps $x_{15}$ to $\mathrm{PSigma}$ applied to the function that maps $d$ to the proposition that the composition of $d$ and $f$ is equal to $0$. Let $n$ be a natural number. Then the isomorphism of $x_{13}$ and $x_{14}$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{mk'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{succ'}$ applied to $x_{5}$ and $x_{6}$ and $n + 2$ and $\operatorname{fst}$ applied to $\mathrm{succ'}$ applied to $\operatorname{X}$ applied to $\operatorname{mk'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{succ'}$ applied to $x_{7}$ and $x_{8}$ and $n$, $\operatorname{X}$ applied to $\operatorname{mk'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and the function that maps $x_{9}$ and $x_{10}$ to $\mathrm{succ'}$ applied to $x_{9}$ and $x_{10}$ and $n + 1$ and $\operatorname{d}$ applied to $\operatorname{mk'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and the function that maps $x_{11}$ and $x_{12}$ to $\mathrm{succ'}$ applied to $x_{11}$ and $x_{12}$, $n + 1$ and $n$.

ChainComplex.mkHomdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the homomorphism of one and succ (from the name)

English

Let $P$ and $Q$ be chain complexes of $V$ and $\Natural$. Let $\mathrm{zero}$ be a homomorphism of $\operatorname{X}$ applied to $P$ and $0$ and $\operatorname{X}$ applied to $Q$ and $0$. Let $\mathrm{one}$ be a homomorphism of $\operatorname{X}$ applied to $P$ and $1$ and $\operatorname{X}$ applied to $Q$ and $1$ such that the composition of $\mathrm{one}$ and $\operatorname{d}$ applied to $Q$, $1$ and $0$ is equal to the composition of $\operatorname{d}$ applied to $P$, $1$ and $0$ and $\mathrm{zero}$. Let $\mathrm{succ}$ be a function from elements $n$ of $\Natural$ and elements $p$ of $\mathrm{PSigma}$ applied to the function that maps $f$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{f'}$ to the proposition that the composition of $\mathrm{f'}$ and $\operatorname{d}$ applied to $Q$, $n + 1$ and $n$ is equal to the composition of $\operatorname{d}$ applied to $P$, $n + 1$ and $n$ and $f$ to elements of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{f''}$ to the proposition that the composition of $\mathrm{f''}$ and $\operatorname{d}$ applied to $Q$, $n + 2$ and $n + 1$ is equal to the composition of $\operatorname{d}$ applied to $P$, $n + 2$ and $n + 1$ and $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $p$. Then the homomorphism of $\mathrm{one}$ and $n$ is a homomorphism of $P$ and $Q$.

ChainComplex.mkXIsodefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the isomorphism of succ and S (from the name)

English

Let $x_{2}$, $x_{3}$ and $x_{4}$ be elements of $V$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{2}$. Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{3}$ such that the composition of $x_{6}$ and $x_{5}$ is equal to $0$. Let $\mathrm{succ}$ be a function from short complexes $S$ of $V$ to elements of $\mathrm{PSigma}$ applied to the function that maps $x_{7}$ to $\mathrm{PSigma}$ applied to the function that maps $x_{8}$ to the proposition that the composition of $x_{8}$ and $\operatorname{f}$ applied to $S$ is equal to $0$. Let $n$ be a natural number. Then the isomorphism of $S$ and $\mathrm{succ}$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $s$ and $\mathrm{succ}$ and $n + 3$ and $\operatorname{fst}$ applied to $\mathrm{succ}$ applied to $\operatorname{mk}$ applied to $\operatorname{d}$ applied to $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $s$ and $\mathrm{succ}$, $n + 2$ and $n + 1$, $\operatorname{d}$ applied to $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $s$ and $\mathrm{succ}$, $n + 1$ and $n$ and $\mathrm{HomologicalComplex\_\_d\_comp\_d}$ applied to $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $s$ and $\mathrm{succ}$, $n + 2$, $n + 1$ and $n$.

ChainComplex.ofdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $x_{2}$ to elements of $V$. Let $d$ be a function from elements $n_{1}$ of $x_{2}$ to homomorphisms of $X$ applied to $n_{1} + 1$ and $X$ applied to $n_{1}$ such that for all elements $n$ of $x_{2}$, the composition of $d$ applied to $n + 1$ and $d$ applied to $n$ is equal to $0$. Then $\operatorname{of}$ applied to $X$, $n_{1}$, $d$ and $\mathrm{sq}$ is a chain complex of $V$ and $x_{2}$.

ChainComplex.ofHomdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the chain complex of f and i1 (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x_{2}$ to homomorphisms of $\operatorname{X}$ applied to $X$ and $i_{1}$ and $\operatorname{X}$ applied to $Y$ and $i_{1}$ such that for all elements $i$ of $x_{2}$, the composition of $f$ applied to $i + 1$ and $\operatorname{d}$ applied to $Y$, $i + 1$ and $i$ is equal to the composition of $\operatorname{d}$ applied to $X$, $i + 1$ and $i$ and $f$ applied to $i$. Then the chain complex of $i_{1}$ and $f$ is a homomorphism of $X$ and $Y$.

CochainComplexdefMathlib.Algebra.Homology.HomologicalComplex, type

Wording

cochain complex of V and x2 (from the name)

English

Let $V$ and $x_{2}$ be sets. Then a cochain complex of $V$ and $x_{2}$ is an element of the function that maps $V$ and $x_{2}$ to the set of homological complexes of $V$ and $\operatorname{up}$ applied to $x_{2}$.

CochainComplex.mkdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $x_{2}$, $x_{3}$ and $x_{4}$ be elements of $V$. Let $x_{5}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{6}$ be a homomorphism of $x_{3}$ and $x_{4}$ such that the composition of $x_{5}$ and $x_{6}$ is equal to $0$. Let $\mathrm{succ}$ be a function from short complexes $S$ of $V$ to elements of $\mathrm{PSigma}$ applied to the function that maps $x_{7}$ to $\mathrm{PSigma}$ applied to the function that maps $x_{8}$ to the proposition that the composition of $\operatorname{g}$ applied to $S$ and $x_{8}$ is equal to $0$. Then $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $s$, $S$ and $\mathrm{succ}$ is a cochain complex of $V$ and $\Natural$.

CochainComplex.mk'defMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $V$. Let $d$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $\mathrm{succ'}$ be a function from elements $x_{4}$ of $V$ and elements $x_{5}$ of $V$ and homomorphisms $f$ of $x_{4}$ and $x_{5}$ to elements of $\mathrm{PSigma}$ applied to the function that maps $x_{6}$ to $\mathrm{PSigma}$ applied to the function that maps $d_{1}$ to the proposition that the composition of $f$ and $d_{1}$ is equal to $0$. Then $\operatorname{mk'}$ applied to $x_{2}$, $x_{3}$, $d$, $x_{4}$, $x_{5}$, $f$ and $\mathrm{succ'}$ is a cochain complex of $V$ and $\Natural$.

CochainComplex.mkHomdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the homomorphism of one and succ (from the name)

English

Let $P$ and $Q$ be cochain complexes of $V$ and $\Natural$. Let $\mathrm{zero}$ be a homomorphism of $\operatorname{X}$ applied to $P$ and $0$ and $\operatorname{X}$ applied to $Q$ and $0$. Let $\mathrm{one}$ be a homomorphism of $\operatorname{X}$ applied to $P$ and $1$ and $\operatorname{X}$ applied to $Q$ and $1$ such that the composition of $\mathrm{zero}$ and $\operatorname{d}$ applied to $Q$, $0$ and $1$ is equal to the composition of $\operatorname{d}$ applied to $P$, $0$ and $1$ and $\mathrm{one}$. Let $\mathrm{succ}$ be a function from elements $n$ of $\Natural$ and elements $p$ of $\mathrm{PSigma}$ applied to the function that maps $f$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{f'}$ to the proposition that the composition of $f$ and $\operatorname{d}$ applied to $Q$, $n$ and $n + 1$ is equal to the composition of $\operatorname{d}$ applied to $P$, $n$ and $n + 1$ and $\mathrm{f'}$ to elements of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{f''}$ to the proposition that the composition of $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $p$ and $\operatorname{d}$ applied to $Q$, $n + 1$ and $n + 2$ is equal to the composition of $\operatorname{d}$ applied to $P$, $n + 1$ and $n + 2$ and $\mathrm{f''}$. Then the homomorphism of $\mathrm{one}$ and $n$ is a homomorphism of $P$ and $Q$.

CochainComplex.ofdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $x_{2}$ to elements of $V$. Let $d$ be a function from elements $n_{1}$ of $x_{2}$ to homomorphisms of $X$ applied to $n_{1}$ and $X$ applied to $n_{1} + 1$ such that for all elements $n$ of $x_{2}$, the composition of $d$ applied to $n$ and $d$ applied to $n + 1$ is equal to $0$. Then $\operatorname{of}$ applied to $X$, $n_{1}$, $d$ and $\mathrm{sq}$ is a cochain complex of $V$ and $x_{2}$.

CochainComplex.ofHomdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the cochain complex of f and i1 (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x_{2}$ to homomorphisms of $\operatorname{X}$ applied to $X$ and $i_{1}$ and $\operatorname{X}$ applied to $Y$ and $i_{1}$ such that for all elements $i$ of $x_{2}$, the composition of $f$ applied to $i$ and $\operatorname{d}$ applied to $Y$, $i$ and $i + 1$ is equal to the composition of $\operatorname{d}$ applied to $X$, $i$ and $i + 1$ and $f$ applied to $i + 1$. Then the cochain complex of $i_{1}$ and $f$ is a homomorphism of $X$ and $Y$.

HomologicalComplexstructureMathlib.Algebra.Homology.HomologicalComplex, type

Wording

homological complex of V and c (from the name)

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Then the homological complexes of $V$ and $c$ are a basic type.

HomologicalComplex.HomstructureMathlib.Algebra.Homology.HomologicalComplex, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be homological complexes of $V$ and $c$. Then the homomorphisms of $A$ and $B$ are a basic type.

HomologicalComplex.Hom.fdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Let $i$ be an element of $x$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $A$ and $i$ and $\operatorname{X}$ applied to $B$ and $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

HomologicalComplex.Hom.isoAppdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the isomorphism application of f and i (from the name)

English

Let $f$ be an isomorphism of $x_{3}$ and $x_{4}$. Let $i$ be an element of $x$. Then the isomorphism application of $f$ and $i$ is an isomorphism of $\operatorname{X}$ applied to $x_{3}$ and $i$ and $\operatorname{X}$ applied to $x_{4}$ and $i$ defined as the map isomorphism of the evaluation of $c$ and $i$ and $f$.

HomologicalComplex.Hom.isoOfComponentsdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the isomorphism of f and i1 (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x$ to isomorphisms of $\operatorname{X}$ applied to $x_{3}$ and $i_{1}$ and $\operatorname{X}$ applied to $x_{4}$ and $i_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ and $j$ of $x$, if $\operatorname{Rel}$ holds for $c$, $i$ and $j$, then the composition of the homomorphism of $f$ applied to $i$ and $\operatorname{d}$ applied to $x_{4}$, $i$ and $j$ is equal to the composition of $\operatorname{d}$ applied to $x_{3}$, $i$ and $j$ and the homomorphism of $f$ applied to $j$ and $\mathrm{HomologicalComplex\_\_Hom\_\_isoOfComponents\_\_\_auto\_1}$. Then the isomorphism of $i_{1}$ and $f$ is an isomorphism of $x_{3}$ and $x_{4}$.

HomologicalComplex.Hom.nextdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $i$ be an element of $x$. Then $\operatorname{next}$ applied to $f$ and $i$ is a homomorphism of $\operatorname{xNext}$ applied to $x_{3}$ and $i$ and $\operatorname{xNext}$ applied to $x_{4}$ and $i$ defined as $\operatorname{f}$ applied to $f$ and $\operatorname{next}$ applied to $c$ and $i$.

HomologicalComplex.Hom.prevdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $j$ be an element of $x$. Then $\operatorname{prev}$ applied to $f$ and $j$ is a homomorphism of $\operatorname{xPrev}$ applied to $x_{3}$ and $j$ and $\operatorname{xPrev}$ applied to $x_{4}$ and $j$ defined as $\operatorname{f}$ applied to $f$ and $\operatorname{prev}$ applied to $c$ and $j$.

HomologicalComplex.Hom.sqFromdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $i$ be an element of $x$. Then $\operatorname{sqFrom}$ applied to $f$ and $i$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{dFrom}$ applied to $x_{3}$ and $i$ and $\operatorname{mk}$ applied to $\operatorname{dFrom}$ applied to $x_{4}$ and $i$ defined as the homomorphism of $\operatorname{f}$ applied to $f$ and $i$ and $\operatorname{next}$ applied to $f$ and $i$.

HomologicalComplex.Hom.sqTodefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $j$ be an element of $x$. Then $\operatorname{sqTo}$ applied to $f$ and $j$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{dTo}$ applied to $x_{3}$ and $j$ and $\operatorname{mk}$ applied to $\operatorname{dTo}$ applied to $x_{4}$ and $j$ defined as the homomorphism of $\operatorname{prev}$ applied to $f$ and $j$ and $\operatorname{f}$ applied to $f$ and $j$.

HomologicalComplex.XdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homological complex of $V$ and $c$. Let $x_{3}$ be an element of $x$. Then $\operatorname{X}$ applied to $\mathrm{self}$ and $x_{3}$ is an element of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

HomologicalComplex.XIsoOfEqdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the obvious isomorphism of K and h (from the docstring)

English

Let $K$ be a homological complex of $V$ and $c$. Assume that $\EqtMACRoH {p}{q}$. Then the obvious isomorphism of $K$ and $h$ is an isomorphism of $\operatorname{X}$ applied to $K$ and $p$ and $\operatorname{X}$ applied to $K$ and $q$.

HomologicalComplex.compdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the composition of x3 and x4 (from the name)

English

Let $A$, $B$ and $C$ be homological complexes of $V$ and $c$. Let $x_{3}$ be a homomorphism of $A$ and $B$. Let $x_{4}$ be a homomorphism of $B$ and $C$. Then the composition of $x_{3}$ and $x_{4}$ is a homomorphism of $A$ and $C$.

HomologicalComplex.ddefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homological complex of $V$ and $c$. Let $i$ and $j$ be elements of $x$. Then $\operatorname{d}$ applied to $\mathrm{self}$, $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to $\mathrm{self}$ and $i$ and $\operatorname{X}$ applied to $\mathrm{self}$ and $j$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $i$ and $j$.

HomologicalComplex.dFromdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $C$ be a homological complex of $V$ and $c$. Let $i$ be an element of $x$. Then $\operatorname{dFrom}$ applied to $C$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $C$ and $i$ and $\operatorname{xNext}$ applied to $C$ and $i$ defined as $\operatorname{d}$ applied to $C$, $i$ and $\operatorname{next}$ applied to $c$ and $i$.

HomologicalComplex.dNatTransdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the differential as a natural transformation between V (from the docstring)

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Let $i$ and $j$ be elements of $x$. Then the differential as a natural transformation between $V$ is a homomorphism of the evaluation of $c$ and $i$ and the evaluation of $c$ and $j$.

HomologicalComplex.dTodefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $C$ be a homological complex of $V$ and $c$. Let $j$ be an element of $x$. Then $\operatorname{dTo}$ applied to $C$ and $j$ is a homomorphism of $\operatorname{xPrev}$ applied to $C$ and $j$ and $\operatorname{X}$ applied to $C$ and $j$ defined as $\operatorname{d}$ applied to $C$, $\operatorname{prev}$ applied to $c$ and $j$ and $j$.

HomologicalComplex.evaldefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the evaluation of c and i (from the name)

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then the evaluation of $c$ and $i$ is a functor of the set of homological complexes of $V$ and $c$ and $V$.

HomologicalComplex.forgetdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Then $\operatorname{forget}$ applied to $V$ and $c$ is a functor of the set of homological complexes of $V$ and $c$ and the set of graded objects of $x$ and $V$.

HomologicalComplex.forgetEvaldefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then $\operatorname{forgetEval}$ applied to $V$, $c$ and $i$ is an isomorphism of the composition of $\operatorname{forget}$ applied to $V$ and $c$ and the evaluation of $i$ and the evaluation of $c$ and $i$.

HomologicalComplex.iddefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the identity of A (from the name)

English

Let $A$ be a homological complex of $V$ and $c$. Then the identity of $A$ is a homomorphism of $A$ and $A$.

HomologicalComplex.xNextdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $C$ be a homological complex of $V$ and $c$. Let $i$ be an element of $x$. Then $\operatorname{xNext}$ applied to $C$ and $i$ is an element of $V$ defined as $\operatorname{X}$ applied to $C$ and $\operatorname{next}$ applied to $c$ and $i$.

HomologicalComplex.xNextIsodefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the next isomorphism of C and r (from the name)

English

Let $C$ be a homological complex of $V$ and $c$. Assume that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the next isomorphism of $C$ and $r$ is an isomorphism of $\operatorname{xNext}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $C$ and $j$.

HomologicalComplex.xNextIsoSelfdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the next isomorphism self of C and h (from the name)

English

Let $C$ be a homological complex of $V$ and $c$. Assume that it is not the case that $\operatorname{Rel}$ holds for $c$, $i$ and $\operatorname{next}$ applied to $c$ and $i$. Then the next isomorphism self of $C$ and $h$ is an isomorphism of $\operatorname{xNext}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $C$ and $i$.

HomologicalComplex.xPrevdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $C$ be a homological complex of $V$ and $c$. Let $j$ be an element of $x$. Then $\operatorname{xPrev}$ applied to $C$ and $j$ is an element of $V$ defined as $\operatorname{X}$ applied to $C$ and $\operatorname{prev}$ applied to $c$ and $j$.

HomologicalComplex.xPrevIsodefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $C$ be a homological complex of $V$ and $c$. Assume that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then $\operatorname{xPrevIso}$ applied to $C$ and $r$ is an isomorphism of $\operatorname{xPrev}$ applied to $C$ and $j$ and $\operatorname{X}$ applied to $C$ and $i$.

HomologicalComplex.xPrevIsoSelfdefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

no wording

English

Let $C$ be a homological complex of $V$ and $c$. Assume that it is not the case that $\operatorname{Rel}$ holds for $c$, $\operatorname{prev}$ applied to $c$ and $j$ and $j$. Then $\operatorname{xPrevIsoSelf}$ applied to $C$ and $h$ is an isomorphism of $\operatorname{xPrev}$ applied to $C$ and $j$ and $\operatorname{X}$ applied to $C$ and $j$.

HomologicalComplex.zerodefMathlib.Algebra.Homology.HomologicalComplex, function or constant

Wording

the zero complex (from the docstring)

English

The zero complex is a homological complex of $V$ and $c$.

Mathlib.Algebra.Homology.HomologicalComplexBiprod

HomologicalComplex.biprodXIsodefMathlib.Algebra.Homology.HomologicalComplexBiprod, function or constant

Wording

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

English

Let $K$ and $L$ be homological complexes of $C$ and $c$. Let $i$ be an element of $x$. Then the biproduct isomorphism of $L$ and $i$ is an isomorphism of $\operatorname{X}$ applied to the biproduct of $K$ and $L$ and $i$ and the biproduct of $\operatorname{X}$ applied to $K$ and $i$ and $\operatorname{X}$ applied to $L$ and $i$ defined as the map biproduct of $K$ and $L$.

Mathlib.Algebra.Homology.HomologicalComplexLimits

HomologicalComplex.coconeOfHasColimitEvaldefMathlib.Algebra.Homology.HomologicalComplexLimits, function or constant

Wording

the cocone of F (from the name)

English

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

HomologicalComplex.coneOfHasLimitEvaldefMathlib.Algebra.Homology.HomologicalComplexLimits, function or constant

Wording

the cone of F (from the name)

English

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

HomologicalComplex.isColimitCoconeOfHasColimitEvaldefMathlib.Algebra.Homology.HomologicalComplexLimits, function or constant

Wording

the cocone of F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of homological complexes of $C$ and $c$. Then the cocone of $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $F$ defined as $\operatorname{isColimitOfEval}$ applied to $F$, the cocone of $F$ and the function that maps $x_{4}$ to $\operatorname{isColimit}$ applied to the composition of $F$ and the evaluation of $c$ and $x_{4}$.

HomologicalComplex.isColimitOfEvaldefMathlib.Algebra.Homology.HomologicalComplexLimits, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of homological complexes of $C$ and $c$. Let $s$ be a cocone of $F$. Let $\mathrm{hs}$ be a function from elements $i$ of $x$ to elements of $\operatorname{IsColimit}$ applied to the map cocone of the evaluation of $c$ and $i$ and $s$. Then $\operatorname{isColimitOfEval}$ applied to $F$, $s$, $i$ and $\mathrm{hs}$ is an element of $\operatorname{IsColimit}$ applied to $s$.

HomologicalComplex.isLimitConeOfHasLimitEvaldefMathlib.Algebra.Homology.HomologicalComplexLimits, function or constant

Wording

the cone of F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of homological complexes of $C$ and $c$. Then the cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the cone of $F$ defined as $\operatorname{isLimitOfEval}$ applied to $F$, the cone of $F$ and the function that maps $x_{4}$ to $\operatorname{isLimit}$ applied to the composition of $F$ and the evaluation of $c$ and $x_{4}$.

HomologicalComplex.isLimitOfEvaldefMathlib.Algebra.Homology.HomologicalComplexLimits, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of homological complexes of $C$ and $c$. Let $s$ be a cone of $F$. Let $\mathrm{hs}$ be a function from elements $i$ of $x$ to elements of $\operatorname{IsLimit}$ applied to the map cone of the evaluation of $c$ and $i$ and $s$. Then $\operatorname{isLimitOfEval}$ applied to $F$, $s$, $i$ and $\mathrm{hs}$ is an element of $\operatorname{IsLimit}$ applied to $s$.

Mathlib.Algebra.Homology.HomologySequence

CategoryTheory.ShortComplex.ShortExact.δdefMathlib.Algebra.Homology.HomologySequence, function or constant

Wording

no wording

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Let $i$ and $j$ be elements of $x$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_ShortExact\_\_\_u3b4\_}$ applied to $\mathrm{hS}$, $i$, $j$ and $\mathrm{hij}$ is a homomorphism of the homology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and $i$ and the homology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $j$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_\_u3b4\_}$ applied to the snake input of $i$ and $j$.

CategoryTheory.ShortComplex.ShortExact.δIsodefMathlib.Algebra.Homology.HomologySequence, function or constant

Wording

the isomorphism of i and j (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Let $i$ and $j$ be elements of $x$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$, the homology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $i$ is a zero and the homology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $j$ is a zero. Then the isomorphism of $i$ and $j$ is an isomorphism of the homology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and $i$ and the homology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $j$ defined as $\operatorname{asIso}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_ShortExact\_\_\_u3b4\_}$ applied to $\mathrm{hS}$, $i$, $j$ and $\mathrm{hij}$.

HomologicalComplex.HomologySequence.composableArrows₃defMathlib.Algebra.Homology.HomologySequence, function or constant

Wording

the composable arrow of i and j (from the name)

English

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x$. Then the composable arrow of $i$ and $j$ is a composable arrow of $C$ and $3$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the inclusion map of the homology of $K$ and $i$, $\operatorname{opcyclesToCycles}$ applied to $K$, $i$ and $j$ and the homology projection of $K$ and $j$.

HomologicalComplex.HomologySequence.composableArrows₃FunctordefMathlib.Algebra.Homology.HomologySequence, function or constant

Wording

the composable arrow functor of i and j (from the name)

English

Let $C$ be a set. Let $i$ and $j$ be elements of $x$. Then the composable arrow functor of $i$ and $j$ is a functor of the set of homological complexes of $C$ and $c$ and the set of composable arrows of $C$ and $3$.

HomologicalComplex.HomologySequence.snakeInputdefMathlib.Algebra.Homology.HomologySequence, function or constant

Wording

the snake input of i and j (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Let $i$ and $j$ be elements of $x$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the snake input of $i$ and $j$ is a snake input of $C$.

HomologicalComplex.natTransOpCyclesToCyclesdefMathlib.Algebra.Homology.HomologySequence, function or constant

Wording

the natural transformation opposite cycle to cycle of i and j (from the name)

English

Let $C$ be a set. Let $c$ be a complex shape of $x$. Let $i$ and $j$ be elements of $x$. Then the natural transformation opposite cycle to cycle of $i$ and $j$ is a homomorphism of $\operatorname{opcyclesFunctor}$ applied to $C$, $c$ and $i$ and the cycle functor of $c$ and $j$.

HomologicalComplex.opcyclesToCyclesdefMathlib.Algebra.Homology.HomologySequence, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $c$. Let $i$ and $j$ be elements of $x$. Then $\operatorname{opcyclesToCycles}$ applied to $K$, $i$ and $j$ is a homomorphism of $\operatorname{opcycles}$ applied to $K$ and $i$ and the cycle of $K$ and $j$.

Mathlib.Algebra.Homology.HomologySequenceLemmas

HomologicalComplex.HomologySequence.composableArrows₂defMathlib.Algebra.Homology.HomologySequenceLemmas, function or constant

Wording

the composable arrow of S and i (from the name)

English

Let $S$ be a short complex of the set of homological complexes of $C$ and $c$. Let $i$ be an element of $x$. Then the composable arrow of $S$ and $i$ is a composable arrow of $C$ and $2$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to the map of $\operatorname{f}$ applied to $S$ and $i$ and the map of $\operatorname{g}$ applied to $S$ and $i$.

HomologicalComplex.HomologySequence.composableArrows₅defMathlib.Algebra.Homology.HomologySequenceLemmas, function or constant

Wording

the composable arrow of i and j (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $x_{3}$. Let $i$ and $j$ be elements of $x$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the composable arrow of $i$ and $j$ is a composable arrow of $C$ and $5$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2085\_}$ applied to the map of $\operatorname{f}$ applied to $x_{3}$ and $i$, the map of $\operatorname{g}$ applied to $x_{3}$ and $i$, $\mathrm{CategoryTheory\_\_ShortComplex\_\_ShortExact\_\_\_u3b4\_}$ applied to $h$, $i$, $j$ and $\mathrm{hij}$, the map of $\operatorname{f}$ applied to $x_{3}$ and $j$ and the map of $\operatorname{g}$ applied to $x_{3}$ and $j$.

HomologicalComplex.HomologySequence.mapComposableArrows₂defMathlib.Algebra.Homology.HomologySequenceLemmas, function or constant

Wording

the map between the exact sequences of x5 and i (from the docstring)

English

Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $i$ be an element of $x$. Then the map between the exact sequences of $x_{5}$ and $i$ is a homomorphism of the composable arrow of $x_{3}$ and $i$ and the composable arrow of $x_{4}$ and $i$.

HomologicalComplex.HomologySequence.mapComposableArrows₅defMathlib.Algebra.Homology.HomologySequenceLemmas, function or constant

Wording

the map composable arrow of i and j (from the name)

English

Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Assume that $\operatorname{ShortExact}$ holds for $x_{3}$. Assume that $\operatorname{ShortExact}$ holds for $x_{4}$. Let $i$ and $j$ be elements of $x$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the map composable arrow of $i$ and $j$ is a homomorphism of the composable arrow of $i$ and $j$ and the composable arrow of $i$ and $j$.

HomologicalComplex.HomologySequence.mapSnakeInputdefMathlib.Algebra.Homology.HomologySequenceLemmas, function or constant

Wording

the map snake input of i and j (from the name)

English

Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Assume that $\operatorname{ShortExact}$ holds for $x_{3}$. Assume that $\operatorname{ShortExact}$ holds for $x_{4}$. Let $i$ and $j$ be elements of $x$ such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Then the map snake input of $i$ and $j$ is a homomorphism of the snake input of $i$ and $j$ and the snake input of $i$ and $j$.

Mathlib.Algebra.Homology.Homotopy

CategoryTheory.Functor.mapHomotopydefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the map homotopy of F and h1 (from the name)

English

Let $F$ be a functor of $V$ and $W$. Let $h_{1}$ be a homotopy of $f$ and $g$. Then the map homotopy of $F$ and $h_{1}$ is a homotopy of the map of the map homological complex of $F$ and $c$ and $f$ and the map of the map homological complex of $F$ and $c$ and $g$.

CategoryTheory.Functor.mapHomotopyEquivdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the map homotopy equivalence of F and h1 (from the name)

English

Let $F$ be a functor of $V$ and $W$. Let $h_{1}$ be a homotopy equivalence of $C$ and $D$. Then the map homotopy equivalence of $F$ and $h_{1}$ is a homotopy equivalence of the action of the map homological complex of $F$ and $c$ and $C$ and the action of the map homological complex of $F$ and $c$ and $D$.

HomologicalComplex.homotopyEquivalencesdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

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

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Then the homotopy equivalence of $V$ and $c$ is a morphism property of the set of homological complexes of $V$ and $c$ defined as the function that maps $X$, $Y$ and $f$ to the proposition that there exists a homotopy equivalence $e$ of $X$ and $Y$, such that the homomorphism of $e$ is equal to $f$.

HomotopystructureMathlib.Algebra.Homology.Homotopy, type

Wording

homotopy of f and g (from the name)

English

Let $f$ and $g$ be homomorphisms of $C$ and $D$. Then the homotopies of $f$ and $g$ are a basic type.

Homotopy.adddefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the sum of x7 and x8 (from the name)

English

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

Homotopy.compdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the composition of x10 and x11 (from the name)

English

Let $x_{10}$ be a homotopy of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homotopy of $x_{8}$ and $x_{9}$. Then the composition of $x_{10}$ and $x_{11}$ is a homotopy of the composition of $x_{6}$ and $x_{8}$ and the composition of $x_{7}$ and $x_{9}$ defined as the composition of the right composition of $x_{10}$ and $x_{8}$ and the left composition of $x_{11}$ and $x_{7}$.

Homotopy.compLeftdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

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

English

Let $h$ be a homotopy of $f$ and $g$. Let $e$ be a homomorphism of $C$ and $D$. Then the left composition of $h$ and $e$ is a homotopy of the composition of $e$ and $f$ and the composition of $e$ and $g$.

Homotopy.compLeftIddefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the composition left identity of h and g (from the name)

English

Let $h$ be a homotopy of $f$ and the identity morphism of $D$. Let $g$ be a homomorphism of $C$ and $D$. Then the composition left identity of $h$ and $g$ is a homotopy of the composition of $g$ and $f$ and $g$.

Homotopy.compRightdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

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

English

Let $h$ be a homotopy of $e$ and $f$. Let $g$ be a homomorphism of $D$ and $E$. Then the right composition of $h$ and $g$ is a homotopy of the composition of $e$ and $g$ and the composition of $f$ and $g$.

Homotopy.compRightIddefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the composition right identity of h and g (from the name)

English

Let $h$ be a homotopy of $f$ and the identity morphism of $C$. Let $g$ be a homomorphism of $C$ and $D$. Then the composition right identity of $h$ and $g$ is a homotopy of the composition of $f$ and $g$ and $g$.

Homotopy.equivSubZerodefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the equivalence difference zero (from the name)

English

The equivalence difference zero is an equivalence from the set of homotopies of $f$ and $g$ to the set of homotopies of $f - g$ and $0$.

Homotopy.homdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the homomorphism of i and j (from the name)

English

Let $\mathrm{self}$ be a homotopy of $f$ and $g$. Let $i$ and $j$ be elements of $x$. Then the homomorphism of $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $D$ and $j$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $i$ and $j$.

Homotopy.mkCoinductivedefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

no wording

English

Let $e$ be a homomorphism of $P$ and $Q$. Let $\mathrm{zero}$ be a homomorphism of $\operatorname{X}$ applied to $P$ and $1$ and $\operatorname{X}$ applied to $Q$ and $0$ such that $\operatorname{f}$ applied to $e$ and $0$ is equal to the composition of $\operatorname{d}$ applied to $P$, $0$ and $1$ and $\mathrm{zero}$. Let $\mathrm{one}$ be a homomorphism of $\operatorname{X}$ applied to $P$ and $2$ and $\operatorname{X}$ applied to $Q$ and $1$ such that $\operatorname{f}$ applied to $e$ and $1$ is equal to the sum of the composition of $\mathrm{zero}$ and $\operatorname{d}$ applied to $Q$, $0$ and $1$ and the composition of $\operatorname{d}$ applied to $P$, $1$ and $2$ and $\mathrm{one}$. Let $\mathrm{succ}$ be a function from elements $n$ of $\Natural$ and elements $p$ of $\mathrm{PSigma}$ applied to the function that maps $f$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{f'}$ to the proposition that $\operatorname{f}$ applied to $e$ and $n + 1$ is equal to the sum of the composition of $f$ and $\operatorname{d}$ applied to $Q$, $n$ and $n + 1$ and the composition of $\operatorname{d}$ applied to $P$, $n + 1$ and $n + 2$ and $\mathrm{f'}$ to elements of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{f''}$ to the proposition that $\operatorname{f}$ applied to $e$ and $n + 2$ is equal to the sum of the composition of $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $p$ and $\operatorname{d}$ applied to $Q$, $n + 1$ and $n + 2$ and the composition of $\operatorname{d}$ applied to $P$, $n + 2$ and $n + 3$ and $\mathrm{f''}$. Then $\operatorname{mkCoinductive}$ applied to $e$, $\mathrm{zero}$, $\mathrm{comm\_zero}$, $\mathrm{one}$, $\mathrm{comm\_one}$, $n$, $p$ and $\mathrm{succ}$ is a homotopy of $e$ and $0$.

Homotopy.mkInductivedefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

no wording

English

Let $e$ be a homomorphism of $P$ and $Q$. Let $\mathrm{zero}$ be a homomorphism of $\operatorname{X}$ applied to $P$ and $0$ and $\operatorname{X}$ applied to $Q$ and $1$ such that $\operatorname{f}$ applied to $e$ and $0$ is equal to the composition of $\mathrm{zero}$ and $\operatorname{d}$ applied to $Q$, $1$ and $0$. Let $\mathrm{one}$ be a homomorphism of $\operatorname{X}$ applied to $P$ and $1$ and $\operatorname{X}$ applied to $Q$ and $2$ such that $\operatorname{f}$ applied to $e$ and $1$ is equal to the sum of the composition of $\operatorname{d}$ applied to $P$, $1$ and $0$ and $\mathrm{zero}$ and the composition of $\mathrm{one}$ and $\operatorname{d}$ applied to $Q$, $2$ and $1$. Let $\mathrm{succ}$ be a function from elements $n$ of $\Natural$ and elements $p$ of $\mathrm{PSigma}$ applied to the function that maps $f$ to $\mathrm{PSigma}$ applied to the function that maps $\mathrm{f'}$ to the proposition that $\operatorname{f}$ applied to $e$ and $n + 1$ is equal to the sum of the composition of $\operatorname{d}$ applied to $P$, $n + 1$ and $n$ and $f$ and the composition of $\mathrm{f'}$ and $\operatorname{d}$ applied to $Q$, $n + 2$ and $n + 1$ to elements of $\mathrm{PSigma}$ applied to the function that maps $\mathrm{f''}$ to the proposition that $\operatorname{f}$ applied to $e$ and $n + 2$ is equal to the sum of the composition of $\operatorname{d}$ applied to $P$, $n + 2$ and $n + 1$ and $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $p$ and the composition of $\mathrm{f''}$ and $\operatorname{d}$ applied to $Q$, $n + 3$ and $n + 2$. Then $\operatorname{mkInductive}$ applied to $e$, $\mathrm{zero}$, $\mathrm{comm\_zero}$, $\mathrm{one}$, $\mathrm{comm\_one}$, $n$, $p$ and $\mathrm{succ}$ is a homotopy of $e$ and $0$.

Homotopy.nullHomotopicMapdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the null homotopic map of hom (from the name)

English

Let $\mathrm{hom}$ be a function from elements $i$ of $x$ and elements $j$ of $x$ to homomorphisms of $\operatorname{X}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $D$ and $j$. Then the null homotopic map of $i$ is a homomorphism of $C$ and $D$.

Homotopy.nullHomotopicMap'defMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the null homotopic map of h (from the name)

English

Let $h$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\operatorname{Rel}$ applied to $c$, $j$ and $i$ to homomorphisms of $\operatorname{X}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $D$ and $j$. Then the null homotopic map of $i$ is a homomorphism of $C$ and $D$ defined as the function that maps $j$ and $h$ to the null homotopic map of the function that maps $i$ and $j$ to $\mathrm{dite}$ applied to $\operatorname{Rel}$ applied to $c$, $j$ and $i$, $i$ applied to $i$ and $j$ and the function that maps $h_{1}$ to $0$.

Homotopy.nullHomotopydefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the null homotopy of hom and i1 (from the name)

English

Let $\mathrm{hom}$ be a function from elements $i_{1}$ of $x$ and elements $j_{1}$ of $x$ to homomorphisms of $\operatorname{X}$ applied to $C$ and $i_{1}$ and $\operatorname{X}$ applied to $D$ and $j_{1}$ such that for all elements $i$ and $j$ of $x$, if it is not the case that $\operatorname{Rel}$ holds for $c$, $j$ and $i$, then $\EqtMACRoH {\mathrm{hom} (i , j)}{0}$. Then the null homotopy of $i_{1}$ and $j_{1}$ is a homotopy of the null homotopic map of $\mathrm{hom}$ and $0$.

Homotopy.nullHomotopy'defMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the null homotopy of h (from the name)

English

Homotopy.ofEqdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the homotopy of h (from the name)

English

Assume that $\EqtMACRoH {f}{g}$. Then the homotopy of $h$ is a homotopy of $f$ and $g$.

Homotopy.refldefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the identity of f (from the name)

English

Let $f$ be a homomorphism of $C$ and $D$. Then the identity of $f$ is a homotopy of $f$ and $f$.

Homotopy.smuldefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the scalar multiplication of h and a (from the docstring)

English

Let $h$ be a homotopy of $f$ and $g$. Let $a$ be an element of $R$. Then the scalar multiplication of $h$ and $a$ is a homotopy of $\HSMulhSMulMACRoAL {a}{f}$ and $\HSMulhSMulMACRoAL {a}{g}$.

Homotopy.symmdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the inverse of h (from the name)

English

Let $h$ be a homotopy of $f$ and $g$. Then the inverse of $h$ is a homotopy of $g$ and $f$.

Homotopy.toShortComplexdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the short complex of ho and i (from the name)

English

Let $\mathrm{ho}$ be a homotopy of $f$ and $g$. Let $i$ be an element of $x_{2}$. Then the short complex of $\mathrm{ho}$ and $i$ is a homotopy of the map of the short complex functor of $c$ and $i$ and $f$ and the map of the short complex functor of $c$ and $i$ and $g$.

Homotopy.transdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the composition of h and k (from the name)

English

Let $h$ be a homotopy of $e$ and $f$. Let $k$ be a homotopy of $f$ and $g$. Then the composition of $h$ and $k$ is a homotopy of $e$ and $g$.

HomotopyEquivstructureMathlib.Algebra.Homology.Homotopy, type

Wording

homotopy equivalence of C and D (from the name)

English

Let $C$ and $D$ be homological complexes of $V$ and $c$. Then the homotopy equivalences of $C$ and $D$ are a basic type.

HomotopyEquiv.copydefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a homotopy equivalence of $C$ and $D$. Let $h$ be a homotopy of the homomorphism of $f$ and $g$. Then the copy of $f$ and $h$ is a homotopy equivalence of $C$ and $D$ defined as $\operatorname{mk}$ applied to $g$, the inverse of $f$, the composition of the right composition of the inverse of $h$ and the inverse of $f$ and the homotopy homomorphism inverse identity of $f$ and the composition of the left composition of the inverse of $h$ and the inverse of $f$ and the homotopy inverse homomorphism identity of $f$.

HomotopyEquiv.homdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homotopy equivalence of $C$ and $D$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $C$ and $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

HomotopyEquiv.homotopyHomInvIddefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

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

English

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

HomotopyEquiv.homotopyInvHomIddefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

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

English

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

HomotopyEquiv.invdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the inverse of self (from the name)

English

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

HomotopyEquiv.ofIsodefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the homotopy equivalence of f (from the name)

English

Let $f$ be an isomorphism of $C$ and $D$. Then the homotopy equivalence of $f$ is a homotopy equivalence of $C$ and $D$.

HomotopyEquiv.refldefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the identity of C (from the name)

English

Let $C$ be a homological complex of $V$ and $c$. Then the identity of $C$ is a homotopy equivalence of $C$ and $C$.

HomotopyEquiv.symmdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the inverse of f (from the name)

English

Let $f$ be a homotopy equivalence of $C$ and $D$. Then the inverse of $f$ is a homotopy equivalence of $D$ and $C$ defined as $\operatorname{mk}$ applied to the inverse of $f$, the homomorphism of $f$, the homotopy inverse homomorphism identity of $f$ and the homotopy homomorphism inverse identity of $f$.

HomotopyEquiv.toHomologyIsodefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the isomorphism in homology induced by a homotopy equivalence of h and i (from the docstring)

English

Let $h$ be a homotopy equivalence of $K$ and $L$. Let $i$ be an element of $x_{2}$. Then the isomorphism in homology induced by a homotopy equivalence of $h$ and $i$ is an isomorphism of the homology of $K$ and $i$ and the homology of $L$ and $i$.

HomotopyEquiv.transdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a homotopy equivalence of $C$ and $D$. Let $g$ be a homotopy equivalence of $D$ and $E$. Then the composition of $f$ and $g$ is a homotopy equivalence of $C$ and $E$.

dNextdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Then $\mathrm{dNext}$ applied to $i$ is an additive monoid homomorphism of the set of functions from elements $i_{1}$ of $x$ and elements $j$ of $x$ to homomorphisms of $\operatorname{X}$ applied to $C$ and $i_{1}$ and $\operatorname{X}$ applied to $D$ and $j$ and the set of homomorphisms of $\operatorname{X}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $D$ and $i$.

fromNextdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Then $\mathrm{fromNext}$ applied to $i$ is an additive monoid homomorphism of the set of functions from elements $i_{1}$ of $x$ and elements $j$ of $x$ to homomorphisms of $\operatorname{X}$ applied to $C$ and $i_{1}$ and $\operatorname{X}$ applied to $D$ and $j$ and the set of homomorphisms of $\operatorname{xNext}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $D$ and $i$.

prevDdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

no wording

English

Let $j$ be an element of $x$. Then $\mathrm{prevD}$ applied to $j$ is an additive monoid homomorphism of the set of functions from elements $i$ of $x$ and elements $j_{1}$ of $x$ to homomorphisms of $\operatorname{X}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $D$ and $j_{1}$ and the set of homomorphisms of $\operatorname{X}$ applied to $C$ and $j$ and $\operatorname{X}$ applied to $D$ and $j$.

toPrevdefMathlib.Algebra.Homology.Homotopy, function or constant

Wording

no wording

English

Let $j$ be an element of $x$. Then $\mathrm{toPrev}$ applied to $j$ is an additive monoid homomorphism of the set of functions from elements $i$ of $x$ and elements $j_{1}$ of $x$ to homomorphisms of $\operatorname{X}$ applied to $C$ and $i$ and $\operatorname{X}$ applied to $D$ and $j_{1}$ and the set of homomorphisms of $\operatorname{X}$ applied to $C$ and $j$ and $\operatorname{xPrev}$ applied to $D$ and $j$.

Mathlib.Algebra.Homology.HomotopyCategory

CategoryTheory.Functor.mapHomotopyCategorydefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the map homotopy category of F and c (from the name)

English

Let $F$ be a functor of $V$ and $W$. Let $c$ be a complex shape of $x$. Then the map homotopy category of $F$ and $c$ is a functor of the set of homotopy categories of $V$ and $c$ and the set of homotopy categories of $W$ and $c$.

CategoryTheory.Functor.mapHomotopyCategoryCompIsodefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the map homotopy category composition isomorphism of e and c (from the name)

English

Let $e$ be an isomorphism of the composition of $F$ and $G$ and $H$. Let $c$ be a complex shape of $x$. Then the map homotopy category composition isomorphism of $e$ and $c$ is an isomorphism of the composition of the map homotopy category of $F$ and $c$ and the map homotopy category of $G$ and $c$ and the map homotopy category of $H$ and $c$ defined as the natural isomorphism lift of $\mathrm{homotopic}$ applied to $V$ and $c$ and the right isomorphism whisker of the map homological complex composition isomorphism of $e$ and $c$ and the quotient of $\mathrm{W'}$ and $c$.

CategoryTheory.Functor.mapHomotopyCategoryFactorsdefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the map homotopy category factor of F and c (from the name)

English

Let $F$ be a functor of $V$ and $W$. Let $c$ be a complex shape of $x$. Then the map homotopy category factor of $F$ and $c$ is an isomorphism of the composition of the quotient of $V$ and $c$ and the map homotopy category of $F$ and $c$ and the composition of the map homological complex of $F$ and $c$ and the quotient of $W$ and $c$.

CategoryTheory.Functor.preimageHomotopydefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the preimage by a fully faithful functor of F and H (from the docstring)

English

generation took over the time limit

CategoryTheory.NatIso.mapHomotopyCategorydefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the map homotopy category of e and c (from the name)

English

Let $e$ be an isomorphism of $F$ and $G$. Let $c$ be a complex shape of $x$. Then the map homotopy category of $e$ and $c$ is an isomorphism of the map homotopy category of $F$ and $c$ and the map homotopy category of $G$ and $c$ defined as the natural isomorphism lift of $\mathrm{homotopic}$ applied to $V$ and $c$ and the right isomorphism whisker of the map homological complex of $e$ and $c$ and the quotient of $W$ and $c$.

CategoryTheory.NatTrans.mapHomotopyCategorydefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the map homotopy category of x5 and c (from the name)

English

Let $x_{5}$ be a homomorphism of $F$ and $G$. Let $c$ be a complex shape of $x$. Then the map homotopy category of $x_{5}$ and $c$ is a homomorphism of the map homotopy category of $F$ and $c$ and the map homotopy category of $G$ and $c$ defined as the natural transformation lift of $\mathrm{homotopic}$ applied to $V$ and $c$ and the right whisker of the map homological complex of $x_{5}$ and $c$ and the quotient of $W$ and $c$.

HomotopyCategorydefMathlib.Algebra.Homology.HomotopyCategory, type

Wording

homotopy category of V and c (from the name)

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Then a homotopy category of $V$ and $c$ is an element of the function that maps $V$ and $c$ to the set of quotients of $\mathrm{homotopic}$ applied to $V$ and $c$.

HomotopyCategory.homologyFunctordefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

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

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then the homology functor of $c$ and $i$ is a functor of the set of homotopy categories of $V$ and $c$ and $V$.

HomotopyCategory.homologyFunctorFactorsdefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

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

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then the homology functor factor of $c$ and $i$ is an isomorphism of the composition of the quotient of $V$ and $c$ and the homology functor of $c$ and $i$ and the homology functor of $c$ and $i$.

HomotopyCategory.homotopyEquivOfIsodefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the homotopy equivalence of i (from the name)

English

Let $i$ be an isomorphism of the action of the quotient of $V$ and $c$ and $C$ and the action of the quotient of $V$ and $c$ and $D$. Then the homotopy equivalence of $i$ is a homotopy equivalence of $C$ and $D$.

HomotopyCategory.homotopyOfEqdefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the homotopy of f and g (from the name)

English

Let $f$ and $g$ be homomorphisms of $C$ and $D$ such that the map of the quotient of $V$ and $c$ and $f$ is equal to the map of the quotient of $V$ and $c$ and $g$. Then the homotopy of $f$ and $g$ is a homotopy of $f$ and $g$.

HomotopyCategory.homotopyOutMapdefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $C$ and $D$. Then $\operatorname{homotopyOutMap}$ applied to $f$ is a homotopy of $\operatorname{out}$ applied to the map of the quotient of $V$ and $c$ and $f$ and $f$.

HomotopyCategory.isoOfHomotopyEquivdefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the isomorphism of f (from the name)

English

Let $f$ be a homotopy equivalence of $C$ and $D$. Then the isomorphism of $f$ is an isomorphism of the action of the quotient of $V$ and $c$ and $C$ and the action of the quotient of $V$ and $c$ and $D$.

HomotopyCategory.quotientdefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

the quotient of V and c (from the name)

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Then the quotient of $V$ and $c$ is a functor of the set of homological complexes of $V$ and $c$ and the set of homotopy categories of $V$ and $c$ defined as the functor of $\mathrm{homotopic}$ applied to $V$ and $c$.

homotopicdefMathlib.Algebra.Homology.HomotopyCategory, function or constant

Wording

no wording

English

Let $V$ be a set. Let $c$ be a complex shape of $x$. Then there is a homomorphism relation of the set of homological complexes of $V$ and $c$. Proof. Let $V$ be arbitrary. Let $c$ be arbitrary. Let $x_{3}$ be arbitrary. Let $x_{4}$ be arbitrary. Let $f$ be arbitrary. Let $g$ be arbitrary. By f. By g. By Homotopy. By Nonempty.

Mathlib.Algebra.Homology.HomotopyCategory.Acyclic

HomotopyCategory.subcategoryAcyclicdefMathlib.Algebra.Homology.HomotopyCategory.Acyclic, function or constant

Wording

the triangulated subcategory of C (from the docstring)

English

Let $C$ be a set. Then the triangulated subcategory of $C$ is an object property of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as the kernel of the homology functor of $\operatorname{up}$ applied to $\Integer$ and $0$.

Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

CochainComplex.cocycleOfDegreewiseSplitdefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

the cocycle of S and x2 (from the name)

English

Let $S$ be a short complex of the set of cochain complexes of $C$ and $\Integer$. Let $x_{2}$ be a function from integers $n$ to splittings of the map of $S$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$. Then the cocycle of $S$ and $n$ is a cocycle of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $1$.

CochainComplex.homOfDegreewiseSplitdefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

the homomorphism of S and x2 (from the name)

English

Let $S$ be a short complex of the set of cochain complexes of $C$ and $\Integer$. Let $x_{2}$ be a function from integers $n$ to splittings of the map of $S$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$. Then the homomorphism of $S$ and $n$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $1$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$.

CochainComplex.mappingCone.triangleRotateIsoTriangleOfDegreewiseSplitdefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

the triangle of x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the triangle of $x_{2}$ is an isomorphism of $\operatorname{rotate}$ applied to the standard triangle of $x_{2}$ and the triangle of $\operatorname{triangleRotateShortComplex}$ applied to $x_{2}$ and $\operatorname{triangleRotateShortComplexSplitting}$ applied to $x_{2}$.

CochainComplex.mappingCone.triangleRotateShortComplexdefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then $\operatorname{triangleRotateShortComplex}$ applied to $x_{2}$ is a short complex of the set of cochain complexes of $C$ and $\Integer$.

CochainComplex.mappingCone.triangleRotateShortComplexSplittingdefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $n$ be an integer. Then $\operatorname{triangleRotateShortComplexSplitting}$ applied to $x_{2}$ and $n$ is a splitting of the map of $\operatorname{triangleRotateShortComplex}$ applied to $x_{2}$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$.

CochainComplex.mappingCone.trianglehRotateIsoTrianglehOfDegreewiseSplitdefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

the triangle of x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the triangle of $x_{2}$ is an isomorphism of $\operatorname{rotate}$ applied to $\operatorname{triangleh}$ applied to $x_{2}$ and $\operatorname{trianglehOfDegreewiseSplit}$ applied to $\operatorname{triangleRotateShortComplex}$ applied to $x_{2}$ and $\operatorname{triangleRotateShortComplexSplitting}$ applied to $x_{2}$ defined as the composition of the application of $\operatorname{mapTriangleRotateIso}$ applied to the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the standard triangle of $x_{2}$ and the map isomorphism of the map triangle of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the triangle of $x_{2}$.

CochainComplex.mappingConeHomOfDegreewiseSplitIsodefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

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

English

Let $S$ be a short complex of the set of cochain complexes of $C$ and $\Integer$. Let $x_{2}$ be a function from integers $n$ to splittings of the map of $S$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$. Then the canonical isomorphism of $S$ and $n$ is an isomorphism of the mapping cone of the homomorphism of $S$ and $x_{2}$ and the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $1$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$.

CochainComplex.mappingConeHomOfDegreewiseSplitXIsodefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

the mapping cone homomorphism of n and p (from the name)

English

Let $S$ be a short complex of the set of cochain complexes of $C$ and $\Integer$. Let $x_{2}$ be a function from integers $n$ to splittings of the map of $S$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$. Let $p$ and $q$ be integers such that $p + 1 = q$. Then the mapping cone homomorphism of $x_{2}$ and $p$ is an isomorphism of $\operatorname{X}$ applied to the mapping cone of the homomorphism of $S$ and $x_{2}$ and $p$ and $\operatorname{X}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $S$ and $q$.

CochainComplex.triangleOfDegreewiseSplitdefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

the triangle of S and x2 (from the name)

English

Let $S$ be a short complex of the set of cochain complexes of $C$ and $\Integer$. Let $x_{2}$ be a function from integers $n$ to splittings of the map of $S$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$. Then the triangle of $S$ and $n$ is a triangle of the set of cochain complexes of $C$ and $\Integer$ defined as the function that maps $x_{2}$ to $\operatorname{mk}$ applied to $\operatorname{f}$ applied to $S$, $\operatorname{g}$ applied to $S$, the homomorphism of $S$ and $n$ and $x_{2}$.

CochainComplex.triangleOfDegreewiseSplitRotateRotateIsodefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

the triangle of S and x2 (from the name)

English

Let $S$ be a short complex of the set of cochain complexes of $C$ and $\Integer$. Let $x_{2}$ be a function from integers $n$ to splittings of the map of $S$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$. Then the triangle of $S$ and $n$ is an isomorphism of $\operatorname{rotate}$ applied to $\operatorname{rotate}$ applied to the triangle of $S$ and $x_{2}$ and the standard triangle of the homomorphism of $S$ and $x_{2}$.

CochainComplex.trianglehOfDegreewiseSplitdefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

no wording

English

CochainComplex.trianglehOfDegreewiseSplitRotateRotateIsodefMathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit, function or constant

Wording

no wording

English

Let $S$ be a short complex of the set of cochain complexes of $C$ and $\Integer$. Let $x_{2}$ be a function from integers $n$ to splittings of the map of $S$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$. Then $\operatorname{trianglehOfDegreewiseSplitRotateRotateIso}$ applied to $S$, $n$ and $x_{2}$ is an isomorphism of $\operatorname{rotate}$ applied to $\operatorname{rotate}$ applied to $\operatorname{trianglehOfDegreewiseSplit}$ applied to $S$ and $x_{2}$ and $\operatorname{triangleh}$ applied to the homomorphism of $S$ and $x_{2}$ defined as the function that maps $x_{2}$ to the composition of the map isomorphism of $\operatorname{rotate}$ applied to the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ and the application of $\operatorname{mapTriangleRotateIso}$ applied to the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the triangle of $S$ and $n$ and the composition of the application of $\operatorname{mapTriangleRotateIso}$ applied to the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the action of $\operatorname{rotate}$ applied to the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and the triangle of $S$ and $n$ and the map isomorphism of the map triangle of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the triangle of $S$ and $n$.

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

CochainComplex.HomComplexdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the homomorphism complex of F and G (from the name)

English

Let $F$ and $G$ be cochain complexes of $C$ and $\Integer$. Then the homomorphism complex of $F$ and $G$ is a cochain complex of the set of additive commutative group categories and $\Integer$.

CochainComplex.HomComplex.CochaindefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, type

Wording

cochain of G and n (from the name)

English

Let $F$ and $G$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then a cochain of $G$ and $n$ is an element of the function that maps $F$, $G$ and $n$ to the set of functions from triplets $T$ of $n$ to homomorphisms of $\operatorname{X}$ applied to $F$ and $\operatorname{p}$ applied to $T$ and $\operatorname{X}$ applied to $G$ and $\operatorname{q}$ applied to $T$.

CochainComplex.HomComplex.Cochain.compdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the composition of x5 and x6 (from the name)

English

Let $x_{5}$ be a cochain of $G$ and $x_{2}$. Let $x_{6}$ be a cochain of $K$ and $x_{3}$. Assume that $x_{2} + x_{3} = x_{4}$. Then the composition of $x_{5}$ and $x_{6}$ is a cochain of $K$ and $x_{4}$.

CochainComplex.HomComplex.Cochain.diffdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the difference of K (from the name)

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Then the difference of $K$ is a cochain of $K$ and $1$ defined as $\operatorname{mk}$ applied to the function that maps $p$, $q$ and $h$ to $\operatorname{d}$ applied to $K$, $p$ and $q$.

CochainComplex.HomComplex.Cochain.equivHomotopydefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the equivalence homotopy of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the equivalence homotopy of $x_{2}$ and $x_{3}$ is an element of $\EquivMACRoAE {\mathrm{Homotopy} (x_{2} , x_{3})}{(\SubtypeSet {z}{(\EqtMACRoH {\operatorname{ofHom} (x_{2})}{(\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_} (\operatorname{neg} (1), 0 , z)+ \operatorname{ofHom} (x_{3}))})})}$.

CochainComplex.HomComplex.Cochain.mapdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the map of z and x4 (from the name)

English

Let $z$ be a cochain of $L$ and $n$. Let $x_{4}$ be a functor of $C$ and $D$. Then the map of $z$ and $x_{4}$ is a cochain of the action of the map homological complex of $x_{4}$ and $\operatorname{up}$ applied to $\Integer$ and $L$ and $n$ defined as $\operatorname{mk}$ applied to the function that maps $p$, $q$ and $\mathrm{hpq}$ to the map of $x_{4}$ and $\operatorname{v}$ applied to $z$, $p$, $q$ and $\mathrm{hpq}$.

CochainComplex.HomComplex.Cochain.mkdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $v$ be a function from integers $p$ and integers $q$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Eq} (p + n , q)$ to homomorphisms of $\operatorname{X}$ applied to $F$ and $p$ and $\operatorname{X}$ applied to $G$ and $q$. Then there is a cochain of $G$ and $n$.

CochainComplex.HomComplex.Cochain.ofHomdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the cochain of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the cochain of $x_{2}$ is a cochain of $G$ and $0$ defined as the cochain of the function that maps $p$ to $\operatorname{f}$ applied to $x_{2}$ and $p$.

CochainComplex.HomComplex.Cochain.ofHomotopydefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the cochain of degree of ho (from the docstring)

English

Let $\mathrm{ho}$ be a homotopy of $x_{2}$ and $x_{3}$. Then the cochain of degree of $\mathrm{ho}$ is a cochain of $G$ and $\operatorname{neg}$ applied to $1$ defined as $\operatorname{mk}$ applied to the function that maps $p$, $q$ and $h$ to the homomorphism of $p$ and $q$.

CochainComplex.HomComplex.Cochain.ofHomsdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the cochain of x2 (from the name)

English

Let $x_{2}$ be a function from integers $p$ to homomorphisms of $\operatorname{X}$ applied to $F$ and $p$ and $\operatorname{X}$ applied to $G$ and $p$. Then the cochain of $p$ is a cochain of $G$ and $0$.

CochainComplex.HomComplex.Cochain.singledefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $K$ and $p$ and $\operatorname{X}$ applied to $L$ and $q$. Let $n$ be an integer. Then there is a cochain of $L$ and $n$.

CochainComplex.HomComplex.Cochain.vdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $x_{2}$ be a cochain of $G$ and $n$. Let $p$ and $q$ be integers such that $p + n = q$. Then $\operatorname{v}$ applied to $x_{2}$, $p$, $q$ and $\mathrm{hpq}$ is a homomorphism of $\operatorname{X}$ applied to $F$ and $p$ and $\operatorname{X}$ applied to $G$ and $q$ defined as $x_{2}$ applied to $\operatorname{mk}$ applied to $p$, $q$ and $\mathrm{hpq}$.

CochainComplex.HomComplex.CocycledefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, type

Wording

cocycle of G and n (from the name)

English

Let $F$ and $G$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an element of $\Integer$. Then a cocycle of $G$ and $n$ is an element of the function that maps $F$, $G$ and $n$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{cocycle} (G , n)}{x_{2}})}$.

CochainComplex.HomComplex.Cocycle.compdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the composition of x2 and x3 (from the name)

English

Let $x_{2}$ be a cocycle of $G$ and $a$. Let $x_{3}$ be a cocycle of $K$ and $b$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (a + b , c)$ and $\mathrm{CochainComplex\_\_HomComplex\_\_Cocycle\_\_comp\_\_\_auto\_1}$. Then the composition of $x_{2}$ and $x_{3}$ is a cocycle of $K$ and $c$.

CochainComplex.HomComplex.Cocycle.diffdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the difference of K (from the name)

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Then the difference of $K$ is a cocycle of $K$ and $1$.

CochainComplex.HomComplex.Cocycle.equivHomdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the equivalence homomorphism of F and G (from the name)

English

Let $F$ and $G$ be cochain complexes of $C$ and $\Integer$. Then the equivalence homomorphism of $F$ and $G$ is an additive equivalence of the set of homomorphisms of $F$ and $G$ and the set of cocycles of $G$ and $0$.

CochainComplex.HomComplex.Cocycle.homOfdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the homomorphism of z (from the name)

English

Let $z$ be a cocycle of $G$ and $0$. Then the homomorphism of $z$ is a homomorphism of $F$ and $G$.

CochainComplex.HomComplex.Cocycle.isKerneldefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ and $m$ be integers such that $n + 1 = m$. Then $\operatorname{isKernel}$ applied to $K$, $L$, $n$, $m$ and $\mathrm{hm}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the additive commutative group category of the cochain additive monoid homomorphism of $L$ and $n$ and $\mathrm{CochainComplex\_\_HomComplex\_\_Cocycle\_\_isKernel\_\_\_proof\_2}$ applied to $K$, $L$, $n$, $m$ and $\mathrm{hm}$.

CochainComplex.HomComplex.Cocycle.isKernel'defMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ and $m$ be integers such that $n + 1 = m$. Then $\operatorname{isKernel'}$ applied to $R$, $K$, $L$, $n$, $m$ and $\mathrm{hm}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the module category of the cochain linear map of $L$ and $n$ and $\mathrm{CochainComplex\_\_HomComplex\_\_Cocycle\_\_isKernel'\_\_\_proof\_2}$ applied to $R$, $K$, $L$, $n$, $m$ and $\mathrm{hm}$.

CochainComplex.HomComplex.Cocycle.mkdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $z$ be a cochain of $G$ and $n$. Let $m$ be an integer such that $n + 1 = m$ and $\EqtMACRoH {\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_} (n , m , z)}{0}$. Then $\operatorname{mk}$ applied to $z$, $m$, $\mathrm{hnm}$ and $h$ is a cocycle of $G$ and $n$ defined as $z$.

CochainComplex.HomComplex.Cocycle.ofHomdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the cocycle of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the cocycle of $x_{2}$ is a cocycle of $G$ and $0$.

CochainComplex.HomComplex.Cocycle.postcompdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the postcomposition of z and f (from the docstring)

English

Let $z$ be a cocycle of $G$ and $n$. Let $f$ be a homomorphism of $G$ and $K$. Then the postcomposition of $z$ and $f$ is a cocycle of $K$ and $n$.

CochainComplex.HomComplex.Cocycle.precompdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the precomposition of z and f (from the docstring)

English

Let $z$ be a cocycle of $K$ and $n$. Let $f$ be a homomorphism of $F$ and $G$. Then the precomposition of $z$ and $f$ is a cocycle of $K$ and $n$.

CochainComplex.HomComplex.Cocycle.toCochainAddMonoidHomdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the cochain additive monoid homomorphism of L and n (from the name)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the cochain additive monoid homomorphism of $L$ and $n$ is an additive monoid homomorphism of the set of cocycles of $L$ and $n$ and the set of cochains of $L$ and $n$.

CochainComplex.HomComplex.Cocycle.toCochainLinearMapdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the cochain linear map of L and n (from the name)

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the cochain linear map of $L$ and $n$ is a linear map of the set of cocycles of $L$ and $n$ and the set of cochains of $L$ and $n$.

CochainComplex.HomComplex.TripletstructureMathlib.Algebra.Homology.HomotopyCategory.HomComplex, type

Wording

triplet of n (from the name)

English

Let $n$ be an integer. Then the triplets of $n$ are a basic type.

CochainComplex.HomComplex.Triplet.pdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a triplet of $n$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is an integer defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CochainComplex.HomComplex.Triplet.qdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a triplet of $n$. Then $\operatorname{q}$ applied to $\mathrm{self}$ is an integer defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CochainComplex.HomComplex.cocycledefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the cocycle of G and n (from the name)

English

Let $F$ and $G$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the cocycle of $G$ and $n$ is an additive subgroup of the set of cochains of $G$ and $n$ defined as the additive kernel of the additive monoid homomorphism of the homomorphism of $n$ and $n + 1$.

CochainComplex.HomComplex.δdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

no wording

English

Let $n$ and $m$ be integers. Let $z$ be a cochain of $G$ and $n$. Then there is a cochain of $G$ and $m$.

CochainComplex.HomComplex.δ_homdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the homomorphism of n and m (from the name)

English

Let $R$ be a set. Let $F$ and $G$ be cochain complexes of $C$ and $\Integer$. Let $n$ and $m$ be integers. Then the homomorphism of $n$ and $m$ is a linear map of the set of cochains of $G$ and $n$ and the set of cochains of $G$ and $m$.

CochainComplex.linearHomComplexdefMathlib.Algebra.Homology.HomotopyCategory.HomComplex, function or constant

Wording

the linear homomorphism complex of F and G (from the name)

English

Let $R$ be a set. Let $F$ and $G$ be cochain complexes of $C$ and $\Integer$. Then the linear homomorphism complex of $F$ and $G$ is a cochain complex of the set of module categories of $R$ and $\Integer$.

Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

CochainComplex.HomComplex.CohomologyClassdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, type

Wording

cohomology class of L and n (from the name)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then a cohomology class of $L$ and $n$ is an element of the function that maps $K$, $L$ and $n$ to the set of quotients of the set of cocycles of $L$ and $n$ and $\operatorname{coboundaries}$ applied to $K$, $L$ and $n$.

CochainComplex.HomComplex.CohomologyClass.descAddMonoidHomdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

no wording

English

Let $f$ be an additive monoid homomorphism of the set of cocycles of $L$ and $n$ and $G$ such that $\operatorname{coboundaries}$ applied to $K$, $L$ and $n$ is less than or equal to the additive kernel of $f$. Then $\operatorname{descAddMonoidHom}$ applied to $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of the set of cohomology classes of $L$ and $n$ and $G$ defined as the lift of $\operatorname{coboundaries}$ applied to $K$, $L$ and $n$ and $f$.

CochainComplex.HomComplex.CohomologyClass.homAddEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the homomorphism additive equivalence (from the name)

English

The homomorphism additive equivalence is an additive equivalence of the set of cohomology classes of $L$ and $n$ and the set of homomorphisms of the action of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and $K$ and the action of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the action of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $n$ and $L$ defined as the additive equivalence of the homomorphism and $\mathrm{CochainComplex\_\_HomComplex\_\_CohomologyClass\_\_toHom\_bijective}$ applied to $K$, $L$ and $n$.

CochainComplex.HomComplex.CohomologyClass.mkdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

no wording

English

Let $x_{2}$ be a cocycle of $L$ and $n$. Then $\operatorname{mk}$ applied to $x_{2}$ is a cohomology class of $L$ and $n$ defined as $\operatorname{mk}$ applied to $\operatorname{leftRel}$ applied to $\operatorname{coboundaries}$ applied to $K$, $L$ and $n$ and $x_{2}$.

CochainComplex.HomComplex.CohomologyClass.mkAddMonoidHomdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the additive monoid homomorphism of L and n (from the name)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the additive monoid homomorphism of $L$ and $n$ is an additive monoid homomorphism of the set of cocycles of $L$ and $n$ and the set of cohomology classes of $L$ and $n$.

CochainComplex.HomComplex.CohomologyClass.mkLinearMapdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the linear map of L and n (from the name)

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the linear map of $L$ and $n$ is a linear map of the set of cocycles of $L$ and $n$ and the set of cohomology classes of $L$ and $n$.

CochainComplex.HomComplex.CohomologyClass.toHomdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the homomorphism (from the name)

English

The homomorphism is an additive monoid homomorphism of the set of cohomology classes of $L$ and $n$ and the set of homomorphisms of the action of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and $K$ and the action of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the action of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $n$ and $L$.

CochainComplex.HomComplex.coboundariesdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

no wording

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{coboundaries}$ applied to $K$, $L$ and $n$ is an additive subgroup of the set of cocycles of $L$ and $n$.

CochainComplex.HomComplex.homologyAddEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the homology of K (from the docstring)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the homology of $K$ is an additive equivalence of the set of carriers of the homology of the homomorphism complex of $K$ and $L$ and $n$ and the set of cohomology classes of $L$ and $n$ defined as the additive commutative group isomorphism to additive equivalence of the homology isomorphism of the left homology data of $L$ and $n$.

CochainComplex.HomComplex.homologyLinearEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the homology of R (from the docstring)

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the homology of $R$ is a linear equivalence of the set of carriers of the homology of the linear homomorphism complex of $K$ and $L$ and $n$ and the set of cohomology classes of $L$ and $n$ defined as the linear equivalence of the homology isomorphism of the linear left homology data of $L$ and $n$.

CochainComplex.HomComplex.leftHomologyDatadefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the left homology data of L and n (from the name)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the left homology data of $L$ and $n$ is a left homology data of $\operatorname{sc}$ applied to the homomorphism complex of $K$ and $L$ and $n$.

CochainComplex.HomComplex.leftHomologyData'defMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the left homology data of m and p (from the name)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$, $m$ and $p$ be integers such that $n + 1 = m$ and $m + 1 = p$. Then the left homology data of $m$ and $p$ is a left homology data of $\operatorname{sc'}$ applied to the homomorphism complex of $K$ and $L$, $n$, $m$ and $p$.

CochainComplex.HomComplex.linearLeftHomologyDatadefMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the linear left homology data of L and n (from the name)

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ be an integer. Then the linear left homology data of $L$ and $n$ is a left homology data of $\operatorname{sc}$ applied to the linear homomorphism complex of $K$ and $L$ and $n$.

CochainComplex.HomComplex.linearLeftHomologyData'defMathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology, function or constant

Wording

the linear left homology data of m and p (from the name)

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$, $m$ and $p$ be integers such that $n + 1 = m$ and $m + 1 = p$. Then the linear left homology data of $m$ and $p$ is a left homology data of $\operatorname{sc'}$ applied to the linear homomorphism complex of $K$ and $L$, $n$, $m$ and $p$.

Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

CochainComplex.HomComplex.Cochain.EqUpTodefMathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction, predicate

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be cochains of $L$ and $n$. Let $x_{4}$ be an integer. Then $\operatorname{EqUpTo}$ holds for $x_{2}$, $x_{3}$ and $x_{4}$, if for all integers $p$ and $q$, for all elements $\mathrm{hpq}$ of $\mathrm{Proof}$ applied to $\mathrm{Eq} (p + n , q)$, if $p \leq x_{4}$, then $\EqtMACRoH {\operatorname{v} (x_{2} , p , q , \mathrm{hpq})}{\operatorname{v} (x_{3} , p , q , \mathrm{hpq})}$.

CochainComplex.HomComplex.Cochain.InductionUp.limitSequencedefMathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction, function or constant

Wording

the limit sequence of x2 and h (from the name)

English

Let $x_{2}$ be a function from natural numbers $n_{1}$ and elements of $X$ applied to $n_{1}$ to elements of $X$ applied to $n_{1} + 1$ such that for all natural numbers $n$, for all elements $x_{5}$ of $X$ applied to $n$, $\operatorname{EqUpTo}$ holds for $x_{2}$ applied to $n$ and $x_{5}$, $x_{5}$ and $x_{3} + n$. Let $x_{4}$ be an element of $X$ applied to $0$. Then the limit sequence of $n_{1}$ and $h$ is a cochain of $L$ and $d$ defined as the function that maps $x_{4}$ to $\operatorname{mk}$ applied to the function that maps $p$, $q$ and $\mathrm{hpq}$ to $\operatorname{v}$ applied to the sequence of $h$ and $\operatorname{toNat}$ applied to $p - x_{3}$, $p$, $q$ and $\mathrm{hpq}$ and $x_{4}$.

CochainComplex.HomComplex.Cochain.InductionUp.sequencedefMathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction, function or constant

Wording

the sequence of n1 and x3 (from the name)

English

Let $x_{2}$ be a function from natural numbers $n_{1}$ and elements of $X$ applied to $n_{1}$ to elements of $X$ applied to $n_{1} + 1$. Let $x_{3}$ be an element of $X$ applied to $0$. Let $n$ be a natural number. Then the sequence of $x_{2}$ and $x_{3}$ is an element of $X$ applied to $n$ defined as the function that maps $n$ to $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{CochainComplex\_\_HomComplex\_\_Cochain\_\_InductionUp\_\_sequence\_\_\_f}$ applied to $n_{1}$ and $x_{2}$ and $n$.

Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

CochainComplex.HomComplex.Cochain.leftShiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the left shift of a and #3 (from the name)

English

Let $x_{2}$ be a cochain of $L$ and $n$. Let $a$ and $\mathrm{n'}$ be integers such that $n + a = \mathrm{n'}$. Then the left shift of $a$ and $\mathrm{n'}$ is a cochain of $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cochain.leftShiftAddEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the left shift additive equivalence of a and #5 (from the name)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$, $a$ and $\mathrm{n'}$ be integers such that $n + a = \mathrm{n'}$. Then the left shift additive equivalence of $a$ and $\mathrm{n'}$ is an additive equivalence of the set of cochains of $L$ and $n$ and the set of cochains of $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cochain.leftShiftLinearEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the left shift linear equivalence of a and hn (from the name)

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$, $a$ and $\mathrm{n'}$ be integers such that $n + a = \mathrm{n'}$. Then the left shift linear equivalence of $a$ and $\mathrm{n'}$ is a linear equivalence of the set of cochains of $L$ and $n$ and the set of cochains of $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cochain.leftUnshiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

no wording

English

Let $x_{2}$ be a cochain of $L$ and $\mathrm{n'}$. Let $n$ be an integer such that $n + a = \mathrm{n'}$. Then there is a cochain of $L$ and $n$.

CochainComplex.HomComplex.Cochain.rightShiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the right shift of a and #3 (from the name)

English

Let $x_{2}$ be a cochain of $L$ and $n$. Let $a$ and $\mathrm{n'}$ be integers such that $\mathrm{n'} + a = n$. Then the right shift of $a$ and $\mathrm{n'}$ is a cochain of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cochain.rightShiftAddEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the right shift additive equivalence of a and #5 (from the name)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$, $a$ and $\mathrm{n'}$ be integers such that $\mathrm{n'} + a = n$. Then the right shift additive equivalence of $a$ and $\mathrm{n'}$ is an additive equivalence of the set of cochains of $L$ and $n$ and the set of cochains of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cochain.rightShiftLinearEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the right shift linear equivalence of a and #6 (from the name)

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$, $a$ and $\mathrm{n'}$ be integers such that $\mathrm{n'} + a = n$. Then the right shift linear equivalence of $a$ and $\mathrm{n'}$ is a linear equivalence of the set of cochains of $L$ and $n$ and the set of cochains of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cochain.rightUnshiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

no wording

English

Let $x_{2}$ be a cochain of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $\mathrm{n'}$. Let $n$ be an integer such that $\mathrm{n'} + a = n$. Then there is a cochain of $L$ and $n$.

CochainComplex.HomComplex.Cochain.shiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the shift of x2 and a (from the name)

English

Let $x_{2}$ be a cochain of $L$ and $n$. Let $a$ be an integer. Then the shift of $x_{2}$ and $a$ is a cochain of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $n$.

CochainComplex.HomComplex.Cochain.shiftAddHomdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the shift additive homomorphism of n and a (from the name)

English

Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ and $a$ be integers. Then the shift additive homomorphism of $n$ and $a$ is an additive monoid homomorphism of the set of cochains of $L$ and $n$ and the set of cochains of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $n$.

CochainComplex.HomComplex.Cochain.shiftLinearMapdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the shift linear map of n and a (from the name)

English

Let $R$ be a set. Let $K$ and $L$ be cochain complexes of $C$ and $\Integer$. Let $n$ and $a$ be integers. Then the shift linear map of $n$ and $a$ is a linear map of the set of cochains of $L$ and $n$ and the set of cochains of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $n$.

CochainComplex.HomComplex.Cocycle.equivHomShiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the additive equivalence (from the docstring)

English

The additive equivalence is an additive equivalence of the set of homomorphisms of $K$ and the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and $L$ and the set of cocycles of $L$ and $n$.

CochainComplex.HomComplex.Cocycle.equivHomShift'defMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the equivalence homomorphism shift of n and m (from the name)

English

Let $n$ and $m$ be integers such that $m + n = 0$. Then the equivalence homomorphism shift of $n$ and $m$ is an additive equivalence of the set of homomorphisms of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and $K$ and $L$ and the set of cocycles of $L$ and $m$ defined as the composition of the equivalence homomorphism of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and $K$ and $L$ and the inverse of the left shift additive equivalence of $n$ and $0$.

CochainComplex.HomComplex.Cocycle.leftShiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the left shift of a and #3 (from the name)

English

Let $x_{2}$ be a cocycle of $L$ and $n$. Let $a$ and $\mathrm{n'}$ be integers such that $n + a = \mathrm{n'}$. Then the left shift of $a$ and $\mathrm{n'}$ is a cocycle of $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cocycle.leftShiftAddEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the left shift additive equivalence of a and #3 (from the name)

English

Let $n$, $a$ and $\mathrm{n'}$ be integers such that $n + a = \mathrm{n'}$. Then the left shift additive equivalence of $a$ and $\mathrm{n'}$ is an additive equivalence of the set of cocycles of $L$ and $n$ and the set of cocycles of $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cocycle.leftUnshiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

no wording

English

Let $x_{2}$ be a cocycle of $L$ and $\mathrm{n'}$. Let $n$ be an integer such that $n + a = \mathrm{n'}$. Then $\operatorname{leftUnshift}$ applied to $x_{2}$, $n$ and $\mathrm{hn}$ is a cocycle of $L$ and $n$.

CochainComplex.HomComplex.Cocycle.rightShiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the right shift of a and #3 (from the name)

English

Let $x_{2}$ be a cocycle of $L$ and $n$. Let $a$ and $\mathrm{n'}$ be integers such that $\mathrm{n'} + a = n$. Then the right shift of $a$ and $\mathrm{n'}$ is a cocycle of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cocycle.rightShiftAddEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the right shift additive equivalence of a and #3 (from the name)

English

Let $n$, $a$ and $\mathrm{n'}$ be integers such that $\mathrm{n'} + a = n$. Then the right shift additive equivalence of $a$ and $\mathrm{n'}$ is an additive equivalence of the set of cocycles of $L$ and $n$ and the set of cocycles of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $\mathrm{n'}$.

CochainComplex.HomComplex.Cocycle.rightUnshiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

no wording

English

Let $x_{2}$ be a cocycle of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $\mathrm{n'}$. Let $n$ be an integer such that $\mathrm{n'} + a = n$. Then $\operatorname{rightUnshift}$ applied to $x_{2}$, $n$ and $\mathrm{hn}$ is a cocycle of $L$ and $n$.

CochainComplex.HomComplex.Cocycle.shiftdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexShift, function or constant

Wording

the shift of x2 and a (from the name)

English

Let $x_{2}$ be a cocycle of $L$ and $n$. Let $a$ be an integer. Then the shift of $x_{2}$ and $a$ is a cocycle of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $a$ and $L$ and $n$.

Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

CochainComplex.HomComplex.Cochain.fromSingleEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle, function or constant

Wording

no wording

English

Assume that $p + n = q$. Then $\operatorname{fromSingleEquiv}$ applied to $h_{1}$ is an additive equivalence of the set of cochains of $K$ and $n$ and the set of homomorphisms of $X$ and $\operatorname{X}$ applied to $K$ and $q$.

CochainComplex.HomComplex.Cochain.fromSingleLinearEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle, function or constant

Wording

no wording

English

Assume that $p + n = q$. Then $\operatorname{fromSingleLinearEquiv}$ applied to $h_{1}$ is a linear equivalence of the set of cochains of $K$ and $n$ and the set of homomorphisms of $X$ and $\operatorname{X}$ applied to $K$ and $q$.

CochainComplex.HomComplex.Cochain.fromSingleMkdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $\operatorname{X}$ applied to $K$ and $q$. Assume that $p + n = q$. Then there is a cochain of $K$ and $n$. Proof. Let $f$ be arbitrary. Let $h_{1}$ be arbitrary. By p. By X. By HomologicalComplex__singleObjXSelf. By CategoryTheory__Iso__hom. By f. By CategoryTheory__CategoryStruct__comp. By n. By CochainComplex__HomComplex__Cochain__single.

CochainComplex.HomComplex.Cochain.toSingleEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle, function or constant

Wording

the single equivalence of h1 (from the name)

English

Assume that $p + n = q$. Then the single equivalence of $h_{1}$ is an additive equivalence of the set of cochains of the action of the single functor of $C$ and $q$ and $X$ and $n$ and the set of homomorphisms of $\operatorname{X}$ applied to $K$ and $p$ and $X$.

CochainComplex.HomComplex.Cochain.toSingleLinearEquivdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle, function or constant

Wording

the single linear equivalence of h1 (from the name)

English

Assume that $p + n = q$. Then the single linear equivalence of $h_{1}$ is a linear equivalence of the set of cochains of the action of the single functor of $C$ and $q$ and $X$ and $n$ and the set of homomorphisms of $\operatorname{X}$ applied to $K$ and $p$ and $X$.

CochainComplex.HomComplex.Cochain.toSingleMkdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $K$ and $p$ and $X$. Assume that $p + n = q$. Then there is a cochain of the action of the single functor of $C$ and $q$ and $X$ and $n$. Proof. Let $f$ be arbitrary. Let $h_{1}$ be arbitrary. By f. By q. By X. By HomologicalComplex__singleObjXSelf. By CategoryTheory__Iso__inv. By CategoryTheory__CategoryStruct__comp. By n. By CochainComplex__HomComplex__Cochain__single.

CochainComplex.HomComplex.Cocycle.fromSingleMkdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $\operatorname{X}$ applied to $K$ and $q$. Assume that $p + n = q$. Let $\mathrm{q'}$ be an integer such that $q + 1 = \mathrm{q'}$ and the composition of $f$ and $\operatorname{d}$ applied to $K$, $q$ and $\mathrm{q'}$ is equal to $0$. Then $\operatorname{fromSingleMk}$ applied to $f$, $h_{1}$, $\mathrm{q'}$, $\mathrm{hq'}$ and $\mathrm{hf}$ is a cocycle of $K$ and $n$.

CochainComplex.HomComplex.Cocycle.toSingleMkdefMathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $K$ and $p$ and $X$. Assume that $p + n = q$. Let $\mathrm{p'}$ be an integer such that $\mathrm{p'} + 1 = p$ and the composition of $\operatorname{d}$ applied to $K$, $\mathrm{p'}$ and $p$ and $f$ is equal to $0$. Then $\operatorname{toSingleMk}$ applied to $f$, $h_{1}$, $\mathrm{p'}$, $\mathrm{hp'}$ and $\mathrm{hf}$ is a cocycle of the action of the single functor of $C$ and $q$ and $X$ and $n$.

Mathlib.Algebra.Homology.HomotopyCategory.KInjective

CochainComplex.IsKInjectiveclassMathlib.Algebra.Homology.HomotopyCategory.KInjective, predicate

Wording

L is injective (from the name)

English

Let $L$ be a cochain complex of $C$ and $\Integer$. Then we can say that $L$ is injective.

CochainComplex.IsKInjective.homotopyZerodefMathlib.Algebra.Homology.HomotopyCategory.KInjective, function or constant

Wording

the homotopy zero of f and hK (from the name)

English

Let $f$ be a homomorphism of $K$ and $L$. Assume that $K$ is acyclic. Then the homotopy zero of $f$ and $\mathrm{hK}$ is a homotopy of $f$ and $0$ defined as $\operatorname{proj0}$ applied to $\mathrm{CochainComplex\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_Homology\_\_HomotopyCategory\_\_KInjective\_\_2101789899\_\_\_hygCtx\_\_\_hyg\_\_2}$, $f$ and $\mathrm{hK}$.

Mathlib.Algebra.Homology.HomotopyCategory.KProjective

CochainComplex.IsKProjectiveclassMathlib.Algebra.Homology.HomotopyCategory.KProjective, predicate

Wording

K is projective (from the name)

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Then we can say that $K$ is projective.

CochainComplex.IsKProjective.homotopyZerodefMathlib.Algebra.Homology.HomotopyCategory.KProjective, function or constant

Wording

the homotopy zero of f and hL (from the name)

English

Let $f$ be a homomorphism of $K$ and $L$. Assume that $L$ is acyclic. Then the homotopy zero of $f$ and $\mathrm{hL}$ is a homotopy of $f$ and $0$ defined as $\operatorname{proj0}$ applied to $\mathrm{CochainComplex\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Algebra\_\_Homology\_\_HomotopyCategory\_\_KProjective\_\_595972877\_\_\_hygCtx\_\_\_hyg\_\_2}$, $f$ and $\mathrm{hL}$.

Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

CochainComplex.mappingCoconedefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the mapping cocone of x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the mapping cocone of $x_{2}$ is a cochain complex of $C$ and $\Integer$ defined as the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $\operatorname{neg}$ applied to $1$ and the mapping cone of $x_{2}$.

CochainComplex.mappingCocone.descdefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $x_{3}$ be a cochain of $M$ and $0$. Let $x_{4}$ be a cocycle of $M$ and $1$ such that the sum of $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $0$, $1$ and $x_{3}$ and the composition of the cochain of $x_{2}$ and $x_{4}$ is equal to $0$. Then $\operatorname{desc}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and $h_{1}$ is a homomorphism of the mapping cocone of $x_{2}$ and $M$.

CochainComplex.mappingCocone.descCochaindefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $x_{3}$ be a cochain of $M$ and $m$. Let $x_{4}$ be a cochain of $M$ and $n$. Assume that $m + 1 = n$. Then there is a cochain of $M$ and $m$.

CochainComplex.mappingCocone.descCocycledefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $x_{3}$ be a cochain of $M$ and $m$. Let $x_{4}$ be a cocycle of $M$ and $n$. Assume that $m + 1 = n$. Assume that $\EqtMACRoH {\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_} (m , n , x_{3})+ \HSMulhSMulMACRoAL {\operatorname{negOnePow} (m)}{\operatorname{comp} (\operatorname{ofHom} (x_{2}), x_{4})}}{0}$. Then $\operatorname{descCocycle}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $h_{1}$ and $h_{2}$ is a cocycle of $M$ and $m$ defined as $\operatorname{descCochain}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and $h_{1}$.

CochainComplex.mappingCocone.fstdefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the first projection of x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the first projection of $x_{2}$ is a homomorphism of the mapping cocone of $x_{2}$ and $K$.

CochainComplex.mappingCocone.inldefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the left inclusion in x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the left inclusion in $x_{2}$ is a cochain of the mapping cocone of $x_{2}$ and $0$.

CochainComplex.mappingCocone.inrdefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the right inclusion in x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the right inclusion in $x_{2}$ is a cocycle of the mapping cocone of $x_{2}$ and $1$.

CochainComplex.mappingCocone.liftdefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the lift of x3 and x4 (from the name)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $x_{3}$ be a homomorphism of $M$ and $K$. Let $x_{4}$ be a cochain of $L$ and $\operatorname{neg}$ applied to $1$ such that the sum of $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $\operatorname{neg}$ applied to $1$, $0$ and $x_{4}$ and the cochain of the composition of $x_{3}$ and $x_{2}$ is equal to $0$. Then the lift of $x_{3}$ and $x_{4}$ is a homomorphism of $M$ and the mapping cocone of $x_{2}$.

CochainComplex.mappingCocone.liftCochaindefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the lift cochain of x3 and x4 (from the name)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $x_{3}$ be a cochain of $K$ and $n$. Let $x_{4}$ be a cochain of $L$ and $m$. Assume that $m + 1 = n$. Then the lift cochain of $x_{3}$ and $x_{4}$ is a cochain of the mapping cocone of $x_{2}$ and $n$.

CochainComplex.mappingCocone.liftCocycledefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the lift cocycle of x3 and x4 (from the name)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $x_{3}$ be a cocycle of $K$ and $n$. Let $x_{4}$ be a cochain of $L$ and $m$. Assume that $m + 1 = n$. Assume that the sum of $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $m$, $n$ and $x_{4}$ and the composition of $x_{3}$ and the cochain of $x_{2}$ is equal to $0$. Then the lift cocycle of $x_{3}$ and $x_{4}$ is a cocycle of the mapping cocone of $x_{2}$ and $n$ defined as the lift cochain of $x_{3}$ and $x_{4}$.

CochainComplex.mappingCocone.rotateTriangleIsodefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then $\operatorname{rotateTriangleIso}$ applied to $x_{2}$ is an isomorphism of $\operatorname{rotate}$ applied to the triangle of $x_{2}$ and the standard triangle of $x_{2}$.

CochainComplex.mappingCocone.snddefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the second projection in x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the second projection in $x_{2}$ is a cochain of $L$ and $\operatorname{neg}$ applied to $1$.

CochainComplex.mappingCocone.triangledefMathlib.Algebra.Homology.HomotopyCategory.MappingCocone, function or constant

Wording

the triangle of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the triangle of $x_{2}$ is a triangle of the set of cochain complexes of $C$ and $\Integer$.

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

CochainComplex.mappingConedefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the mapping cone of x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the mapping cone of $x_{2}$ is a cochain complex of $C$ and $\Integer$ defined as the homotopy cofiber of $x_{2}$.

CochainComplex.mappingCone.descdefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a cochain of $K$ and $\operatorname{neg}$ applied to $1$. Let $x_{4}$ be a homomorphism of $G$ and $K$ such that $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $\operatorname{neg}$ applied to $1$, $0$ and $x_{3}$ is equal to the cochain of the composition of $x_{2}$ and $x_{4}$. Then $\operatorname{desc}$ applied to $x_{2}$, $x_{3}$, $x_{4}$ and $\mathrm{eq}$ is a homomorphism of the mapping cone of $x_{2}$ and $K$.

CochainComplex.mappingCone.descCochaindefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a cochain of $K$ and $m$. Let $x_{4}$ be a cochain of $K$ and $n$. Assume that $m + 1 = n$. Then there is a cochain of $K$ and $n$.

CochainComplex.mappingCone.descCocycledefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a cochain of $K$ and $m$. Let $x_{4}$ be a cocycle of $K$ and $n$. Assume that $m + 1 = n$. Assume that $\EqtMACRoH {\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_} (m , n , x_{3})}{\HSMulhSMulMACRoAL {\operatorname{negOnePow} (n)}{\operatorname{comp} (\operatorname{ofHom} (x_{2}), x_{4})}}$. Then $\operatorname{descCocycle}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $h_{1}$ and $\mathrm{eq}$ is a cocycle of $K$ and $n$.

CochainComplex.mappingCone.descHomotopydefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ and $x_{4}$ be homomorphisms of the mapping cone of $x_{2}$ and $K$. Let $x_{5}$ be a cochain of $K$ and $\operatorname{neg}$ applied to $2$. Let $x_{6}$ be a cochain of $K$ and $\operatorname{neg}$ applied to $1$ such that the composition of the left injection of $x_{2}$ and the cochain of $x_{3}$ is equal to the sum of the sum of $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $\operatorname{neg}$ applied to $2$, $\operatorname{neg}$ applied to $1$ and $x_{5}$ and the composition of the cochain of $x_{2}$ and $x_{6}$ and the composition of the left injection of $x_{2}$ and the cochain of $x_{4}$ and the cochain of the composition of the right inclusion in the mapping cone of $x_{2}$ and $x_{3}$ is equal to the sum of $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $\operatorname{neg}$ applied to $1$, $0$ and $x_{6}$ and the cochain of the composition of the right inclusion in the mapping cone of $x_{2}$ and $x_{4}$. Then $\operatorname{descHomotopy}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $h_{1}$ and $h_{2}$ is a homotopy of $x_{3}$ and $x_{4}$.

CochainComplex.mappingCone.fstdefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the first component of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the first component of $x_{2}$ is a cocycle of $F$ and $1$.

CochainComplex.mappingCone.inldefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the left injection of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the left injection of $x_{2}$ is a cochain of the mapping cone of $x_{2}$ and $\operatorname{neg}$ applied to $1$.

CochainComplex.mappingCone.inrdefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the right inclusion in the mapping cone of x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the right inclusion in the mapping cone of $x_{2}$ is a homomorphism of $G$ and the mapping cone of $x_{2}$ defined as the right inclusion of $x_{2}$.

CochainComplex.mappingCone.liftdefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the lift of x3 and x4 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a cocycle of $F$ and $1$. Let $x_{4}$ be a cochain of $G$ and $0$ such that the sum of $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $0$, $1$ and $x_{4}$ and the composition of $x_{3}$ and the cochain of $x_{2}$ is equal to $0$. Then the lift of $x_{3}$ and $x_{4}$ is a homomorphism of $K$ and the mapping cone of $x_{2}$.

CochainComplex.mappingCone.liftCochaindefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the lift cochain of x3 and x4 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a cochain of $F$ and $m$. Let $x_{4}$ be a cochain of $G$ and $n$. Assume that $n + 1 = m$. Then the lift cochain of $x_{3}$ and $x_{4}$ is a cochain of the mapping cone of $x_{2}$ and $n$.

CochainComplex.mappingCone.liftCocycledefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the lift cocycle of x3 and x4 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a cocycle of $F$ and $m$. Let $x_{4}$ be a cochain of $G$ and $n$. Assume that $n + 1 = m$. Assume that the sum of $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $n$, $m$ and $x_{4}$ and the composition of $x_{3}$ and the cochain of $x_{2}$ is equal to $0$. Then the lift cocycle of $x_{3}$ and $x_{4}$ is a cocycle of the mapping cone of $x_{2}$ and $n$.

CochainComplex.mappingCone.liftHomotopydefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

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

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ and $x_{4}$ be homomorphisms of $K$ and the mapping cone of $x_{2}$. Let $x_{5}$ be a cochain of $F$ and $0$. Let $x_{6}$ be a cochain of $G$ and $\operatorname{neg}$ applied to $1$. Assume that the composition of the cochain of $x_{3}$ and the first component of $x_{2}$ is equal to the sum of $\operatorname{neg}$ applied to $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $0$, $1$ and $x_{5}$ and the composition of the cochain of $x_{4}$ and the first component of $x_{2}$. Assume that the composition of the cochain of $x_{3}$ and the second component of $x_{2}$ is equal to the sum of $\mathrm{CochainComplex\_\_HomComplex\_\_\_u3b4\_}$ applied to $\operatorname{neg}$ applied to $1$, $0$ and $x_{6}$, the composition of $x_{5}$ and the cochain of $x_{2}$ and the composition of the cochain of $x_{4}$ and the second component of $x_{2}$. Then the lift homotopy of $x_{5}$ and $x_{6}$ is a homotopy of $x_{3}$ and $x_{4}$.

CochainComplex.mappingCone.mapHomologicalComplexIsodefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

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

English

Let $x_{4}$ be a homomorphism of $F$ and $G$. Let $H$ be a functor of $C$ and $D$. Then the map homological complex isomorphism of $x_{4}$ and $H$ is an isomorphism of the action of the map homological complex of $H$ and $\operatorname{up}$ applied to $\Integer$ and the mapping cone of $x_{4}$ and the mapping cone of the map of the map homological complex of $H$ and $\operatorname{up}$ applied to $\Integer$ and $x_{4}$.

CochainComplex.mappingCone.mapHomologicalComplexXIsodefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

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

English

Let $x_{4}$ be a homomorphism of $F$ and $G$. Let $H$ be a functor of $C$ and $D$. Let $n$ be an integer. Then the map homological complex isomorphism of $H$ and $n$ is an isomorphism of $\operatorname{X}$ applied to the action of the map homological complex of $H$ and $\operatorname{up}$ applied to $\Integer$ and the mapping cone of $x_{4}$ and $n$ and $\operatorname{X}$ applied to the mapping cone of the map of the map homological complex of $H$ and $\operatorname{up}$ applied to $\Integer$ and $x_{4}$ and $n$.

CochainComplex.mappingCone.mapHomologicalComplexXIso'defMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the map homological complex isomorphism of n and m (from the name)

English

Let $x_{4}$ be a homomorphism of $F$ and $G$. Let $H$ be a functor of $C$ and $D$. Let $n$ and $m$ be integers such that $n + 1 = m$. Then the map homological complex isomorphism of $n$ and $m$ is an isomorphism of $\operatorname{X}$ applied to the action of the map homological complex of $H$ and $\operatorname{up}$ applied to $\Integer$ and the mapping cone of $x_{4}$ and $n$ and $\operatorname{X}$ applied to the mapping cone of the map of the map homological complex of $H$ and $\operatorname{up}$ applied to $\Integer$ and $x_{4}$ and $n$.

CochainComplex.mappingCone.snddefMathlib.Algebra.Homology.HomotopyCategory.MappingCone, function or constant

Wording

the second component of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the second component of $x_{2}$ is a cochain of $G$ and $0$ defined as the cochain of $\operatorname{sndX}$ applied to $x_{2}$.

Mathlib.Algebra.Homology.HomotopyCategory.Plus

CategoryTheory.Functor.mapHomotopyCategoryPlusdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the map homotopy category plus of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the map homotopy category plus of $F$ is a functor of the set of pluses of $C$ and the set of pluses of $D$.

CategoryTheory.Functor.mapHomotopyCategoryPlusCompIsodefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the map homotopy category plus composition isomorphism of e (from the name)

English

Let $e$ be an isomorphism of the composition of $F$ and $G$ and $H$. Then the map homotopy category plus composition isomorphism of $e$ is an isomorphism of the composition of the map homotopy category plus of $F$ and the map homotopy category plus of $G$ and the map homotopy category plus of $H$ defined as the unique isomorphism of the right whiskering of the inclusion of the plus of $E$ and the set of pluses of $C$ and the left isomorphism whisker of the inclusion of $C$ and the map homotopy category composition isomorphism of $e$ and $\operatorname{up}$ applied to $\Integer$.

CategoryTheory.Functor.mapHomotopyCategoryPlusCompιdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the map homotopy category plus composition inclusion of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the map homotopy category plus composition inclusion of $F$ is an isomorphism of the composition of the map homotopy category plus of $F$ and the inclusion of $D$ and the composition of the inclusion of $C$ and the map homotopy category of $F$ and $\operatorname{up}$ applied to $\Integer$ defined as the identity of the composition of the map homotopy category plus of $F$ and the inclusion of $D$.

CategoryTheory.Functor.quotientCompMapHomotopyCategoryPlusIsodefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the quotient composition map homotopy category plus isomorphism of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the quotient composition map homotopy category plus isomorphism of $F$ is an isomorphism of the composition of the quotient of $C$ and the map homotopy category plus of $F$ and the composition of the map cochain complex plus of $F$ and the quotient of $D$ defined as the identity of the composition of the quotient of $C$ and the map homotopy category plus of $F$.

CategoryTheory.NatTrans.mapHomotopyCategoryPlusdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the map homotopy category plus of x6 (from the name)

English

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{5}$. Then the map homotopy category plus of $x_{6}$ is a homomorphism of the map homotopy category plus of $x_{4}$ and the map homotopy category plus of $x_{5}$.

CochainComplex.Plus.precylinderdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the precylinder of K (from the name)

English

Let $K$ be a plus of $C$. Then the precylinder of $K$ is a precylinder of $K$.

CochainComplex.Plus.prepathObjectdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

no wording

English

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

HomotopyCategory.PlusdefMathlib.Algebra.Homology.HomotopyCategory.Plus, type

Wording

plus of C (from the name)

English

Let $C$ be a set. Then a plus of $C$ is an element of the function that maps $C$ to the set of full subcategories of the plus of $C$.

HomotopyCategory.Plus.fullyFaithfulιdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the inclusion functor of C (from the docstring)

English

Let $C$ be a set. Then the inclusion functor of $C$ is an element of $\operatorname{FullyFaithful}$ applied to the inclusion of $C$ defined as the inclusion of the plus of $C$.

HomotopyCategory.Plus.quasiIsodefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

no wording

English

Let $A$ be a set. Then there is a morphism property of the set of pluses of $A$. Proof. Let $A$ be arbitrary. By A. By Int. By ComplexShape__up. By HomotopyCategory__quasiIso. By A. By HomotopyCategory__Plus___u3b9_. By CategoryTheory__MorphismProperty__inverseImage.

HomotopyCategory.Plus.quotientdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the quotient of C (from the name)

English

Let $C$ be a set. Then the quotient of $C$ is a functor of the set of pluses of $C$ and the set of pluses of $C$.

HomotopyCategory.Plus.quotientCompιIsodefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the quotient composition inclusion isomorphism of C (from the name)

English

Let $C$ be a set. Then the quotient composition inclusion isomorphism of $C$ is an isomorphism of the composition of the quotient of $C$ and the inclusion of $C$ and the composition of the inclusion of the full subcategory of bounded below cochain complexes of $C$ and the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$.

HomotopyCategory.Plus.singleFunctordefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the single functor of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the single functor of $C$ and $n$ is a functor of $C$ and the set of pluses of $C$ defined as the functor of the collection of all single functors of $C$ and $n$.

HomotopyCategory.Plus.singleFunctorCompιIsodefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the single functor of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the single functor of $C$ and $n$ is an isomorphism of the composition of the single functor of $C$ and $n$ and the inclusion of $C$ and the single functor of $C$ and $n$ defined as the identity of the composition of the single functor of $C$ and $n$ and the inclusion of $C$.

HomotopyCategory.Plus.singleFunctorsdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the collection of all single functors of C (from the docstring)

English

Let $C$ be a set. Then the collection of all single functors of $C$ is a single functor of the set of pluses of $C$ and $\Integer$.

HomotopyCategory.Plus.ιdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the inclusion of C (from the name)

English

Let $C$ be a set. Then the inclusion of $C$ is a functor of the set of pluses of $C$ and the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as the inclusion of the plus of $C$.

HomotopyCategory.plusdefMathlib.Algebra.Homology.HomotopyCategory.Plus, function or constant

Wording

the plus of C (from the name)

English

Let $C$ be a set. Then the plus of $C$ is an object property of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as the strict image of the plus of $C$ and the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$.

Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

CochainComplex.mappingCone.homotopyToZeroOfIddefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the mapping cone of the identity of K (from the docstring)

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Then the mapping cone of the identity of $K$ is a homotopy of the identity morphism of the mapping cone of the identity morphism of $K$ and $0$.

CochainComplex.mappingCone.mapdefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the map of a and b (from the name)

English

Let $x_{6}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $a$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $b$ be a homomorphism of $x_{3}$ and $x_{5}$ such that the composition of $x_{6}$ and $b$ is equal to the composition of $a$ and $x_{7}$. Then the map of $a$ and $b$ is a homomorphism of the mapping cone of $x_{6}$ and the mapping cone of $x_{7}$.

CochainComplex.mappingCone.mapOfHomotopydefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the map of H (from the name)

English

Let $H$ be a homotopy of the composition of $x_{6}$ and $b$ and the composition of $a$ and $x_{7}$. Then the map of $H$ is a homomorphism of the mapping cone of $x_{6}$ and the mapping cone of $x_{7}$.

CochainComplex.mappingCone.mapTriangleIsodefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the map triangle isomorphism of x4 and G (from the name)

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $G$ be a functor of $C$ and $D$. Then the map triangle isomorphism of $x_{4}$ and $G$ is an isomorphism of the action of the map triangle of the map homological complex of $G$ and $\operatorname{up}$ applied to $\Integer$ and the standard triangle of $x_{4}$ and the standard triangle of the map of the map homological complex of $G$ and $\operatorname{up}$ applied to $\Integer$ and $x_{4}$.

CochainComplex.mappingCone.mapTrianglehIsodefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $G$ be a functor of $C$ and $D$. Then $\operatorname{mapTrianglehIso}$ applied to $x_{4}$ and $G$ is an isomorphism of the action of the map triangle of the map homotopy category of $G$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{triangleh}$ applied to $x_{4}$ and $\operatorname{triangleh}$ applied to the map of the map homological complex of $G$ and $\operatorname{up}$ applied to $\Integer$ and $x_{4}$ defined as the composition of the application of the inverse of the canonical isomorphism of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the map homotopy category of $G$ and $\operatorname{up}$ applied to $\Integer$ and the standard triangle of $x_{4}$ and the composition of the application of the map triangle isomorphism of the map homotopy category factor of $G$ and $\operatorname{up}$ applied to $\Integer$ and the standard triangle of $x_{4}$ and the composition of the application of the canonical isomorphism of the map homological complex of $G$ and $\operatorname{up}$ applied to $\Integer$ and the quotient of $D$ and $\operatorname{up}$ applied to $\Integer$ and the standard triangle of $x_{4}$ and the map isomorphism of the map triangle of the quotient of $D$ and $\operatorname{up}$ applied to $\Integer$ and the map triangle isomorphism of $x_{4}$ and $G$.

CochainComplex.mappingCone.rotateHomotopyEquivdefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then $\operatorname{rotateHomotopyEquiv}$ applied to $x_{2}$ is a homotopy equivalence of the action of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $1$ and $K$ and the mapping cone of the right inclusion in the mapping cone of $x_{2}$.

CochainComplex.mappingCone.rotateTrianglehIsodefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then $\operatorname{rotateTrianglehIso}$ applied to $x_{2}$ is an isomorphism of $\operatorname{rotate}$ applied to $\operatorname{triangleh}$ applied to $x_{2}$ and $\operatorname{triangleh}$ applied to the right inclusion in the mapping cone of $x_{2}$.

CochainComplex.mappingCone.shiftIsodefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the canonical isomorphism of x2 and n (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $n$ be an integer. Then the canonical isomorphism of $x_{2}$ and $n$ is an isomorphism of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and the mapping cone of $x_{2}$ and the mapping cone of the map of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and $x_{2}$.

CochainComplex.mappingCone.shiftTriangleIsodefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the canonical isomorphism of x2 and n (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $n$ be an integer. Then the canonical isomorphism of $x_{2}$ and $n$ is an isomorphism of the action of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and the standard triangle of $x_{2}$ and the standard triangle of the map of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and $x_{2}$.

CochainComplex.mappingCone.shiftTrianglehIsodefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the canonical isomorphism of x2 and n (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $n$ be an integer. Then the canonical isomorphism of $x_{2}$ and $n$ is an isomorphism of the action of the shift functor of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ and $n$ and $\operatorname{triangleh}$ applied to $x_{2}$ and $\operatorname{triangleh}$ applied to the map of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and $x_{2}$ defined as the composition of the application of the inverse of the commutative shift isomorphism of the map triangle of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and $n$ and the standard triangle of $x_{2}$ and the map isomorphism of the map triangle of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the canonical isomorphism of $x_{2}$ and $n$.

CochainComplex.mappingCone.triangledefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the standard triangle of x2 (from the docstring)

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then the standard triangle of $x_{2}$ is a triangle of the set of cochain complexes of $C$ and $\Integer$.

CochainComplex.mappingCone.triangleMapdefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the triangle map of a and b (from the name)

English

Let $x_{6}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $a$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $b$ be a homomorphism of $x_{3}$ and $x_{5}$ such that the composition of $x_{6}$ and $b$ is equal to the composition of $a$ and $x_{7}$. Then the triangle map of $a$ and $b$ is a homomorphism of the standard triangle of $x_{6}$ and the standard triangle of $x_{7}$.

CochainComplex.mappingCone.trianglehdefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Then $\operatorname{triangleh}$ applied to $x_{2}$ is a triangle of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as the action of the map triangle of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the standard triangle of $x_{2}$.

CochainComplex.mappingCone.trianglehMapOfHomotopydefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

no wording

English

Let $H$ be a homotopy of the composition of $x_{6}$ and $b$ and the composition of $a$ and $x_{7}$. Then $\operatorname{trianglehMapOfHomotopy}$ applied to $H$ is a homomorphism of $\operatorname{triangleh}$ applied to $x_{6}$ and $\operatorname{triangleh}$ applied to $x_{7}$.

HomotopyCategory.Pretriangulated.distinguishedTrianglesdefMathlib.Algebra.Homology.HomotopyCategory.Pretriangulated, function or constant

Wording

the distinguished triangle of C (from the name)

English

Let $C$ be a set. Then the distinguished triangle of $C$ is an element of the power set of the set of triangles of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as $\operatorname{ofPred}$ applied to the function that maps $T$ to the proposition that there exist cochain complexes $X$ and $Y$ of $C$ and $\Integer$, such that there exists a homomorphism $x_{2}$ of $X$ and $Y$, such that $\mathrm{Nonempty}$ holds for the set of isomorphisms of $T$ and $\operatorname{triangleh}$ applied to $x_{2}$.

Mathlib.Algebra.Homology.HomotopyCategory.Shift

CategoryTheory.Functor.mapCochainComplexShiftIsodefMathlib.Algebra.Homology.HomotopyCategory.Shift, function or constant

Wording

the map cochain complex shift isomorphism of F and n (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $n$ be an integer. Then the map cochain complex shift isomorphism of $F$ and $n$ is an isomorphism of the composition of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $n$ and the map homological complex of $F$ and $\operatorname{up}$ applied to $\Integer$ and the composition of the map homological complex of $F$ and $\operatorname{up}$ applied to $\Integer$ and the shift functor of the set of homological complexes of $D$ and $\operatorname{up}$ applied to $\Integer$ and $n$.

CochainComplex.shiftEvaldefMathlib.Algebra.Homology.HomotopyCategory.Shift, function or constant

Wording

the shift evaluation of i and hi (from the name)

English

Let $C$ be a set. Let $n$, $i$ and $\mathrm{i'}$ be integers such that $n + i = \mathrm{i'}$. Then the shift evaluation of $i$ and $\mathrm{i'}$ is an isomorphism of the composition of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $i$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $\mathrm{i'}$.

CochainComplex.shiftFunctordefMathlib.Algebra.Homology.HomotopyCategory.Shift, function or constant

Wording

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

English

Let $C$ be a set. Let $n$ be an integer. Then the shift functor of $C$ and $n$ is a functor of the set of cochain complexes of $C$ and $\Integer$ and the set of cochain complexes of $C$ and $\Integer$.

CochainComplex.shiftFunctorAdd'defMathlib.Algebra.Homology.HomotopyCategory.Shift, function or constant

Wording

the shift functor sum of x3 and x4 (from the name)

English

Let $C$ be a set. Let $x_{2}$, $x_{3}$ and $x_{4}$ be integers such that $x_{2} + x_{3} = x_{4}$. Then the shift functor sum of $x_{3}$ and $x_{4}$ is an isomorphism of the shift functor of $C$ and $x_{4}$ and the composition of the shift functor of $C$ and $x_{2}$ and the shift functor of $C$ and $x_{3}$.

CochainComplex.shiftFunctorObjXIsodefMathlib.Algebra.Homology.HomotopyCategory.Shift, function or constant

Wording

the shift functor object isomorphism of i and m (from the name)

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$, $i$ and $m$ be integers such that $m = i + n$. Then the shift functor object isomorphism of $i$ and $m$ is an isomorphism of $\operatorname{X}$ applied to the action of the shift functor of $C$ and $n$ and $K$ and $i$ and $\operatorname{X}$ applied to $K$ and $m$.

CochainComplex.shiftFunctorZero'defMathlib.Algebra.Homology.HomotopyCategory.Shift, function or constant

Wording

the shift functor zero of n (from the name)

English

Let $C$ be a set. Let $n$ be an integer such that $n = 0$. Then the shift functor zero of $n$ is an isomorphism of the shift functor of $C$ and $n$ and the identity of the set of cochain complexes of $C$ and $\Integer$.

Homotopy.shiftdefMathlib.Algebra.Homology.HomotopyCategory.Shift, function or constant

Wording

the shift of h and n (from the name)

English

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

Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

CochainComplex.ShiftSequence.shiftIsodefMathlib.Algebra.Homology.HomotopyCategory.ShiftSequence, function or constant

Wording

the shift isomorphism of a and #4 (from the name)

English

Let $C$ be a set. Let $n$, $a$ and $\mathrm{a'}$ be integers such that $n + a = \mathrm{a'}$. Then the shift isomorphism of $a$ and $\mathrm{a'}$ is an isomorphism of the composition of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $n$ and the homology functor of $\operatorname{up}$ applied to $\Integer$ and $a$ and the homology functor of $\operatorname{up}$ applied to the set of integers and $\mathrm{a'}$ defined as the composition of the left isomorphism whisker of the shift functor of the set of homological complexes of $C$ and $\operatorname{up}$ applied to $\Integer$ and $n$ and the homology functor isomorphism of $\operatorname{up}$ applied to $\Integer$ and $a$ and the composition of the inverse of the associator of the short complex functor of $\operatorname{up}$ applied to $\Integer$ and $a$ and the homology functor of $C$ and the composition of the right isomorphism whisker of the shift short complex functor isomorphism of $a$ and $\mathrm{a'}$ and the homology functor of $C$ and the inverse of the homology functor isomorphism of $\operatorname{up}$ applied to $\Integer$ and $\mathrm{a'}$.

CochainComplex.shiftShortComplexFunctor'defMathlib.Algebra.Homology.HomotopyCategory.ShiftSequence, function or constant

Wording

the shift short complex functor of hj and hk (from the name)

English

Let $C$ be a set. Let $n$, $i$, $j$, $k$, $\mathrm{i'}$, $\mathrm{j'}$ and $\mathrm{k'}$ be integers such that $n + i = \mathrm{i'}$, $n + j = \mathrm{j'}$ and $n + k = \mathrm{k'}$. Then the shift short complex functor of $\mathrm{j'}$ and $\mathrm{k'}$ is an isomorphism of the composition of the shift functor of the set of cochain complexes of $C$ and $\Integer$ and $n$ and the short complex functor of $j$ and $k$ and the short complex functor of $\mathrm{j'}$ and $\mathrm{k'}$.

CochainComplex.shiftShortComplexFunctorIsodefMathlib.Algebra.Homology.HomotopyCategory.ShiftSequence, function or constant

Wording

the shift short complex functor isomorphism of i and hi (from the name)

English

Let $C$ be a set. Let $n$, $i$ and $\mathrm{i'}$ be integers such that $n + i = \mathrm{i'}$. Then the shift short complex functor isomorphism of $i$ and $\mathrm{i'}$ is an isomorphism of the composition of the shift functor of $C$ and $n$ and the short complex functor of $\operatorname{up}$ applied to $\Integer$ and $i$ and the short complex functor of $\operatorname{up}$ applied to $\Integer$ and $\mathrm{i'}$.

Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

CochainComplex.mappingCone.descShortComplexdefMathlib.Algebra.Homology.HomotopyCategory.ShortExact, function or constant

Wording

no wording

English

Let $S$ be a short complex of the set of cochain complexes of $C$ and $\Integer$. Then $\operatorname{descShortComplex}$ applied to $S$ is a homomorphism of the mapping cone of $\operatorname{f}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$.

Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

CategoryTheory.Functor.mapCochainComplexSingleFunctordefMathlib.Algebra.Homology.HomotopyCategory.SingleFunctors, function or constant

Wording

the map cochain complex single functor of F and n (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $n$ be an integer. Then the map cochain complex single functor of $F$ and $n$ is an isomorphism of the composition of the single functor of $C$ and $n$ and the map homological complex of $F$ and $\operatorname{up}$ applied to $\Integer$ and the composition of $F$ and the single functor of $D$ and $n$ defined as the single map homological complex of $\operatorname{up}$ applied to $\Integer$ and $n$.

CochainComplex.singleFunctordefMathlib.Algebra.Homology.HomotopyCategory.SingleFunctors, function or constant

Wording

the single functor of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the single functor of $C$ and $n$ is a functor of $C$ and the set of cochain complexes of $C$ and $\Integer$ defined as the functor of the collection of all single functors of $C$ and $n$.

CochainComplex.singleFunctorsdefMathlib.Algebra.Homology.HomotopyCategory.SingleFunctors, function or constant

Wording

the collection of all single functors of C (from the docstring)

English

Let $C$ be a set. Then the collection of all single functors of $C$ is a single functor of the set of cochain complexes of $C$ and $\Integer$ and $\Integer$.

HomotopyCategory.singleFunctordefMathlib.Algebra.Homology.HomotopyCategory.SingleFunctors, function or constant

Wording

the single functor of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the single functor of $C$ and $n$ is a functor of $C$ and the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as the functor of the collection of all single functors of $C$ and $n$.

HomotopyCategory.singleFunctorPostcompQuotientIsodefMathlib.Algebra.Homology.HomotopyCategory.SingleFunctors, function or constant

Wording

the single functor postcomposition quotient isomorphism of C and n (from the name)

English

Let $C$ be a set. Let $n$ be an integer. Then the single functor postcomposition quotient isomorphism of $C$ and $n$ is an isomorphism of the single functor of $C$ and $n$ and the composition of the single functor of $C$ and $n$ and the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as the map isomorphism of the evaluation of $n$ and the single functor postcomposition quotient isomorphism of $C$.

HomotopyCategory.singleFunctorsdefMathlib.Algebra.Homology.HomotopyCategory.SingleFunctors, function or constant

Wording

the collection of all single functors of C (from the docstring)

English

Let $C$ be a set. Then the collection of all single functors of $C$ is a single functor of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ and $\Integer$ defined as the postcomposition of the collection of all single functors of $C$ and the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$.

HomotopyCategory.singleFunctorsPostcompQuotientIsodefMathlib.Algebra.Homology.HomotopyCategory.SingleFunctors, function or constant

Wording

the single functor postcomposition quotient isomorphism of C (from the name)

English

Let $C$ be a set. Then the single functor postcomposition quotient isomorphism of $C$ is an isomorphism of the collection of all single functors of $C$ and the postcomposition of the collection of all single functors of $C$ and the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as the identity of the collection of all single functors of $C$.

Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject

HomotopyCategory.composableArrowsFunctordefMathlib.Algebra.Homology.HomotopyCategory.SpectralObject, function or constant

Wording

the functor of C (from the docstring)

English

Let $C$ be a set. Then the functor of $C$ is a functor of the set of composable arrows of the set of cochain complexes of $C$ and $\Integer$ and $1$ and the set of cochain complexes of $C$ and $\Integer$.

HomotopyCategory.spectralObjectMappingConedefMathlib.Algebra.Homology.HomotopyCategory.SpectralObject, function or constant

Wording

the spectral object mapping cone of C (from the name)

English

Let $C$ be a set. Then the spectral object mapping cone of $C$ is a spectral object of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ and the set of cochain complexes of $C$ and $\Integer$.

Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

CochainComplex.MappingConeCompHomotopyEquiv.homdefMathlib.Algebra.Homology.HomotopyCategory.Triangulated, function or constant

Wording

the homomorphism of f and g (from the name)

English

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

CochainComplex.MappingConeCompHomotopyEquiv.homotopyInvHomIddefMathlib.Algebra.Homology.HomotopyCategory.Triangulated, function or constant

Wording

the homotopy inverse homomorphism identity of f and g (from the name)

English

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the homotopy inverse homomorphism identity of $f$ and $g$ is a homotopy of the composition of the inverse of $f$ and $g$ and the homomorphism of $f$ and $g$ and the identity morphism of the mapping cone of the first morphism of the mapping cone composition triangle of $f$ and $g$.

CochainComplex.MappingConeCompHomotopyEquiv.invdefMathlib.Algebra.Homology.HomotopyCategory.Triangulated, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the inverse of $f$ and $g$ is a homomorphism of the mapping cone of the first morphism of the mapping cone composition triangle of $f$ and $g$ and the mapping cone of $g$.

CochainComplex.mappingConeCompHomotopyEquivdefMathlib.Algebra.Homology.HomotopyCategory.Triangulated, function or constant

Wording

the mapping cone composition homotopy equivalence of f and g (from the name)

English

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the mapping cone composition homotopy equivalence of $f$ and $g$ is a homotopy equivalence of the mapping cone of $g$ and the mapping cone of the first morphism of the mapping cone composition triangle of $f$ and $g$.

CochainComplex.mappingConeCompTriangledefMathlib.Algebra.Homology.HomotopyCategory.Triangulated, function or constant

Wording

the mapping cone composition triangle of f and g (from the name)

English

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the mapping cone composition triangle of $f$ and $g$ is a triangle of the set of cochain complexes of $C$ and $\Integer$.

CochainComplex.mappingConeCompTrianglehdefMathlib.Algebra.Homology.HomotopyCategory.Triangulated, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Then $\operatorname{mappingConeCompTriangleh}$ applied to $f$ and $g$ is a triangle of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ defined as the action of the map triangle of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and the mapping cone composition triangle of $f$ and $g$.