AlgebraicTopology.AlternatingCofaceMapComplex.mapdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the map of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $f$ is a homomorphism of the object of $X$ and the object of $Y$.
AlgebraicTopology.AlternatingCofaceMapComplex.objdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the object of X (from the name)
English
Let $X$ be a cosimplicial object of $C$. Then the object of $X$ is a cochain complex of $C$ and $\Natural$ defined as $\operatorname{of}$ applied to the function that maps $n$ to the action of $X$ and $\operatorname{mk}$ applied to $n$, $\operatorname{objD}$ applied to $X$ and $\mathrm{AlgebraicTopology\_\_AlternatingCofaceMapComplex\_\_d\_squared}$ applied to $X$.
AlgebraicTopology.AlternatingCofaceMapComplex.objDdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the object of X and n (from the name)
English
Let $X$ be a cosimplicial object of $C$. Let $n$ be a natural number. Then the object of $X$ and $n$ is a homomorphism of the action of $X$ and $\operatorname{mk}$ applied to $n$ and the action of $X$ and $\operatorname{mk}$ applied to $n + 1$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{(\HSMulhSMulMACRoAL {(\operatorname{neg} (1)^ {\operatorname{val} (i)})}{\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_} (X , i)})}$.
AlgebraicTopology.AlternatingFaceMapComplex.mapdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the map of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $f$ is a homomorphism of the object of $X$ and the object of $Y$.
AlgebraicTopology.AlternatingFaceMapComplex.objdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the object of X (from the name)
English
Let $X$ be a simplicial object of $C$. Then the object of $X$ is a chain complex of $C$ and $\Natural$ defined as $\operatorname{of}$ applied to the function that maps $n$ to the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$, $\operatorname{objD}$ applied to $X$ and $\mathrm{AlgebraicTopology\_\_AlternatingFaceMapComplex\_\_d\_squared}$ applied to $X$.
AlgebraicTopology.AlternatingFaceMapComplex.objDdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the object of X and n (from the name)
English
Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Then the object of $X$ and $n$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{(\HSMulhSMulMACRoAL {(\operatorname{neg} (1)^ {\operatorname{val} (i)})}{\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_} (X , i)})}$.
AlgebraicTopology.AlternatingFaceMapComplex.εdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_AlternatingFaceMapComplex\_\_\_u3b5\_}$ is a homomorphism of the composition of $\operatorname{drop}$ and the alternating face map complex of $C$ and the composition of the point of the augmentation and $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $C$.
AlgebraicTopology.alternatingCofaceMapComplexdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the alternating coface map complex of C (from the name)
English
Let $C$ be a set. Then the alternating coface map complex of $C$ is a functor of the set of cosimplicial objects of $C$ and the set of cochain complexes of $C$ and $\Natural$.
AlgebraicTopology.alternatingFaceMapComplexdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the alternating face map complex of C (from the name)
English
Let $C$ be a set. Then the alternating face map complex of $C$ is a functor of the set of simplicial objects of $C$ and the set of chain complexes of $C$ and $\Natural$.
AlgebraicTopology.alternatingFaceMapComplexCompMapHomologicalComplexIsodefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the alternating face map complex composition map homological complex isomorphism of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the alternating face map complex composition map homological complex isomorphism of $F$ is an isomorphism of the composition of the alternating face map complex of $C$ and the map homological complex of $F$ and $\operatorname{down}$ applied to $\Natural$ and the composition of the action of the whiskering of $C$ and $D$ and $F$ and the alternating face map complex of $D$.
AlgebraicTopology.inclusionOfMooreComplexdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the inclusion of A (from the name)
English
Let $A$ be a set. Then the inclusion of $A$ is a homomorphism of the normalized Moore complex of $A$ and the alternating face map complex of $A$.
AlgebraicTopology.inclusionOfMooreComplexMapdefMathlib.AlgebraicTopology.AlternatingFaceMapComplex, function or constantWording
the inclusion of X (from the name)
English
Let $X$ be a simplicial object of $A$. Then the inclusion of $X$ is a homomorphism of the action of the normalized Moore complex of $A$ and $X$ and the action of the alternating face map complex of $A$ and $X$.
CategoryTheory.Arrow.augmentedCechConervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the augmented Cech conerve of f (from the name)
English
Let $f$ be an arrow of $C$. Then the augmented Cech conerve of $f$ is an element of $\operatorname{Augmented}$ applied to $C$.
CategoryTheory.Arrow.augmentedCechNervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the augmented Cech nerve of f (from the name)
English
Let $f$ be an arrow of $C$. Then the augmented Cech nerve of $f$ is an element of $\operatorname{Augmented}$ applied to $C$.
CategoryTheory.Arrow.cechConervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the Cech conerve of f (from the name)
English
Let $f$ be an arrow of $C$. Then the Cech conerve of $f$ is a cosimplicial object of $C$.
CategoryTheory.Arrow.cechNervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the Cech nerve of f (from the name)
English
Let $f$ be an arrow of $C$. Then the Cech nerve of $f$ is a simplicial object of $C$.
CategoryTheory.Arrow.mapAugmentedCechConervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the map augmented Cech conerve of F (from the name)
English
Let $F$ be a homomorphism of $f$ and $g$. Then the map augmented Cech conerve of $F$ is a homomorphism of the augmented Cech conerve of $f$ and the augmented Cech conerve of $g$.
CategoryTheory.Arrow.mapAugmentedCechNervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the map augmented Cech nerve of F (from the name)
English
Let $F$ be a homomorphism of $f$ and $g$. Then the map augmented Cech nerve of $F$ is a homomorphism of the augmented Cech nerve of $f$ and the augmented Cech nerve of $g$.
CategoryTheory.Arrow.mapCechConervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the map Cech conerve of F (from the name)
English
Let $F$ be a homomorphism of $f$ and $g$. Then the map Cech conerve of $F$ is a homomorphism of the Cech conerve of $f$ and the Cech conerve of $g$.
CategoryTheory.Arrow.mapCechNervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the map Cech nerve of F (from the name)
English
Let $F$ be a homomorphism of $f$ and $g$. Then the map Cech nerve of $F$ is a homomorphism of the Cech nerve of $f$ and the Cech nerve of $g$.
CategoryTheory.CechNerveTerminalFrom.isodefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the isomorphism of X (from the name)
English
Let $X$ be an element of $C$. Then the isomorphism of $X$ is an isomorphism of the Cech nerve of $\operatorname{mk}$ applied to the map of $X$ and $\operatorname{cechNerveTerminalFrom}$ applied to $X$.
CategoryTheory.CechNerveTerminalFrom.wideCospandefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the wide cospan of x1 and X (from the name)
English
Let $x_{1}$ be a set. Let $X$ be an element of $C$. Then the wide cospan of $x_{1}$ and $X$ is a functor of the set of wide pullback shapes of $x_{1}$ and $C$ defined as the wide cospan of the function that maps $x_{2}$ to $X$ and the function that maps $x_{3}$ to the map of $X$.
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitConedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the limit cone of x1 and X (from the name)
English
Let $x_{1}$ be a set. Let $X$ be an element of $C$. Then the limit cone of $x_{1}$ and $X$ is a limit cone of the wide cospan of $x_{1}$ and $X$.
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPidefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the isomorphism to the product induced by the limit cone of x1 and X (from the docstring)
English
Let $x_{1}$ be a set. Let $X$ be an element of $C$. Then the isomorphism to the product induced by the limit cone of $x_{1}$ and $X$ is an isomorphism of the limit of the wide cospan of $x_{1}$ and $X$ and the product object of the function that maps $x_{2}$ to $X$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the wide cospan of $x_{1}$ and $X$ and $\operatorname{isLimit}$ applied to the limit cone of $x_{1}$ and $X$.
CategoryTheory.CosimplicialObject.augmentedCechConervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the augmented Cech conerve (from the name)
English
The augmented Cech conerve is a functor of the set of arrows of $C$ and $\operatorname{Augmented}$ applied to $C$.
CategoryTheory.CosimplicialObject.cechConervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the Cech conerve (from the name)
English
The Cech conerve is a functor of the set of arrows of $C$ and the set of cosimplicial objects of $C$.
CategoryTheory.CosimplicialObject.cechConerveAdjunctiondefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the Cech conerve adjunction (from the name)
English
The Cech conerve adjunction is an adjunction of the augmented Cech conerve and the arrow.
CategoryTheory.CosimplicialObject.cechConerveEquivdefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the Cech conerve equivalence of F and X (from the name)
English
Let $F$ be an arrow of $C$. Let $X$ be an element of $\operatorname{Augmented}$ applied to $C$. Then the Cech conerve equivalence of $F$ and $X$ is an equivalence from the set of homomorphisms of the augmented Cech conerve of $F$ and $X$ to the set of homomorphisms of $F$ and the action of the arrow and $X$.
CategoryTheory.CosimplicialObject.equivalenceLeftToRightdefMathlib.AlgebraicTopology.CechNerve, function or constantEnglish
Let $F$ be an arrow of $C$. Let $X$ be an element of $\operatorname{Augmented}$ applied to $C$. Let $G$ be a homomorphism of the augmented Cech conerve of $F$ and $X$. Then $\operatorname{equivalenceLeftToRight}$ applied to $F$, $X$ and $G$ is a homomorphism of $F$ and the action of the arrow and $X$.
CategoryTheory.CosimplicialObject.equivalenceRightToLeftdefMathlib.AlgebraicTopology.CechNerve, function or constantEnglish
Let $F$ be an arrow of $C$. Let $X$ be an element of $\operatorname{Augmented}$ applied to $C$. Let $G$ be a homomorphism of $F$ and the action of the arrow and $X$. Then $\operatorname{equivalenceRightToLeft}$ applied to $F$, $X$ and $G$ is a homomorphism of the augmented Cech conerve of $F$ and $X$.
CategoryTheory.SimplicialObject.augmentedCechNervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the augmented Cech nerve (from the name)
English
The augmented Cech nerve is a functor of the set of arrows of $C$ and $\operatorname{Augmented}$ applied to $C$.
CategoryTheory.SimplicialObject.cechNervedefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the Cech nerve (from the name)
English
The Cech nerve is a functor of the set of arrows of $C$ and the set of simplicial objects of $C$.
CategoryTheory.SimplicialObject.cechNerveAdjunctiondefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the Cech nerve adjunction (from the name)
English
The Cech nerve adjunction is an adjunction of the arrow and the augmented Cech nerve.
CategoryTheory.SimplicialObject.cechNerveEquivdefMathlib.AlgebraicTopology.CechNerve, function or constantWording
the Cech nerve equivalence of X and F (from the name)
English
Let $X$ be an element of $\operatorname{Augmented}$ applied to $C$. Let $F$ be an arrow of $C$. Then the Cech nerve equivalence of $X$ and $F$ is an equivalence from the set of homomorphisms of the action of the arrow and $X$ and $F$ to the set of homomorphisms of $X$ and the augmented Cech nerve of $F$.
CategoryTheory.SimplicialObject.equivalenceLeftToRightdefMathlib.AlgebraicTopology.CechNerve, function or constantEnglish
Let $X$ be an element of $\operatorname{Augmented}$ applied to $C$. Let $F$ be an arrow of $C$. Let $G$ be a homomorphism of the action of the arrow and $X$ and $F$. Then $\operatorname{equivalenceLeftToRight}$ applied to $X$, $F$ and $G$ is a homomorphism of $X$ and the augmented Cech nerve of $F$.
CategoryTheory.SimplicialObject.equivalenceRightToLeftdefMathlib.AlgebraicTopology.CechNerve, function or constantEnglish
Let $X$ be an element of $\operatorname{Augmented}$ applied to $C$. Let $F$ be an arrow of $C$. Let $G$ be a homomorphism of $X$ and the augmented Cech nerve of $F$. Then $\operatorname{equivalenceRightToLeft}$ applied to $X$, $F$ and $G$ is a homomorphism of the action of the arrow and $X$ and $F$.
CategoryTheory.cechNerveTerminalFromdefMathlib.AlgebraicTopology.CechNerve, function or constantEnglish
Let $X$ be an element of $C$. Then $\operatorname{cechNerveTerminalFrom}$ applied to $X$ is a simplicial object of $C$.
AlgebraicTopology.DoldKan.Compatibility.equivalencedefMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the equivalence of hF and hG (from the docstring)
English
Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Let $\mathrm{hG}$ be an isomorphism of the composition of the functor of $\mathrm{eB}$ and the inverse of $\mathrm{e'}$ and the composition of $G$ and the functor of $\mathrm{eA}$. Then the equivalence of $\mathrm{hF}$ and $\mathrm{hG}$ is an equivalence of $A$ and $B$ defined as the change inverse of the equivalence of $\mathrm{eB}$ and $\mathrm{hF}$ and $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the associator of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the right isomorphism whisker of $\mathrm{hG}$ and the inverse of $\mathrm{eA}$ and the associator of the functor of $\mathrm{eA}$ and the inverse of $\mathrm{eA}$ and the left isomorphism whisker of $G$ and the inverse of the unit isomorphism of $\mathrm{eA}$ and the right unitor of $G$.
AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIsodefMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the counit isomorphism of x3 (from the docstring)
English
Let $x_{3}$ be an isomorphism of the composition of $G$ and $F$ and the functor of $\mathrm{eB}$. Then the counit isomorphism of $x_{3}$ is an isomorphism of the composition of $G$ and the composition of $F$ and the inverse of $\mathrm{eB}$ and the identity of $B$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the associator of $F$ and the inverse of $\mathrm{eB}$ and the right isomorphism whisker of $x_{3}$ and the inverse of $\mathrm{eB}$ and the inverse of the unit isomorphism of $\mathrm{eB}$.
AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIsodefMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the equivalence unit isomorphism of hG and x4 (from the name)
English
Let $\mathrm{hG}$ be an isomorphism of the composition of the functor of $\mathrm{eB}$ and the inverse of $\mathrm{e'}$ and the composition of $G$ and the functor of $\mathrm{eA}$. Let $x_{4}$ be an isomorphism of the functor of $\mathrm{eA}$ and the composition of $F$ and the inverse of $\mathrm{e'}$. Then the equivalence unit isomorphism of $\mathrm{hG}$ and $x_{4}$ is an isomorphism of the identity of $A$ and the composition of the composition of $F$ and the inverse of $\mathrm{eB}$ and $G$.
AlgebraicTopology.DoldKan.Compatibility.equivalence₀defMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the equivalence of eA and #2 (from the name)
English
Let $\mathrm{eA}$ be an equivalence of $A$ and $\mathrm{A'}$. Let $\mathrm{e'}$ be an equivalence of $\mathrm{A'}$ and $\mathrm{B'}$. Then the equivalence of $\mathrm{eA}$ and $\mathrm{e'}$ is an equivalence of $A$ and $\mathrm{B'}$ defined as the composition of $\mathrm{eA}$ and $\mathrm{e'}$.
AlgebraicTopology.DoldKan.Compatibility.equivalence₁defMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the equivalence of hF (from the name)
English
Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Then the equivalence of $\mathrm{hF}$ is an equivalence of $A$ and $\mathrm{B'}$ defined as the change functor of the equivalence of $\mathrm{eA}$ and $\mathrm{e'}$ and $\mathrm{hF}$.
AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIsodefMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the counit isomorphism of the equivalence of hF (from the docstring)
English
Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Then the counit isomorphism of the equivalence of $\mathrm{hF}$ is an isomorphism of the composition of the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and $F$ and the identity of $\mathrm{B'}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the left isomorphism whisker of the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the inverse of $\mathrm{hF}$ and the associator of the inverse of $\mathrm{eA}$ and the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and the left isomorphism whisker of the inverse of $\mathrm{e'}$ and the inverse of the associator of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and the left isomorphism whisker of the inverse of $\mathrm{e'}$ and the right isomorphism whisker of the counit isomorphism of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and the left isomorphism whisker of the inverse of $\mathrm{e'}$ and the left unitor of the functor of $\mathrm{e'}$ and the counit isomorphism of $\mathrm{e'}$.
AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIsodefMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the unit isomorphism of the equivalence of hF (from the docstring)
English
Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Then the unit isomorphism of the equivalence of $\mathrm{hF}$ is an isomorphism of the identity of $A$ and the composition of $F$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the unit isomorphism of $\mathrm{eA}$ and the left isomorphism whisker of the functor of $\mathrm{eA}$ and the inverse of the left unitor of the inverse of $\mathrm{eA}$ and the left isomorphism whisker of the functor of $\mathrm{eA}$ and the right isomorphism whisker of the unit isomorphism of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the left isomorphism whisker of the functor of $\mathrm{eA}$ and the associator of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the inverse of the associator of the functor of $\mathrm{e'}$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the right isomorphism whisker of $\mathrm{hF}$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$.
AlgebraicTopology.DoldKan.Compatibility.equivalence₂defMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the equivalence of eB and hF (from the name)
English
Let $\mathrm{eB}$ be an equivalence of $B$ and $\mathrm{B'}$. Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Then the equivalence of $\mathrm{eB}$ and $\mathrm{hF}$ is an equivalence of $A$ and $B$ defined as the composition of the equivalence of $\mathrm{hF}$ and the inverse of $\mathrm{eB}$.
AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIsodefMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the counit isomorphism of the equivalence of eB and hF (from the docstring)
English
Let $\mathrm{eB}$ be an equivalence of $B$ and $\mathrm{B'}$. Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Then the counit isomorphism of the equivalence of $\mathrm{eB}$ and $\mathrm{hF}$ is an isomorphism of the composition of the composition of the functor of $\mathrm{eB}$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the composition of $F$ and the inverse of $\mathrm{eB}$ and the identity of $B$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the associator of the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the composition of $F$ and the inverse of $\mathrm{eB}$ and the left isomorphism whisker of the functor of $\mathrm{eB}$ and the inverse of the associator of $F$ and the inverse of $\mathrm{eB}$ and the left isomorphism whisker of the functor of $\mathrm{eB}$ and the right isomorphism whisker of the counit isomorphism of the equivalence of $\mathrm{hF}$ and the inverse of $\mathrm{eB}$ and the left isomorphism whisker of the functor of $\mathrm{eB}$ and the left unitor of the inverse of $\mathrm{eB}$ and the inverse of the unit isomorphism of $\mathrm{eB}$.
AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIsodefMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantWording
the unit isomorphism of the equivalence of eB and hF (from the docstring)
English
Let $\mathrm{eB}$ be an equivalence of $B$ and $\mathrm{B'}$. Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Then the unit isomorphism of the equivalence of $\mathrm{eB}$ and $\mathrm{hF}$ is an isomorphism of the identity of $A$ and the composition of the composition of $F$ and the inverse of $\mathrm{eB}$ and the composition of the functor of $\mathrm{eB}$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the unit isomorphism of the equivalence of $\mathrm{hF}$ and the left isomorphism whisker of $F$ and the inverse of the left unitor of the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the left isomorphism whisker of $F$ and the right isomorphism whisker of the inverse of the counit isomorphism of $\mathrm{eB}$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the inverse of the associator of the composition of the inverse of $\mathrm{eB}$ and the functor of $\mathrm{eB}$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the right isomorphism whisker of the inverse of the associator of the inverse of $\mathrm{eB}$ and the functor of $\mathrm{eB}$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$ and the associator of the functor of $\mathrm{eB}$ and the composition of the inverse of $\mathrm{e'}$ and the inverse of $\mathrm{eA}$.
AlgebraicTopology.DoldKan.Compatibility.τ₀defMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_Compatibility\_\_\_u3c4\_\_u2080\_}$ is an isomorphism of the composition of the functor of $\mathrm{eB}$ and the composition of the inverse of $\mathrm{e'}$ and the functor of $\mathrm{e'}$ and the functor of $\mathrm{eB}$ defined as $\operatorname{trans}$ applied to the left isomorphism whisker of the functor of $\mathrm{eB}$ and the counit isomorphism of $\mathrm{e'}$ and the right unitor of the functor of $\mathrm{eB}$.
AlgebraicTopology.DoldKan.Compatibility.τ₁defMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantEnglish
Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Let $\mathrm{hG}$ be an isomorphism of the composition of the functor of $\mathrm{eB}$ and the inverse of $\mathrm{e'}$ and the composition of $G$ and the functor of $\mathrm{eA}$. Let $x_{4}$ be an isomorphism of the composition of $G$ and $F$ and the functor of $\mathrm{eB}$. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_Compatibility\_\_\_u3c4\_\_u2081\_}$ applied to $\mathrm{hF}$, $\mathrm{hG}$ and $x_{4}$ is an isomorphism of the composition of the functor of $\mathrm{eB}$ and the composition of the inverse of $\mathrm{e'}$ and the functor of $\mathrm{e'}$ and the functor of $\mathrm{eB}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the associator of the inverse of $\mathrm{e'}$ and the functor of $\mathrm{e'}$ and the right isomorphism whisker of $\mathrm{hG}$ and the functor of $\mathrm{e'}$ and the associator of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and the left isomorphism whisker of $G$ and $\mathrm{hF}$ and $x_{4}$.
AlgebraicTopology.DoldKan.Compatibility.υdefMathlib.AlgebraicTopology.DoldKan.Compatibility, function or constantEnglish
Let $\mathrm{hF}$ be an isomorphism of the composition of the functor of $\mathrm{eA}$ and the functor of $\mathrm{e'}$ and $F$. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_Compatibility\_\_\_u3c5\_}$ applied to $\mathrm{hF}$ is an isomorphism of the functor of $\mathrm{eA}$ and the composition of $F$ and the inverse of $\mathrm{e'}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the right unitor of the functor of $\mathrm{eA}$ and the left isomorphism whisker of the functor of $\mathrm{eA}$ and the unit isomorphism of $\mathrm{e'}$ and the inverse of the associator of the functor of $\mathrm{e'}$ and the inverse of $\mathrm{e'}$ and the right isomorphism whisker of $\mathrm{hF}$ and the inverse of $\mathrm{e'}$.
AlgebraicTopology.DoldKan.MorphComponentsstructureMathlib.AlgebraicTopology.DoldKan.Decomposition, typeEnglish
Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Let $Z$ be an element of $C$. Then the elements of $\operatorname{MorphComponents}$ applied to $X$, $n$ and $Z$ are a basic type.
AlgebraicTopology.DoldKan.MorphComponents.adefMathlib.AlgebraicTopology.DoldKan.Decomposition, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{MorphComponents}$ applied to $X$, $n$ and $Z$. Then $\operatorname{a}$ applied to $\mathrm{self}$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ and $Z$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
AlgebraicTopology.DoldKan.MorphComponents.bdefMathlib.AlgebraicTopology.DoldKan.Decomposition, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{MorphComponents}$ applied to $X$, $n$ and $Z$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{b}$ applied to $\mathrm{self}$ and $x_{1}$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and $Z$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.
AlgebraicTopology.DoldKan.MorphComponents.iddefMathlib.AlgebraicTopology.DoldKan.Decomposition, function or constantWording
the identity of X and n (from the name)
English
Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Then the identity of $X$ and $n$ is an element of $\operatorname{MorphComponents}$ applied to $X$, $n$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ defined as $\operatorname{mk}$ applied to $\operatorname{f}$ applied to the infty and $n + 1$ and the function that maps $i$ to $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3c3\_}$ applied to $X$ and $i$.
AlgebraicTopology.DoldKan.MorphComponents.postCompdefMathlib.AlgebraicTopology.DoldKan.Decomposition, function or constantWording
the post composition of f and h (from the name)
English
Let $f$ be an element of $\operatorname{MorphComponents}$ applied to $X$, $n$ and $Z$. Let $h$ be a homomorphism of $Z$ and $\mathrm{Z'}$. Then the post composition of $f$ and $h$ is an element of $\operatorname{MorphComponents}$ applied to $X$, $n$ and $\mathrm{Z'}$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{a}$ applied to $f$ and $h$ and the function that maps $i$ to the composition of $\operatorname{b}$ applied to $f$ and $i$ and $h$.
AlgebraicTopology.DoldKan.MorphComponents.preCompdefMathlib.AlgebraicTopology.DoldKan.Decomposition, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be an element of $\operatorname{MorphComponents}$ applied to $X$, $n$ and $Z$. Let $g$ be a homomorphism of $\mathrm{X'}$ and $X$. Then the composition of $f$ and $g$ is an element of $\operatorname{MorphComponents}$ applied to $\mathrm{X'}$, $n$ and $Z$ defined as $\operatorname{mk}$ applied to the composition of the component of $g$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ and $\operatorname{a}$ applied to $f$ and the function that maps $i$ to the composition of the component of $g$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and $\operatorname{b}$ applied to $f$ and $i$.
AlgebraicTopology.DoldKan.MorphComponents.φdefMathlib.AlgebraicTopology.DoldKan.Decomposition, function or constantEnglish
Let $f$ be an element of $\operatorname{MorphComponents}$ applied to $X$, $n$ and $Z$. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_MorphComponents\_\_\_u3c6\_}$ applied to $f$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ and $Z$ defined as $\operatorname{comp} (\operatorname{f} (\operatorname{PInfty} , n + 1), \operatorname{a} (f))+ \FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{comp} (\operatorname{f} (\operatorname{P} (\operatorname{val} (i)), n + 1), \operatorname{comp} (\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_} (X , \operatorname{succ} (\operatorname{rev} (i))), \operatorname{b} (f , \operatorname{rev} (i))))}$.
AlgebraicTopology.DoldKan.DegeneraciesVanishdefMathlib.AlgebraicTopology.DoldKan.Degeneracies, predicateEnglish
Let $f$ be a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and $T$. Then we can say that $\operatorname{DegeneraciesVanish}$ holds for $f$.
CategoryTheory.Abelian.DoldKan.NdefMathlib.AlgebraicTopology.DoldKan.Equivalence, function or constantEnglish
$\operatorname{N}$ is a functor of the set of simplicial objects of $A$ and the set of chain complexes of $A$ and $\Natural$ defined as the normalized Moore complex of $A$.
CategoryTheory.Abelian.DoldKan.comparisonNdefMathlib.AlgebraicTopology.DoldKan.Equivalence, function or constantWording
the comparison (from the name)
English
The comparison is an isomorphism of $\operatorname{N}$ and $\operatorname{N}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the left unitor of $\operatorname{N}$ and the left isomorphism whisker of $\operatorname{N}$ and the unit isomorphism of the equivalence of the set of chain complexes of $A$ and $\Natural$ and the identity of the composition of $\operatorname{N}$ and the composition of the functor of the equivalence of the set of chain complexes of $A$ and $\Natural$ and the inverse of the equivalence of the set of chain complexes of $A$ and $\Natural$ and the right isomorphism whisker of the inverse of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_\_iso\_normalizedMooreComplex\_comp\_toKaroubi}$ applied to $A$ and the inverse of the equivalence of the set of chain complexes of $A$ and $\Natural$ and the identity of the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and the inverse of the equivalence of the set of chain complexes of $A$ and $\Natural$.
CategoryTheory.Abelian.DoldKan.equivalencedefMathlib.AlgebraicTopology.DoldKan.Equivalence, function or constantWording
the equivalence (from the name)
English
The equivalence is an equivalence of the set of simplicial objects of $A$ and the set of chain complexes of $A$ and $\Natural$ defined as the change functor of the equivalence and the inverse of the comparison.
CategoryTheory.Abelian.DoldKan.ΓdefMathlib.AlgebraicTopology.DoldKan.Equivalence, function or constantEnglish
$\mathrm{CategoryTheory\_\_Abelian\_\_DoldKan\_\_\_u393\_}$ is a functor of the set of chain complexes of $A$ and $\Natural$ and the set of simplicial objects of $A$ defined as $\mathrm{CategoryTheory\_\_Idempotents\_\_DoldKan\_\_\_u393\_}$.
CategoryTheory.Preadditive.DoldKan.NdefMathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive, function or constantEnglish
$\operatorname{N}$ is a functor of $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ and $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$ defined as $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$.
CategoryTheory.Preadditive.DoldKan.equivalencedefMathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive, function or constantWording
the equivalence (from the name)
English
The equivalence is an equivalence of $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ and $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$.
CategoryTheory.Preadditive.DoldKan.ΓdefMathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive, function or constantEnglish
$\mathrm{CategoryTheory\_\_Preadditive\_\_DoldKan\_\_\_u393\_}$ is a functor of $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ defined as $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$.
CategoryTheory.Idempotents.DoldKan.NdefMathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian, function or constantEnglish
$\operatorname{N}$ is a functor of the set of simplicial objects of $C$ and the set of chain complexes of $C$ and $\Natural$ defined as the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and the inverse of the equivalence of the set of chain complexes of $C$ and $\Natural$.
CategoryTheory.Idempotents.DoldKan.equivalencedefMathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian, function or constantWording
the equivalence (from the name)
English
The equivalence is an equivalence of the set of simplicial objects of $C$ and the set of chain complexes of $C$ and $\Natural$ defined as the equivalence of the isomorphism and the isomorphism.
CategoryTheory.Idempotents.DoldKan.isoN₁defMathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian, function or constantWording
the isomorphism (from the name)
English
The isomorphism is an isomorphism of the composition of the functor of the equivalence of the set of simplicial objects of $C$ and the functor of the equivalence and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ defined as the canonical isomorphism.
CategoryTheory.Idempotents.DoldKan.isoΓ₀defMathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian, function or constantWording
the isomorphism (from the name)
English
The isomorphism is an isomorphism of the composition of the functor of the equivalence of the set of chain complexes of $C$ and $\Natural$ and the inverse of the equivalence and the composition of $\mathrm{CategoryTheory\_\_Idempotents\_\_DoldKan\_\_\_u393\_}$ and the functor of the equivalence of the set of simplicial objects of $C$ defined as the application of $\mathrm{CategoryTheory\_\_Idempotents\_\_functorExtension\_u2082\_CompWhiskeringLeftToKaroubiIso}$ applied to the set of chain complexes of $C$ and $\Natural$ and the set of simplicial objects of $C$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_}$.
CategoryTheory.Idempotents.DoldKan.ΓdefMathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian, function or constantEnglish
$\mathrm{CategoryTheory\_\_Idempotents\_\_DoldKan\_\_\_u393\_}$ is a functor of the set of chain complexes of $C$ and $\Natural$ and the set of simplicial objects of $C$ defined as $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_}$.
CategoryTheory.Idempotents.DoldKan.εdefMathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian, function or constantEnglish
$\mathrm{CategoryTheory\_\_Idempotents\_\_DoldKan\_\_\_u3b5\_}$ is an isomorphism of the identity of the set of simplicial objects of $C$ and the composition of $\operatorname{N}$ and $\mathrm{CategoryTheory\_\_Idempotents\_\_DoldKan\_\_\_u393\_}$ defined as the equivalence unit isomorphism of the isomorphism and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_N\_u2081\_}$.
CategoryTheory.Idempotents.DoldKan.ηdefMathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian, function or constantEnglish
$\mathrm{CategoryTheory\_\_Idempotents\_\_DoldKan\_\_\_u3b7\_}$ is an isomorphism of the composition of $\mathrm{CategoryTheory\_\_Idempotents\_\_DoldKan\_\_\_u393\_}$ and $\operatorname{N}$ and the identity of the set of chain complexes of $C$ and $\Natural$ defined as the counit isomorphism of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_\_u393\_\_u2080\_}$.
AlgebraicTopology.DoldKan.HigherFacesVanishdefMathlib.AlgebraicTopology.DoldKan.Faces, predicateEnglish
Let $q$ be a natural number. Let $x_{2}$ be a homomorphism of $Y$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$. Then $\operatorname{HigherFacesVanish}$ holds for $q$ and $x_{2}$, if for all elements $j$ of $\mathrm{Fin}$ applied to $n + 1$, if $n + 1 \leq \operatorname{val} (j)+ q$, then the composition of $x_{2}$ and $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $\operatorname{succ}$ applied to $j$ is equal to $0$.
AlgebraicTopology.DoldKan.Isδ₀defMathlib.AlgebraicTopology.DoldKan.FunctorGamma, predicateEnglish
Let $i$ be a homomorphism of $x_{1}$ and $x$. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_Is\_u3b4\_\_u2080\_}$ holds for $i$, if the length in $x$ is equal to the sum of the length in $x_{1}$ and $1$ and $\operatorname{toOrderHom} (i , 0)\neq 0$.
AlgebraicTopology.DoldKan.Γ₀defMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_}$ is a functor of the set of chain complexes of $C$ and $\Natural$ and the set of simplicial objects of $C$ defined as the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_'}$ and $\operatorname{forget}$ applied to $C$.
AlgebraicTopology.DoldKan.Γ₀'defMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_'}$ is a functor of the set of chain complexes of $C$ and $\Natural$ and the set of splits of $C$.
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMonodefMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantEnglish
Let $K$ be a chain complex of $C$ and $\Natural$. Let $i$ be a homomorphism of $x_{2}$ and $x_{3}$. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_\_\_Obj\_\_Termwise\_\_mapMono}$ applied to $K$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $K$ and the length in $x_{3}$ and $\operatorname{X}$ applied to $K$ and the length in $x_{2}$.
AlgebraicTopology.DoldKan.Γ₀.Obj.mapdefMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantWording
the map of K and x4 (from the name)
English
Let $K$ be a chain complex of $C$ and $\Natural$. Let $x_{4}$ be a homomorphism of $x_{3}$ and $x_{2}$. Then the map of $K$ and $x_{4}$ is a homomorphism of the object of $K$ and $x_{3}$ and the object of $K$ and $x_{2}$ defined as $\operatorname{desc}$ applied to the function that maps $A$ to the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_\_\_Obj\_\_Termwise\_\_mapMono}$ applied to $K$ and the inclusion of the image of the composition of the opposite of $x_{4}$ and $\operatorname{e}$ applied to $A$ and the inclusion of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_\_\_Obj\_\_summand}$ applied to $x_{2}$ and $\operatorname{pull}$ applied to $A$ and $x_{4}$.
AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂defMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantWording
the object of K and x2 (from the name)
English
Let $K$ be a chain complex of $C$ and $\Natural$. Let $x_{2}$ be an opposite of the set of simplex categories. Then the object of $K$ and $x_{2}$ is an element of $C$ defined as the sigma object of the function that maps $A$ to the summand of $x_{2}$ and $A$.
AlgebraicTopology.DoldKan.Γ₀.Obj.summanddefMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantWording
the summand of x2 and A (from the name)
English
Let $K$ be a chain complex of $C$ and $\Natural$. Let $x_{2}$ be an opposite of the set of simplex categories. Let $A$ be an index set of $x_{2}$. Then the summand of $x_{2}$ and $A$ is an element of $C$ defined as $\operatorname{X}$ applied to $K$ and the length in the opposite of $\operatorname{fst}$ applied to $A$.
AlgebraicTopology.DoldKan.Γ₀.mapdefMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantWording
the map of f (from the name)
English
Let $f$ be a homomorphism of $K$ and $\mathrm{K'}$. Then the map of $f$ is a homomorphism of the object of $K$ and the object of $\mathrm{K'}$.
AlgebraicTopology.DoldKan.Γ₀.objdefMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantWording
the object of K (from the name)
English
Let $K$ be a chain complex of $C$ and $\Natural$. Then the object of $K$ is a simplicial object of $C$.
AlgebraicTopology.DoldKan.Γ₀.splittingdefMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantWording
the splitting of K (from the name)
English
Let $K$ be a chain complex of $C$ and $\Natural$. Then the splitting of $K$ is a splitting of the object of $K$.
AlgebraicTopology.DoldKan.Γ₂defMathlib.AlgebraicTopology.DoldKan.FunctorGamma, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ is a functor of $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ defined as the action of the canonical functor of the set of chain complexes of $C$ and $\Natural$ and the set of simplicial objects of $C$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_}$.
AlgebraicTopology.DoldKan.N₁defMathlib.AlgebraicTopology.DoldKan.FunctorN, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ is a functor of the set of simplicial objects of $C$ and $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$.
AlgebraicTopology.DoldKan.N₂defMathlib.AlgebraicTopology.DoldKan.FunctorN, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ is a functor of $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ and $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$ defined as the action of the canonical functor of the set of simplicial objects of $C$ and the set of chain complexes of $C$ and $\Natural$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$.
AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁defMathlib.AlgebraicTopology.DoldKan.FunctorN, function or constantWording
the canonical isomorphism (from the docstring)
English
The canonical isomorphism is an isomorphism of the composition of $\operatorname{toKaroubi}$ applied to the set of simplicial objects of $C$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ defined as the application of $\mathrm{CategoryTheory\_\_Idempotents\_\_functorExtension\_u2081\_CompWhiskeringLeftToKaroubiIso}$ applied to the set of simplicial objects of $C$ and the set of chain complexes of $C$ and $\Natural$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$.
AlgebraicTopology.DoldKan.N₁Γ₀defMathlib.AlgebraicTopology.DoldKan.GammaCompN, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_\_u393\_\_u2080\_}$ is an isomorphism of the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and $\operatorname{toKaroubi}$ applied to the set of chain complexes of $C$ and $\Natural$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the associator of $\operatorname{forget}$ applied to $C$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and the left isomorphism whisker of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_'}$ and the inverse of $\mathrm{CategoryTheory\_\_SimplicialObject\_\_Split\_\_toKaroubiNondegComplexFunctorIsoN\_u2081\_}$ and the inverse of the associator of $\operatorname{nondegComplexFunctor}$ and $\operatorname{toKaroubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and the right isomorphism whisker of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_'CompNondegComplexFunctor}$ and $\operatorname{toKaroubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and the left unitor of $\operatorname{toKaroubi}$ applied to the set of chain complexes of $C$ and $\Natural$.
AlgebraicTopology.DoldKan.N₂Γ₂defMathlib.AlgebraicTopology.DoldKan.GammaCompN, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_\_u393\_\_u2082\_}$ is an isomorphism of the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and the identity of $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$ defined as the preimage isomorphism of the action of the left whiskering of $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and $\operatorname{toKaroubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_\_u393\_\_u2082\_ToKaroubiIso}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_\_u393\_\_u2080\_}$.
AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIsodefMathlib.AlgebraicTopology.DoldKan.GammaCompN, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_\_u393\_\_u2082\_ToKaroubiIso}$ is an isomorphism of the composition of $\operatorname{toKaroubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the associator of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and the right isomorphism whisker of the application of $\mathrm{CategoryTheory\_\_Idempotents\_\_functorExtension\_u2082\_CompWhiskeringLeftToKaroubiIso}$ applied to the set of chain complexes of $C$ and $\Natural$ and the set of simplicial objects of $C$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and the associator of $\operatorname{toKaroubi}$ applied to the set of simplicial objects of $C$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and the left isomorphism whisker of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_}$ and the application of $\mathrm{CategoryTheory\_\_Idempotents\_\_functorExtension\_u2081\_CompWhiskeringLeftToKaroubiIso}$ applied to the set of simplicial objects of $C$ and the set of chain complexes of $C$ and $\Natural$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$.
AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctordefMathlib.AlgebraicTopology.DoldKan.GammaCompN, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_'CompNondegComplexFunctor}$ is an isomorphism of the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2080\_'}$ and $\operatorname{nondegComplexFunctor}$ and the identity of the set of chain complexes of $C$ and $\Natural$.
AlgebraicTopology.DoldKan.Γ₀NondegComplexIsodefMathlib.AlgebraicTopology.DoldKan.GammaCompN, function or constantWording
the isomorphism of K (from the docstring)
English
Let $K$ be a chain complex of $C$ and $\Natural$. Then the isomorphism of $K$ is an isomorphism of $\operatorname{nondegComplex}$ applied to the splitting of $K$ and $K$.
AlgebraicTopology.DoldKan.HσdefMathlib.AlgebraicTopology.DoldKan.Homotopies, function or constantEnglish
Let $q$ be a natural number. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_H\_u3c3\_}$ applied to $q$ is a homomorphism of the object of $X$ and the object of $X$ defined as the null homotopic map of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_h\_u3c3\_'}$ applied to $q$.
AlgebraicTopology.DoldKan.cdefMathlib.AlgebraicTopology.DoldKan.Homotopies, function or constantEnglish
$\operatorname{c}$ is a complex shape of $\Natural$ defined as $\operatorname{down}$ applied to $\Natural$.
AlgebraicTopology.DoldKan.homotopyHσToZerodefMathlib.AlgebraicTopology.DoldKan.Homotopies, function or constantWording
the homotopy to zero of q (from the name)
English
Let $q$ be a natural number. Then the homotopy to zero of $q$ is a homotopy of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_H\_u3c3\_}$ applied to $q$ and $0$ defined as the null homotopy of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_h\_u3c3\_'}$ applied to $q$.
AlgebraicTopology.DoldKan.hσdefMathlib.AlgebraicTopology.DoldKan.Homotopies, function or constantEnglish
Let $q$ and $n$ be natural numbers. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_h\_u3c3\_}$ applied to $q$ and $n$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$.
AlgebraicTopology.DoldKan.hσ'defMathlib.AlgebraicTopology.DoldKan.Homotopies, function or constantEnglish
Let $q$, $n$ and $m$ be natural numbers such that $\operatorname{Rel}$ holds for $\operatorname{c}$, $m$ and $n$. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_h\_u3c3\_'}$ applied to $q$, $n$, $m$ and $h$ is a homomorphism of $\operatorname{X}$ applied to the object of $X$ and $n$ and $\operatorname{X}$ applied to the object of $X$ and $m$.
AlgebraicTopology.DoldKan.natTransHσdefMathlib.AlgebraicTopology.DoldKan.Homotopies, function or constantWording
the natural transformation of q (from the name)
English
Let $q$ be a natural number. Then the natural transformation of $q$ is a homomorphism of the alternating face map complex of $C$ and the alternating face map complex of $C$.
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplexdefMathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence, function or constantWording
the inclusion of the Moore complex in the alternating face map complex (from the docstring)
English
The inclusion of the Moore complex in the alternating face map complex is a homotopy equivalence of the action of the normalized Moore complex of $A$ and $Y$ and the action of the alternating face map complex of $A$ and $Y$.
AlgebraicTopology.DoldKan.homotopyPInftyToIddefMathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence, function or constantWording
the homotopy infty to identity of X (from the name)
English
Let $X$ be a simplicial object of $C$. Then the homotopy infty to identity of $X$ is a homotopy of the infty and the identity morphism of the object of $X$.
AlgebraicTopology.DoldKan.homotopyPToIddefMathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence, function or constantWording
the homotopy to identity of X and q (from the name)
English
Let $X$ be a simplicial object of $C$. Let $q$ be a natural number. Then the homotopy to identity of $X$ and $q$ is a homotopy of $\operatorname{P}$ applied to $q$ and the identity morphism of the object of $X$ defined as $\operatorname{brecOn}$ applied to $q$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_homotopyPToId\_\_\_f}$ applied to $X$.
AlgebraicTopology.DoldKan.homotopyQToZerodefMathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence, function or constantWording
the homotopy to zero of X and q (from the name)
English
Let $X$ be a simplicial object of $C$. Let $q$ be a natural number. Then the homotopy to zero of $X$ and $q$ is a homotopy of $\operatorname{Q}$ applied to $q$ and $0$ defined as the forward map of the equivalence difference zero and the inverse of the homotopy to identity of $X$ and $q$.
AlgebraicTopology.DoldKan.Γ₂N₁defMathlib.AlgebraicTopology.DoldKan.NCompGamma, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_N\_u2081\_}$ is an isomorphism of $\operatorname{toKaroubi}$ applied to the set of simplicial objects of $C$ and the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ defined as the inverse of $\operatorname{asIso}$ applied to the natural transformation.
AlgebraicTopology.DoldKan.Γ₂N₁.natTransdefMathlib.AlgebraicTopology.DoldKan.NCompGamma, function or constantWording
the natural transformation (from the docstring)
English
The natural transformation is a homomorphism of the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ and $\operatorname{toKaroubi}$ applied to the set of simplicial objects of $C$.
AlgebraicTopology.DoldKan.Γ₂N₂defMathlib.AlgebraicTopology.DoldKan.NCompGamma, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_N\_u2082\_}$ is an isomorphism of the identity of $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ and the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ defined as the inverse of $\operatorname{asIso}$ applied to the natural transformation.
AlgebraicTopology.DoldKan.Γ₂N₂.natTransdefMathlib.AlgebraicTopology.DoldKan.NCompGamma, function or constantWording
the natural transformation (from the docstring)
English
The natural transformation is a homomorphism of the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ and the identity of $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ defined as the choice of the action of the left whiskering of $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ and $\operatorname{Karoubi}$ applied to the set of simplicial objects of $C$ and $\operatorname{toKaroubi}$ applied to the set of simplicial objects of $C$ and the composition of the homomorphism of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_N\_u2082\_ToKaroubiIso}$ and the natural transformation.
AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIsodefMathlib.AlgebraicTopology.DoldKan.NCompGamma, function or constantEnglish
$\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_N\_u2082\_ToKaroubiIso}$ is an isomorphism of the composition of $\operatorname{toKaroubi}$ applied to the set of simplicial objects of $C$ and the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ and the composition of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ defined as the composition of the inverse of the associator of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2082\_}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$ and the right isomorphism whisker of the canonical isomorphism and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_\_u393\_\_u2082\_}$.
AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubidefMathlib.AlgebraicTopology.DoldKan.Normalized, function or constantEnglish
Let $A$ be a set. Then $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_\_iso\_normalizedMooreComplex\_comp\_toKaroubi}$ applied to $A$ is an isomorphism of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and the composition of the normalized Moore complex of $A$ and $\operatorname{toKaroubi}$ applied to the set of chain complexes of $A$ and $\Natural$.
AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplexdefMathlib.AlgebraicTopology.DoldKan.Normalized, function or constantWording
the infty to normalized Moore complex of X (from the name)
English
Let $X$ be a simplicial object of $A$. Then the infty to normalized Moore complex of $X$ is a homomorphism of the object of $X$ and the object of $X$.
AlgebraicTopology.DoldKan.splitMonoInclusionOfMooreComplexMapdefMathlib.AlgebraicTopology.DoldKan.Normalized, function or constantWording
the split monotone inclusion of X (from the name)
English
Let $X$ be a simplicial object of $A$. Then the split monotone inclusion of $X$ is a split monomorphism of the inclusion of $X$.
AlgebraicTopology.DoldKan.PInftydefMathlib.AlgebraicTopology.DoldKan.PInfty, function or constantWording
the infty (from the name)
English
The infty is a homomorphism of the object of $X$ and the object of $X$.
AlgebraicTopology.DoldKan.QInftydefMathlib.AlgebraicTopology.DoldKan.PInfty, function or constantWording
the infty (from the name)
English
The infty is a homomorphism of the object of $X$ and the object of $X$ defined as the difference between the identity morphism of the object of $X$ and the infty.
AlgebraicTopology.DoldKan.natTransPInftydefMathlib.AlgebraicTopology.DoldKan.PInfty, function or constantWording
the natural transformation infty of C (from the name)
English
Let $C$ be a set. Then the natural transformation infty of $C$ is a homomorphism of the alternating face map complex of $C$ and the alternating face map complex of $C$.
AlgebraicTopology.DoldKan.natTransPInfty_fdefMathlib.AlgebraicTopology.DoldKan.PInfty, function or constantWording
the natural transformation of C and n (from the docstring)
English
Let $C$ be a set. Let $n$ be a natural number. Then the natural transformation of $C$ and $n$ is a homomorphism of the composition of the alternating face map complex of $C$ and the evaluation of $\operatorname{down}$ applied to $\Natural$ and $n$ and the composition of the alternating face map complex of $C$ and the evaluation of $\operatorname{down}$ applied to $\Natural$ and $n$ defined as $\operatorname{hcomp}$ applied to the natural transformation infty of $C$ and the identity morphism of the evaluation of $\operatorname{down}$ applied to $\Natural$ and $n$.
AlgebraicTopology.DoldKan.PdefMathlib.AlgebraicTopology.DoldKan.Projections, function or constantEnglish
Let $x_{2}$ be a natural number. Then $\operatorname{P}$ applied to $x_{2}$ is a homomorphism of the object of $X$ and the object of $X$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_P\_\_\_f}$.
AlgebraicTopology.DoldKan.QdefMathlib.AlgebraicTopology.DoldKan.Projections, function or constantEnglish
Let $q$ be a natural number. Then $\operatorname{Q}$ applied to $q$ is a homomorphism of the object of $X$ and the object of $X$ defined as the difference between the identity morphism of the object of $X$ and $\operatorname{P}$ applied to $q$.
AlgebraicTopology.DoldKan.natTransPdefMathlib.AlgebraicTopology.DoldKan.Projections, function or constantWording
the natural transformation of q (from the name)
English
Let $q$ be a natural number. Then the natural transformation of $q$ is a homomorphism of the alternating face map complex of $C$ and the alternating face map complex of $C$.
AlgebraicTopology.DoldKan.natTransQdefMathlib.AlgebraicTopology.DoldKan.Projections, function or constantWording
the natural transformation of q (from the name)
English
Let $q$ be a natural number. Then the natural transformation of $q$ is a homomorphism of the alternating face map complex of $C$ and the alternating face map complex of $C$.
CategoryTheory.SimplicialObject.Split.nondegComplexFunctordefMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantEnglish
$\operatorname{nondegComplexFunctor}$ is a functor of the set of splits of $C$ and the set of chain complexes of $C$ and $\Natural$.
CategoryTheory.SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁defMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantEnglish
$\mathrm{CategoryTheory\_\_SimplicialObject\_\_Split\_\_toKaroubiNondegComplexFunctorIsoN\_u2081\_}$ is an isomorphism of the composition of $\operatorname{nondegComplexFunctor}$ and $\operatorname{toKaroubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and the composition of $\operatorname{forget}$ applied to $C$ and $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$.
CategoryTheory.SimplicialObject.Splitting.ddefMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantEnglish
Let $s$ be a splitting of $X$. Let $i$ and $j$ be natural numbers. Then $\operatorname{d}$ applied to $s$, $i$ and $j$ is a homomorphism of $\operatorname{N}$ applied to $s$ and $i$ and $\operatorname{N}$ applied to $s$ and $j$ defined as the composition of the injection of the cofan of $s$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $i$ and the identity of $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $i$ and the composition of $\operatorname{d}$ applied to the object of $X$, $i$ and $j$ and the projection summand of $s$ and the identity of $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $j$.
CategoryTheory.SimplicialObject.Splitting.fromNondegComplexdefMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantEnglish
Let $s$ be a splitting of $X$. Then $\operatorname{fromNondegComplex}$ applied to $s$ is a homomorphism of $\operatorname{nondegComplex}$ applied to $s$ and the object of $X$.
CategoryTheory.SimplicialObject.Splitting.homotopyEquivNondegComplexdefMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantEnglish
Let $s$ be a splitting of $X$. Then $\operatorname{homotopyEquivNondegComplex}$ applied to $s$ is a homotopy equivalence of the object of $X$ and $\operatorname{nondegComplex}$ applied to $s$.
CategoryTheory.SimplicialObject.Splitting.nondegComplexdefMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantEnglish
Let $s$ be a splitting of $X$. Then $\operatorname{nondegComplex}$ applied to $s$ is a chain complex of $C$ and $\Natural$.
CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁defMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantWording
the chain complex of s (from the docstring)
English
Let $s$ be a splitting of $X$. Then the chain complex of $s$ is an isomorphism of the action of $\operatorname{toKaroubi}$ applied to the set of chain complexes of $C$ and $\Natural$ and $\operatorname{nondegComplex}$ applied to $s$ and the action of $\mathrm{AlgebraicTopology\_\_DoldKan\_\_N\_u2081\_}$ and $X$.
CategoryTheory.SimplicialObject.Splitting.toNondegComplexdefMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantEnglish
Let $s$ be a splitting of $X$. Then $\operatorname{toNondegComplex}$ applied to $s$ is a homomorphism of the object of $X$ and $\operatorname{nondegComplex}$ applied to $s$.
CategoryTheory.SimplicialObject.Splitting.πSummanddefMathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject, function or constantWording
the projection summand of s and A (from the name)
English
Let $s$ be a splitting of $X$. Let $A$ be an index set of $x_{2}$. Then the projection summand of $s$ and $A$ is a homomorphism of the action of $X$ and $x_{2}$ and $\operatorname{N}$ applied to $s$ and the length in the opposite of $\operatorname{fst}$ applied to $A$.
TopPair.HomologyPretheorystructureMathlib.AlgebraicTopology.EilenbergSteenrod, typeEnglish
Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Then the elements of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$ are a basic type.
TopPair.HomologyPretheory.HdefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$. Let $i$ be an element of $x_{2}$. Then $\operatorname{H}$ applied to $\mathrm{self}$ and $i$ is a functor of the set of topological categories and $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.
TopPair.HomologyPretheory.HomstructureMathlib.AlgebraicTopology.EilenbergSteenrod, typeWording
homomorphism of HP and #2 (from the name)
English
Let $\mathrm{HP}$ and $\mathrm{HP'}$ be elements of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$. Then the homomorphisms of $\mathrm{HP}$ and $\mathrm{HP'}$ are a basic type.
TopPair.HomologyPretheory.Hom.homdefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantWording
the homomorphism of self and i (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $\mathrm{HP}$ and $\mathrm{HP'}$. Let $i$ be an element of $x_{2}$. Then the homomorphism of $\mathrm{self}$ and $i$ is a homomorphism of $\operatorname{H}$ applied to $\mathrm{HP}$ and $i$ and $\operatorname{H}$ applied to $\mathrm{HP'}$ and $i$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.
TopPair.HomologyPretheory.Hom.homₚdefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantWording
the homomorphism of self and i (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $\mathrm{HP}$ and $\mathrm{HP'}$. Let $i$ be an element of $x_{2}$. Then the homomorphism of $\mathrm{self}$ and $i$ is a homomorphism of $\mathrm{TopPair\_\_HomologyPretheory\_\_H\_u209a\_}$ applied to $\mathrm{HP}$ and $i$ and $\mathrm{TopPair\_\_HomologyPretheory\_\_H\_u209a\_}$ applied to $\mathrm{HP'}$ and $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.
TopPair.HomologyPretheory.HₚdefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$. Let $i$ be an element of $x_{2}$. Then $\mathrm{TopPair\_\_HomologyPretheory\_\_H\_u209a\_}$ applied to $\mathrm{self}$ and $i$ is a functor of the set of top pairs and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.
TopPair.HomologyPretheory.IsHomotopyInvariantclassMathlib.AlgebraicTopology.EilenbergSteenrod, predicateWording
HP is a homotopy invariant (from the name)
English
Let $\mathrm{HP}$ be an element of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$. Then we can say that $\mathrm{HP}$ is a homotopy invariant.
TopPair.HomologyPretheory.hFunctordefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantWording
the functor of i (from the name)
English
Let $i$ be an element of $x_{2}$. Then the functor of $i$ is a functor of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$ and the set of functors of the set of topological categories and $C$.
TopPair.HomologyPretheory.hₚFunctordefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantWording
the functor of i (from the name)
English
Let $i$ be an element of $x_{2}$. Then the functor of $i$ is a functor of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$ and the set of functors of the set of top pairs and $C$.
TopPair.HomologyPretheory.isHomotopyInvariantdefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantEnglish
Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Then there is an object property of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$. Proof. Let $C$ be arbitrary. Let $c$ be arbitrary. By TopPair__HomologyPretheory__IsHomotopyInvariant.
TopPair.HomologyPretheory.isodefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantWording
the isomorphism of self and i (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$. Let $i$ be an element of $x_{2}$. Then the isomorphism of $\mathrm{self}$ and $i$ is an isomorphism of $\operatorname{H}$ applied to $\mathrm{self}$ and $i$ and the composition of the inclusion and $\mathrm{TopPair\_\_HomologyPretheory\_\_H\_u209a\_}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $i$.
TopPair.HomologyPretheory.δdefMathlib.AlgebraicTopology.EilenbergSteenrod, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{HomologyPretheory}$ applied to $C$ and $c$. Let $i$ and $j$ be elements of $x_{2}$. Then $\mathrm{TopPair\_\_HomologyPretheory\_\_\_u3b4\_}$ applied to $\mathrm{self}$, $i$ and $j$ is a homomorphism of $\mathrm{TopPair\_\_HomologyPretheory\_\_H\_u209a\_}$ applied to $\mathrm{self}$ and $i$ and the composition of the projection and $\operatorname{H}$ applied to $\mathrm{self}$ and $j$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $i$ and $j$.
SSet.Augmented.StandardSimplex.extraDegeneracydefMathlib.AlgebraicTopology.ExtraDegeneracy, function or constantWording
the obvious extra degeneracy on the standard simplex of x (from the docstring)
English
Let $x$ be a simplex category. Then the obvious extra degeneracy on the standard simplex of $x$ is an extra degeneracy of the action of $\operatorname{stdSimplex}$ and $x$.
SSet.Augmented.StandardSimplex.shiftdefMathlib.AlgebraicTopology.ExtraDegeneracy, function or constantWording
the shift of f (from the docstring)
English
Let $f$ be a homomorphism of $\operatorname{mk}$ applied to $n$ and $x$. Then the shift of $f$ is a homomorphism of $\operatorname{mk}$ applied to $n + 1$ and $x$.
SSet.Augmented.StandardSimplex.shiftFundefMathlib.AlgebraicTopology.ExtraDegeneracy, function or constantWording
the shift function of f and i (from the name)
English
Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $X$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the shift function of $f$ and $i$ is an element of $X$ defined as $\operatorname{vecCons}$ applied to $0$, $f$ and $i$.
FundamentalGroupoidstructureMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, typeWording
fundamental groupoid of X (from the name)
English
Let $X$ be a set. Then the fundamental groupoids of $X$ are a basic type.
FundamentalGroupoid.asdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantEnglish
Let $\mathrm{self}$ be a fundamental groupoid of $X$. Then $\operatorname{as}$ applied to $\mathrm{self}$ is an element of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
FundamentalGroupoid.equivdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the equivalence of X (from the name)
English
Let $X$ be a set. Then the equivalence of $X$ is an equivalence from the set of fundamental groupoids of $X$ to $X$.
FundamentalGroupoid.fromPathdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantEnglish
Let $p$ be a quotient of $x_{1}$ and $x_{2}$. Then $\operatorname{fromPath}$ applied to $p$ is a homomorphism of $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{mk}$ applied to $x_{2}$ defined as $p$.
FundamentalGroupoid.fromTopdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantEnglish
Let $x$ be a carrier of $X$. Then $\operatorname{fromTop}$ applied to $x$ is an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $X$ defined as $\operatorname{mk}$ applied to $x$.
FundamentalGroupoid.fundamentalGroupoidFunctordefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the fundamental groupoid functor (from the name)
English
The fundamental groupoid functor is a functor of the set of topological categories and $\operatorname{Grpd}$.
FundamentalGroupoid.mapdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the functor on fundamental groupoid induced by a continuous map of f (from the docstring)
English
Let $f$ be a continuous map of $X$ and $Y$. Then the functor on fundamental groupoid induced by a continuous map of $f$ is a functor of the set of fundamental groupoids of $X$ and the set of fundamental groupoids of $Y$.
FundamentalGroupoid.toPathdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the path of p (from the name)
English
Let $p$ be a homomorphism of $x$ and $x_{1}$. Then the path of $p$ is a quotient of $\operatorname{as}$ applied to $x$ and $\operatorname{as}$ applied to $x_{1}$ defined as $p$.
FundamentalGroupoid.toTopdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the top of x (from the name)
English
Let $x$ be an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $X$. Then the top of $x$ is a carrier of $X$ defined as $\operatorname{as}$ applied to $x$.
Path.Homotopy.reflSymmTransdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the identity inverse composition of p (from the name)
English
Let $p$ be a path of $x_{1}$ and $x_{2}$. Then the identity inverse composition of $p$ is a homotopy of the identity of $x_{2}$ and the composition of the inverse of $p$ and $p$.
Path.Homotopy.reflTransdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the identity composition of p (from the name)
English
Let $p$ be a path of $x_{1}$ and $x_{2}$. Then the identity composition of $p$ is a homotopy of the composition of the identity of $x_{1}$ and $p$ and $p$.
Path.Homotopy.reflTransSymmdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the identity composition inverse of p (from the name)
English
Let $p$ be a path of $x_{1}$ and $x_{2}$. Then the identity composition inverse of $p$ is a homotopy of the identity of $x_{1}$ and the composition of $p$ and the inverse of $p$.
Path.Homotopy.transAssocdefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the composition associator of q and r (from the name)
English
Let $p$ be a path of $x_{1}$ and $x_{2}$. Let $q$ be a path of $x_{2}$ and $x_{3}$. Let $r$ be a path of $x_{3}$ and $x_{4}$. Then the composition associator of $q$ and $r$ is a homotopy of the composition of the composition of $p$ and $q$ and $r$ and the composition of $p$ and the composition of $q$ and $r$.
Path.Homotopy.transRefldefMathlib.AlgebraicTopology.FundamentalGroupoid.Basic, function or constantWording
the composition identity of p (from the name)
English
Let $p$ be a path of $x_{1}$ and $x_{2}$. Then the composition identity of $p$ is a homotopy of the composition of $p$ and the identity of $x_{2}$ and $p$.
FundamentalGroupdefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, typeWording
fundamental group of X and x1 (from the name)
English
Let $X$ be a set. Let $x_{1}$ be an element of $X$. Then a fundamental group of $X$ and $x_{1}$ is an element of the function that maps $X$ and $x_{1}$ to the set of ends of $\operatorname{mk}$ applied to $x_{1}$.
FundamentalGroup.fromArrowdefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, function or constantEnglish
Let $p$ be a homomorphism of $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{mk}$ applied to $x_{1}$. Then $\operatorname{fromArrow}$ applied to $p$ is a fundamental group of $X$ and $x_{1}$ defined as $\operatorname{of}$ applied to $p$.
FundamentalGroup.fromPathdefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, function or constantEnglish
Let $p$ be a quotient of $x_{1}$ and $x_{1}$. Then $\operatorname{fromPath}$ applied to $p$ is a fundamental group of $X$ and $x_{1}$ defined as $\operatorname{fromArrow}$ applied to $p$.
FundamentalGroup.fundamentalGroupMulEquivOfPathdefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, function or constantWording
the fundamental group multiplicative equivalence of p (from the name)
English
Let $p$ be a path of $x_{1}$ and $x_{2}$. Then the fundamental group multiplicative equivalence of $p$ is a multiplicative equivalence of the set of fundamental groups of $X$ and $x_{1}$ and the set of fundamental groups of $X$ and $x_{2}$ defined as the conjugate of $\operatorname{symm}$ applied to the isomorphism equivalence homomorphism of $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{mk}$ applied to $x_{2}$ and $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $\operatorname{as}$ applied to $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{as}$ applied to $\operatorname{mk}$ applied to $x_{2}$ and $p$.
FundamentalGroup.fundamentalGroupMulEquivOfPathConnecteddefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, function or constantWording
the fundamental group of x1 and x2 (from the docstring)
English
Let $x_{1}$ and $x_{2}$ be elements of $X$. Then the fundamental group of $x_{1}$ and $x_{2}$ is a multiplicative equivalence of the set of fundamental groups of $X$ and $x_{1}$ and the set of fundamental groups of $X$ and $x_{2}$ defined as the fundamental group multiplicative equivalence of $\operatorname{somePath}$ applied to $x_{1}$ and $x_{2}$.
FundamentalGroup.mapdefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, function or constantWording
the map of f and x2 (from the name)
English
Let $f$ be a continuous map of $X$ and $Y$. Let $x_{2}$ be an element of $X$. Then the map of $f$ and $x_{2}$ is a monoid homomorphism of the set of fundamental groups of $X$ and $x_{2}$ and the set of fundamental groups of $Y$ and $f$ applied to $x_{2}$ defined as the map end of $\operatorname{mk}$ applied to $x_{2}$ and the functor on fundamental groupoid induced by a continuous map of $f$.
FundamentalGroup.mapOfEqdefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, function or constantWording
the map of f and h (from the name)
English
Let $f$ be a continuous map of $X$ and $Y$ such that $\EqtMACRoH {f (x_{2})}{y}$. Then the map of $f$ and $h$ is a monoid homomorphism of the set of fundamental groups of $X$ and $x_{2}$ and the set of fundamental groups of $Y$ and $y$.
FundamentalGroup.toArrowdefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, function or constantWording
the arrow of p (from the name)
English
Let $p$ be a fundamental group of $X$ and $x_{1}$. Then the arrow of $p$ is a homomorphism of $\operatorname{mk}$ applied to $x_{1}$ and $\operatorname{mk}$ applied to $x_{1}$ defined as $\operatorname{asHom}$ applied to $p$.
FundamentalGroup.toPathdefMathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup, function or constantWording
the path of p (from the name)
English
Let $p$ be a fundamental group of $X$ and $x_{1}$. Then the path of $p$ is a quotient of $x_{1}$ and $x_{1}$ defined as the arrow of $p$.
ContinuousMap.Homotopy.diagonalPathdefMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantWording
the diagonal path of H and p (from the docstring)
English
Let $H$ be a homotopy of $f$ and $g$. Let $p$ be a homomorphism of $\operatorname{fromTop}$ applied to $x$ and $\operatorname{fromTop}$ applied to $x_{1}$. Then the diagonal path of $H$ and $p$ is a homomorphism of $\operatorname{fromTop}$ applied to $H$ applied to $\ProdmkMACRoU {0}{x}$ and $\operatorname{fromTop}$ applied to $H$ applied to $\ProdmkMACRoU {1}{x_{1}}$ defined as the map of the map of the fundamental groupoid functor and the topological category of the lift map of $H$ and the product to product top of $\operatorname{uhpath01}$ and $p$.
ContinuousMap.Homotopy.diagonalPath'defMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantWording
the diagonal path of H and p (from the name)
English
Let $H$ be a homotopy of $f$ and $g$. Let $p$ be a homomorphism of $\operatorname{fromTop}$ applied to $x$ and $\operatorname{fromTop}$ applied to $x_{1}$. Then the diagonal path of $H$ and $p$ is a homomorphism of $\operatorname{fromTop}$ applied to $f$ applied to $x$ and $\operatorname{fromTop}$ applied to $g$ applied to $x_{1}$.
ContinuousMap.Homotopy.hcastdefMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantEnglish
Assume that $\EqtMACRoH {x}{x_{1}}$. Then $\operatorname{hcast}$ applied to $\mathrm{hx}$ is a homomorphism of $\operatorname{fromTop}$ applied to $x$ and $\operatorname{fromTop}$ applied to $x_{1}$.
ContinuousMap.Homotopy.prodToProdTopIdefMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantWording
the product to product top of x4 and x5 (from the name)
English
Let $x_{4}$ be a homomorphism of $\operatorname{fromTop}$ applied to $x$ and $\operatorname{fromTop}$ applied to $x_{1}$. Let $x_{5}$ be a homomorphism of $\operatorname{fromTop}$ applied to $x_{2}$ and $\operatorname{fromTop}$ applied to $x_{3}$. Then the product to product top of $x_{4}$ and $x_{5}$ is a homomorphism of the action of the product to product top of $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of elements of the unit interval and $X$ and $\ProdmkMACRoU {\operatorname{mk} (x)}{\operatorname{mk} (x_{2})}$ and the action of the product to product top of $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of elements of the unit interval and $X$ and $\ProdmkMACRoU {\operatorname{mk} (x_{1})}{\operatorname{mk} (x_{3})}$ defined as the map of the product to product top of $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of elements of the unit interval and $X$ and $\ProdmkMACRoU {x_{4}}{x_{5}}$.
ContinuousMap.Homotopy.uliftMapdefMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantWording
the lift map of H (from the name)
English
Let $H$ be a homotopy of $f$ and $g$. Then the lift map of $H$ is a continuous map of the set of carriers of $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to $\mathrm{ULift}$ applied to the set of elements of the unit interval and the set of carriers of $X$ and the set of carriers of $Y$.
FundamentalGroupoidFunctor.equivOfHomotopyEquivdefMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantWording
the equivalence of hequiv (from the name)
English
Let $\mathrm{hequiv}$ be a homotopy equivalence of $X$ and $Y$. Then the equivalence of $\mathrm{hequiv}$ is an equivalence of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $\operatorname{of}$ applied to $X$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $\operatorname{of}$ applied to $Y$.
FundamentalGroupoidFunctor.homotopicMapsNatIsodefMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantWording
the homotopic map natural isomorphism of H (from the name)
English
Let $H$ be a homotopy of $f$ and $g$. Then the homotopic map natural isomorphism of $H$ is a homomorphism of the functor on fundamental groupoid induced by a continuous map of $f$ and the functor on fundamental groupoid induced by a continuous map of $g$.
unitInterval.uhpath01defMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantEnglish
$\operatorname{uhpath01}$ is a homomorphism of $\operatorname{fromTop}$ applied to $\operatorname{up}$ applied to $0$ and $\operatorname{fromTop}$ applied to $\operatorname{up}$ applied to $1$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $\operatorname{as}$ applied to $\operatorname{fromTop}$ applied to $\operatorname{up}$ applied to $0$ and $\operatorname{as}$ applied to $\operatorname{fromTop}$ applied to $\operatorname{up}$ applied to $1$ and $\operatorname{upath01}$.
unitInterval.upath01defMathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps, function or constantEnglish
$\operatorname{upath01}$ is a path of $\operatorname{up}$ applied to $0$ and $\operatorname{up}$ applied to $1$.
FundamentalGroupoid.punitEquivDiscretePUnitdefMathlib.AlgebraicTopology.FundamentalGroupoid.PUnit, function or constantEnglish
$\operatorname{punitEquivDiscretePUnit}$ is an equivalence of the set of fundamental groupoids of $\mathrm{PUnit}$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$.
FundamentalGroupoidFunctor.coneDiscreteCompdefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the cone discrete composition of X (from the name)
English
Let $X$ be a function from elements of $I$ to topological categories. Then the cone discrete composition of $X$ is an equivalence of the set of cones of the composition of the functor of $X$ and the fundamental groupoid functor and the set of cones of the functor of the function that maps $i$ to the action of the fundamental groupoid functor and $X$ applied to $i$ defined as the postcomposition equivalence of $\operatorname{compNatIsoDiscrete}$ applied to $X$ and the fundamental groupoid functor.
FundamentalGroupoidFunctor.piIsodefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the product isomorphism of X (from the name)
English
Let $X$ be a function from elements of $I$ to topological categories. Then the product isomorphism of $X$ is an isomorphism of $\operatorname{of}$ applied to the set of functions from elements $i$ of $I$ to elements of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $X$ applied to $i$ and the action of the fundamental groupoid functor and $\operatorname{of}$ applied to the set of functions from elements $i_{1}$ of $I$ to carriers of $X$ applied to $i_{1}$.
FundamentalGroupoidFunctor.piToPiTopdefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the product to product top of X (from the name)
English
Let $X$ be a function from elements of $I$ to topological categories. Then the product to product top of $X$ is a functor of the set of functions from elements $i$ of $I$ to elements of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $X$ applied to $i$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $\operatorname{of}$ applied to the set of functions from elements $i_{1}$ of $I$ to carriers of $X$ applied to $i_{1}$.
FundamentalGroupoidFunctor.piTopToPiConedefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the product top to product cone of X (from the name)
English
Let $X$ be a function from elements of $I$ to topological categories. Then the product top to product cone of $X$ is a homomorphism of $\operatorname{mk}$ applied to the action of the fundamental groupoid functor and $\operatorname{of}$ applied to the set of functions from elements $i$ of $I$ to carriers of $X$ applied to $i$ and $\operatorname{proj}$ applied to $X$ and $\operatorname{piLimitFan}$ applied to the function that maps $i_{1}$ to the action of the fundamental groupoid functor and $X$ applied to $i_{1}$.
FundamentalGroupoidFunctor.prodIsodefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the product isomorphism of A and B (from the name)
English
Let $A$ and $B$ be topological categories. Then the product isomorphism of $A$ and $B$ is an isomorphism of $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $A$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $B$ and the action of the fundamental groupoid functor and $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of carriers of $A$ and the set of carriers of $B$.
FundamentalGroupoidFunctor.prodToProdTopdefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the product to product top of A and B (from the name)
English
Let $A$ and $B$ be topological categories. Then the product to product top of $A$ and $B$ is a functor of $\mathrm{Prod}$ applied to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $A$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $B$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of carriers of $A$ and the set of carriers of $B$.
FundamentalGroupoidFunctor.projdefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the projection of X and i (from the name)
English
Let $X$ be a function from elements of $I$ to topological categories. Let $i$ be an element of $I$. Then the projection of $X$ and $i$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $\operatorname{of}$ applied to the set of functions from elements $i_{1}$ of $I$ to carriers of $X$ applied to $i_{1}$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $X$ applied to $i$.
FundamentalGroupoidFunctor.projLeftdefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the left projection of A and B (from the name)
English
Let $A$ and $B$ be topological categories. Then the left projection of $A$ and $B$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of carriers of $A$ and the set of carriers of $B$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $A$ defined as the functor on fundamental groupoid induced by a continuous map of the first component.
FundamentalGroupoidFunctor.projRightdefMathlib.AlgebraicTopology.FundamentalGroupoid.Product, function or constantWording
the right projection of A and B (from the name)
English
Let $A$ and $B$ be topological categories. Then the right projection of $A$ and $B$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of carriers of $A$ and the set of carriers of $B$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of the fundamental groupoid functor and $B$ defined as the functor on fundamental groupoid induced by a continuous map of the second component.
IsSimplyConnecteddefMathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected, predicateWording
s is simply connected (from the name)
English
generation took over the time limit
SimplyConnectedSpaceclassMathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected, predicateWording
X is a simply connected space (from the name)
English
generation took over the time limit
HomotopicalAlgebra.ModelCategoryclassMathlib.AlgebraicTopology.ModelCategory.Basic, predicateWording
C is a model category (from the name)
English
Let $C$ be a set. Then we can say that $C$ is a model category.
HomotopicalAlgebra.BifibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, typeWording
bifibrant object of C (from the name)
English
Let $C$ be a set. Then a bifibrant object of $C$ is an element of the function that maps $C$ to the set of full subcategories of the bifibrant object of $C$.
HomotopicalAlgebra.BifibrantObject.homMkdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a homomorphism of $\operatorname{mk}$ applied to $X$ and $\operatorname{mk}$ applied to $Y$ defined as the homomorphism of $f$.
HomotopicalAlgebra.BifibrantObject.mkdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantEnglish
Let $X$ be an element of $C$. Then $\operatorname{mk}$ applied to $X$ is a bifibrant object of $C$.
HomotopicalAlgebra.BifibrantObject.ιdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the inclusion functor (from the docstring)
English
The inclusion functor is a functor of the set of bifibrant objects of $C$ and $C$ defined as the inclusion of the bifibrant object of $C$.
HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the inclusion (from the docstring)
English
The inclusion is a functor of the set of bifibrant objects of $C$ and the set of cofibrant objects of $C$ defined as the inclusion of $\mathrm{HomotopicalAlgebra\_\_bifibrantObjects\_le\_cofibrantObject}$ applied to $C$.
HomotopicalAlgebra.BifibrantObject.ιFibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the inclusion functor (from the docstring)
English
The inclusion functor is a functor of the set of bifibrant objects of $C$ and the set of fibrant objects of $C$ defined as the inclusion of $\mathrm{HomotopicalAlgebra\_\_bifibrantObjects\_le\_fibrantObject}$ applied to $C$.
HomotopicalAlgebra.CofibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, typeWording
cofibrant object of C (from the name)
English
Let $C$ be a set. Then a cofibrant object of $C$ is an element of the function that maps $C$ to the set of full subcategories of the cofibrant object of $C$.
HomotopicalAlgebra.CofibrantObject.homMkdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a homomorphism of $\operatorname{mk}$ applied to $X$ and $\operatorname{mk}$ applied to $Y$ defined as the homomorphism of $f$.
HomotopicalAlgebra.CofibrantObject.mkdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantEnglish
Let $X$ be an element of $C$. Then $\operatorname{mk}$ applied to $X$ is a cofibrant object of $C$ defined as $\operatorname{mk}$ applied to $X$ and $h_{1}$.
HomotopicalAlgebra.CofibrantObject.ιdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the inclusion functor (from the docstring)
English
The inclusion functor is a functor of the set of cofibrant objects of $C$ and $C$ defined as the inclusion of the cofibrant object of $C$.
HomotopicalAlgebra.FibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, typeWording
fibrant object of C (from the name)
English
Let $C$ be a set. Then a fibrant object of $C$ is an element of the function that maps $C$ to the set of full subcategories of the fibrant object of $C$.
HomotopicalAlgebra.FibrantObject.homMkdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a homomorphism of $\operatorname{mk}$ applied to $X$ and $\operatorname{mk}$ applied to $Y$ defined as the homomorphism of $f$.
HomotopicalAlgebra.FibrantObject.mkdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantEnglish
Let $X$ be an element of $C$. Then $\operatorname{mk}$ applied to $X$ is a fibrant object of $C$ defined as $\operatorname{mk}$ applied to $X$ and $h_{1}$.
HomotopicalAlgebra.FibrantObject.ιdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the inclusion functor (from the docstring)
English
The inclusion functor is a functor of the set of fibrant objects of $C$ and $C$ defined as the inclusion of the fibrant object of $C$.
HomotopicalAlgebra.bifibrantObjectsdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the bifibrant object of C (from the name)
English
Let $C$ be a set. Then the bifibrant object of $C$ is an object property of $C$ defined as the minimum of the cofibrant object of $C$ and the fibrant object of $C$.
HomotopicalAlgebra.cofibrantObjectsdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the cofibrant object of C (from the name)
English
Let $C$ be a set. Then the cofibrant object of $C$ is an object property of $C$ defined as the proposition that $\operatorname{IsCofibrant}$.
HomotopicalAlgebra.fibrantObjectsdefMathlib.AlgebraicTopology.ModelCategory.Bifibrant, function or constantWording
the fibrant object of C (from the name)
English
Let $C$ be a set. Then the fibrant object of $C$ is an object property of $C$ defined as the function that maps $X$ to the proposition that $X$ is fibrant.
HomotopicalAlgebra.BifibrantObject.HoCatdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, typeEnglish
Let $C$ be a set. Then an element of $\operatorname{HoCat}$ applied to $C$ is an element of the function that maps $C$ to the set of quotients of the homomorphism relation of $C$.
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeftdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the left homomorphism equivalence (from the name)
English
The left homomorphism equivalence is an equivalence from the set of left homotopy classes of $X$ and $Y$ to the set of homomorphisms of the action of $\operatorname{toHoCat}$ and $\operatorname{mk}$ applied to $X$ and the action of $\operatorname{toHoCat}$ and $\operatorname{mk}$ applied to $Y$ defined as the composition of the left homotopy class equivalence right homotopy class and the right homomorphism equivalence.
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRightdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the right homomorphism equivalence (from the name)
English
The right homomorphism equivalence is an equivalence from the set of right homotopy classes of $X$ and $Y$ to the set of homomorphisms of the action of $\operatorname{toHoCat}$ and $\operatorname{mk}$ applied to $X$ and the action of $\operatorname{toHoCat}$ and $\operatorname{mk}$ applied to $Y$.
HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the inclusion functor (from the docstring)
English
The inclusion functor is a functor of $\operatorname{HoCat}$ applied to $C$ and $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the inclusion functor (from the docstring)
English
The inclusion functor is a functor of $\operatorname{HoCat}$ applied to $C$ and $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.BifibrantObject.homReldefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the homomorphism relation of C (from the name)
English
Let $C$ be a set. Then the homomorphism relation of $C$ is a homomorphism relation of the set of bifibrant objects of $C$ defined as the function that maps $x_{2}$, $x_{3}$, $f$ and $g$ to the right homotopy relation.
HomotopicalAlgebra.BifibrantObject.localizerMorphismdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the localizer morphism of C (from the name)
English
Let $C$ be a set. Then the localizer morphism of $C$ is a localizer morphism of the weak equivalence of the set of bifibrant objects of $C$ and the weak equivalence of $C$.
HomotopicalAlgebra.BifibrantObject.strictUniversalPropertyFixedTargetToHoCatdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantEnglish
$\operatorname{strictUniversalPropertyFixedTargetToHoCat}$ is a strict universal property fixed target of the weak equivalence of the set of bifibrant objects of $C$ and $D$.
HomotopicalAlgebra.BifibrantObject.toHoCatdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantEnglish
$\operatorname{toHoCat}$ is a functor of the set of bifibrant objects of $C$ and $\operatorname{HoCat}$ applied to $C$ defined as the functor of the homomorphism relation of $C$.
HomotopicalAlgebra.BifibrantObject.toHoCatCompιCofibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantEnglish
$\mathrm{HomotopicalAlgebra\_\_BifibrantObject\_\_toHoCatComp\_u3b9\_CofibrantObject}$ is an isomorphism of the composition of $\operatorname{toHoCat}$ and the inclusion functor and the composition of the inclusion and $\operatorname{toHoCat}$ defined as the identity of the composition of $\operatorname{toHoCat}$ and the inclusion functor.
HomotopicalAlgebra.BifibrantObject.toHoCatCompιFibrantObjectdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantEnglish
$\mathrm{HomotopicalAlgebra\_\_BifibrantObject\_\_toHoCatComp\_u3b9\_FibrantObject}$ is an isomorphism of the composition of $\operatorname{toHoCat}$ and the inclusion functor and the composition of the inclusion functor and $\operatorname{toHoCat}$ defined as the identity of the composition of $\operatorname{toHoCat}$ and the inclusion functor.
HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphismdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the inclusion of C (from the docstring)
English
Let $C$ be a set. Then the inclusion of $C$ is a localizer morphism of the weak equivalence of the set of bifibrant objects of $C$ and the weak equivalence of the set of cofibrant objects of $C$ defined as $\operatorname{mk}$ applied to the inclusion and the function that maps $x_{2}$, $x_{3}$, $x_{4}$ and $h$ to $h$.
HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphismdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the inclusion of C (from the docstring)
English
Let $C$ be a set. Then the inclusion of $C$ is a localizer morphism of the weak equivalence of the set of bifibrant objects of $C$ and the weak equivalence of the set of fibrant objects of $C$ defined as $\operatorname{mk}$ applied to the inclusion functor and the function that maps $x_{2}$, $x_{3}$, $x_{4}$ and $h$ to $h$.
HomotopicalAlgebra.CofibrantObject.HoCat.adjdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the adjoint (from the name)
English
The adjoint is an adjunction of the bifibrant resolution and the inclusion functor.
HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolutiondefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the bifibrant resolution (from the name)
English
The bifibrant resolution is a functor of $\operatorname{HoCat}$ applied to $C$ and $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'defMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the bifibrant resolution (from the name)
English
The bifibrant resolution is a functor of the set of cofibrant objects of $C$ and $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMapdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the bifibrant resolution map of f (from the name)
English
Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the bifibrant resolution map of $f$ is a homomorphism of the bifibrant resolution object of $x_{2}$ and the bifibrant resolution object of $x_{3}$ defined as $\operatorname{choose}$ applied to $\mathrm{HomotopicalAlgebra\_\_CofibrantObject\_\_exists\_bifibrant\_map}$ applied to $f$.
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObjdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the bifibrant resolution object of X (from the name)
English
Let $X$ be a cofibrant object of $C$. Then the bifibrant resolution object of $X$ is a bifibrant object of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{HomotopicalAlgebra\_\_CofibrantObject\_\_exists\_bifibrant}$ applied to $X$.
HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObjdefMathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy, function or constantWording
the bifibrant resolution object of X (from the name)
English
Let $X$ be a cofibrant object of $C$. Then the bifibrant resolution object of $X$ is a homomorphism of $X$ and the action of the inclusion and the bifibrant resolution object of $X$.
HomotopicalAlgebra.CofibrantBrownFactorizationstructureMathlib.AlgebraicTopology.ModelCategory.BrownLemma, typeEnglish
Let $f$ be a homomorphism of $X$ and $Y$. Then the elements of $\operatorname{CofibrantBrownFactorization}$ applied to $f$ are a basic type.
HomotopicalAlgebra.CofibrantBrownFactorization.mk'defMathlib.AlgebraicTopology.ModelCategory.BrownLemma, function or constantEnglish
Let $f$ be a homomorphism of $X$ and $Y$. Let $h_{2}$ be a map factorization data of the trivial fibration of $C$ and $\operatorname{desc}$ applied to $f$ and the identity morphism of $Y$. Then $\operatorname{mk'}$ applied to $f$ and $h_{2}$ is an element of $\operatorname{CofibrantBrownFactorization}$ applied to $f$.
HomotopicalAlgebra.CofibrantBrownFactorization.sdefMathlib.AlgebraicTopology.ModelCategory.BrownLemma, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{CofibrantBrownFactorization}$ applied to $f$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a homomorphism of $Y$ and $\operatorname{Z}$ applied to $\operatorname{toMapFactorizationData}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.FibrantBrownFactorizationstructureMathlib.AlgebraicTopology.ModelCategory.BrownLemma, typeEnglish
Let $f$ be a homomorphism of $X$ and $Y$. Then the elements of $\operatorname{FibrantBrownFactorization}$ applied to $f$ are a basic type.
HomotopicalAlgebra.FibrantBrownFactorization.mk'defMathlib.AlgebraicTopology.ModelCategory.BrownLemma, function or constantEnglish
Let $f$ be a homomorphism of $X$ and $Y$. Let $h_{2}$ be a map factorization data of the fibration of $C$ and the lift of $f$ and the identity morphism of $X$. Then $\operatorname{mk'}$ applied to $f$ and $h_{2}$ is an element of $\operatorname{FibrantBrownFactorization}$ applied to $f$.
HomotopicalAlgebra.FibrantBrownFactorization.rdefMathlib.AlgebraicTopology.ModelCategory.BrownLemma, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{FibrantBrownFactorization}$ applied to $f$. Then $\operatorname{r}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{Z}$ applied to $\operatorname{toMapFactorizationData}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.CategoryWithCofibrationsclassMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, predicateEnglish
Let $C$ be a set. Then we can say that $\operatorname{CategoryWithCofibrations}$ holds for $C$.
HomotopicalAlgebra.CategoryWithCofibrations.cofibrationsdefMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, function or constantWording
the cofibration (from the name)
English
The cofibration is a morphism property of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.CategoryWithFibrationsclassMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, predicateEnglish
Let $C$ be a set. Then we can say that $\operatorname{CategoryWithFibrations}$ holds for $C$.
HomotopicalAlgebra.CategoryWithFibrations.fibrationsdefMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, function or constantWording
the fibration (from the name)
English
The fibration is a morphism property of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.CategoryWithWeakEquivalencesclassMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, predicateEnglish
Let $C$ be a set. Then we can say that $\operatorname{CategoryWithWeakEquivalences}$ holds for $C$.
HomotopicalAlgebra.CategoryWithWeakEquivalences.weakEquivalencesdefMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, function or constantWording
the weak equivalence (from the name)
English
The weak equivalence is a morphism property of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.CofibrationclassMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, predicateWording
f is a cofibration (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is a cofibration.
HomotopicalAlgebra.FibrationclassMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, predicateWording
f is a fibration (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is a fibration.
HomotopicalAlgebra.WeakEquivalenceclassMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, predicateWording
f is a weak equivalence (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is a weak equivalence.
HomotopicalAlgebra.cofibrationsdefMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, function or constantWording
the cofibration of C (from the name)
English
Let $C$ be a set. Then the cofibration of $C$ is a morphism property of $C$ defined as the cofibration.
HomotopicalAlgebra.fibrationsdefMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, function or constantWording
the fibration of C (from the name)
English
Let $C$ be a set. Then the fibration of $C$ is a morphism property of $C$ defined as the fibration.
HomotopicalAlgebra.trivialCofibrationsdefMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, function or constantWording
the trivial cofibration of C (from the name)
English
Let $C$ be a set. Then the trivial cofibration of $C$ is a morphism property of $C$ defined as the minimum of the cofibration of $C$ and the weak equivalence of $C$.
HomotopicalAlgebra.trivialFibrationsdefMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, function or constantWording
the trivial fibration of C (from the name)
English
Let $C$ be a set. Then the trivial fibration of $C$ is a morphism property of $C$ defined as the minimum of the fibration of $C$ and the weak equivalence of $C$.
HomotopicalAlgebra.weakEquivalencesdefMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations, function or constantWording
the weak equivalence of C (from the name)
English
Let $C$ be a set. Then the weak equivalence of $C$ is a morphism property of $C$ defined as the weak equivalence.
HomotopicalAlgebra.CofibrantObject.HoCatdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, typeEnglish
Let $C$ be a set. Then an element of $\operatorname{HoCat}$ applied to $C$ is an element of the function that maps $C$ to the set of quotients of the homomorphism relation of $C$.
HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolutiondefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the cofibrant resolution functor of C (from the docstring)
English
Let $C$ be a set. Then the cofibrant resolution functor of $C$ is a localizer morphism of the weak equivalence of $C$ and the weak equivalence of $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObjdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the resolution object of X (from the name)
English
Let $X$ be an element of $C$. Then the resolution object of $X$ is a homomorphism of the resolution object of $X$ and $X$.
HomotopicalAlgebra.CofibrantObject.HoCat.resolutiondefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the resolution (from the name)
English
The resolution is a functor of $C$ and $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionCompToLocalizationNatTransdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the natural isomorphism of L (from the docstring)
English
Let $L$ be a functor of $C$ and $D$. Then the natural isomorphism of $L$ is a homomorphism of the composition of the resolution and the localization of $L$ and $L$.
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMapdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the resolution map of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the resolution map of $f$ is a homomorphism of the resolution object of $X$ and the resolution object of $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{HomotopicalAlgebra\_\_CofibrantObject\_\_HoCat\_\_exists\_resolution\_map}$ applied to $f$.
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObjdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the resolution object of X (from the name)
English
Let $X$ be an element of $C$. Then the resolution object of $X$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{HomotopicalAlgebra\_\_CofibrantObject\_\_HoCat\_\_exists\_resolution}$ applied to $X$.
HomotopicalAlgebra.CofibrantObject.HoCat.toHoCatCompToLocalizationIsodefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the isomorphism of L (from the docstring)
English
Let $L$ be a functor of $C$ and $D$. Then the isomorphism of $L$ is an isomorphism of the composition of $\operatorname{toHoCat}$ and the localization of $L$ and the composition of the inclusion functor and $L$ defined as the identity of the composition of $\operatorname{toHoCat}$ and the localization of $L$.
HomotopicalAlgebra.CofibrantObject.HoCat.toLocalizationdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the localization of L (from the name)
English
Let $L$ be a functor of $C$ and $D$. Then the localization of $L$ is a functor of $\operatorname{HoCat}$ applied to $C$ and $D$.
HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTransdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the inclusion composition resolution natural transformation (from the name)
English
The inclusion composition resolution natural transformation is a homomorphism of the composition of the inclusion functor and the resolution and $\operatorname{toHoCat}$.
HomotopicalAlgebra.CofibrantObject.homReldefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the homomorphism relation of C (from the name)
English
Let $C$ be a set. Then the homomorphism relation of $C$ is a homomorphism relation of the set of cofibrant objects of $C$ defined as the function that maps $x_{2}$, $x_{3}$, $f$ and $g$ to the right homotopy relation.
HomotopicalAlgebra.CofibrantObject.localizerMorphismdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantWording
the localizer morphism of C (from the name)
English
Let $C$ be a set. Then the localizer morphism of $C$ is a localizer morphism of the weak equivalence of the set of cofibrant objects of $C$ and the weak equivalence of $C$.
HomotopicalAlgebra.CofibrantObject.toHoCatdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantEnglish
$\operatorname{toHoCat}$ is a functor of the set of cofibrant objects of $C$ and $\operatorname{HoCat}$ applied to $C$ defined as the functor of the homomorphism relation of $C$.
HomotopicalAlgebra.CofibrantObject.toHoCatLocalizerMorphismdefMathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy, function or constantEnglish
Let $C$ be a set. Then $\operatorname{toHoCatLocalizerMorphism}$ applied to $C$ is a localizer morphism of the weak equivalence of the set of cofibrant objects of $C$ and the weak equivalence of $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.CylinderstructureMathlib.AlgebraicTopology.ModelCategory.Cylinder, typeWording
cylinder of A (from the name)
English
Let $A$ be an element of $C$. Then the cylinders of $A$ are a basic type.
HomotopicalAlgebra.Cylinder.IsGoodclassMathlib.AlgebraicTopology.ModelCategory.Cylinder, predicateWording
P is good (from the name)
English
Let $P$ be a cylinder of $A$. Then we can say that $P$ is good.
HomotopicalAlgebra.Cylinder.IsVeryGoodclassMathlib.AlgebraicTopology.ModelCategory.Cylinder, predicateEnglish
Let $P$ be a cylinder of $A$. Then we can say that $\operatorname{IsVeryGood}$ holds for $P$.
HomotopicalAlgebra.Cylinder.ofFactorizationDatadefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantWording
the cylinder of h (from the name)
English
Let $h$ be a map factorization data of the trivial fibration of $C$ and $\operatorname{codiag}$ applied to $A$. Then the cylinder of $h$ is a cylinder of $A$.
HomotopicalAlgebra.Cylinder.symmdefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantWording
the inverse of P (from the name)
English
Let $P$ be a cylinder of $A$. Then the inverse of $P$ is a cylinder of $A$.
HomotopicalAlgebra.Cylinder.transdefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantWording
the composition of P and #2 (from the name)
English
Let $P$ and $\mathrm{P'}$ be cylinders of $A$. Then the composition of $P$ and $\mathrm{P'}$ is a cylinder of $A$.
HomotopicalAlgebra.PrecylinderstructureMathlib.AlgebraicTopology.ModelCategory.Cylinder, typeWording
precylinder of A (from the name)
English
Let $A$ be an element of $C$. Then the precylinders of $A$ are a basic type.
HomotopicalAlgebra.Precylinder.IdefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantEnglish
Let $\mathrm{self}$ be a precylinder of $A$. Then $\operatorname{I}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.Precylinder.idefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantEnglish
Let $P$ be a precylinder of $A$. Then $\operatorname{i}$ applied to $P$ is a homomorphism of the coproduct of $A$ and $A$ and $\operatorname{I}$ applied to $P$ defined as $\operatorname{desc}$ applied to $\mathrm{HomotopicalAlgebra\_\_Precylinder\_\_i\_u2080\_}$ applied to $P$ and $\mathrm{HomotopicalAlgebra\_\_Precylinder\_\_i\_u2081\_}$ applied to $P$.
HomotopicalAlgebra.Precylinder.i₀defMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantEnglish
Let $\mathrm{self}$ be a precylinder of $A$. Then $\mathrm{HomotopicalAlgebra\_\_Precylinder\_\_i\_u2080\_}$ applied to $\mathrm{self}$ is a homomorphism of $A$ and $\operatorname{I}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.Precylinder.i₁defMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantEnglish
Let $\mathrm{self}$ be a precylinder of $A$. Then $\mathrm{HomotopicalAlgebra\_\_Precylinder\_\_i\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $A$ and $\operatorname{I}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.Precylinder.mapdefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantWording
the map of P and F (from the name)
English
Let $P$ be a precylinder of $X$. Let $F$ be a functor of $C$ and $D$. Then the map of $P$ and $F$ is a precylinder of the action of $F$ and $X$.
HomotopicalAlgebra.Precylinder.symmdefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantWording
the inverse of P (from the name)
English
Let $P$ be a precylinder of $A$. Then the inverse of $P$ is a precylinder of $A$.
HomotopicalAlgebra.Precylinder.toFullSubcategorydefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantWording
the full subcategory of Q and hQ (from the name)
English
Let $Q$ be a precylinder of the object of $X$ such that $P$ holds for $\operatorname{I}$ applied to $Q$. Then the full subcategory of $Q$ and $\mathrm{hQ}$ is a precylinder of $X$.
HomotopicalAlgebra.Precylinder.transdefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantWording
the composition of P and #2 (from the name)
English
Let $P$ and $\mathrm{P'}$ be precylinders of $A$. Then the composition of $P$ and $\mathrm{P'}$ is a precylinder of $A$.
HomotopicalAlgebra.Precylinder.πdefMathlib.AlgebraicTopology.ModelCategory.Cylinder, function or constantWording
the projection of self (from the name)
English
Let $\mathrm{self}$ be a precylinder of $A$. Then the projection of $\mathrm{self}$ is a homomorphism of $\operatorname{I}$ applied to $\mathrm{self}$ and $A$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.FibrantObject.HoCatdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, typeEnglish
Let $C$ be a set. Then an element of $\operatorname{HoCat}$ applied to $C$ is an element of the function that maps $C$ to the set of quotients of the homomorphism relation of $C$.
HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObjdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the resolution object of X (from the name)
English
Let $X$ be an element of $C$. Then the resolution object of $X$ is a homomorphism of $X$ and the resolution object of $X$.
HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolutiondefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the fibrant resolution functor of C (from the docstring)
English
Let $C$ be a set. Then the fibrant resolution functor of $C$ is a localizer morphism of the weak equivalence of $C$ and the weak equivalence of $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.FibrantObject.HoCat.resolutiondefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the resolution (from the name)
English
The resolution is a functor of $C$ and $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.FibrantObject.HoCat.resolutionCompToLocalizationNatTransdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the natural isomorphism of L (from the docstring)
English
Let $L$ be a functor of $C$ and $D$. Then the natural isomorphism of $L$ is a homomorphism of $L$ and the composition of the resolution and the localization of $L$.
HomotopicalAlgebra.FibrantObject.HoCat.resolutionMapdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the resolution map of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the resolution map of $f$ is a homomorphism of the resolution object of $X$ and the resolution object of $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{HomotopicalAlgebra\_\_FibrantObject\_\_HoCat\_\_exists\_resolution\_map}$ applied to $f$.
HomotopicalAlgebra.FibrantObject.HoCat.resolutionObjdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the resolution object of X (from the name)
English
Let $X$ be an element of $C$. Then the resolution object of $X$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{HomotopicalAlgebra\_\_FibrantObject\_\_HoCat\_\_exists\_resolution}$ applied to $X$.
HomotopicalAlgebra.FibrantObject.HoCat.toHoCatCompToLocalizationIsodefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the isomorphism of L (from the docstring)
English
Let $L$ be a functor of $C$ and $D$. Then the isomorphism of $L$ is an isomorphism of the composition of $\operatorname{toHoCat}$ and the localization of $L$ and the composition of the inclusion functor and $L$ defined as the identity of the composition of $\operatorname{toHoCat}$ and the localization of $L$.
HomotopicalAlgebra.FibrantObject.HoCat.toLocalizationdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the localization of L (from the name)
English
Let $L$ be a functor of $C$ and $D$. Then the localization of $L$ is a functor of $\operatorname{HoCat}$ applied to $C$ and $D$.
HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTransdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the inclusion composition resolution natural transformation (from the name)
English
The inclusion composition resolution natural transformation is a homomorphism of $\operatorname{toHoCat}$ and the composition of the inclusion functor and the resolution.
HomotopicalAlgebra.FibrantObject.homReldefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the homomorphism relation of C (from the name)
English
Let $C$ be a set. Then the homomorphism relation of $C$ is a homomorphism relation of the set of fibrant objects of $C$ defined as the function that maps $x_{2}$, $x_{3}$, $f$ and $g$ to the left homotopy relation.
HomotopicalAlgebra.FibrantObject.localizerMorphismdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantWording
the localizer morphism of C (from the name)
English
Let $C$ be a set. Then the localizer morphism of $C$ is a localizer morphism of the weak equivalence of the set of fibrant objects of $C$ and the weak equivalence of $C$.
HomotopicalAlgebra.FibrantObject.toHoCatdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantEnglish
$\operatorname{toHoCat}$ is a functor of the set of fibrant objects of $C$ and $\operatorname{HoCat}$ applied to $C$ defined as the functor of the homomorphism relation of $C$.
HomotopicalAlgebra.FibrantObject.toHoCatLocalizerMorphismdefMathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy, function or constantEnglish
Let $C$ be a set. Then $\operatorname{toHoCatLocalizerMorphism}$ applied to $C$ is a localizer morphism of the weak equivalence of the set of fibrant objects of $C$ and the weak equivalence of $\operatorname{HoCat}$ applied to $C$.
HomotopicalAlgebra.leftHomotopyClassToHomdefMathlib.AlgebraicTopology.ModelCategory.FundamentalLemma, function or constantWording
the left homotopy class to homomorphism of L and x3 (from the name)
English
Let $L$ be a functor of $C$ and $H$. Let $x_{3}$ be a left homotopy class of $X$ and $Y$. Then the left homotopy class to homomorphism of $L$ and $x_{3}$ is a homomorphism of the action of $L$ and $X$ and the action of $L$ and $Y$.
HomotopicalAlgebra.rightHomotopyClassToHomdefMathlib.AlgebraicTopology.ModelCategory.FundamentalLemma, function or constantWording
the right homotopy class to homomorphism of L and x3 (from the name)
English
Let $L$ be a functor of $C$ and $H$. Let $x_{3}$ be a right homotopy class of $X$ and $Y$. Then the right homotopy class to homomorphism of $L$ and $x_{3}$ is a homomorphism of the action of $L$ and $X$ and the action of $L$ and $Y$.
HomotopicalAlgebra.LeftHomotopyRel.leftHomotopydefMathlib.AlgebraicTopology.ModelCategory.Homotopy, function or constantWording
the left homotopy of h2 and Q (from the name)
English
Assume that $\operatorname{LeftHomotopyRel}$. Let $Q$ be a cylinder of $X$. Then the left homotopy of $h_{2}$ and $Q$ is a left homotopy of $f$ and $g$.
HomotopicalAlgebra.LeftHomotopyRel.rightHomotopydefMathlib.AlgebraicTopology.ModelCategory.Homotopy, function or constantWording
the right homotopy of h1 and Q (from the name)
English
Assume that $\operatorname{LeftHomotopyRel}$. Let $Q$ be a path object of $Y$. Then the right homotopy of $h_{1}$ and $Q$ is a right homotopy of $f$ and $g$.
HomotopicalAlgebra.RightHomotopyRel.leftHomotopydefMathlib.AlgebraicTopology.ModelCategory.Homotopy, function or constantWording
the left homotopy of h1 and Q (from the name)
English
Assume that $\operatorname{RightHomotopyRel}$. Let $Q$ be a cylinder of $X$. Then the left homotopy of $h_{1}$ and $Q$ is a left homotopy of $f$ and $g$.
HomotopicalAlgebra.RightHomotopyRel.rightHomotopydefMathlib.AlgebraicTopology.ModelCategory.Homotopy, function or constantWording
the right homotopy of h2 and P (from the name)
English
Assume that $\operatorname{RightHomotopyRel}$. Let $P$ be a path object of $Y$. Then the right homotopy of $h_{2}$ and $P$ is a right homotopy of $f$ and $g$.
HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClassdefMathlib.AlgebraicTopology.ModelCategory.Homotopy, function or constantWording
the left homotopy class equivalence right homotopy class (from the name)
English
The left homotopy class equivalence right homotopy class is an equivalence from the set of left homotopy classes of $X$ and $Y$ to the set of right homotopy classes of $X$ and $Y$.
HomotopicalAlgebra.IsCofibrantdefMathlib.AlgebraicTopology.ModelCategory.IsCofibrant, predicateWording
X is cofibrant (from the name)
English
Let $X$ be an element of $C$. Then $X$ is cofibrant, if $\operatorname{to}$ applied to $X$ is a cofibration.
HomotopicalAlgebra.IsFibrantdefMathlib.AlgebraicTopology.ModelCategory.IsCofibrant, predicateWording
X is fibrant (from the name)
English
Let $X$ be an element of $C$. Then $X$ is fibrant, if the map of $X$ is a fibration.
HomotopicalAlgebra.Cylinder.LeftHomotopydefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, typeWording
left homotopy of f and g (from the name)
English
Let $P$ be a cylinder of $X$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then a left homotopy of $f$ and $g$ is an element of the function that maps $P$, $f$ and $g$ to the set of left homotopies of $f$ and $g$.
HomotopicalAlgebra.Cylinder.LeftHomotopy.postcompdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the postcomposition of h and p (from the name)
English
Let $h$ be a left homotopy of $f$ and $g$. Let $p$ be a homomorphism of $Y$ and $Z$. Then the postcomposition of $h$ and $p$ is a left homotopy of the composition of $f$ and $p$ and the composition of $g$ and $p$ defined as the postcomposition of $h$ and $p$.
HomotopicalAlgebra.Cylinder.LeftHomotopy.refldefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the identity of P and f (from the name)
English
Let $P$ be a cylinder of $X$. Let $f$ be a homomorphism of $X$ and $Y$. Then the identity of $P$ and $f$ is a left homotopy of $f$ and $f$ defined as the identity of $\operatorname{toPrecylinder}$ applied to $P$ and $f$.
HomotopicalAlgebra.Cylinder.LeftHomotopy.symmdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the inverse of h (from the name)
English
Let $h$ be a left homotopy of $f$ and $g$. Then the inverse of $h$ is a left homotopy of $g$ and $f$ defined as the inverse of $h$.
HomotopicalAlgebra.Cylinder.LeftHomotopy.transdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the composition of h1 and #2 (from the name)
English
Let $h_{1}$ be a left homotopy of $x_{2}$ and $x_{3}$. Let $\mathrm{h'}$ be a left homotopy of $x_{3}$ and $x_{4}$. Then the composition of $h_{1}$ and $\mathrm{h'}$ is a left homotopy of $x_{2}$ and $x_{4}$ defined as the composition of $h_{1}$ and $\mathrm{h'}$.
HomotopicalAlgebra.LeftHomotopyClassdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, typeWording
left homotopy class of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $C$. Then a left homotopy class of $X$ and $Y$ is an element of the function that maps $X$ and $Y$ to $\mathrm{Quot}$ applied to the left homotopy relation.
HomotopicalAlgebra.LeftHomotopyClass.mkdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantEnglish
Let $x_{2}$ be a homomorphism of $X$ and $Y$. Then $\operatorname{mk}$ applied to $x_{2}$ is a left homotopy class of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the left homotopy relation and $x_{2}$.
HomotopicalAlgebra.LeftHomotopyClass.postcompdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the postcomposition map of x2 and x3 (from the docstring)
English
Let $x_{2}$ be a left homotopy class of $X$ and $Y$. Let $x_{3}$ be a homomorphism of $Y$ and $Z$. Then the postcomposition map of $x_{2}$ and $x_{3}$ is a left homotopy class of $X$ and $Z$.
HomotopicalAlgebra.LeftHomotopyReldefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the left homotopy relation (from the name)
English
The left homotopy relation is a homomorphism relation of $C$ defined as the function that maps $X$, $x_{2}$, $f$ and $g$ to the proposition that there exists a cylinder $P$ of $X$, such that $\mathrm{Nonempty}$ holds for the set of left homotopies of $f$ and $g$.
HomotopicalAlgebra.Precylinder.LeftHomotopystructureMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, typeWording
left homotopy of f and g (from the name)
English
Let $P$ be a precylinder of $X$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the left homotopies of $f$ and $g$ are a basic type.
HomotopicalAlgebra.Precylinder.LeftHomotopy.fullSubcategoryEquivdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the full subcategory equivalence (from the name)
English
The full subcategory equivalence is an equivalence from the set of left homotopies of $f$ and $g$ to the set of left homotopies of the homomorphism of $f$ and the homomorphism of $g$.
HomotopicalAlgebra.Precylinder.LeftHomotopy.hdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantEnglish
Let $\mathrm{self}$ be a left homotopy of $f$ and $g$. Then $\operatorname{h}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{I}$ applied to $P$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.Precylinder.LeftHomotopy.postcompdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the postcomposition of h and p (from the name)
English
Let $h$ be a left homotopy of $f$ and $g$. Let $p$ be a homomorphism of $Y$ and $Z$. Then the postcomposition of $h$ and $p$ is a left homotopy of the composition of $f$ and $p$ and the composition of $g$ and $p$.
HomotopicalAlgebra.Precylinder.LeftHomotopy.refldefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the identity of P and f (from the name)
English
Let $P$ be a precylinder of $X$. Let $f$ be a homomorphism of $X$ and $Y$. Then the identity of $P$ and $f$ is a left homotopy of $f$ and $f$.
HomotopicalAlgebra.Precylinder.LeftHomotopy.symmdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the inverse of h (from the name)
English
Let $h$ be a left homotopy of $f$ and $g$. Then the inverse of $h$ is a left homotopy of $g$ and $f$.
HomotopicalAlgebra.Precylinder.LeftHomotopy.transdefMathlib.AlgebraicTopology.ModelCategory.LeftHomotopy, function or constantWording
the composition of h and #2 (from the name)
English
Let $h$ be a left homotopy of $x_{1}$ and $x_{2}$. Let $\mathrm{h'}$ be a left homotopy of $x_{2}$ and $x_{3}$. Then the composition of $h$ and $\mathrm{h'}$ is a left homotopy of $x_{1}$ and $x_{3}$.
HomotopicalAlgebra.PathObjectstructureMathlib.AlgebraicTopology.ModelCategory.PathObject, typeWording
path object of A (from the name)
English
Let $A$ be an element of $C$. Then the path objects of $A$ are a basic type.
HomotopicalAlgebra.PathObject.IsGoodclassMathlib.AlgebraicTopology.ModelCategory.PathObject, predicateWording
P is good (from the name)
English
Let $P$ be a path object of $A$. Then we can say that $P$ is good.
HomotopicalAlgebra.PathObject.IsVeryGoodclassMathlib.AlgebraicTopology.ModelCategory.PathObject, predicateEnglish
Let $P$ be a path object of $A$. Then we can say that $\operatorname{IsVeryGood}$ holds for $P$.
HomotopicalAlgebra.PathObject.ofFactorizationDatadefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the path object of h (from the name)
English
Let $h$ be a map factorization data of the fibration of $C$ and the diagonal of $A$. Then the path object of $h$ is a path object of $A$.
HomotopicalAlgebra.PathObject.symmdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the inverse of P (from the name)
English
Let $P$ be a path object of $A$. Then the inverse of $P$ is a path object of $A$.
HomotopicalAlgebra.PathObject.transdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the composition of P and #2 (from the name)
English
Let $P$ and $\mathrm{P'}$ be path objects of $A$. Then the composition of $P$ and $\mathrm{P'}$ is a path object of $A$.
HomotopicalAlgebra.Precylinder.opdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the opposite of P (from the docstring)
English
Let $P$ be a precylinder of $A$. Then the opposite of $P$ is an element of $\operatorname{PrepathObject}$ applied to $\operatorname{op}$ applied to $A$.
HomotopicalAlgebra.Precylinder.unopdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the opposite of P (from the name)
English
Let $P$ be a precylinder of $A$. Then the opposite of $P$ is an element of $\operatorname{PrepathObject}$ applied to the opposite of $A$.
HomotopicalAlgebra.PrepathObjectstructureMathlib.AlgebraicTopology.ModelCategory.PathObject, typeEnglish
Let $A$ be an element of $C$. Then the elements of $\operatorname{PrepathObject}$ applied to $A$ are a basic type.
HomotopicalAlgebra.PrepathObject.PdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{PrepathObject}$ applied to $A$. Then $\operatorname{P}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.PrepathObject.mapdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the map of P and F (from the name)
English
Let $P$ be an element of $\operatorname{PrepathObject}$ applied to $X$. Let $F$ be a functor of $C$ and $D$. Then the map of $P$ and $F$ is an element of $\operatorname{PrepathObject}$ applied to the action of $F$ and $X$.
HomotopicalAlgebra.PrepathObject.opdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the opposite of P (from the docstring)
English
Let $P$ be an element of $\operatorname{PrepathObject}$ applied to $A$. Then the opposite of $P$ is a precylinder of $\operatorname{op}$ applied to $A$.
HomotopicalAlgebra.PrepathObject.pdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantEnglish
Let $P$ be an element of $\operatorname{PrepathObject}$ applied to $A$. Then $\operatorname{p}$ applied to $P$ is a homomorphism of $\operatorname{P}$ applied to $P$ and the product of $A$ and $A$ defined as the lift of $\mathrm{HomotopicalAlgebra\_\_PrepathObject\_\_p\_u2080\_}$ applied to $P$ and $\mathrm{HomotopicalAlgebra\_\_PrepathObject\_\_p\_u2081\_}$ applied to $P$.
HomotopicalAlgebra.PrepathObject.p₀defMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{PrepathObject}$ applied to $A$. Then $\mathrm{HomotopicalAlgebra\_\_PrepathObject\_\_p\_u2080\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{P}$ applied to $\mathrm{self}$ and $A$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.PrepathObject.p₁defMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{PrepathObject}$ applied to $A$. Then $\mathrm{HomotopicalAlgebra\_\_PrepathObject\_\_p\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{P}$ applied to $\mathrm{self}$ and $A$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.PrepathObject.symmdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the inverse of P (from the name)
English
Let $P$ be an element of $\operatorname{PrepathObject}$ applied to $A$. Then the inverse of $P$ is an element of $\operatorname{PrepathObject}$ applied to $A$.
HomotopicalAlgebra.PrepathObject.toFullSubcategorydefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the full subcategory of Q and hQ (from the name)
English
Let $Q$ be an element of $\operatorname{PrepathObject}$ applied to the object of $X$ such that $P$ holds for $\operatorname{P}$ applied to $Q$. Then the full subcategory of $Q$ and $\mathrm{hQ}$ is an element of $\operatorname{PrepathObject}$ applied to $X$.
HomotopicalAlgebra.PrepathObject.transdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the composition of P and #2 (from the name)
English
Let $P$ and $\mathrm{P'}$ be elements of $\operatorname{PrepathObject}$ applied to $A$. Then the composition of $P$ and $\mathrm{P'}$ is an element of $\operatorname{PrepathObject}$ applied to $A$.
HomotopicalAlgebra.PrepathObject.unopdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the opposite of P (from the name)
English
Let $P$ be an element of $\operatorname{PrepathObject}$ applied to $A$. Then the opposite of $P$ is a precylinder of the opposite of $A$.
HomotopicalAlgebra.PrepathObject.ιdefMathlib.AlgebraicTopology.ModelCategory.PathObject, function or constantWording
the inclusion of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{PrepathObject}$ applied to $A$. Then the inclusion of $\mathrm{self}$ is a homomorphism of $A$ and $\operatorname{P}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.PathObject.RightHomotopydefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, typeWording
right homotopy of f and g (from the name)
English
Let $P$ be a path object of $Y$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then a right homotopy of $f$ and $g$ is an element of the function that maps $P$, $f$ and $g$ to the set of right homotopies of $f$ and $g$.
HomotopicalAlgebra.PathObject.RightHomotopy.precompdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the precomposition of h and i (from the name)
English
Let $h$ be a right homotopy of $f$ and $g$. Let $i$ be a homomorphism of $Z$ and $X$. Then the precomposition of $h$ and $i$ is a right homotopy of the composition of $i$ and $f$ and the composition of $i$ and $g$ defined as the precomposition of $h$ and $i$.
HomotopicalAlgebra.PathObject.RightHomotopy.refldefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the identity of P and f (from the name)
English
Let $P$ be a path object of $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then the identity of $P$ and $f$ is a right homotopy of $f$ and $f$ defined as the identity of $\operatorname{toPrepathObject}$ applied to $P$ and $f$.
HomotopicalAlgebra.PathObject.RightHomotopy.symmdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the inverse of h (from the name)
English
Let $h$ be a right homotopy of $f$ and $g$. Then the inverse of $h$ is a right homotopy of $g$ and $f$ defined as the inverse of $h$.
HomotopicalAlgebra.PathObject.RightHomotopy.transdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the composition of h1 and #2 (from the name)
English
Let $h_{1}$ be a right homotopy of $x_{2}$ and $x_{3}$. Let $\mathrm{h'}$ be a right homotopy of $x_{3}$ and $x_{4}$. Then the composition of $h_{1}$ and $\mathrm{h'}$ is a right homotopy of $x_{2}$ and $x_{4}$ defined as the composition of $h_{1}$ and $\mathrm{h'}$.
HomotopicalAlgebra.Precylinder.LeftHomotopy.opdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the opposite of h (from the name)
English
Let $h$ be a left homotopy of $f$ and $g$. Then the opposite of $h$ is a right homotopy of the opposite in $f$ and the opposite in $g$.
HomotopicalAlgebra.Precylinder.LeftHomotopy.unopdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the opposite of h (from the name)
English
Let $h$ be a left homotopy of $f$ and $g$. Then the opposite of $h$ is a right homotopy of the opposite of $f$ and the opposite of $g$.
HomotopicalAlgebra.PrepathObject.RightHomotopystructureMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, typeWording
right homotopy of f and g (from the name)
English
Let $P$ be an element of $\operatorname{PrepathObject}$ applied to $Y$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the right homotopies of $f$ and $g$ are a basic type.
HomotopicalAlgebra.PrepathObject.RightHomotopy.fullSubcategoryEquivdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the full subcategory equivalence (from the name)
English
The full subcategory equivalence is an equivalence from the set of right homotopies of $f$ and $g$ to the set of right homotopies of the homomorphism of $f$ and the homomorphism of $g$.
HomotopicalAlgebra.PrepathObject.RightHomotopy.hdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantEnglish
Let $\mathrm{self}$ be a right homotopy of $f$ and $g$. Then $\operatorname{h}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\operatorname{P}$ applied to $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HomotopicalAlgebra.PrepathObject.RightHomotopy.opdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the opposite of h (from the name)
English
Let $h$ be a right homotopy of $f$ and $g$. Then the opposite of $h$ is a left homotopy of the opposite in $f$ and the opposite in $g$.
HomotopicalAlgebra.PrepathObject.RightHomotopy.precompdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the precomposition of h and i (from the name)
English
Let $h$ be a right homotopy of $f$ and $g$. Let $i$ be a homomorphism of $Z$ and $X$. Then the precomposition of $h$ and $i$ is a right homotopy of the composition of $i$ and $f$ and the composition of $i$ and $g$.
HomotopicalAlgebra.PrepathObject.RightHomotopy.refldefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the identity of P and f (from the name)
English
Let $P$ be an element of $\operatorname{PrepathObject}$ applied to $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then the identity of $P$ and $f$ is a right homotopy of $f$ and $f$.
HomotopicalAlgebra.PrepathObject.RightHomotopy.symmdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the inverse of h (from the name)
English
Let $h$ be a right homotopy of $f$ and $g$. Then the inverse of $h$ is a right homotopy of $g$ and $f$.
HomotopicalAlgebra.PrepathObject.RightHomotopy.transdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the composition of h and #2 (from the name)
English
Let $h$ be a right homotopy of $x_{1}$ and $x_{2}$. Let $\mathrm{h'}$ be a right homotopy of $x_{2}$ and $x_{3}$. Then the composition of $h$ and $\mathrm{h'}$ is a right homotopy of $x_{1}$ and $x_{3}$.
HomotopicalAlgebra.PrepathObject.RightHomotopy.unopdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the opposite of h (from the name)
English
Let $h$ be a right homotopy of $f$ and $g$. Then the opposite of $h$ is a left homotopy of the opposite of $f$ and the opposite of $g$.
HomotopicalAlgebra.RightHomotopyClassdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, typeWording
right homotopy class of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $C$. Then a right homotopy class of $X$ and $Y$ is an element of the function that maps $X$ and $Y$ to $\mathrm{Quot}$ applied to the right homotopy relation.
HomotopicalAlgebra.RightHomotopyClass.mkdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantEnglish
Let $x_{2}$ be a homomorphism of $X$ and $Y$. Then $\operatorname{mk}$ applied to $x_{2}$ is a right homotopy class of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the right homotopy relation and $x_{2}$.
HomotopicalAlgebra.RightHomotopyClass.precompdefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the precomposition map of x2 and x3 (from the docstring)
English
Let $x_{2}$ be a right homotopy class of $Y$ and $Z$. Let $x_{3}$ be a homomorphism of $X$ and $Y$. Then the precomposition map of $x_{2}$ and $x_{3}$ is a right homotopy class of $X$ and $Z$.
HomotopicalAlgebra.RightHomotopyReldefMathlib.AlgebraicTopology.ModelCategory.RightHomotopy, function or constantWording
the right homotopy relation (from the name)
English
The right homotopy relation is a homomorphism relation of $C$ defined as the function that maps $x_{2}$, $Y$, $f$ and $g$ to the proposition that there exists a path object $P$ of $Y$, such that $\mathrm{Nonempty}$ holds for the set of right homotopies of $f$ and $g$.
AlgebraicTopology.NormalizedMooreComplex.mapdefMathlib.AlgebraicTopology.MooreComplex, function or constantWording
the map of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $f$ is a homomorphism of the object of $X$ and the object of $Y$.
AlgebraicTopology.NormalizedMooreComplex.objdefMathlib.AlgebraicTopology.MooreComplex, function or constantWording
the object of X (from the name)
English
Let $X$ be a simplicial object of $C$. Then the object of $X$ is a chain complex of $C$ and $\Natural$ defined as $\operatorname{of}$ applied to the function that maps $n$ to the action of $\operatorname{underlying}$ and the object of $X$ and $n$, $\operatorname{objD}$ applied to $X$ and $\mathrm{AlgebraicTopology\_\_NormalizedMooreComplex\_\_d\_squared}$ applied to $X$.
AlgebraicTopology.NormalizedMooreComplex.objDdefMathlib.AlgebraicTopology.MooreComplex, function or constantWording
the object of X and n (from the name)
English
Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Then the object of $X$ and $n$ is a homomorphism of the action of $\operatorname{underlying}$ and the object of $X$ and $n + 1$ and the action of $\operatorname{underlying}$ and the object of $X$ and $n$.
AlgebraicTopology.NormalizedMooreComplex.objXdefMathlib.AlgebraicTopology.MooreComplex, function or constantWording
the object of X and n (from the name)
English
Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Then the object of $X$ and $n$ is a subobject of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$.
AlgebraicTopology.normalizedMooreComplexdefMathlib.AlgebraicTopology.MooreComplex, function or constantWording
the normalized Moore complex of C (from the name)
English
Let $C$ be a set. Then the normalized Moore complex of $C$ is a functor of the set of simplicial objects of $C$ and the set of chain complexes of $C$ and $\Natural$.
SSet.QuasicategoryclassMathlib.AlgebraicTopology.Quasicategory.Basic, predicateWording
S is a quasicategory (from the name)
English
Let $S$ be a set. Then we can say that $S$ is a quasicategory.
SSet.Edge.CompStruct.uniquedefMathlib.AlgebraicTopology.Quasicategory.CompStruct, function or constantEnglish
Let $h_{1}$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Let $\mathrm{h'}$ be an element of $\operatorname{CompStruct}$ applied to $x_{6}$, $x_{7}$ and $x_{8}$. Let $x_{9}$ be a homotopy of $x_{3}$ and $x_{6}$. Let $x_{10}$ be a homotopy of $x_{4}$ and $x_{7}$. Then $\operatorname{unique}$ applied to $h_{1}$, $\mathrm{h'}$, $x_{9}$ and $x_{10}$ is a homotopy of $x_{5}$ and $x_{8}$ defined as $\operatorname{unique}$ applied to $h_{1}$, $\mathrm{h'}$, $x_{9}$ and $x_{10}$.
SSet.Edge.CompStruct.unique'defMathlib.AlgebraicTopology.Quasicategory.CompStruct, function or constantEnglish
Let $h_{1}$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Let $\mathrm{h'}$ be a homotopy of $x_{5}$ and $x_{6}$. Then $\operatorname{unique'}$ applied to $h_{1}$ and $\mathrm{h'}$ is an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{6}$ defined as the associator of the composition identity of $x_{4}$ and $\mathrm{h'}$.
SSet.Edge.HomotopyLdefMathlib.AlgebraicTopology.Quasicategory.CompStruct, typeWording
homotopy of e and #2 (from the name)
English
Let $e$ and $\mathrm{e'}$ be edges of $x$ and $x_{1}$. Then a homotopy of $e$ and $\mathrm{e'}$ is an element of the function that maps $e$ and $\mathrm{e'}$ to $\operatorname{CompStruct}$ applied to $e$, the identity of $x_{1}$ and $\mathrm{e'}$.
SSet.Edge.HomotopyL.homotopyRdefMathlib.AlgebraicTopology.Quasicategory.CompStruct, function or constantWording
the homotopy of h1 (from the name)
English
Let $h_{1}$ be a homotopy of $e$ and $\mathrm{e'}$. Then the homotopy of $h_{1}$ is a homotopy of $e$ and $\mathrm{e'}$ defined as the associator of the composition identity of $e$ and $h_{1}$.
SSet.Edge.HomotopyRdefMathlib.AlgebraicTopology.Quasicategory.CompStruct, typeWording
homotopy of e and #2 (from the name)
English
Let $e$ and $\mathrm{e'}$ be edges of $x$ and $x_{1}$. Then a homotopy of $e$ and $\mathrm{e'}$ is an element of the function that maps $e$ and $\mathrm{e'}$ to $\operatorname{CompStruct}$ applied to the identity of $x$, $e$ and $\mathrm{e'}$.
SSet.Edge.HomotopyR.homotopyLdefMathlib.AlgebraicTopology.Quasicategory.CompStruct, function or constantWording
the homotopy of h1 (from the name)
English
Let $h_{1}$ be a homotopy of $e$ and $\mathrm{e'}$. Then the homotopy of $h_{1}$ is a homotopy of $e$ and $\mathrm{e'}$ defined as the associator of the composition identity of $e$ and $h_{1}$.
SSet.Edge.assocdefMathlib.AlgebraicTopology.Quasicategory.CompStruct, function or constantWording
the associator of x11 and h1 (from the name)
English
Let $x_{10}$ be an element of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{5}$ and $x_{7}$. Let $x_{11}$ be an element of $\operatorname{CompStruct}$ applied to $x_{5}$, $x_{6}$ and $x_{8}$. Let $h_{1}$ be an element of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{8}$ and $x_{9}$. Then the associator of $x_{11}$ and $h_{1}$ is an element of $\operatorname{CompStruct}$ applied to $x_{7}$, $x_{6}$ and $x_{9}$ defined as the associator of $x_{11}$ and $h_{1}$.
SSet.Edge.assoc'defMathlib.AlgebraicTopology.Quasicategory.CompStruct, function or constantWording
the associator of x11 and h1 (from the name)
English
Let $x_{10}$ be an element of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{5}$ and $x_{7}$. Let $x_{11}$ be an element of $\operatorname{CompStruct}$ applied to $x_{5}$, $x_{6}$ and $x_{8}$. Let $h_{1}$ be an element of $\operatorname{CompStruct}$ applied to $x_{7}$, $x_{6}$ and $x_{9}$. Then the associator of $x_{11}$ and $h_{1}$ is an element of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{8}$ and $x_{9}$ defined as the associator of $x_{11}$ and $h_{1}$.
SSet.Edge.compdefMathlib.AlgebraicTopology.Quasicategory.CompStruct, function or constantWording
the composition of x3 and x4 (from the name)
English
Let $x_{3}$ be an edge of $x$ and $x_{1}$. Let $x_{4}$ be an edge of $x_{1}$ and $x_{2}$. Then the composition of $x_{3}$ and $x_{4}$ is an edge of $x$ and $x_{2}$ defined as the composition of $x_{3}$ and $x_{4}$.
SSet.Edge.compStructdefMathlib.AlgebraicTopology.Quasicategory.CompStruct, function or constantEnglish
Let $x_{3}$ be an edge of $x$ and $x_{1}$. Let $x_{4}$ be an edge of $x_{1}$ and $x_{2}$. Then $\operatorname{compStruct}$ applied to $x_{3}$ and $x_{4}$ is an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and the composition of $x_{3}$ and $x_{4}$ defined as $\operatorname{compStruct}$ applied to $x_{3}$ and $x_{4}$.
SSet.InnerFibrationclassMathlib.AlgebraicTopology.Quasicategory.InnerFibration, predicateWording
q is a inner fibration (from the name)
English
Let $q$ be a homomorphism of $X$ and $Y$. Then we can say that $q$ is an inner fibration.
SSet.innerFibrationsdefMathlib.AlgebraicTopology.Quasicategory.InnerFibration, function or constantWording
the inner fibration (from the name)
English
The inner fibration is a morphism property of the set of sets defined as $\operatorname{rlp}$ applied to the inner horn inclusion.
SSet.innerHornInclusionsinductiveMathlib.AlgebraicTopology.Quasicategory.InnerFibration, function or constantWording
the inner horn inclusion (from the name)
English
The inner horn inclusion is a morphism property of the set of sets.
SSet.QCatdefMathlib.AlgebraicTopology.Quasicategory.StrictBicategory, typeWording
category (from the name)
English
A category is a full subcategory of the proposition that $\operatorname{Quasicategory}$.
SSet.QCat.forgetEnrichment.equivdefMathlib.AlgebraicTopology.Quasicategory.StrictBicategory, function or constantWording
the equivalence (from the name)
English
The equivalence is an equivalence of $\operatorname{ForgetEnrichment}$ applied to the set of categories and the set of categories and the set of categories defined as the equivalence of the set of categories.