Definitions: Mathlib.CategoryTheory, part 20 of 25

399 definitions of 47 modules, Mathlib.CategoryTheory.PEmpty to Mathlib.CategoryTheory.Profunctor.Bicategory. ‹ previous next ›

Mathlib.CategoryTheory.PEmpty

CategoryTheory.Functor.emptydefMathlib.CategoryTheory.PEmpty, function or constant
Wording
no wording
English
Let $C$ be a set. Then $\operatorname{empty}$ applied to $C$ is a functor of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $C$ defined as the functor of $\operatorname{elim}$.
CategoryTheory.Functor.emptyExtdefMathlib.CategoryTheory.PEmpty, function or constant
Wording
the empty extension of F and G (from the name)
English
Let $F$ and $G$ be functors of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $C$. Then the empty extension of $F$ and $G$ is an isomorphism of $F$ and $G$ defined as the natural isomorphism of the function that maps $x_{1}$ to $\operatorname{elim}$ applied to $\operatorname{as}$ applied to $x_{1}$.
CategoryTheory.Functor.isEmptyExtdefMathlib.CategoryTheory.PEmpty, function or constant
Wording
no wording
English
Let $F$ and $G$ be functors of $C$ and $D$. Then $\operatorname{isEmptyExt}$ applied to $F$ and $G$ is an isomorphism of $F$ and $G$.
CategoryTheory.Functor.uniqueFromEmptydefMathlib.CategoryTheory.PEmpty, function or constant
Wording
no wording
English
Let $F$ be a functor of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $C$. Then $\operatorname{uniqueFromEmpty}$ applied to $F$ is an isomorphism of $F$ and $\operatorname{empty}$ applied to $C$ defined as the empty extension of $F$ and $\operatorname{empty}$ applied to $C$.
CategoryTheory.emptyEquivalencedefMathlib.CategoryTheory.PEmpty, function or constant
Wording
the empty equivalence (from the name)
English
The empty equivalence is an equivalence of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ defined as the equivalence of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$.
CategoryTheory.equivalenceOfIsEmptydefMathlib.CategoryTheory.PEmpty, function or constant
Wording
the equivalence of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the equivalence of $C$ and $D$ is an equivalence of $C$ and $D$.
CategoryTheory.functorOfIsEmptydefMathlib.CategoryTheory.PEmpty, function or constant
Wording
the functor of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the functor of $C$ and $D$ is a functor of $C$ and $D$.

Mathlib.CategoryTheory.PUnit

CategoryTheory.Functor.equivdefMathlib.CategoryTheory.PUnit, function or constant
Wording
the equivalence (from the name)
English
The equivalence is an equivalence of the set of functors of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$ and $C$.
CategoryTheory.Functor.fromPUnitdefMathlib.CategoryTheory.PUnit, function or constant
Wording
no wording
English
Let $X$ be an element of $C$. Then $\operatorname{fromPUnit}$ applied to $X$ is a functor of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$ defined as the action of the constant of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $X$.
CategoryTheory.Functor.punitExtdefMathlib.CategoryTheory.PUnit, function or constant
Wording
no wording
English
Let $F$ and $G$ be functors of $C$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Then $\operatorname{punitExt}$ applied to $F$ and $G$ is an isomorphism of $F$ and $G$.
CategoryTheory.Functor.stardefMathlib.CategoryTheory.PUnit, function or constant
Wording
the star of C (from the name)
English
Let $C$ be a set. Then the star of $C$ is a functor of $C$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ defined as the action of the constant of $C$ and $\operatorname{mk}$ applied to $\operatorname{unit}$.

Mathlib.CategoryTheory.PathCategory.Basic

CategoryTheory.PathsdefMathlib.CategoryTheory.PathCategory.Basic, type
Wording
path of V (from the name)
English
Let $V$ be a set. Then a path of $V$ is an element of the function that maps $V$ to $V$.
CategoryTheory.Paths.liftdefMathlib.CategoryTheory.PathCategory.Basic, function or constant
Wording
the lift of x2 (from the name)
English
Let $x_{2}$ be a prefunctor of $V$ and $C$. Then the lift of $x_{2}$ is a functor of the set of paths of $V$ and $C$.
CategoryTheory.Paths.ofdefMathlib.CategoryTheory.PathCategory.Basic, function or constant
Wording
no wording
English
Let $V$ be a set. Then $\operatorname{of}$ applied to $V$ is a prefunctor of $V$ and the set of paths of $V$ defined as $\operatorname{mk}$ applied to the function that maps $X$ to $X$ and the function that maps $x_{1}$, $x_{2}$ and $f$ to the path of $f$.
CategoryTheory.composePathdefMathlib.CategoryTheory.PathCategory.Basic, function or constant
Wording
no wording
English
Let $x_{1}$ be a path of $X$ and $Y$. Then $\operatorname{composePath}$ applied to $x_{1}$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_composePath\_\_\_f}$.
CategoryTheory.pathCompositiondefMathlib.CategoryTheory.PathCategory.Basic, function or constant
Wording
the path composition of C (from the name)
English
Let $C$ be a set. Then the path composition of $C$ is a functor of the set of paths of $C$ and $C$.
CategoryTheory.pathsHomReldefMathlib.CategoryTheory.PathCategory.Basic, function or constant
Wording
the canonical relation on the path category of C (from the docstring)
English
Let $C$ be a set. Then the canonical relation on the path category of $C$ is a homomorphism relation of the set of paths of $C$ defined as the function that maps $x_{1}$, $x_{2}$, $p$ and $q$ to the proposition that the map of the path composition of $C$ and $p$ is equal to the map of the path composition of $C$ and $q$.
CategoryTheory.quotientPathsEquivdefMathlib.CategoryTheory.PathCategory.Basic, function or constant
Wording
the canonical quotient of the path category of C (from the docstring)
English
Let $C$ be a set. Then the canonical quotient of the path category of $C$ is an equivalence of the set of quotients of the canonical relation on the path category of $C$ and $C$.
CategoryTheory.quotientPathsTodefMathlib.CategoryTheory.PathCategory.Basic, function or constant
Wording
the functor from the canonical quotient of C (from the docstring)
English
Let $C$ be a set. Then the functor from the canonical quotient of $C$ is a functor of the set of quotients of the canonical relation on the path category of $C$ and $C$ defined as the lift of the canonical relation on the path category of $C$ and the path composition of $C$.
CategoryTheory.toQuotientPathsdefMathlib.CategoryTheory.PathCategory.Basic, function or constant
Wording
the quotient path of C (from the name)
English
Let $C$ be a set. Then the quotient path of $C$ is a functor of $C$ and the set of quotients of the canonical relation on the path category of $C$.

Mathlib.CategoryTheory.PathCategory.MorphismProperty

CategoryTheory.MorphismProperty.pathsdefMathlib.CategoryTheory.PathCategory.MorphismProperty, function or constant
Wording
the path of W (from the name)
English
Let $W$ be a morphism property of $C$. Then the path of $W$ is a morphism property of the set of paths of $C$.
CategoryTheory.Paths.liftNatIsodefMathlib.CategoryTheory.PathCategory.MorphismProperty, function or constant
Wording
the lift natural isomorphism of x2 and v (from the name)
English
Let $x_{2}$ be a function from elements $v$ of $V$ to isomorphisms of the action of $F$ and $v$ and the action of $G$ and $v$ such that for all elements $X$ and $Y$ of $V$, for all homomorphisms $f$ of $X$ and $Y$, the composition of the map of $F$ and the path of $f$ and the homomorphism of $x_{2}$ applied to $Y$ is equal to the composition of the homomorphism of $x_{2}$ applied to $X$ and the map of $G$ and the path of $f$. Then the lift natural isomorphism of $v$ and $x_{2}$ is an isomorphism of $F$ and $G$.
CategoryTheory.Paths.liftNatTransdefMathlib.CategoryTheory.PathCategory.MorphismProperty, function or constant
Wording
the lift natural transformation of x2 and v (from the name)
English
Let $x_{2}$ be a function from elements $v$ of $V$ to homomorphisms of the action of $F$ and $v$ and the action of $G$ and $v$ such that for all elements $X$ and $Y$ of $V$, for all homomorphisms $f$ of $X$ and $Y$, the composition of the map of $F$ and the path of $f$ and $x_{2}$ applied to $Y$ is equal to the composition of $x_{2}$ applied to $X$ and the map of $G$ and the path of $f$. Then the lift natural transformation of $v$ and $x_{2}$ is a homomorphism of $F$ and $G$.

Mathlib.CategoryTheory.Pi.Basic

CategoryTheory.Equivalence.pidefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the product of E (from the name)
English
Let $E$ be a function from elements $i_{2}$ of $I$ to equivalences of $C$ applied to $i_{2}$ and $D$ applied to $i_{2}$. Then the product of $i_{2}$ is an equivalence of the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$ and the set of functions from elements $i_{1}$ of $I$ to elements of $D$ applied to $i_{1}$.
CategoryTheory.Functor.pidefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the product of F (from the name)
English
Let $F$ be a function from elements $i_{2}$ of $I$ to functors of $C$ applied to $i_{2}$ and $D$ applied to $i_{2}$. Then the product of $i_{2}$ is a functor of the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$ and the set of functions from elements $i_{1}$ of $I$ to elements of $D$ applied to $i_{1}$.
CategoryTheory.Functor.pi'defMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the product of f (from the name)
English
Let $f$ be a function from elements $i_{1}$ of $I$ to functors of $A$ and $C$ applied to $i_{1}$. Then the product of $i_{1}$ is a functor of $A$ and the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$.
CategoryTheory.Functor.pi'CompEvaldefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the product composition evaluation of F and i1 (from the name)
English
Let $F$ be a function from elements $i_{1}$ of $I$ to functors of $A$ and $C$ applied to $i_{1}$. Let $i$ be an element of $I$. Then the product composition evaluation of $i_{1}$ and $F$ is an isomorphism of the composition of the product of $F$ and the evaluation of $C$ and $i$ and $F$ applied to $i$ defined as the function that maps $i$ to the identity of the composition of the product of $i_{1}$ and the evaluation of $C$ and $F$.
CategoryTheory.NatIso.pidefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the product of e (from the name)
English
Let $e$ be a function from elements $i$ of $I$ to isomorphisms of $F$ applied to $i$ and $G$ applied to $i$. Then the product of $i$ is an isomorphism of the product of $F$ and the product of $G$.
CategoryTheory.NatIso.pi'defMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the product of e (from the name)
English
Let $e$ be a function from elements $i$ of $I$ to isomorphisms of the composition of $F$ and the evaluation of $C$ and $i$ and the composition of $G$ and the evaluation of $C$ and $i$. Then the product of $i$ is an isomorphism of $F$ and $G$.
CategoryTheory.NatTrans.pidefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the product of x2 (from the name)
English
Let $x_{2}$ be a function from elements $i$ of $I$ to homomorphisms of $F$ applied to $i$ and $G$ applied to $i$. Then the product of $i$ is a homomorphism of the product of $F$ and the product of $G$.
CategoryTheory.NatTrans.pi'defMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the product of x2 (from the name)
English
Let $x_{2}$ be a function from elements $i$ of $I$ to homomorphisms of the composition of $F$ and the evaluation of $C$ and $i$ and the composition of $G$ and the evaluation of $C$ and $i$. Then the product of $i$ is a homomorphism of $F$ and $G$.
CategoryTheory.Pi.comapdefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the preimage of C and h (from the name)
English
Let $C$ be a function from elements of $I$ to sets. Let $h$ be a function from elements of $J$ to elements of $I$. Then the preimage of $C$ and $h$ is a functor of the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$ and the set of functions from elements $j$ of $J$ to elements of $C$ applied to $h$ applied to $j$.
CategoryTheory.Pi.comapCompdefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the preimage composition of f and g (from the name)
English
Let $C$ be a function from elements of $I$ to sets. Let $f$ be a function from elements of $K$ to elements of $J$. Let $g$ be a function from elements of $J$ to elements of $I$. Then the preimage composition of $f$ and $g$ is an isomorphism of the composition of the preimage of $C$ and $g$ and the preimage of $\operatorname{comp}$ applied to $C$ and $g$ and $f$ and the preimage of $C$ and $\operatorname{comp}$ applied to $g$ and $f$.
CategoryTheory.Pi.comapEvalIsoEvaldefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the preimage evaluation isomorphism evaluation of h and j (from the name)
English
Let $C$ be a function from elements of $I$ to sets. Let $h$ be a function from elements of $J$ to elements of $I$. Let $j$ be an element of $J$. Then the preimage evaluation isomorphism evaluation of $h$ and $j$ is an isomorphism of the composition of the preimage of $C$ and $h$ and the evaluation of $\operatorname{comp}$ applied to $C$ and $h$ and $j$ and the evaluation of $C$ and $h$ applied to $j$.
CategoryTheory.Pi.comapIddefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the preimage identity of I and C (from the name)
English
Let $I$ be a set. Let $C$ be a function from elements of $I$ to sets. Then the preimage identity of $I$ and $C$ is an isomorphism of the preimage of $C$ and $\mathrm{id}$ and the identity of the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$.
CategoryTheory.Pi.eqToEquivalencedefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
no wording
English
Let $C$ be a function from elements of $I$ to sets. Assume that $\EqtMACRoH {i}{j}$. Then $\operatorname{eqToEquivalence}$ applied to $C$ and $h$ is an equivalence of $C$ applied to $i$ and $C$ applied to $j$ defined as $\operatorname{ndrec}$ applied to the identity and $h$.
CategoryTheory.Pi.eqToEquivalenceFunctorIsodefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
no wording
English
Let $C$ be a function from elements of $I$ to sets. Let $f$ be a function from elements of $J$ to elements of $I$. Assume that $\EqtMACRoH {\mathrm{i'}}{\mathrm{j'}}$. Then $\operatorname{eqToEquivalenceFunctorIso}$ applied to $C$, $f$ and $h$ is an isomorphism of the functor of $\operatorname{eqToEquivalence}$ applied to $C$ and $\mathrm{congr\_arg}$ applied to $f$ and $h$ and the functor of $\operatorname{eqToEquivalence}$ applied to the function that maps $\mathrm{i'1}$ to $C$ applied to $f$ applied to $\mathrm{i'1}$ and $h$.
CategoryTheory.Pi.equivalenceOfEquivdefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the equivalence of C and e (from the name)
English
Let $C$ be a function from elements of $I$ to sets. Let $e$ be an equivalence from $J$ to $I$. Then the equivalence of $C$ and $e$ is an equivalence of the set of functions from elements $j$ of $J$ to elements of $C$ applied to $e$ applied to $j$ and the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$.
CategoryTheory.Pi.evaldefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the evaluation of C and i (from the name)
English
Let $C$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then the evaluation of $C$ and $i$ is a functor of the set of functions from elements $i_{1}$ of $I$ to elements of $C$ applied to $i_{1}$ and $C$ applied to $i$.
CategoryTheory.Pi.evalCompEqToEquivalenceFunctordefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
no wording
English
Let $C$ be a function from elements of $I$ to sets. Assume that $\EqtMACRoH {i}{j}$. Then $\operatorname{evalCompEqToEquivalenceFunctor}$ applied to $C$ and $h$ is an isomorphism of the composition of the evaluation of $C$ and $i$ and the functor of $\operatorname{eqToEquivalence}$ applied to $C$ and $h$ and the evaluation of $C$ and $j$.
CategoryTheory.Pi.isoAppdefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the isomorphism application of f and i (from the name)
English
Let $f$ be an isomorphism of $X$ and $Y$. Let $i$ be an element of $I$. Then the isomorphism application of $f$ and $i$ is an isomorphism of $X$ applied to $i$ and $Y$ applied to $i$.
CategoryTheory.Pi.isoMkdefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the isomorphism of iso (from the name)
English
Let $\mathrm{iso}$ be a function from elements $i$ of $I$ to isomorphisms of $X$ applied to $i$ and $Y$ applied to $i$. Then the isomorphism of $i$ is an isomorphism of $X$ and $Y$.
CategoryTheory.Pi.optionEquivalencedefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the option equivalence of i (from the name)
English
Let $\mathrm{C'}$ be a function from elements of $\mathrm{Option}$ applied to $J$ to sets. Then the option equivalence of $\mathrm{C'}$ is an equivalence of the set of functions from elements $i$ of $\mathrm{Option}$ applied to $J$ to elements of $\mathrm{C'}$ applied to $i$ and $\mathrm{Prod}$ applied to $\mathrm{C'}$ applied to $\operatorname{none}$ and the set of functions from elements $j$ of $J$ to elements of $\mathrm{C'}$ applied to $\operatorname{some}$ applied to $j$.
CategoryTheory.Pi.sumdefMathlib.CategoryTheory.Pi.Basic, function or constant
Wording
the sum of C (from the name)
English
Let $C$ be a function from elements of $I$ to sets. Then the sum of $C$ is a functor of the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$ and the set of functors of the set of functions from elements $j$ of $J$ to elements of $D$ applied to $j$ and the set of functions from elements $s$ of $\mathrm{Sum}$ applied to $I$ and $J$ to elements of $\operatorname{elim}$ applied to $C$, $D$ and $s$.

Mathlib.CategoryTheory.Pi.Monoidal

CategoryTheory.Pi.closedCounitdefMathlib.CategoryTheory.Pi.Monoidal, function or constant
Wording
the counit for the adjunction of X (from the docstring)
English
Let $X$ be a function from elements $i_{1}$ of $I$ to elements of $C$ applied to $i_{1}$. Then the counit for the adjunction of $i_{1}$ is a homomorphism of the composition of $\operatorname{ihom}$ applied to $X$ and the left tensor of $X$ and the identity of the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$.
CategoryTheory.Pi.closedUnitdefMathlib.CategoryTheory.Pi.Monoidal, function or constant
Wording
the unit for the adjunction of X (from the docstring)
English
Let $X$ be a function from elements $i_{1}$ of $I$ to elements of $C$ applied to $i_{1}$. Then the unit for the adjunction of $i_{1}$ is a homomorphism of the identity of the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$ and the composition of the left tensor of $X$ and $\operatorname{ihom}$ applied to $X$.
CategoryTheory.Pi.ihomdefMathlib.CategoryTheory.Pi.Monoidal, function or constant
Wording
no wording
English
Let $X$ be a function from elements $i_{2}$ of $I$ to elements of $C$ applied to $i_{2}$. Then $\operatorname{ihom}$ applied to $i_{2}$ and $X$ is a functor of the set of functions from elements $i$ of $I$ to elements of $C$ applied to $i$ and the set of functions from elements $i_{1}$ of $I$ to elements of $C$ applied to $i_{1}$.

Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

CategoryTheory.AdditiveFunctordefMathlib.CategoryTheory.Preadditive.AdditiveFunctor, type
Wording
additive functor of C and D (from the name)
English
Let $C$ and $D$ be sets. Then an additive functor of $C$ and $D$ is an element of the function that maps $C$ and $D$ to the set of full subcategories of the additivity of $C$ and $D$.
CategoryTheory.AdditiveFunctor.forgetdefMathlib.CategoryTheory.Preadditive.AdditiveFunctor, function or constant
Wording
no wording
English
Let $C$ and $D$ be sets. Then $\operatorname{forget}$ applied to $C$ and $D$ is a functor of the set of additive functors of $C$ and $D$ and the set of functors of $C$ and $D$ defined as the inclusion of the additivity of $C$ and $D$.
CategoryTheory.AdditiveFunctor.ofdefMathlib.CategoryTheory.Preadditive.AdditiveFunctor, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Then $\operatorname{of}$ applied to $F$ is an additive functor of $C$ and $D$ defined as $\operatorname{mk}$ applied to $F$ and $h$.
CategoryTheory.AdditiveFunctor.ofExactdefMathlib.CategoryTheory.Preadditive.AdditiveFunctor, function or constant
Wording
the additive functor of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the additive functor of $C$ and $D$ is a functor of the set of exact functors of $C$ and $D$ and the set of additive functors of $C$ and $D$ defined as the inclusion of $\mathrm{CategoryTheory\_\_exactFunctor\_le\_additiveFunctor}$ applied to $C$ and $D$.
CategoryTheory.AdditiveFunctor.ofLeftExactdefMathlib.CategoryTheory.Preadditive.AdditiveFunctor, function or constant
Wording
the additive functor of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the additive functor of $C$ and $D$ is a functor of the set of left exact functors of $C$ and $D$ and the set of additive functors of $C$ and $D$ defined as the inclusion of $\mathrm{CategoryTheory\_\_leftExactFunctor\_le\_additiveFunctor}$ applied to $C$ and $D$.
CategoryTheory.AdditiveFunctor.ofRightExactdefMathlib.CategoryTheory.Preadditive.AdditiveFunctor, function or constant
Wording
the additive functor of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the additive functor of $C$ and $D$ is a functor of the set of right exact functors of $C$ and $D$ and the set of additive functors of $C$ and $D$ defined as the inclusion of $\mathrm{CategoryTheory\_\_rightExactFunctor\_le\_additiveFunctor}$ applied to $C$ and $D$.
CategoryTheory.Functor.AdditiveclassMathlib.CategoryTheory.Preadditive.AdditiveFunctor, predicate
Wording
F is additive (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ is additive.
CategoryTheory.Functor.mapAddHomdefMathlib.CategoryTheory.Preadditive.AdditiveFunctor, function or constant
Wording
the map additive homomorphism of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the map additive homomorphism of $F$ is an additive monoid homomorphism of the set of homomorphisms of $X$ and $Y$ and the set of homomorphisms of the action of $F$ and $X$ and the action of $F$ and $Y$ defined as $\operatorname{mk'}$ applied to the function that maps $f$ to the map of $F$ and $f$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{CategoryTheory\_\_Functor\_\_map\_add}$ applied to $F$.
CategoryTheory.additiveFunctordefMathlib.CategoryTheory.Preadditive.AdditiveFunctor, function or constant
Wording
the additivity of C and D (from the docstring)
English
Let $C$ and $D$ be sets. Then the additivity of $C$ and $D$ is an object property of the set of functors of $C$ and $D$ defined as the function that maps $F$ to the proposition that $F$ is additive.

Mathlib.CategoryTheory.Preadditive.Basic

CategoryTheory.End.addEquivdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the additive bijection (from the docstring)
English
The additive bijection is an additive equivalence of the set of ends of $X$ and the set of homomorphisms of $X$ and $X$.
CategoryTheory.InducedCategory.homAddEquivdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the additive equivalence (from the docstring)
English
The additive equivalence is an additive equivalence of the set of homomorphisms of $X$ and $Y$ and the set of homomorphisms of $F$ applied to $X$ and $F$ applied to $Y$.
CategoryTheory.PreadditiveclassMathlib.CategoryTheory.Preadditive.Basic, predicate
Wording
C is preadditive (from the docstring)
English
Let $C$ be a set. Then we can say that $C$ is preadditive.
CategoryTheory.Preadditive.coforkOfCokernelCoforkdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the cofork of c (from the name)
English
Let $c$ be a cokernel cofork of $f - g$. Then the cofork of $c$ is a cofork of $f$ and $g$.
CategoryTheory.Preadditive.cokernelCoforkOfCoforkdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the cokernel cofork of c (from the name)
English
Let $c$ be a cofork of $f$ and $g$. Then the cokernel cofork of $c$ is a cokernel cofork of $f - g$.
CategoryTheory.Preadditive.compHomdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the composition homomorphism (from the name)
English
The composition homomorphism is an additive monoid homomorphism of the set of homomorphisms of $P$ and $Q$ and the set of additive monoid homomorphisms of the set of homomorphisms of $Q$ and $R$ and the set of homomorphisms of $P$ and $R$.
CategoryTheory.Preadditive.forkOfKernelForkdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the fork of c (from the name)
English
Let $c$ be a kernel fork of $f - g$. Then the fork of $c$ is a fork of $f$ and $g$.
CategoryTheory.Preadditive.isColimitCoforkOfCokernelCoforkdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
no wording
English
Let $i$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCoforkOfCokernelCofork}$ applied to $i$ is an element of $\operatorname{IsColimit}$ applied to the cofork of $c$ defined as $\operatorname{mk'}$ applied to the cofork of $c$ and the function that maps $s$ to $\operatorname{desc}$ applied to $i$ and the cokernel cofork of $s$.
CategoryTheory.Preadditive.isColimitCokernelCoforkOfCoforkdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
no wording
English
Let $i$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCokernelCoforkOfCofork}$ applied to $i$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork of $c$ defined as $\operatorname{mk'}$ applied to the cokernel cofork of $c$ and the function that maps $s$ to $\operatorname{desc}$ applied to $i$ and the cofork of $s$.
CategoryTheory.Preadditive.isLimitForkOfKernelForkdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
no wording
English
Let $i$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitForkOfKernelFork}$ applied to $i$ is an element of $\operatorname{IsLimit}$ applied to the fork of $c$ defined as $\operatorname{mk'}$ applied to the fork of $c$ and the function that maps $s$ to the lift of $i$ and the kernel fork of $s$.
CategoryTheory.Preadditive.isLimitKernelForkOfForkdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
no wording
English
Let $i$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitKernelForkOfFork}$ applied to $i$ is an element of $\operatorname{IsLimit}$ applied to the kernel fork of $c$ defined as $\operatorname{mk'}$ applied to the kernel fork of $c$ and the function that maps $s$ to the lift of $i$ and the fork of $s$.
CategoryTheory.Preadditive.kernelForkOfForkdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the kernel fork of c (from the name)
English
Let $c$ be a fork of $f$ and $g$. Then the kernel fork of $c$ is a kernel fork of $f - g$.
CategoryTheory.Preadditive.leftCompdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the left composition of R and f (from the name)
English
Let $R$ be an element of $C$. Let $f$ be a homomorphism of $P$ and $Q$. Then the left composition of $R$ and $f$ is an additive monoid homomorphism of the set of homomorphisms of $Q$ and $R$ and the set of homomorphisms of $P$ and $R$.
CategoryTheory.Preadditive.rightCompdefMathlib.CategoryTheory.Preadditive.Basic, function or constant
Wording
the right composition of P and g (from the name)
English
Let $P$ be an element of $C$. Let $g$ be a homomorphism of $Q$ and $R$. Then the right composition of $P$ and $g$ is an additive monoid homomorphism of the set of homomorphisms of $P$ and $Q$ and the set of homomorphisms of $P$ and $R$.

Mathlib.CategoryTheory.Preadditive.Biproducts

CategoryTheory.Biprod.gaussiandefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of the biproduct of $x_{2}$ and $x_{3}$ and the biproduct of $x_{4}$ and $x_{5}$. Then $\operatorname{gaussian}$ applied to $f$ is an element of $\mathrm{PSigma}$ applied to the function that maps $L$ to $\mathrm{PSigma}$ applied to the function that maps $R$ to $\mathrm{PSigma}$ applied to the function that maps $x_{6}$ to the proposition that the composition of the homomorphism of $L$ and the composition of $f$ and the homomorphism of $R$ is equal to the map of the composition of the left injection and the composition of $f$ and the projection onto the first summand and $x_{6}$.
CategoryTheory.Biprod.gaussian'defMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $x_{6}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{5}$. Let $x_{8}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{5}$. Then $\operatorname{gaussian'}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\mathrm{PSigma}$ applied to the function that maps $L$ to $\mathrm{PSigma}$ applied to the function that maps $R$ to $\mathrm{PSigma}$ applied to the function that maps $x_{10}$ to the proposition that the composition of the homomorphism of $L$ and the composition of the biproduct of $x_{8}$ and $x_{9}$ and the homomorphism of $R$ is equal to the map of $x_{6}$ and $x_{10}$.
CategoryTheory.Biprod.isoElimdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the isomorphism eliminator of f (from the name)
English
Let $f$ be an isomorphism of the biproduct of $x_{2}$ and $x_{3}$ and the biproduct of $x_{4}$ and $x_{5}$. Then the isomorphism eliminator of $f$ is an isomorphism of $x_{3}$ and $x_{5}$ defined as the isomorphism eliminator of the composition of the right injection and the composition of the homomorphism of $f$ and the projection onto the first summand and the composition of the right injection and the composition of the homomorphism of $f$ and the projection onto the second summand.
CategoryTheory.Biprod.isoElim'defMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the isomorphism eliminator of x8 and x9 (from the name)
English
Let $x_{6}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{5}$. Let $x_{8}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{5}$. Then the isomorphism eliminator of $x_{8}$ and $x_{9}$ is an isomorphism of $x_{3}$ and $x_{5}$.
CategoryTheory.Biprod.ofComponentsdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the biproduct of x8 and x9 (from the name)
English
Let $x_{6}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{5}$. Let $x_{8}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{5}$. Then the biproduct of $x_{8}$ and $x_{9}$ is a homomorphism of the biproduct of $x_{2}$ and $x_{3}$ and the biproduct of $x_{4}$ and $x_{5}$ defined as the sum of the composition of the projection onto the first summand and the composition of $x_{6}$ and the left injection, the composition of the projection onto the first summand and the composition of $x_{7}$ and the right injection, the composition of the projection onto the second summand and the composition of $x_{8}$ and the left injection and the composition of the projection onto the second summand and the composition of $x_{9}$ and the right injection.
CategoryTheory.Biprod.unipotentLowerdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the unipotent lower triangular matrix of r (from the docstring)
English
Let $r$ be a homomorphism of $x_{3}$ and $x_{2}$. Then the unipotent lower triangular matrix of $r$ is an isomorphism of the biproduct of $x_{2}$ and $x_{3}$ and the biproduct of $x_{2}$ and $x_{3}$.
CategoryTheory.Biprod.unipotentUpperdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the unipotent upper triangular matrix of r (from the docstring)
English
Let $r$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the unipotent upper triangular matrix of $r$ is an isomorphism of the biproduct of $x_{2}$ and $x_{3}$ and the biproduct of $x_{2}$ and $x_{3}$.
CategoryTheory.Biproduct.columnNonzeroOfIsodefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the column nonzero of s and f (from the name)
English
Let $s$ be an element of $x_{2}$ such that the identity morphism of $S$ applied to $s$ is distinct from $0$. Let $f$ be a homomorphism of the biproduct of $S$ and the biproduct of $T$. Then the column nonzero of $s$ and $f$ is a truncation of $\mathrm{PSigma}$ applied to the function that maps $t$ to the proposition that the composition of the inclusion into a summand of $S$ and $s$ and the composition of $f$ and the projection onto a summand of $T$ and $t$ is distinct from $0$.
CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFstdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $b$ be a binary bicone of $X$ and $Y$. Let $\mathrm{hb}$ be an element of $\operatorname{IsColimit}$ applied to the right injection cokernel cofork of $b$. Then $\operatorname{isBilimitOfCokernelFst}$ applied to $b$ and $\mathrm{hb}$ is an element of $\operatorname{IsBilimit}$ applied to $b$.
CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelSnddefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $b$ be a binary bicone of $X$ and $Y$. Let $\mathrm{hb}$ be an element of $\operatorname{IsColimit}$ applied to the left injection cokernel cofork of $b$. Then $\operatorname{isBilimitOfCokernelSnd}$ applied to $b$ and $\mathrm{hb}$ is an element of $\operatorname{IsBilimit}$ applied to $b$.
CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInldefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $b$ be a binary bicone of $X$ and $Y$. Let $\mathrm{hb}$ be an element of $\operatorname{IsLimit}$ applied to the second component kernel fork of $b$. Then $\operatorname{isBilimitOfKernelInl}$ applied to $b$ and $\mathrm{hb}$ is an element of $\operatorname{IsBilimit}$ applied to $b$.
CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInrdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $b$ be a binary bicone of $X$ and $Y$. Let $\mathrm{hb}$ be an element of $\operatorname{IsLimit}$ applied to the first component kernel fork of $b$. Then $\operatorname{isBilimitOfKernelInr}$ applied to $b$ and $\mathrm{hb}$ is an element of $\operatorname{IsBilimit}$ applied to $b$.
CategoryTheory.Limits.BinaryBicone.ofColimitCoconedefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the binary bicone of ht (from the name)
English
Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then the binary bicone of $\mathrm{ht}$ is a binary bicone of $X$ and $Y$.
CategoryTheory.Limits.BinaryBicone.ofLimitConedefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the binary bicone of ht (from the name)
English
Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then the binary bicone of $\mathrm{ht}$ is a binary bicone of $X$ and $Y$.
CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimitdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then $\operatorname{biconeIsBilimitOfColimitCoconeOfIsColimit}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsBilimit}$ applied to the bicone of $\mathrm{ht}$.
CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimitdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then $\operatorname{biconeIsBilimitOfLimitConeOfIsLimit}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsBilimit}$ applied to the bicone of $\mathrm{ht}$.
CategoryTheory.Limits.binaryBiconeIsBilimitOfColimitCoconeOfIsColimitdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then $\operatorname{binaryBiconeIsBilimitOfColimitCoconeOfIsColimit}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsBilimit}$ applied to the binary bicone of $\mathrm{ht}$.
CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimitdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then $\operatorname{binaryBiconeIsBilimitOfLimitConeOfIsLimit}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsBilimit}$ applied to the binary bicone of $\mathrm{ht}$.
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKerneldefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the binary bicone of i (from the name)
English
Let $i$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the binary bicone of $i$ is a binary bicone of $\operatorname{pt}$ applied to $c$ and $Y$.
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokerneldefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the binary bicone of i (from the name)
English
Let $i$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the binary bicone of $i$ is a binary bicone of $X$ and $\operatorname{pt}$ applied to $c$.
CategoryTheory.Limits.biproduct.reindexdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
the reindexing of x4 and f (from the name)
English
Let $x_{4}$ be an equivalence from $x_{2}$ to $x_{3}$. Let $f$ be a function from elements of $x_{3}$ to elements of $C$. Then the reindexing of $x_{4}$ and $f$ is an isomorphism of the biproduct of $\operatorname{comp}$ applied to $f$ and $\operatorname{coe}$ applied to $x_{4}$ and the biproduct of $f$.
CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKerneldefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $i$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isBilimitBinaryBiconeOfIsSplitEpiOfKernel}$ applied to $i$ is an element of $\operatorname{IsBilimit}$ applied to the binary bicone of $i$.
CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokerneldefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $i$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isBilimitBinaryBiconeOfIsSplitMonoOfCokernel}$ applied to $i$ is an element of $\operatorname{IsBilimit}$ applied to the binary bicone of $i$.
CategoryTheory.Limits.isBilimitOfIsColimitdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $t$ be a bicone of $f$. Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to the cocone of $t$. Then $\operatorname{isBilimitOfIsColimit}$ applied to $t$ and $\mathrm{ht}$ is an element of $\operatorname{IsBilimit}$ applied to $t$.
CategoryTheory.Limits.isBilimitOfIsLimitdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $t$ be a bicone of $f$. Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to the cone of $t$. Then $\operatorname{isBilimitOfIsLimit}$ applied to $t$ and $\mathrm{ht}$ is an element of $\operatorname{IsBilimit}$ applied to $t$.
CategoryTheory.Limits.isBilimitOfTotaldefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $b$ be a bicone of $f$ such that $\EqtMACRoH {\FinsetSum {\FinsetunivMACRoAC}{j}{\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_Bicone\_\_\_u3c0\_} (b , j), \mathrm{CategoryTheory\_\_Limits\_\_Bicone\_\_\_u3b9\_} (b , j))}}{\operatorname{id} (\operatorname{pt} (b))}$. Then $\operatorname{isBilimitOfTotal}$ applied to $b$ and $\mathrm{total}$ is an element of $\operatorname{IsBilimit}$ applied to $b$.
CategoryTheory.Limits.isBinaryBilimitOfIsColimitdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $t$ be a binary bicone of $X$ and $Y$. Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to the cocone of $t$. Then $\operatorname{isBinaryBilimitOfIsColimit}$ applied to $t$ and $\mathrm{ht}$ is an element of $\operatorname{IsBilimit}$ applied to $t$.
CategoryTheory.Limits.isBinaryBilimitOfIsLimitdefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $t$ be a binary bicone of $X$ and $Y$. Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to the cone of $t$. Then $\operatorname{isBinaryBilimitOfIsLimit}$ applied to $t$ and $\mathrm{ht}$ is an element of $\operatorname{IsBilimit}$ applied to $t$.
CategoryTheory.Limits.isBinaryBilimitOfTotaldefMathlib.CategoryTheory.Preadditive.Biproducts, function or constant
Wording
no wording
English
Let $b$ be a binary bicone of $X$ and $Y$ such that the sum of the composition of the first component of $b$ and the left injection of $b$ and the composition of the second component of $b$ and the right injection of $b$ is equal to the identity morphism of $\operatorname{pt}$ applied to $b$. Then $\operatorname{isBinaryBilimitOfTotal}$ applied to $b$ and $\mathrm{total}$ is an element of $\operatorname{IsBilimit}$ applied to $b$.

Mathlib.CategoryTheory.Preadditive.CommGrp_

CategoryTheory.Preadditive.commGrpEquivalencedefMathlib.CategoryTheory.Preadditive.CommGrp_, function or constant
Wording
the commutative group equivalence (from the name)
English
The commutative group equivalence is an equivalence of $C$ and the set of commutative groups of $C$.
CategoryTheory.Preadditive.toCommGrpdefMathlib.CategoryTheory.Preadditive.CommGrp_, function or constant
Wording
the commutative group of C (from the name)
English
Let $C$ be a set. Then the commutative group of $C$ is a functor of $C$ and the set of commutative groups of $C$.

Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

CategoryTheory.Arrow.LeftHomotopystructureMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, type
Wording
left homotopy of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $u$ and $v$. Then the left homotopies of $f$ and $g$ are a basic type.
CategoryTheory.Arrow.LeftHomotopy.adddefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the sum of x6 and x7 (from the name)
English
Let $x_{6}$ be a left homotopy of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a left homotopy of $x_{4}$ and $x_{5}$. Then the sum of $x_{6}$ and $x_{7}$ is a left homotopy of $x_{2} + x_{4}$ and $x_{3} + x_{5}$.
CategoryTheory.Arrow.LeftHomotopy.compdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the composition of x6 and x7 (from the name)
English
Let $x_{6}$ be a left homotopy of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a left homotopy of $x_{4}$ and $x_{5}$. Then the composition of $x_{6}$ and $x_{7}$ is a left homotopy of the composition of $x_{2}$ and $x_{4}$ and the composition of $x_{3}$ and $x_{5}$ defined as the composition of the right composition of $x_{6}$ and $x_{4}$ and the left composition of $x_{7}$ and $x_{3}$.
CategoryTheory.Arrow.LeftHomotopy.compLeftdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the left composition of h and e (from the name)
English
Let $h$ be a left homotopy of $f$ and $g$. Let $e$ be a homomorphism of $u$ and $v$. Then the left composition of $h$ and $e$ is a left homotopy of the composition of $e$ and $f$ and the composition of $e$ and $g$.
CategoryTheory.Arrow.LeftHomotopy.compLeftIddefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the composition left identity of h and g (from the name)
English
Let $h$ be a left homotopy of $f$ and the identity morphism of $v$. Let $g$ be a homomorphism of $u$ and $v$. Then the composition left identity of $h$ and $g$ is a left homotopy of the composition of $g$ and $f$ and $g$.
CategoryTheory.Arrow.LeftHomotopy.compRightdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the right composition of h and g (from the name)
English
Let $h$ be a left homotopy of $e$ and $f$. Let $g$ be a homomorphism of $v$ and $w$. Then the right composition of $h$ and $g$ is a left homotopy of the composition of $e$ and $g$ and the composition of $f$ and $g$.
CategoryTheory.Arrow.LeftHomotopy.compRightIddefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the composition right identity of h and g (from the name)
English
Let $h$ be a left homotopy of $f$ and the identity morphism of $u$. Let $g$ be a homomorphism of $u$ and $v$. Then the composition right identity of $h$ and $g$ is a left homotopy of the composition of $f$ and $g$ and $g$.
CategoryTheory.Arrow.LeftHomotopy.equivSubZerodefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the equivalence difference zero (from the name)
English
The equivalence difference zero is an equivalence from the set of left homotopies of $f$ and $g$ to the set of left homotopies of $f - g$ and $0$.
CategoryTheory.Arrow.LeftHomotopy.homdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a left homotopy of $f$ and $g$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the right object of $u$ and the left object of $v$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Arrow.LeftHomotopy.ofEqdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the left homotopy of h (from the name)
English
Assume that $\EqtMACRoH {f}{g}$. Then the left homotopy of $h$ is a left homotopy of $f$ and $g$.
CategoryTheory.Arrow.LeftHomotopy.refldefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the identity of f (from the name)
English
Let $f$ be a homomorphism of $u$ and $v$. Then the identity of $f$ is a left homotopy of $f$ and $f$.
CategoryTheory.Arrow.LeftHomotopy.symmdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
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$.
CategoryTheory.Arrow.LeftHomotopy.transdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the composition of h and k (from the name)
English
Let $h$ be a left homotopy of $e$ and $f$. Let $k$ be a left homotopy of $f$ and $g$. Then the composition of $h$ and $k$ is a left homotopy of $e$ and $g$.
CategoryTheory.Arrow.RightHomotopystructureMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, type
Wording
right homotopy of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $u$ and $v$. Then the right homotopies of $f$ and $g$ are a basic type.
CategoryTheory.Arrow.RightHomotopy.adddefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the sum of x6 and x7 (from the name)
English
Let $x_{6}$ be a right homotopy of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a right homotopy of $x_{4}$ and $x_{5}$. Then the sum of $x_{6}$ and $x_{7}$ is a right homotopy of $x_{2} + x_{4}$ and $x_{3} + x_{5}$.
CategoryTheory.Arrow.RightHomotopy.compdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the composition of x6 and x7 (from the name)
English
Let $x_{6}$ be a right homotopy of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a right homotopy of $x_{4}$ and $x_{5}$. Then the composition of $x_{6}$ and $x_{7}$ is a right homotopy of the composition of $x_{2}$ and $x_{4}$ and the composition of $x_{3}$ and $x_{5}$ defined as the composition of the right composition of $x_{6}$ and $x_{4}$ and the left composition of $x_{7}$ and $x_{3}$.
CategoryTheory.Arrow.RightHomotopy.compLeftdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the left composition of h and e (from the name)
English
Let $h$ be a right homotopy of $f$ and $g$. Let $e$ be a homomorphism of $u$ and $v$. Then the left composition of $h$ and $e$ is a right homotopy of the composition of $e$ and $f$ and the composition of $e$ and $g$.
CategoryTheory.Arrow.RightHomotopy.compLeftIddefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the composition left identity of h and g (from the name)
English
Let $h$ be a right homotopy of $f$ and the identity morphism of $v$. Let $g$ be a homomorphism of $u$ and $v$. Then the composition left identity of $h$ and $g$ is a right homotopy of the composition of $g$ and $f$ and $g$.
CategoryTheory.Arrow.RightHomotopy.compRightdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the right composition of h and g (from the name)
English
Let $h$ be a right homotopy of $e$ and $f$. Let $g$ be a homomorphism of $v$ and $w$. Then the right composition of $h$ and $g$ is a right homotopy of the composition of $e$ and $g$ and the composition of $f$ and $g$.
CategoryTheory.Arrow.RightHomotopy.compRightIddefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the composition right identity of h and g (from the name)
English
Let $h$ be a right homotopy of $f$ and the identity morphism of $u$. Let $g$ be a homomorphism of $u$ and $v$. Then the composition right identity of $h$ and $g$ is a right homotopy of the composition of $f$ and $g$ and $g$.
CategoryTheory.Arrow.RightHomotopy.equivSubZerodefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the equivalence difference zero (from the name)
English
The equivalence difference zero is an equivalence from the set of right homotopies of $f$ and $g$ to the set of right homotopies of $f - g$ and $0$.
CategoryTheory.Arrow.RightHomotopy.homdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a right homotopy of $f$ and $g$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the right object of $u$ and the left object of $v$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Arrow.RightHomotopy.ofEqdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the right homotopy of h (from the name)
English
Assume that $\EqtMACRoH {f}{g}$. Then the right homotopy of $h$ is a right homotopy of $f$ and $g$.
CategoryTheory.Arrow.RightHomotopy.refldefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the identity of f (from the name)
English
Let $f$ be a homomorphism of $u$ and $v$. Then the identity of $f$ is a right homotopy of $f$ and $f$.
CategoryTheory.Arrow.RightHomotopy.symmdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
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$.
CategoryTheory.Arrow.RightHomotopy.transdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
the composition of h and k (from the name)
English
Let $h$ be a right homotopy of $e$ and $f$. Let $k$ be a right homotopy of $f$ and $g$. Then the composition of $h$ and $k$ is a right homotopy of $e$ and $g$.
CategoryTheory.Arrow.leftHomotopicdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
no wording
English
Let $V$ be a set. Then there is a homomorphism relation of the set of arrows of $V$. Proof. Let $V$ be arbitrary. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $f$ be arbitrary. Let $g$ be arbitrary. By f. By g. By CategoryTheory__Arrow__LeftHomotopy. By Nonempty.
CategoryTheory.Arrow.rightHomotopicdefMathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy, function or constant
Wording
no wording
English
Let $V$ be a set. Then there is a homomorphism relation of the set of arrows of $V$. Proof. Let $V$ be arbitrary. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $f$ be arbitrary. Let $g$ be arbitrary. By f. By g. By CategoryTheory__Arrow__RightHomotopy. By Nonempty.

Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

CategoryTheory.Preadditive.RightFreyddefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, type
Wording
no wording
English
Let $V$ be a set. Then an element of $\operatorname{RightFreyd}$ applied to $V$ is an element of the function that maps $V$ to the set of quotients of $\operatorname{rightHomotopic}$ applied to $V$.
CategoryTheory.Preadditive.RightFreyd.Candidate.cokerneldefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
the cokernel of f (from the name)
English
Let $f$ be a homomorphism of $u$ and $v$. Then the cokernel of $f$ is an arrow of $V$ defined as $\operatorname{mk}$ applied to $\operatorname{desc}$ applied to the homomorphism of $v$ and the right part of $f$.
CategoryTheory.Preadditive.RightFreyd.Candidate.cokernelCoforkdefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
the cokernel cofork of f (from the name)
English
Let $f$ be a homomorphism of $u$ and $v$. Then the cokernel cofork of $f$ is a cokernel cofork of the map of the quotient of $V$ and $f$.
CategoryTheory.Preadditive.RightFreyd.Candidate.conditiondefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
the condition of f (from the name)
English
Let $f$ be a homomorphism of $u$ and $v$. Then the condition of $f$ is a right homotopy of the composition of $f$ and the projection of $f$ and $0$.
CategoryTheory.Preadditive.RightFreyd.Candidate.descdefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $u$ and $v$. Let $g$ be a homomorphism of $v$ and $w$. Let $h_{1}$ be a right homotopy of the composition of $f$ and $g$ and $0$. Then $\operatorname{desc}$ applied to $f$, $g$ and $h_{1}$ is a homomorphism of the cokernel of $f$ and $w$.
CategoryTheory.Preadditive.RightFreyd.Candidate.isColimitCokernelCoforkdefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $u$ and $v$. Then $\operatorname{isColimitCokernelCofork}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork of $f$.
CategoryTheory.Preadditive.RightFreyd.Candidate.πdefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
the projection of f (from the name)
English
Let $f$ be a homomorphism of $u$ and $v$. Then the projection of $f$ is a homomorphism of $v$ and the cokernel of $f$.
CategoryTheory.Preadditive.RightFreyd.functordefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
the functor of V (from the name)
English
Let $V$ be a set. Then the functor of $V$ is a functor of $V$ and $\operatorname{RightFreyd}$ applied to $V$ defined as the composition of the right functor of $V$ and the quotient of $V$.
CategoryTheory.Preadditive.RightFreyd.homotopyOfEqdefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
the homotopy of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $u$ and $v$ such that the map of the quotient of $V$ and $f$ is equal to the map of the quotient of $V$ and $g$. Then the homotopy of $f$ and $g$ is a right homotopy of $f$ and $g$.
CategoryTheory.Preadditive.RightFreyd.quotientdefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
the quotient of V (from the name)
English
Let $V$ be a set. Then the quotient of $V$ is a functor of the set of arrows of $V$ and $\operatorname{RightFreyd}$ applied to $V$ defined as the functor of $\operatorname{rightHomotopic}$ applied to $V$.
CategoryTheory.Preadditive.RightFreyd.rightFunctordefMathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd, function or constant
Wording
the right functor of V (from the name)
English
Let $V$ be a set. Then the right functor of $V$ is a functor of $V$ and the set of arrows of $V$.

Mathlib.CategoryTheory.Preadditive.FunctorCategory

CategoryTheory.NatTrans.appHomdefMathlib.CategoryTheory.Preadditive.FunctorCategory, function or constant
Wording
the application homomorphism of X (from the name)
English
Let $X$ be an element of $C$. Then the application homomorphism of $X$ is an additive monoid homomorphism of the set of homomorphisms of $F$ and $G$ and the set of homomorphisms of the action of $F$ and $X$ and the action of $G$ and $X$.

Mathlib.CategoryTheory.Preadditive.HomOrthogonal

CategoryTheory.HomOrthogonaldefMathlib.CategoryTheory.Preadditive.HomOrthogonal, predicate
Wording
no wording
English
Let $s$ be a function from elements of $x_{1}$ to elements of $C$. Then $\operatorname{HomOrthogonal}$ holds for $s$, if the function that maps $i$ and $j$ to the proposition that the set of homomorphisms of $s$ applied to $i$ and $s$ applied to $j$ is a subsingleton is pairwise.
CategoryTheory.HomOrthogonal.matrixDecompositiondefMathlib.CategoryTheory.Preadditive.HomOrthogonal, function or constant
Wording
the matrix decomposition of o (from the name)
English
Assume that $\operatorname{HomOrthogonal}$ holds for $s$. Then the matrix decomposition of $o$ is an equivalence from the set of homomorphisms of the biproduct of the function that maps $a$ to $s$ applied to $f$ applied to $a$ and the biproduct of the function that maps $b$ to $s$ applied to $g$ applied to $b$ to the set of functions from elements $i$ of $x_{1}$ to matrixes of the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $i$ and the set of ends of $s$ applied to $i$.
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquivdefMathlib.CategoryTheory.Preadditive.HomOrthogonal, function or constant
Wording
the matrix decomposition additive equivalence of o (from the name)
English
Assume that $\operatorname{HomOrthogonal}$ holds for $s$. Then the matrix decomposition additive equivalence of $o$ is an additive equivalence of the set of homomorphisms of the biproduct of the function that maps $a$ to $s$ applied to $f$ applied to $a$ and the biproduct of the function that maps $b$ to $s$ applied to $g$ applied to $b$ and the set of functions from elements $i$ of $x_{1}$ to matrixes of the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $i$ and the set of ends of $s$ applied to $i$.
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquivdefMathlib.CategoryTheory.Preadditive.HomOrthogonal, function or constant
Wording
the matrix decomposition linear equivalence of o (from the name)
English
Assume that $\operatorname{HomOrthogonal}$ holds for $s$. Then the matrix decomposition linear equivalence of $o$ is a linear equivalence of the set of homomorphisms of the biproduct of the function that maps $a$ to $s$ applied to $f$ applied to $a$ and the biproduct of the function that maps $b$ to $s$ applied to $g$ applied to $b$ and the set of functions from elements $i$ of $x_{1}$ to matrixes of the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $i$ and the set of ends of $s$ applied to $i$.

Mathlib.CategoryTheory.Preadditive.Injective.Basic

CategoryTheory.Adjunction.injectivePresentationOfMapdefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
the injective presentation of X and I (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $X$ be an element of $C$. Let $I$ be an injective presentation of the action of $F$ and $X$. Then the injective presentation of $X$ and $I$ is an injective presentation of $X$.
CategoryTheory.Adjunction.mapInjectivePresentationdefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
the map injective presentation of X and I (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $X$ be an element of $D$. Let $I$ be an injective presentation of $X$. Then the map injective presentation of $X$ and $I$ is an injective presentation of the action of $G$ and $X$.
CategoryTheory.EnoughInjectivesclassMathlib.CategoryTheory.Preadditive.Injective.Basic, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{EnoughInjectives}$ holds for $C$.
CategoryTheory.Equivalence.injectivePresentationOfMapInjectivePresentationdefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
the injective presentation of X and I (from the name)
English
Let $F$ be an equivalence of $C$ and $D$. Let $X$ be an element of $C$. Let $I$ be an injective presentation of the action of the functor of $F$ and $X$. Then the injective presentation of $X$ and $I$ is an injective presentation of $X$ defined as the injective presentation of $X$ and $I$.
CategoryTheory.InjectiveclassMathlib.CategoryTheory.Preadditive.Injective.Basic, predicate
Wording
J is injective (from the name)
English
Let $J$ be an element of $C$. Then we can say that $J$ is injective.
CategoryTheory.Injective.ddefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{d}$ applied to $f$ is a homomorphism of $Y$ and $\operatorname{syzygies}$ applied to $f$ defined as the composition of the projection of $f$ and the inclusion of the cokernel of $f$.
CategoryTheory.Injective.factorThrudefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
no wording
English
Let $g$ be a homomorphism of $X$ and $J$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{factorThru}$ applied to $g$ and $f$ is a homomorphism of $Y$ and $J$ defined as $\operatorname{choose}$ applied to $\operatorname{factors}$ applied to $g$ and $f$.
CategoryTheory.Injective.syzygiesdefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{syzygies}$ applied to $f$ is an element of $C$ defined as $\operatorname{under}$ applied to the cokernel of $f$.
CategoryTheory.Injective.underdefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
no wording
English
Let $X$ be an element of $C$. Then $\operatorname{under}$ applied to $X$ is an element of $C$ defined as $\operatorname{J}$ applied to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Injective\_\_exists\_presentation}$ applied to $X$.
CategoryTheory.Injective.ιdefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
the inclusion of X (from the name)
English
Let $X$ be an element of $C$. Then the inclusion of $X$ is a homomorphism of $X$ and $\operatorname{under}$ applied to $X$ defined as $\operatorname{f}$ applied to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Injective\_\_exists\_presentation}$ applied to $X$.
CategoryTheory.InjectivePresentationstructureMathlib.CategoryTheory.Preadditive.Injective.Basic, type
Wording
injective presentation of X (from the name)
English
Let $X$ be an element of $C$. Then the injective presentations of $X$ are a basic type.
CategoryTheory.InjectivePresentation.JdefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an injective presentation of $X$. Then $\operatorname{J}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.InjectivePresentation.fdefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an injective presentation of $X$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\operatorname{J}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.isInjectivedefMathlib.CategoryTheory.Preadditive.Injective.Basic, function or constant
Wording
no wording
English
Let $C$ be a set. Then there is an object property of $C$. Proof. Let $C$ be arbitrary. By CategoryTheory__Injective.

Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject

CategoryTheory.InjectiveObjectdefMathlib.CategoryTheory.Preadditive.Injective.InjectiveObject, type
Wording
injective object of C (from the name)
English
Let $C$ be a set. Then an injective object of $C$ is an element of the function that maps $C$ to the set of full subcategories of $\operatorname{isInjective}$ applied to $C$.
CategoryTheory.InjectiveObject.ιdefMathlib.CategoryTheory.Preadditive.Injective.InjectiveObject, function or constant
Wording
the inclusion of C (from the docstring)
English
Let $C$ be a set. Then the inclusion of $C$ is a functor of the set of injective objects of $C$ and $C$ defined as the inclusion of $\operatorname{isInjective}$ applied to $C$.

Mathlib.CategoryTheory.Preadditive.Injective.Preserves

CategoryTheory.Functor.PreservesInjectiveObjectsclassMathlib.CategoryTheory.Preadditive.Injective.Preserves, predicate
Wording
F preserves injective objects (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ preserves injective objects.

Mathlib.CategoryTheory.Preadditive.Injective.Resolution

CategoryTheory.HasInjectiveResolutionclassMathlib.CategoryTheory.Preadditive.Injective.Resolution, predicate
Wording
Z has injective resolutions (from the name)
English
Let $Z$ be an element of $C$. Then we can say that $Z$ has injective resolutions.
CategoryTheory.HasInjectiveResolutionsclassMathlib.CategoryTheory.Preadditive.Injective.Resolution, predicate
Wording
C has injective resolutions (from the name)
English
Let $C$ be a set. Then we can say that $C$ has injective resolutions.
CategoryTheory.InjectiveResolutionstructureMathlib.CategoryTheory.Preadditive.Injective.Resolution, type
Wording
injective resolution of Z (from the name)
English
Let $Z$ be an element of $C$. Then the injective resolutions of $Z$ are a basic type.
CategoryTheory.InjectiveResolution.HomstructureMathlib.CategoryTheory.Preadditive.Injective.Resolution, type
Wording
homomorphism of f and #3 (from the name)
English
Let $I$ be an injective resolution of $Z$. Let $\mathrm{I'}$ be an injective resolution of $\mathrm{Z'}$. Let $f$ be a homomorphism of $Z$ and $\mathrm{Z'}$. Then the homomorphisms of $\mathrm{I'}$ and $f$ are a basic type.
CategoryTheory.InjectiveResolution.Hom.homdefMathlib.CategoryTheory.Preadditive.Injective.Resolution, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $\mathrm{I'}$ and $f$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $\operatorname{cocomplex}$ applied to $I$ and $\operatorname{cocomplex}$ applied to $\mathrm{I'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.InjectiveResolution.cocomplexdefMathlib.CategoryTheory.Preadditive.Injective.Resolution, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an injective resolution of $Z$. Then $\operatorname{cocomplex}$ applied to $\mathrm{self}$ is a cochain complex of $C$ and $\Natural$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.InjectiveResolution.isLimitKernelForkdefMathlib.CategoryTheory.Preadditive.Injective.Resolution, function or constant
Wording
no wording
English
Let $I$ be an injective resolution of $Z$. Then $\operatorname{isLimitKernelFork}$ applied to $I$ is an element of $\operatorname{IsLimit}$ applied to the kernel fork of $I$.
CategoryTheory.InjectiveResolution.kernelForkdefMathlib.CategoryTheory.Preadditive.Injective.Resolution, function or constant
Wording
the kernel fork of I (from the name)
English
Let $I$ be an injective resolution of $Z$. Then the kernel fork of $I$ is a kernel fork of $\operatorname{d}$ applied to $\operatorname{cocomplex}$ applied to $I$, $0$ and $1$ defined as the inclusion of $\operatorname{f}$ applied to the inclusion of $I$ and $0$ and $\mathrm{CategoryTheory\_\_InjectiveResolution\_\_\_u3b9\_\_f\_zero\_comp\_complex\_d}$ applied to $I$.
CategoryTheory.InjectiveResolution.selfdefMathlib.CategoryTheory.Preadditive.Injective.Resolution, function or constant
Wording
the self of Z (from the name)
English
Let $Z$ be an element of $C$. Then the self of $Z$ is an injective resolution of $Z$.
CategoryTheory.InjectiveResolution.ιdefMathlib.CategoryTheory.Preadditive.Injective.Resolution, function or constant
Wording
the inclusion of self (from the name)
English
Let $\mathrm{self}$ be an injective resolution of $Z$. Then the inclusion of $\mathrm{self}$ is a homomorphism of the action of $\mathrm{CochainComplex\_\_single\_u2080\_}$ applied to $C$ and $Z$ and $\operatorname{cocomplex}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Mathlib.CategoryTheory.Preadditive.LeftExact

CategoryTheory.Functor.isColimitMapCoconeBinaryCofanOfPreservesCokernelsdefMathlib.CategoryTheory.Preadditive.LeftExact, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Let $x_{4}$ be a homomorphism of $X$ and $Z$. Let $x_{5}$ be a homomorphism of $Y$ and $Z$. Let $i$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $x_{4}$ and $x_{5}$. Then $\operatorname{isColimitMapCoconeBinaryCofanOfPreservesCokernels}$ applied to $F$, $x_{4}$, $x_{5}$ and $i$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and $\operatorname{mk}$ applied to $x_{4}$ and $x_{5}$.
CategoryTheory.Functor.isLimitMapConeBinaryFanOfPreservesKernelsdefMathlib.CategoryTheory.Preadditive.LeftExact, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Let $x_{4}$ be a homomorphism of $Z$ and $X$. Let $x_{5}$ be a homomorphism of $Z$ and $Y$. Let $i$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $x_{4}$ and $x_{5}$. Then $\operatorname{isLimitMapConeBinaryFanOfPreservesKernels}$ applied to $F$, $x_{4}$, $x_{5}$ and $i$ is an element of $\operatorname{IsLimit}$ applied to the map cone of $F$ and $\operatorname{mk}$ applied to $x_{4}$ and $x_{5}$.

Mathlib.CategoryTheory.Preadditive.Mat

CategoryTheory.Functor.mapMatCompdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the map matrix composition of F and G (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the map matrix composition of $F$ and $G$ is an isomorphism of the map matrix of the composition of $F$ and $G$ and the composition of the map matrix of $F$ and the map matrix of $G$.
CategoryTheory.Functor.mapMatIddefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the map matrix identity (from the name)
English
The map matrix identity is an isomorphism of the map matrix of the identity of $C$ and the identity of the set of matrixes of $C$.
CategoryTheory.Functor.mapMat_defMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the map matrix of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the map matrix of $F$ is a functor of the set of matrixes of $C$ and the set of matrixes of $D$.
CategoryTheory.MatdefMathlib.CategoryTheory.Preadditive.Mat, type
Wording
matrix of x (from the name)
English
Let $x$ be a set. Then a matrix of $x$ is an element of the function that maps $x$ to the set of finite type categories.
CategoryTheory.Mat.equivalenceSingleObjdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the equivalence single object of R (from the name)
English
Let $R$ be a set. Then the equivalence single object of $R$ is an equivalence of the set of matrixes of $R$ and the set of matrixes of the set of single objects of the set of multiplicative opposites of $R$ defined as the inverse of $\operatorname{asEquivalence}$ applied to $\operatorname{equivalenceSingleObjInverse}$ applied to $R$.
CategoryTheory.Mat_structureMathlib.CategoryTheory.Preadditive.Mat, type
Wording
matrix of C (from the name)
English
Let $C$ be a set. Then the matrixes of $C$ are a basic type.
CategoryTheory.Mat_.HomdefMathlib.CategoryTheory.Preadditive.Mat, type
Wording
homomorphism of M and N (from the name)
English
Let $M$ and $N$ be matrixes of $C$. Then a homomorphism of $M$ and $N$ is an element of the function that maps $M$ and $N$ to the set of matrixes of the set of inclusions of $N$ and the function that maps $i$ and $j$ to the set of homomorphisms of $\mathrm{CategoryTheory\_\_Mat\_\_\_X}$ applied to $M$ and $i$ and $\mathrm{CategoryTheory\_\_Mat\_\_\_X}$ applied to $N$ and $j$.
CategoryTheory.Mat_.Hom.compdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a homomorphism of $M$ and $N$. Let $g$ be a homomorphism of $N$ and $K$. Then the composition of $f$ and $g$ is a homomorphism of $M$ and $K$ defined as the function that maps $i$ and $k$ to $\FinsetSum {\FinsetunivMACRoAC}{j}{\operatorname{comp} (f (i , j), g (j , k))}$.
CategoryTheory.Mat_.Hom.iddefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the identity of M (from the name)
English
Let $M$ be a matrix of $C$. Then the identity of $M$ is a homomorphism of $M$ and $M$.
CategoryTheory.Mat_.XdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a matrix of $C$. Let $x$ be an inclusion of $\mathrm{self}$. Then $\mathrm{CategoryTheory\_\_Mat\_\_\_X}$ applied to $\mathrm{self}$ and $x$ is an element of $C$ defined as $\mathrm{CategoryTheory\_\_Mat\_\_\_proj2}$ applied to $\mathrm{self}$ and $x$.
CategoryTheory.Mat_.additiveObjIsoBiproductdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the additive object isomorphism biproduct of F and M (from the name)
English
Let $F$ be a functor of the set of matrixes of $C$ and $D$. Let $M$ be a matrix of $C$. Then the additive object isomorphism biproduct of $F$ and $M$ is an isomorphism of the action of $F$ and $M$ and the biproduct of the function that maps $i$ to the action of $F$ and the action of the embedding of $C$ and $\mathrm{CategoryTheory\_\_Mat\_\_\_X}$ applied to $M$ and $i$ defined as the composition of the map isomorphism of $F$ and the isomorphism biproduct embedding of $M$ and the map biproduct of $F$ and the function that maps $i$ to the action of the embedding of $C$ and $\mathrm{CategoryTheory\_\_Mat\_\_\_X}$ applied to $M$ and $i$.
CategoryTheory.Mat_.embeddingdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the embedding of C (from the name)
English
Let $C$ be a set. Then the embedding of $C$ is a functor of $C$ and the set of matrixes of $C$.
CategoryTheory.Mat_.embeddingLiftIsodefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the embedding lift isomorphism of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the embedding lift isomorphism of $F$ is an isomorphism of the composition of the embedding of $C$ and the lift of $F$ and $F$.
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproductsdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the equivalence self of C (from the name)
English
Let $C$ be a set. Then the equivalence self of $C$ is an equivalence of the set of matrixes of $C$ and $C$ defined as $\operatorname{mk}$ applied to the lift of the identity of $C$, the embedding of $C$, the extension of $\mathrm{CategoryTheory\_\_Mat\_\_\_equivalenceSelfOfHasFiniteBiproductsAux}$ and the embedding lift isomorphism of the identity of $C$.
CategoryTheory.Mat_.extdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the extension of x4 (from the name)
English
Let $x_{4}$ be an isomorphism of the composition of the embedding of $C$ and $F$ and the composition of the embedding of $C$ and $G$. Then the extension of $x_{4}$ is an isomorphism of $F$ and $G$ defined as the composition of $\mathrm{CategoryTheory\_\_Mat\_\_\_liftUnique}$ applied to the composition of the embedding of $C$ and $G$, $F$ and $x_{4}$ and the inverse of $\mathrm{CategoryTheory\_\_Mat\_\_\_liftUnique}$ applied to the composition of the embedding of $C$ and $G$, $G$ and the identity of the composition of the embedding of $C$ and $G$.
CategoryTheory.Mat_.isoBiproductEmbeddingdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the isomorphism biproduct embedding of M (from the name)
English
Let $M$ be a matrix of $C$. Then the isomorphism biproduct embedding of $M$ is an isomorphism of $M$ and the biproduct of the function that maps $i$ to the action of the embedding of $C$ and $\mathrm{CategoryTheory\_\_Mat\_\_\_X}$ applied to $M$ and $i$.
CategoryTheory.Mat_.liftdefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
the lift of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the lift of $F$ is a functor of the set of matrixes of $C$ and $D$.
CategoryTheory.Mat_.liftUniquedefMathlib.CategoryTheory.Preadditive.Mat, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Let $L$ be a functor of the set of matrixes of $C$ and $D$. Let $x_{4}$ be an isomorphism of the composition of the embedding of $C$ and $L$ and $F$. Then $\mathrm{CategoryTheory\_\_Mat\_\_\_liftUnique}$ applied to $F$, $L$ and $x_{4}$ is an isomorphism of $L$ and the lift of $F$.
CategoryTheory.Mat_.ιdefMathlib.CategoryTheory.Preadditive.Mat, type
Wording
inclusion of self (from the name)
English
Let $\mathrm{self}$ be a matrix of $C$. Then an inclusion of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\mathrm{CategoryTheory\_\_Mat\_\_\_proj0}$ applied to $\mathrm{self}$.

Mathlib.CategoryTheory.Preadditive.OfBiproducts

CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdddefMathlib.CategoryTheory.Preadditive.OfBiproducts, function or constant
Wording
the left sum of f and g (from the name)
English
Let $X$ and $Y$ be elements of $C$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the left sum of $f$ and $g$ is a homomorphism of $X$ and $Y$ defined as the composition of the lift of $f$ and $g$ and $\operatorname{desc}$ applied to the identity morphism of $Y$ and the identity morphism of $Y$.
CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdddefMathlib.CategoryTheory.Preadditive.OfBiproducts, function or constant
Wording
the right sum of f and g (from the name)
English
Let $X$ and $Y$ be elements of $C$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the right sum of $f$ and $g$ is a homomorphism of $X$ and $Y$ defined as the composition of the lift of the identity morphism of $X$ and the identity morphism of $X$ and $\operatorname{desc}$ applied to $f$ and $g$.

Mathlib.CategoryTheory.Preadditive.Opposite

CategoryTheory.Preadditive.homSelfLinearEquivEndMulOppositedefMathlib.CategoryTheory.Preadditive.Opposite, function or constant
Wording
the homomorphism self linear equivalence end multiplicative opposite of G (from the name)
English
Let $G$ be an element of $C$. Then the homomorphism self linear equivalence end multiplicative opposite of $G$ is a linear equivalence of the set of homomorphisms of $G$ and $G$ and the set of multiplicative opposites of the set of ends of $G$.
CategoryTheory.opHomdefMathlib.CategoryTheory.Preadditive.Opposite, function or constant
Wording
the opposite homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $C$. Then the opposite homomorphism of $X$ and $Y$ is an additive monoid homomorphism of the set of homomorphisms of $X$ and $Y$ and the set of homomorphisms of $\operatorname{op}$ applied to $Y$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{mk'}$ applied to the function that maps $f$ to the opposite in $f$ and the function that maps $f_{1}$ and $g$ to $\mathrm{CategoryTheory\_\_op\_add}$ applied to $C$, $f_{1}$ and $g$.
CategoryTheory.unopHomdefMathlib.CategoryTheory.Preadditive.Opposite, function or constant
Wording
the opposite homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be opposites of $C$. Then the opposite homomorphism of $X$ and $Y$ is an additive monoid homomorphism of the set of homomorphisms of $X$ and $Y$ and the set of homomorphisms of the opposite of $Y$ and the opposite of $X$ defined as $\operatorname{mk'}$ applied to the function that maps $f$ to the opposite of $f$ and the function that maps $f_{1}$ and $g$ to $\mathrm{CategoryTheory\_\_unop\_add}$ applied to $C$, $f_{1}$ and $g$.

Mathlib.CategoryTheory.Preadditive.Projective.Basic

CategoryTheory.Adjunction.mapProjectivePresentationdefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
the map projective presentation of X and Y (from the name)
English
Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $X$ be an element of $C$. Let $Y$ be a projective presentation of $X$. Then the map projective presentation of $X$ and $Y$ is a projective presentation of the action of $F$ and $X$ defined as $\operatorname{mk}$ applied to the action of $F$ and $\operatorname{p}$ applied to $Y$ and the map of $F$ and $\operatorname{f}$ applied to $Y$.
CategoryTheory.EnoughProjectivesclassMathlib.CategoryTheory.Preadditive.Projective.Basic, predicate
Wording
no wording
English
Let $C$ be a set. Then we can say that $\operatorname{EnoughProjectives}$ holds for $C$.
CategoryTheory.Equivalence.projectivePresentationOfMapProjectivePresentationdefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
the projective presentation of X and Y (from the name)
English
Let $F$ be an equivalence of $C$ and $D$. Let $X$ be an element of $C$. Let $Y$ be a projective presentation of the action of the functor of $F$ and $X$. Then the projective presentation of $X$ and $Y$ is a projective presentation of $X$ defined as $\operatorname{mk}$ applied to the action of the inverse of $F$ and $\operatorname{p}$ applied to $Y$ and the composition of the map of the inverse of $F$ and $\operatorname{f}$ applied to $Y$ and the component of the inverse of the unit of $F$ and $X$.
CategoryTheory.ProjectiveclassMathlib.CategoryTheory.Preadditive.Projective.Basic, predicate
Wording
P is projective (from the name)
English
Let $P$ be an element of $C$. Then we can say that $P$ is projective.
CategoryTheory.Projective.ddefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{d}$ applied to $f$ is a homomorphism of $\operatorname{syzygies}$ applied to $f$ and $X$ defined as the composition of the projection of the kernel of $f$ and the inclusion of $f$.
CategoryTheory.Projective.factorThrudefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $P$ and $X$. Let $e$ be a homomorphism of $E$ and $X$. Then $\operatorname{factorThru}$ applied to $f$ and $e$ is a homomorphism of $P$ and $E$ defined as $\operatorname{choose}$ applied to $\operatorname{factors}$ applied to $f$ and $e$.
CategoryTheory.Projective.overdefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
no wording
English
Let $X$ be an element of $C$. Then $\operatorname{over}$ applied to $X$ is an element of $C$ defined as $\operatorname{p}$ applied to $\operatorname{some}$ applied to $\operatorname{presentation}$ applied to $X$.
CategoryTheory.Projective.syzygiesdefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{syzygies}$ applied to $f$ is an element of $C$ defined as $\operatorname{over}$ applied to the kernel of $f$.
CategoryTheory.Projective.πdefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
the projection of X (from the name)
English
Let $X$ be an element of $C$. Then the projection of $X$ is a homomorphism of $\operatorname{over}$ applied to $X$ and $X$ defined as $\operatorname{f}$ applied to $\operatorname{some}$ applied to $\operatorname{presentation}$ applied to $X$.
CategoryTheory.ProjectivePresentationstructureMathlib.CategoryTheory.Preadditive.Projective.Basic, type
Wording
projective presentation of X (from the name)
English
Let $X$ be an element of $C$. Then the projective presentations of $X$ are a basic type.
CategoryTheory.ProjectivePresentation.fdefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a projective presentation of $X$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{p}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
CategoryTheory.ProjectivePresentation.pdefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a projective presentation of $X$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.isProjectivedefMathlib.CategoryTheory.Preadditive.Projective.Basic, function or constant
Wording
no wording
English
Let $C$ be a set. Then there is an object property of $C$. Proof. Let $C$ be arbitrary. By CategoryTheory__Projective.

Mathlib.CategoryTheory.Preadditive.Projective.Internal

CategoryTheory.InternallyProjectivedefMathlib.CategoryTheory.Preadditive.Projective.Internal, predicate
Wording
P is internally projective (from the name)
English
generation took over the time limit
CategoryTheory.isInternallyProjectivedefMathlib.CategoryTheory.Preadditive.Projective.Internal, function or constant
Wording
no wording
English
There is an object property of $C$. Proof. Let $P$ be arbitrary. By P. By CategoryTheory__ihom. By CategoryTheory__Functor__PreservesEpimorphisms.

Mathlib.CategoryTheory.Preadditive.Projective.Preserves

CategoryTheory.Functor.PreservesProjectiveObjectsclassMathlib.CategoryTheory.Preadditive.Projective.Preserves, predicate
Wording
F preserves projective objects (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ preserves projective objects.

Mathlib.CategoryTheory.Preadditive.Projective.Resolution

CategoryTheory.Functor.mapProjectiveResolutiondefMathlib.CategoryTheory.Preadditive.Projective.Resolution, function or constant
Wording
the map projective resolution of F and P (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $P$ be a projective resolution of $Z$. Then the map projective resolution of $F$ and $P$ is a projective resolution of the action of $F$ and $Z$.
CategoryTheory.HasProjectiveResolutionclassMathlib.CategoryTheory.Preadditive.Projective.Resolution, predicate
Wording
Z has projective resolutions (from the name)
English
Let $Z$ be an element of $C$. Then we can say that $Z$ has projective resolutions.
CategoryTheory.HasProjectiveResolutionsclassMathlib.CategoryTheory.Preadditive.Projective.Resolution, predicate
Wording
C has projective resolutions (from the name)
English
Let $C$ be a set. Then we can say that $C$ has projective resolutions.
CategoryTheory.ProjectiveResolutionstructureMathlib.CategoryTheory.Preadditive.Projective.Resolution, type
Wording
projective resolution of Z (from the name)
English
Let $Z$ be an element of $C$. Then the projective resolutions of $Z$ are a basic type.
CategoryTheory.ProjectiveResolution.HomstructureMathlib.CategoryTheory.Preadditive.Projective.Resolution, type
Wording
homomorphism of f and #3 (from the name)
English
Let $P$ be a projective resolution of $Z$. Let $\mathrm{P'}$ be a projective resolution of $\mathrm{Z'}$. Let $f$ be a homomorphism of $Z$ and $\mathrm{Z'}$. Then the homomorphisms of $\mathrm{P'}$ and $f$ are a basic type.
CategoryTheory.ProjectiveResolution.Hom.homdefMathlib.CategoryTheory.Preadditive.Projective.Resolution, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $\mathrm{P'}$ and $f$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the complex of $P$ and the complex of $\mathrm{P'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.ProjectiveResolution.cokernelCoforkdefMathlib.CategoryTheory.Preadditive.Projective.Resolution, function or constant
Wording
the cokernel cofork of P (from the name)
English
Let $P$ be a projective resolution of $Z$. Then the cokernel cofork of $P$ is a cokernel cofork of $\operatorname{d}$ applied to the complex of $P$, $1$ and $0$ defined as the projection of $\operatorname{f}$ applied to the projection of $P$ and $0$ and $\mathrm{CategoryTheory\_\_ProjectiveResolution\_\_complex\_d\_comp\_\_u3c0\_\_f\_zero}$ applied to $P$.
CategoryTheory.ProjectiveResolution.complexdefMathlib.CategoryTheory.Preadditive.Projective.Resolution, function or constant
Wording
the complex of self (from the name)
English
Let $\mathrm{self}$ be a projective resolution of $Z$. Then the complex of $\mathrm{self}$ is a chain complex of $C$ and $\Natural$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.ProjectiveResolution.isColimitCokernelCoforkdefMathlib.CategoryTheory.Preadditive.Projective.Resolution, function or constant
Wording
no wording
English
Let $P$ be a projective resolution of $Z$. Then $\operatorname{isColimitCokernelCofork}$ applied to $P$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork of $P$.
CategoryTheory.ProjectiveResolution.selfdefMathlib.CategoryTheory.Preadditive.Projective.Resolution, function or constant
Wording
the self of Z (from the name)
English
Let $Z$ be an element of $C$. Then the self of $Z$ is a projective resolution of $Z$.
CategoryTheory.ProjectiveResolution.πdefMathlib.CategoryTheory.Preadditive.Projective.Resolution, function or constant
Wording
the projection of self (from the name)
English
Let $\mathrm{self}$ be a projective resolution of $Z$. Then the projection of $\mathrm{self}$ is a homomorphism of the complex of $\mathrm{self}$ and the action of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $C$ and $Z$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Mathlib.CategoryTheory.Preadditive.Yoneda.Basic

AddCommGrpCat.preadditiveCoyonedaIsodefMathlib.CategoryTheory.Preadditive.Yoneda.Basic, function or constant
Wording
the preadditive Coyoneda isomorphism (from the name)
English
The preadditive Coyoneda isomorphism is an isomorphism of the preadditive Coyoneda and the Coyoneda.
CategoryTheory.preadditiveCoyonedadefMathlib.CategoryTheory.Preadditive.Yoneda.Basic, function or constant
Wording
the preadditive Coyoneda (from the name)
English
The preadditive Coyoneda is a functor of the set of opposites of $C$ and the set of functors of $C$ and the set of additive commutative group categories.
CategoryTheory.preadditiveCoyonedaObjdefMathlib.CategoryTheory.Preadditive.Yoneda.Basic, function or constant
Wording
the preadditive Coyoneda object of X (from the name)
English
Let $X$ be an element of $C$. Then the preadditive Coyoneda object of $X$ is a functor of $C$ and the set of module categories of the set of multiplicative opposites of the set of ends of $X$.
CategoryTheory.preadditiveYonedadefMathlib.CategoryTheory.Preadditive.Yoneda.Basic, function or constant
Wording
the preadditive Yoneda (from the name)
English
The preadditive Yoneda is a functor of $C$ and the set of functors of the set of opposites of $C$ and the set of additive commutative group categories.
CategoryTheory.preadditiveYonedaMapdefMathlib.CategoryTheory.Preadditive.Yoneda.Basic, function or constant
Wording
the preadditive Yoneda map of F and X (from the name)
English
Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the preadditive Yoneda map of $F$ and $X$ is a homomorphism of the action of the preadditive Yoneda and $X$ and the composition of the opposite of $F$ and the action of the preadditive Yoneda and the action of $F$ and $X$.
CategoryTheory.preadditiveYonedaObjdefMathlib.CategoryTheory.Preadditive.Yoneda.Basic, function or constant
Wording
the preadditive Yoneda object of Y (from the name)
English
Let $Y$ be an element of $C$. Then the preadditive Yoneda object of $Y$ is a functor of the set of opposites of $C$ and the set of module categories of the set of ends of $Y$.

Mathlib.CategoryTheory.Presentable.Basic

CategoryTheory.Functor.IsAccessibleclassMathlib.CategoryTheory.Presentable.Basic, predicate
Wording
F is accessible (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ is accessible.
CategoryTheory.Functor.IsCardinalAccessibleclassMathlib.CategoryTheory.Presentable.Basic, predicate
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Let $x_{2}$ be a cardinal. Then we can say that $\operatorname{IsCardinalAccessible}$ holds for $F$ and $x_{2}$.
CategoryTheory.HasCardinalFilteredColimitsclassMathlib.CategoryTheory.Presentable.Basic, predicate
Wording
x1 has cardinal filtered colimits (from the name)
English
Let $C$ be a set. Let $x_{1}$ be a cardinal. Then we can say that $x_{1}$ has cardinal filtered colimits.
CategoryTheory.IsCardinalPresentabledefMathlib.CategoryTheory.Presentable.Basic, predicate
Wording
X is a cardinal presentable with respect to x1 (from the name)
English
Let $X$ be an element of $C$. Let $x_{1}$ be a cardinal. Then $X$ is a cardinal presentable with respect to $x_{1}$, if $\operatorname{IsCardinalAccessible}$ holds for the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and $x_{1}$.
CategoryTheory.IsPresentabledefMathlib.CategoryTheory.Presentable.Basic, predicate
Wording
X is presentable (from the name)
English
Let $X$ be an element of $C$. Then $X$ is presentable, if the action of the Coyoneda and $\operatorname{op}$ applied to $X$ is accessible.
CategoryTheory.isCardinalPresentabledefMathlib.CategoryTheory.Presentable.Basic, function or constant
Wording
no wording
English
Let $C$ be a set. Let $x_{1}$ be a cardinal. Then there is an object property of $C$. Proof. Let $C$ be arbitrary. Let $x_{1}$ be arbitrary. Let $X$ be arbitrary. By X. By x1. By CategoryTheory__IsCardinalPresentable.

Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

CategoryTheory.CardinalDirectedPosetdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, type
Wording
cardinal directed poset of x (from the name)
English
Let $x$ be a cardinal. Then a cardinal directed poset of $x$ is an element of the function that maps $x$ to the set of full subcategories of $\operatorname{isCardinalFiltered}$ applied to $x$.
CategoryTheory.CardinalDirectedPoset.PropSetdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, predicate
Wording
no wording
English
Let $J$ be a cardinal directed poset of $x$. Let $S$ be an element of the power set of the set of carriers of the object of $J$. Then $\operatorname{PropSet}$ holds for $J$ and $S$, if $\mathrm{HasCardinalLT}$ holds for the set of elements of $S$ and $x$ and the set of elements of $S$ has terminals.
CategoryTheory.CardinalDirectedPoset.PropSetWithTopdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, predicate
Wording
no wording
English
Let $J$ be a cardinal directed poset of $x$. Let $x_{1}$ be a cardinal. Let $S$ be an element of the power set of the set of carriers of the object of $\operatorname{withTop}$ applied to $J$. Then $\operatorname{PropSetWithTop}$ holds for $J$, $x_{1}$ and $S$, if $\mathrm{HasCardinalLT}$ holds for the set of elements of $S$ and $x_{1}$ and the top is an element of $S$.
CategoryTheory.CardinalDirectedPoset.SetCardinalLTdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, type
Wording
no wording
English
Let $x$ be a cardinal. Let $X$ be a set. Then an element of $\operatorname{SetCardinalLT}$ applied to $x$ and $X$ is an element of the function that maps $x$ and $X$ to $\SubtypeSet {S}{\mathrm{HasCardinalLT} (\operatorname{Elem} (S), x)}$.
CategoryTheory.CardinalDirectedPoset.SetCardinalLT.singletondefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
the singleton of x and x1 (from the name)
English
Let $x$ be a cardinal. Let $x_{1}$ be an element of $X$. Then the singleton of $x$ and $x_{1}$ is an element of $\operatorname{SetCardinalLT}$ applied to $x$ and $X$ defined as $\operatorname{singleton}$ applied to $x_{1}$.
CategoryTheory.CardinalDirectedPoset.coconedefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
the cocone of J (from the name)
English
Let $J$ be a cardinal directed poset of $x$. Then the cocone of $J$ is a cocone of the functor of $\operatorname{PropSet}$ applied to $J$ defined as the cocone of $\operatorname{PropSet}$ applied to $J$.
CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSetdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
the cocone of P (from the name)
English
Let $P$ be a function from elements of the power set of the set of carriers of the object of $J$ to propositions. Then the cocone of $P$ is a cocone of the functor of $P$.
CategoryTheory.CardinalDirectedPoset.coconeWithTopdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
the cocone with top of J and x1 (from the name)
English
Let $J$ be a cardinal directed poset of $x$. Let $x_{1}$ be a cardinal. Then the cocone with top of $J$ and $x_{1}$ is a cocone of the functor of $\operatorname{PropSetWithTop}$ applied to $J$ and $x_{1}$ defined as the cocone of $\operatorname{PropSetWithTop}$ applied to $J$ and $x_{1}$.
CategoryTheory.CardinalDirectedPoset.functorOfPredicateSetdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
the functor of P (from the name)
English
Let $P$ be a function from elements of the power set of the set of carriers of the object of $J$ to propositions. Then the functor of $P$ is a functor of $\SubtypeSet {x_{1}}{P (x_{1})}$ and the set of cardinal directed posets of $x$.
CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminaldefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
no wording
English
Let $x$ be a cardinal. Then there is an object property of the set of cardinal directed posets of $x$. Proof. Let $x$ be arbitrary. Let $J$ be arbitrary. By J. By CategoryTheory__ObjectProperty__FullSubcategory__obj. By PartOrdEmb__carrier. By x. By HasCardinalLT. By J. By CategoryTheory__ObjectProperty__FullSubcategory__obj. By PartOrdEmb__carrier. By CategoryTheory__Limits__HasTerminal. By and.
CategoryTheory.CardinalDirectedPoset.isColimitCoconedefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
no wording
English
Let $J$ be a cardinal directed poset of $x$. Then $\operatorname{isColimitCocone}$ applied to $J$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $J$.
CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSetdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
no wording
English
Let $P$ be a function from elements of the power set of the set of carriers of the object of $J$ to propositions such that for all carriers $a$ of the object of $J$, there exists an element $S$ of the power set of the set of carriers of the object of $J$, such that $P$ holds for $S$ and $a$ is an element of $S$. Then $\operatorname{isColimitCoconeOfPredicateSet}$ applied to $P$ and $\mathrm{hP}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $P$ defined as $\operatorname{isColimitOfReflects}$ applied to the inclusion and $\operatorname{isColimitOfPredicateSet}$ applied to $P$ and $\mathrm{hP}$.
CategoryTheory.CardinalDirectedPoset.isColimitCoconeWithTopdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
no wording
English
Let $J$ be a cardinal directed poset of $x$. Let $x_{1}$ be a cardinal. Then $\operatorname{isColimitCoconeWithTop}$ applied to $J$ and $x_{1}$ is an element of $\operatorname{IsColimit}$ applied to the cocone with top of $J$ and $x_{1}$.
CategoryTheory.CardinalDirectedPoset.ofdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
no wording
English
Let $J$ be a part order embedding. Then $\operatorname{of}$ applied to $J$ is a cardinal directed poset of $x$.
CategoryTheory.CardinalDirectedPoset.setCardinalLTdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
no wording
English
Let $x$ be a cardinal. Let $X$ be a set. Then $\operatorname{setCardinalLT}$ applied to $x$ and $X$ is a cardinal directed poset of $x$ defined as $\operatorname{of}$ applied to $\operatorname{of}$ applied to $\operatorname{SetCardinalLT}$ applied to $x$ and $X$.
CategoryTheory.CardinalDirectedPoset.withTopdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
no wording
English
Let $J$ be a cardinal directed poset of $x$. Then $\operatorname{withTop}$ applied to $J$ is a cardinal directed poset of $x$ defined as $\operatorname{of}$ applied to $\operatorname{of}$ applied to $\mathrm{WithTop}$ applied to the set of carriers of the object of $J$.
CategoryTheory.CardinalDirectedPoset.ιdefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
the inclusion (from the name)
English
The inclusion is a functor of the set of cardinal directed posets of $x$ and the set of part order embeddings defined as the inclusion of $\operatorname{isCardinalFiltered}$ applied to $x$.
PartOrdEmb.isCardinalFiltereddefMathlib.CategoryTheory.Presentable.CardinalDirectedPoset, function or constant
Wording
no wording
English
Let $x$ be a cardinal. Then there is an object property of the set of part order embeddings. Proof. Let $x$ be arbitrary. Let $X$ be arbitrary. By X. By PartOrdEmb__carrier. By x. By CategoryTheory__IsCardinalFiltered.

Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

CategoryTheory.HasCardinalFilteredGeneratorclassMathlib.CategoryTheory.Presentable.CardinalFilteredPresentation, predicate
Wording
x has cardinal filtered generators (from the name)
English
Let $C$ be a set. Let $x$ be a cardinal. Then we can say that $x$ has cardinal filtered generators.
CategoryTheory.ObjectProperty.IsCardinalFilteredGeneratorstructureMathlib.CategoryTheory.Presentable.CardinalFilteredPresentation, predicate
Wording
no wording
English
Let $P$ be an object property of $C$. Let $x_{1}$ be a cardinal. Then we can say that $\operatorname{IsCardinalFilteredGenerator}$ holds for $P$ and $x_{1}$.

Mathlib.CategoryTheory.Presentable.CardinalPure

CategoryTheory.IsCardinalPureclassMathlib.CategoryTheory.Presentable.CardinalPure, predicate
Wording
no wording
English
Let $x_{1}$ be a cardinal. Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $\operatorname{IsCardinalPure}$ holds for $x_{1}$ and $f$.
CategoryTheory.isCardinalPuredefMathlib.CategoryTheory.Presentable.CardinalPure, function or constant
Wording
no wording
English
Let $C$ be a set. Let $x_{1}$ be a cardinal. Then there is a morphism property of $C$. Proof. Let $C$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $f$ be arbitrary. By x1. By f. By CategoryTheory__IsCardinalPure.

Mathlib.CategoryTheory.Presentable.ColimitPresentation

CategoryTheory.Limits.ColimitPresentation.TotaldefMathlib.CategoryTheory.Presentable.ColimitPresentation, type
Wording
no wording
English
Let $P$ be a function from elements $j$ of $J$ to colimit presentations of $I$ applied to $j$ and the action of $D$ and $j$. Then an element of $\operatorname{Total}$ applied to $j$ and $P$ is an element of the function that maps $P$ and $P$ to $\Sigma$ applied to the function that maps $j$ to $I$ applied to $j$ and $P$.
CategoryTheory.Limits.ColimitPresentation.Total.HomstructureMathlib.CategoryTheory.Presentable.ColimitPresentation, type
Wording
homomorphism of k and l (from the name)
English
Let $k$ and $l$ be elements of $\operatorname{Total}$ applied to $P$. Then the homomorphisms of $k$ and $l$ are a basic type.
CategoryTheory.Limits.ColimitPresentation.Total.Hom.basedefMathlib.CategoryTheory.Presentable.ColimitPresentation, function or constant
Wording
the base of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $k$ and $l$. Then the base of $\mathrm{self}$ is a homomorphism of $\operatorname{fst}$ applied to $k$ and $\operatorname{fst}$ applied to $l$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
CategoryTheory.Limits.ColimitPresentation.Total.Hom.compdefMathlib.CategoryTheory.Presentable.ColimitPresentation, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a homomorphism of $k$ and $l$. Let $g$ be a homomorphism of $l$ and $m$. Then the composition of $f$ and $g$ is a homomorphism of $k$ and $m$.
CategoryTheory.Limits.ColimitPresentation.Total.Hom.homdefMathlib.CategoryTheory.Presentable.ColimitPresentation, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $k$ and $l$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the action of the diagram of $P$ applied to $\operatorname{fst}$ applied to $k$ and $\operatorname{snd}$ applied to $k$ and the action of the diagram of $P$ applied to $\operatorname{fst}$ applied to $l$ and $\operatorname{snd}$ applied to $l$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
CategoryTheory.Limits.ColimitPresentation.Total.mkdefMathlib.CategoryTheory.Presentable.ColimitPresentation, function or constant
Wording
no wording
English
Let $P$ be a function from elements $j$ of $J$ to colimit presentations of $I$ applied to $j$ and the action of $D$ and $j$. Let $i$ be an element of $J$. Let $k$ be an element of $I$ applied to $i$. Then $\operatorname{mk}$ applied to $j$, $P$, $i$ and $k$ is an element of $\operatorname{Total}$ applied to $P$ defined as the function that maps $k$ to $\operatorname{mk}$ applied to $P$, $i$ and $k$.
CategoryTheory.Limits.ColimitPresentation.binddefMathlib.CategoryTheory.Presentable.ColimitPresentation, function or constant
Wording
no wording
English
Let $P$ be a colimit presentation of $J$ and $X$. Let $Q$ be a function from elements $j$ of $J$ to colimit presentations of $I$ applied to $j$ and the action of the diagram of $P$ and $j$. Then $\operatorname{bind}$ applied to $P$, $j$ and $Q$ is a colimit presentation of $\operatorname{Total}$ applied to $Q$ and $X$.

Mathlib.CategoryTheory.Presentable.Comma

CategoryTheory.Comma.isCardinalPresentabledefMathlib.CategoryTheory.Presentable.Comma, function or constant
Wording
no wording
English
Let $x_{5}$ be a functor of $x$ and $D$. Let $x_{6}$ be a functor of $x_{1}$ and $D$. Let $x_{7}$ be a cardinal. Then there is an object property of the set of commas of $x_{5}$ and $x_{6}$. Proof. Let $x_{5}$ be arbitrary. Let $x_{6}$ be arbitrary. Let $x_{7}$ be arbitrary. By x. By x7. By CategoryTheory__isCardinalPresentable. By x1. By x7. By CategoryTheory__isCardinalPresentable. By CategoryTheory__ObjectProperty__comma.

Mathlib.CategoryTheory.Presentable.Directed

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramstructureMathlib.CategoryTheory.Presentable.Directed, type
Wording
diagram of J and x1 (from the name)
English
Let $J$ be a set. Let $x_{1}$ be a cardinal. Then the diagrams of $J$ and $x_{1}$ are a basic type.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminalstructureMathlib.CategoryTheory.Presentable.Directed, type
Wording
no wording
English
Let $D$ be a diagram of $J$ and $x_{1}$. Let $e$ be an element of $J$. Then the elements of $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_IsTerminal}$ applied to $D$ and $e$ are a basic type.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.liftdefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
the lift of self and hj (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_IsTerminal}$ applied to $D$ and $e$. Assume that $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_P}$ holds for $D$ and $j$. Then the lift of $\mathrm{self}$ and $\mathrm{hj}$ is a homomorphism of $j$ and $e$ defined as $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_IsTerminal\_\_proj1}$ applied to $\mathrm{self}$ and $\mathrm{hj}$.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.ofExistsUniquedefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
no wording
English
Assume that $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_W}$ holds for $D$, $e$, $e$ and the identity morphism of $e$. Assume that for all elements $j_{2}$ of $J$, if $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_P}$ holds for $D$ and $j_{2}$, then there exists a homomorphism $\mathrm{lift}$ of $j_{2}$ and $e$, such that $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_W}$ holds for $D$, $j_{2}$, $e$ and $\mathrm{lift}$. Assume that for all elements $j_{1}$ of $J$, if $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_P}$ holds for $D$ and $j_{1}$, then for all homomorphisms $x_{2}$ and $x_{3}$ of $j_{1}$ and $e$, if $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_W}$ holds for $D$, $j_{1}$, $e$ and $x_{2}$, then if $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_W}$ holds for $D$, $j_{1}$, $e$ and $x_{3}$, then $\EqtMACRoH {x_{2}}{x_{3}}$. Assume that for all elements $i$ and $j$ of $J$, for all homomorphisms $f$ of $i$ and $j$, if $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_W}$ holds for $D$, $i$, $j$ and $f$, then there exists a homomorphism $\mathrm{li}$ of $i$ and $e$, such that there exists a homomorphism $\mathrm{lj}$ of $j$ and $e$, such that $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_W}$ holds for $D$, $i$, $e$ and $\mathrm{li}$, $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_W}$ holds for $D$, $j$, $e$ and $\mathrm{lj}$ and the composition of $f$ and $\mathrm{lj}$ is equal to $\mathrm{li}$. Then $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_IsTerminal\_\_ofExistsUnique}$ applied to $\mathrm{prop\_id}$, $h$, $h_{1}$ and $h_{2}$ is an element of $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_IsTerminal}$ applied to $D$ and $e$.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.PdefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a diagram of $J$ and $x_{1}$. Then there is an object property of $J$. Proof. Let $\mathrm{self}$ be arbitrary. By self. By CategoryTheory__IsCardinalFiltered__exists_cardinal_directed__Diagram__proj1.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.WdefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a diagram of $J$ and $x_{1}$. Then there is a morphism property of $J$. Proof. Let $\mathrm{self}$ be arbitrary. By self. By CategoryTheory__IsCardinalFiltered__exists_cardinal_directed__Diagram__proj0.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSupdefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
the supremum of D and h1 (from the name)
English
Let $D$ be a function from elements of $x_{2}$ to diagrams of $J$ and $x_{1}$. Assume that $\mathrm{HasCardinalLT}$ holds for $x_{2}$ and $x_{1}$. Then the supremum of $D$ and $h_{1}$ is a diagram of $J$ and $x_{1}$.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.singledefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
no wording
English
Let $j$ be an element of $J$. Then $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_single}$ applied to $j$ is a diagram of $J$ and $x_{1}$.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.supdefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
the supremum of x2 and x3 (from the name)
English
Let $x_{2}$ and $x_{3}$ be diagrams of $J$ and $x_{1}$. Then the supremum of $x_{2}$ and $x_{3}$ is a diagram of $J$ and $x_{1}$.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminalstructureMathlib.CategoryTheory.Presentable.Directed, type
Wording
diagram with unique terminal of J and x1 (from the name)
English
Let $J$ be a set. Let $x_{1}$ be a cardinal. Then the diagrams with unique terminal of $J$ and $x_{1}$ are a basic type.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.isTerminaldefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a diagram with unique terminal of $J$ and $x_{1}$. Then $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_DiagramWithUniqueTerminal\_\_isTerminal}$ applied to $\mathrm{self}$ is an element of $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_Diagram\_\_IsTerminal}$ applied to $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_DiagramWithUniqueTerminal\_\_toDiagram}$ applied to $\mathrm{self}$ and the top of $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_DiagramWithUniqueTerminal\_\_proj2}$ applied to $\mathrm{self}$.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.singledefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
no wording
English
Let $j$ be an element of $J$. Then $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_DiagramWithUniqueTerminal\_\_single}$ applied to $j$ is a diagram with unique terminal of $J$ and $x_{1}$.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.topdefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
the top of self (from the name)
English
Let $\mathrm{self}$ be a diagram with unique terminal of $J$ and $x_{1}$. Then the top of $\mathrm{self}$ is an element of $J$ defined as $\mathrm{CategoryTheory\_\_IsCardinalFiltered\_\_exists\_cardinal\_directed\_\_DiagramWithUniqueTerminal\_\_proj1}$ applied to $\mathrm{self}$.
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functordefMathlib.CategoryTheory.Presentable.Directed, function or constant
Wording
the functor of J and x1 (from the name)
English
Let $J$ be a set. Let $x_{1}$ be a cardinal. Then the functor of $J$ and $x_{1}$ is a functor of the set of diagrams with unique terminal of $J$ and $x_{1}$ and $J$.

Mathlib.CategoryTheory.Presentable.Finite

CategoryTheory.Functor.IsFinitelyAccessibledefMathlib.CategoryTheory.Presentable.Finite, predicate
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Then $\operatorname{IsFinitelyAccessible}$ holds for $F$, if $\operatorname{IsCardinalAccessible}$ holds for $F$ and $\operatorname{aleph0}$.
CategoryTheory.IsFinitelyPresentabledefMathlib.CategoryTheory.Presentable.Finite, predicate
Wording
no wording
English
Let $X$ be an element of $C$. Then $\operatorname{IsFinitelyPresentable}$ holds for $X$, if $X$ is a cardinal presentable with respect to $\operatorname{aleph0}$.
CategoryTheory.MorphismProperty.isFinitelyPresentabledefMathlib.CategoryTheory.Presentable.Finite, function or constant
Wording
no wording
English
Let $C$ be a set. Then there is a morphism property of $C$. Proof. Let $C$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $f$ be arbitrary. By x1. By CategoryTheory__Under. By f. By CategoryTheory__Under__mk. By CategoryTheory__ObjectProperty__isFinitelyPresentable.
CategoryTheory.ObjectProperty.isFinitelyPresentabledefMathlib.CategoryTheory.Presentable.Finite, function or constant
Wording
no wording
English
Let $C$ be a set. Then there is an object property of $C$. Proof. Let $C$ be arbitrary. Let $X$ be arbitrary. By X. By CategoryTheory__IsFinitelyPresentable.

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

CategoryTheory.IsCardinalFilteredclassMathlib.CategoryTheory.Presentable.IsCardinalFiltered, predicate
Wording
no wording
English
Let $J$ be a set. Let $x_{1}$ be a cardinal. Then we can say that $\operatorname{IsCardinalFiltered}$ holds for $J$ and $x_{1}$.
CategoryTheory.IsCardinalFiltered.coconedefMathlib.CategoryTheory.Presentable.IsCardinalFiltered, function or constant
Wording
the cocone of F and hA (from the name)
English
Let $F$ be a functor of $A$ and $J$. Assume that $\mathrm{HasCardinalLT}$ holds for the set of arrows of $A$ and $x_{1}$. Then the cocone of $F$ and $\mathrm{hA}$ is a cocone of $F$.
CategoryTheory.IsCardinalFiltered.coeqdefMathlib.CategoryTheory.Presentable.IsCardinalFiltered, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $K$ to homomorphisms of $j$ and $\mathrm{j'}$. Assume that $\mathrm{HasCardinalLT}$ holds for $K$ and $x_{1}$. Then $\operatorname{coeq}$ applied to $f$ and $\mathrm{hK}$ is an element of $J$.
CategoryTheory.IsCardinalFiltered.coeqHomdefMathlib.CategoryTheory.Presentable.IsCardinalFiltered, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $K$ to homomorphisms of $j$ and $\mathrm{j'}$. Assume that $\mathrm{HasCardinalLT}$ holds for $K$ and $x_{1}$. Then $\operatorname{coeqHom}$ applied to $f$ and $\mathrm{hK}$ is a homomorphism of $\mathrm{j'}$ and $\operatorname{coeq}$ applied to $f$ and $\mathrm{hK}$.
CategoryTheory.IsCardinalFiltered.maxdefMathlib.CategoryTheory.Presentable.IsCardinalFiltered, function or constant
Wording
the maximum of S and hS (from the name)
English
Let $S$ be a function from elements of $K$ to elements of $J$. Assume that $\mathrm{HasCardinalLT}$ holds for $K$ and $x_{1}$. Then the maximum of $S$ and $\mathrm{hS}$ is an element of $J$.
CategoryTheory.IsCardinalFiltered.toCoeqdefMathlib.CategoryTheory.Presentable.IsCardinalFiltered, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $K$ to homomorphisms of $j$ and $\mathrm{j'}$. Assume that $\mathrm{HasCardinalLT}$ holds for $K$ and $x_{1}$. Then $\operatorname{toCoeq}$ applied to $f$ and $\mathrm{hK}$ is a homomorphism of $j$ and $\operatorname{coeq}$ applied to $f$ and $\mathrm{hK}$.
CategoryTheory.IsCardinalFiltered.toMaxdefMathlib.CategoryTheory.Presentable.IsCardinalFiltered, function or constant
Wording
the maximum of S and k (from the name)
English
Let $S$ be a function from elements of $K$ to elements of $J$. Assume that $\mathrm{HasCardinalLT}$ holds for $K$ and $x_{1}$. Let $k$ be an element of $K$. Then the maximum of $S$ and $k$ is a homomorphism of $S$ applied to $k$ and the maximum of $S$ and $\mathrm{hS}$.

Mathlib.CategoryTheory.Presentable.LocallyPresentable

CategoryTheory.IsAccessibleCategoryclassMathlib.CategoryTheory.Presentable.LocallyPresentable, predicate
Wording
C is a accessible category (from the name)
English
Let $C$ be a set. Then we can say that $C$ is an accessible category.
CategoryTheory.IsCardinalAccessibleCategoryclassMathlib.CategoryTheory.Presentable.LocallyPresentable, predicate
Wording
x1 is a cardinal accessible category (from the name)
English
Let $C$ be a set. Let $x_{1}$ be a cardinal. Then we can say that $x_{1}$ is a cardinal accessible category.
CategoryTheory.IsCardinalLocallyPresentableclassMathlib.CategoryTheory.Presentable.LocallyPresentable, predicate
Wording
no wording
English
Let $C$ be a set. Let $x_{1}$ be a cardinal. Then we can say that $\operatorname{IsCardinalLocallyPresentable}$ holds for $C$ and $x_{1}$.
CategoryTheory.IsFinitelyAccessibleCategorydefMathlib.CategoryTheory.Presentable.LocallyPresentable, predicate
Wording
no wording
English
Let $C$ be a set. Then $\operatorname{IsFinitelyAccessibleCategory}$ holds for $C$, if $\operatorname{aleph0}$ is a cardinal accessible category.
CategoryTheory.IsLocallyFinitelyPresentabledefMathlib.CategoryTheory.Presentable.LocallyPresentable, predicate
Wording
no wording
English
Let $C$ be a set. Then $\operatorname{IsLocallyFinitelyPresentable}$ holds for $C$, if $\operatorname{IsCardinalLocallyPresentable}$ holds for $C$ and $\operatorname{aleph0}$.
CategoryTheory.IsLocallyPresentableclassMathlib.CategoryTheory.Presentable.LocallyPresentable, predicate
Wording
C is locally presentable (from the name)
English
generation took over the time limit

Mathlib.CategoryTheory.Presentable.OrthogonalReflection

CategoryTheory.OrthogonalReflection.D₁defMathlib.CategoryTheory.Presentable.OrthogonalReflection, type
Wording
no wording
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then an element of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_}$ applied to $W$ and $Z$ is an element of the function that maps $W$ and $Z$ to $\Sigma$ applied to the function that maps $f$ to the set of homomorphisms of the left object of $f$ and $Z$.
CategoryTheory.OrthogonalReflection.D₁.ldefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
no wording
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_l}$ applied to $W$ and $Z$ is a homomorphism of the sigma object of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_obj\_u2081\_}$ and $Z$ defined as $\operatorname{desc}$ applied to the function that maps $d$ to $\operatorname{snd}$ applied to $d$.
CategoryTheory.OrthogonalReflection.D₁.obj₁defMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the object of d (from the name)
English
Let $d$ be an element of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_}$ applied to $W$ and $Z$. Then the object of $d$ is an element of $C$ defined as the left object of $\operatorname{fst}$ applied to $d$.
CategoryTheory.OrthogonalReflection.D₁.obj₂defMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the object of d (from the name)
English
Let $d$ be an element of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_}$ applied to $W$ and $Z$. Then the object of $d$ is an element of $C$ defined as the right object of $\operatorname{fst}$ applied to $d$.
CategoryTheory.OrthogonalReflection.D₁.tdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
no wording
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_t}$ applied to $W$ and $Z$ is a homomorphism of the sigma object of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_obj\_u2081\_}$ and the sigma object of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_obj\_u2082\_}$ defined as the map of the function that maps $d$ to the homomorphism of $\operatorname{fst}$ applied to $d$.
CategoryTheory.OrthogonalReflection.D₁.ιLeftdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the inclusion in f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $f$. Let $g$ be a homomorphism of $X$ and $Z$. Then the inclusion in $f$ is a homomorphism of $X$ and the sigma object of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_obj\_u2081\_}$ defined as the inclusion of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_obj\_u2081\_}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $g$.
CategoryTheory.OrthogonalReflection.D₁.ιRightdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the inclusion in f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $f$. Let $g$ be a homomorphism of $X$ and $Z$. Then the inclusion in $f$ is a homomorphism of $Y$ and the sigma object of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_obj\_u2082\_}$ defined as the inclusion of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_obj\_u2082\_}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $g$.
CategoryTheory.OrthogonalReflection.D₂defMathlib.CategoryTheory.Presentable.OrthogonalReflection, type
Wording
no wording
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then an element of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2082\_}$ applied to $W$ and $Z$ is an element of the function that maps $W$ and $Z$ to $\Sigma$ applied to the function that maps $f$ to $\SubtypeSet {\mathrm{pq}}{(\EqtMACRoH {\operatorname{comp} (\operatorname{hom} (f), \ProdfstMACRoZ {\mathrm{pq}})}{\operatorname{comp} (\operatorname{hom} (f), \ProdsndMACRoAA {\mathrm{pq}})})}$.
CategoryTheory.OrthogonalReflection.D₂.multispanIndexdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the multispan index of W and Z (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then the multispan index of $W$ and $Z$ is a multispan index of the shape of the multicoequalizer of all pairs of morphisms of $W$ and $Z$ and $C$ defined as $\operatorname{mk}$ applied to the function that maps $d$ to the right object of $\operatorname{fst}$ applied to $d$, the function that maps $x_{1}$ to the step of $W$ and $Z$, the function that maps $d_{1}$ to $\ProdfstMACRoZ {\operatorname{snd} (d_{1})}$ and the function that maps $d_{2}$ to $\ProdsndMACRoAA {\operatorname{snd} (d_{2})}$.
CategoryTheory.OrthogonalReflection.D₂.multispanShapedefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the shape of the multicoequalizer of all pairs of morphisms of W and Z (from the docstring)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then the shape of the multicoequalizer of all pairs of morphisms of $W$ and $Z$ is a shape defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2082\_}$ applied to $W$ and $Z$, $\mathrm{Unit}$, the function that maps $x_{1}$ to $\operatorname{unit}$ and the function that maps $x_{2}$ to $\operatorname{unit}$.
CategoryTheory.OrthogonalReflection.corepresentableBydefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
no wording
English
Let $Z$ be an element of $C$. Assume that for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, if $W$ holds for $X$, $Y$ and $f$, then $X$ is a cardinal presentable with respect to $x_{1}$ and $Y$ is a cardinal presentable with respect to $x_{1}$. Then $\operatorname{corepresentableBy}$ applied to $Z$ and $\mathrm{hW}$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the inclusion of $\operatorname{isLocal}$ applied to $W$ and the action of the Coyoneda and $\operatorname{op}$ applied to $Z$ and $\operatorname{mk}$ applied to the reflection object of $Z$ and $x_{1}$ and $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_isLocal\_reflectionObj}$ applied to $Z$ and $\mathrm{hW}$.
CategoryTheory.OrthogonalReflection.fromStepdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
no wording
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then $\operatorname{fromStep}$ applied to $W$ and $Z$ is a homomorphism of the step of $W$ and $Z$ and the successor of $W$ and $Z$ defined as the projection of the multispan index of $W$ and $Z$ and $\operatorname{unit}$.
CategoryTheory.OrthogonalReflection.iterationdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the iteration of Z and x1 (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Let $x_{1}$ be a cardinal. Then the iteration of $Z$ and $x_{1}$ is a functor of the set of types of the order of $x_{1}$ and $C$ defined as $\operatorname{F}$ applied to $\operatorname{toTransfiniteCompositionOfShape}$ applied to the transfinite composition of $Z$ and $x_{1}$.
CategoryTheory.OrthogonalReflection.iterationObjSuccIsodefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the iteration object successor isomorphism of x1 and j (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Let $x_{1}$ be a cardinal. Let $j$ be a type of the order of $x_{1}$. Then the iteration object successor isomorphism of $x_{1}$ and $j$ is an isomorphism of the action of the iteration of $Z$ and $x_{1}$ and the successor of $j$ and the successor of $W$ and the action of the iteration of $Z$ and $x_{1}$ and $j$.
CategoryTheory.OrthogonalReflection.reflectiondefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the reflection of Z and x1 (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Let $x_{1}$ be a cardinal. Then the reflection of $Z$ and $x_{1}$ is a homomorphism of $Z$ and the reflection object of $Z$ and $x_{1}$ defined as the inclusion iteration of $\operatorname{succStruct}$ applied to $W$ and $Z$ and the set of types of the order of $x_{1}$.
CategoryTheory.OrthogonalReflection.reflectionObjdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the reflection object of Z and x1 (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Let $x_{1}$ be a cardinal. Then the reflection object of $Z$ and $x_{1}$ is an element of $C$ defined as the iteration of $\operatorname{succStruct}$ applied to $W$ and $Z$ and the set of types of the order of $x_{1}$.
CategoryTheory.OrthogonalReflection.stepdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the step of W and Z (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then the step of $W$ and $Z$ is an element of $C$ defined as the pushout of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_t}$ applied to $W$ and $Z$ and $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_l}$ applied to $W$ and $Z$.
CategoryTheory.OrthogonalReflection.succdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the successor of W and Z (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then the successor of $W$ and $Z$ is an element of $C$ defined as the multicoequalizer of the multispan index of $W$ and $Z$.
CategoryTheory.OrthogonalReflection.succStructdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
no wording
English
Let $W$ be a morphism property of $C$. Let $x_{1}$ be an element of $C$. Then $\operatorname{succStruct}$ applied to $W$ and $x_{1}$ is an element of $\operatorname{SuccStruct}$ applied to $C$ defined as $\operatorname{mk}$ applied to $x_{1}$, the function that maps $Z$ to the successor of $W$ and $Z$ and the function that maps $Z_{1}$ to the successor of $W$ and $Z_{1}$.
CategoryTheory.OrthogonalReflection.toStepdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the step of W and Z (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then the step of $W$ and $Z$ is a homomorphism of $Z$ and the step of $W$ and $Z$ defined as the right injection of $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_t}$ applied to $W$ and $Z$ and $\mathrm{CategoryTheory\_\_OrthogonalReflection\_\_D\_u2081\_\_\_l}$ applied to $W$ and $Z$.
CategoryTheory.OrthogonalReflection.toSuccdefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the successor of W and Z (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Then the successor of $W$ and $Z$ is a homomorphism of $Z$ and the successor of $W$ and $Z$ defined as the composition of the step of $W$ and $Z$ and $\operatorname{fromStep}$ applied to $W$ and $Z$.
CategoryTheory.OrthogonalReflection.transfiniteCompositionOfShapeReflectiondefMathlib.CategoryTheory.Presentable.OrthogonalReflection, function or constant
Wording
the transfinite composition of Z and x1 (from the name)
English
Let $W$ be a morphism property of $C$. Let $Z$ be an element of $C$. Let $x_{1}$ be a cardinal. Then the transfinite composition of $Z$ and $x_{1}$ is a transfinite composition of shape of the set of types of the order of $x_{1}$ and the reflection of $Z$ and $x_{1}$.

Mathlib.CategoryTheory.Presentable.PreservesCardinalPresentable

CategoryTheory.Functor.PreservesCardinalPresentableclassMathlib.CategoryTheory.Presentable.PreservesCardinalPresentable, predicate
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Let $x_{2}$ be a cardinal. Then we can say that $\operatorname{PreservesCardinalPresentable}$ holds for $F$ and $x_{2}$.

Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Cardinal.SharplyLTstructureMathlib.CategoryTheory.Presentable.SharplyLT.Basic, predicate
Wording
no wording
English
Let $x$ and $x_{1}$ be cardinals. Then we can say that $\operatorname{SharplyLT}$ holds for $x$ and $x_{1}$.
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLTdefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, predicate
Wording
no wording
English
Let $x$ and $x_{1}$ be cardinals. Let $J$ be a set. Let $A$ be an element of $\wp J$. Then $\operatorname{IsCardinalFilteredAndHasCardinalLT}$ holds for $x$, $x_{1}$, $J$ and $A$, if $\operatorname{IsCardinalFiltered}$ holds for the set of elements of $A$ and $x$ and $\mathrm{HasCardinalLT}$ holds for the set of elements of $A$ and $x_{1}$.
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.coconedefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, function or constant
Wording
the cocone of x1 and p (from the name)
English
Let $x$ and $x_{1}$ be cardinals. Let $p$ be a colimit of shape of $J$ and $X$. Then the cocone of $x_{1}$ and $p$ is a cocone of the functor of $x_{1}$ and $p$.
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimitdefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, function or constant
Wording
the colimit of p and A (from the name)
English
Let $x$ and $x_{1}$ be cardinals. Let $p$ be a colimit of shape of $J$ and $X$. Let $A$ be an element of $\SubtypeSet {A_{1}}{\operatorname{IsCardinalFilteredAndHasCardinalLT} (x , x_{1} , J , A_{1})}$. Then the colimit of $p$ and $A$ is an element of $C$.
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.mapdefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, function or constant
Wording
the map of x1 and p (from the name)
English
Let $x$ and $x_{1}$ be cardinals. Let $p$ be a colimit of shape of $J$ and $X$. Assume that $x_{4} \leq x_{5}$. Then the map of $x_{1}$ and $p$ is a homomorphism of the colimit of $p$ and $x_{4}$ and the colimit of $p$ and $x_{5}$.
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.ιdefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, function or constant
Wording
the inclusion of A and a (from the name)
English
Let $x$ and $x_{1}$ be cardinals. Let $p$ be a colimit of shape of $J$ and $X$. Let $A$ be an element of $\SubtypeSet {A_{1}}{\operatorname{IsCardinalFilteredAndHasCardinalLT} (x , x_{1} , J , A_{1})}$. Let $a$ be an element of $J$ such that $a$ is an element of $A$. Then the inclusion of $A$ and $a$ is a homomorphism of the action of the diagram of $\operatorname{toColimitPresentation}$ applied to $p$ and $a$ and the colimit of $p$ and $A$.
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.πdefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, function or constant
Wording
the projection of p and A (from the name)
English
Let $x$ and $x_{1}$ be cardinals. Let $p$ be a colimit of shape of $J$ and $X$. Let $A$ be an element of $\SubtypeSet {A_{1}}{\operatorname{IsCardinalFilteredAndHasCardinalLT} (x , x_{1} , J , A_{1})}$. Then the projection of $p$ and $A$ is a homomorphism of the colimit of $p$ and $A$ and $X$.
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.functordefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, function or constant
Wording
the functor of x1 and p (from the name)
English
Let $x$ and $x_{1}$ be cardinals. Let $p$ be a colimit of shape of $J$ and $X$. Then the functor of $x_{1}$ and $p$ is a functor of $\SubtypeSet {A}{\operatorname{IsCardinalFilteredAndHasCardinalLT} (x , x_{1} , J , A)}$ and $C$.
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.isColimitdefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, function or constant
Wording
no wording
English
Let $x$ and $x_{1}$ be cardinals. Let $p$ be a colimit of shape of $J$ and $X$. Then $\operatorname{isColimit}$ applied to $x$, $x_{1}$ and $p$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $x_{1}$ and $p$.
Cardinal.SharplyLT.generatordefMathlib.CategoryTheory.Presentable.SharplyLT.Basic, function or constant
Wording
the generator of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be cardinals. Let $C$ be a set. Then the generator of $x$ and $x_{1}$ is an object property of $C$ defined as the colimit cardinal closure of $\operatorname{isCardinalPresentable}$ applied to $C$ and $x$ and $x_{1}$.

Mathlib.CategoryTheory.Presentable.SharplyLT.Lemmas

CategoryTheory.CardinalDirectedPoset.SetCardinalLT.fromSigmadefMathlib.CategoryTheory.Presentable.SharplyLT.Lemmas, function or constant
Wording
no wording
English
Let $x$ be a cardinal. Let $X$ be a set. Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $x_{2}$ to the set of functions from types of the order of $x_{2}$ to elements of $X$. Then $\operatorname{fromSigma}$ applied to $x$, $X$ and $x_{1}$ is an element of $\operatorname{SetCardinalLT}$ applied to $x$ and $X$ defined as the range of $\operatorname{snd}$ applied to $x_{1}$.

Mathlib.CategoryTheory.Presentable.Type

HasCardinalLT.SetdefMathlib.CategoryTheory.Presentable.Type, type
Wording
set of X and x (from the name)
English
Let $X$ be a set. Let $x$ be a cardinal. Then a set of $X$ and $x$ is an element of the function that maps $X$ and $x$ to $\SubtypeSet {A}{\mathrm{HasCardinalLT} (\operatorname{Elem} (A), x)}$.
HasCardinalLT.Set.coconedefMathlib.CategoryTheory.Presentable.Type, function or constant
Wording
the cocone of X and x (from the name)
English
Let $X$ be a set. Let $x$ be a cardinal. Then the cocone of $X$ and $x$ is a cocone of the functor of $X$ and $x$.
HasCardinalLT.Set.functordefMathlib.CategoryTheory.Presentable.Type, function or constant
Wording
the functor of X and x (from the docstring)
English
Let $X$ be a set. Let $x$ be a cardinal. Then the functor of $X$ and $x$ is a functor of the set of sets of $X$ and $x$ and the set of sets.
HasCardinalLT.Set.isColimitCoconedefMathlib.CategoryTheory.Presentable.Type, function or constant
Wording
no wording
English
Let $X$ be a set. Let $x$ be a cardinal such that $\operatorname{aleph0} \leq x$. Then $\operatorname{isColimitCocone}$ applied to $X$, $x$ and $h$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $X$ and $x$.

Mathlib.CategoryTheory.Products.Associator

CategoryTheory.prod.associativitydefMathlib.CategoryTheory.Products.Associator, function or constant
Wording
the associativity of D and E (from the name)
English
Let $C$, $D$ and $E$ be sets. Then the associativity of $D$ and $E$ is an equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $C$ and $D$ and $E$ and $\mathrm{Prod}$ applied to $C$ and $\mathrm{Prod}$ applied to $D$ and $E$.
CategoryTheory.prod.associatordefMathlib.CategoryTheory.Products.Associator, function or constant
Wording
the associator of D and E (from the name)
English
Let $C$, $D$ and $E$ be sets. Then the associator of $D$ and $E$ is a functor of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $C$ and $D$ and $E$ and $\mathrm{Prod}$ applied to $C$ and $\mathrm{Prod}$ applied to $D$ and $E$.
CategoryTheory.prod.functorProdToProdFunctorAssociatordefMathlib.CategoryTheory.Products.Associator, function or constant
Wording
the functor product to product functor associator of E and A (from the name)
English
Let $C$, $D$, $E$ and $A$ be sets. Then the functor product to product functor associator of $E$ and $A$ is an isomorphism of the composition of the functor of the right congruence of the associativity of $D$ and $E$ and the composition of the functor product to product functor of $C$ and $\mathrm{Prod}$ applied to $D$ and $E$ and the product of the identity of the set of functors of $A$ and $C$ and the functor product to product functor of $D$ and $E$ and the composition of the functor product to product functor of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$ and the composition of the product of the functor product to product functor of $C$ and $D$ and the identity of the set of functors of $A$ and $E$ and the functor of the associativity of the set of functors of $A$ and $D$ and the set of functors of $A$ and $E$ defined as the identity of the composition of the functor of the right congruence of the associativity of $D$ and $E$ and the composition of the functor product to product functor of $C$ and $\mathrm{Prod}$ applied to $D$ and $E$ and the product of the identity of the set of functors of $A$ and $C$ and the functor product to product functor of $D$ and $E$.
CategoryTheory.prod.inverseAssociatordefMathlib.CategoryTheory.Products.Associator, function or constant
Wording
the inverse associator of D and E (from the name)
English
Let $C$, $D$ and $E$ be sets. Then the inverse associator of $D$ and $E$ is a functor of $\mathrm{Prod}$ applied to $C$ and $\mathrm{Prod}$ applied to $D$ and $E$ and $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $C$ and $D$ and $E$.
CategoryTheory.prod.prodFunctorToFunctorProdAssociatordefMathlib.CategoryTheory.Products.Associator, function or constant
Wording
the product functor to functor product associator of E and A (from the name)
English
Let $C$, $D$, $E$ and $A$ be sets. Then the product functor to functor product associator of $E$ and $A$ is an isomorphism of the composition of the functor of the associativity of the set of functors of $A$ and $D$ and the set of functors of $A$ and $E$ and the composition of the product of the identity of the set of functors of $A$ and $C$ and the product functor to functor product of $D$ and $E$ and the product functor to functor product of $C$ and $\mathrm{Prod}$ applied to $D$ and $E$ and the composition of the product of the product functor to functor product of $C$ and $D$ and the identity of the set of functors of $A$ and $E$ and the composition of the product functor to functor product of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$ and the functor of the right congruence of the associativity of $D$ and $E$ defined as the identity of the composition of the functor of the associativity of the set of functors of $A$ and $D$ and the set of functors of $A$ and $E$ and the composition of the product of the identity of the set of functors of $A$ and $C$ and the product functor to functor product of $D$ and $E$ and the product functor to functor product of $C$ and $\mathrm{Prod}$ applied to $D$ and $E$.
CategoryTheory.prod.prodμdefMathlib.CategoryTheory.Products.Associator, function or constant
Wording
the product of E and A (from the name)
English
Let $C$, $D$, $E$ and $A$ be sets. Then the product of $E$ and $A$ is an equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $A$ and $C$ and $\mathrm{Prod}$ applied to $D$ and $E$ and $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $A$ and $D$ and $\mathrm{Prod}$ applied to $C$ and $E$ defined as the composition of the associativity of $C$ and $\mathrm{Prod}$ applied to $D$ and $E$ and the composition of the product of the identity and the inverse of the associativity of $D$ and $E$ and the composition of the product of the identity and the product of the braiding of $C$ and $D$ and the identity and the composition of the product of the identity and the associativity of $C$ and $E$ and the inverse of the associativity of $D$ and $\mathrm{Prod}$ applied to $C$ and $E$.

Mathlib.CategoryTheory.Products.Basic

CategoryTheory.Equivalence.proddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of x4 and x5 (from the name)
English
Let $x_{4}$ be an equivalence of $A$ and $B$. Let $x_{5}$ be an equivalence of $C$ and $D$. Then the product of $x_{4}$ and $x_{5}$ is an equivalence of $\mathrm{Prod}$ applied to $A$ and $C$ and $\mathrm{Prod}$ applied to $B$ and $D$.
CategoryTheory.Functor.constCompEvaluationObjdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the constant composition evaluation object of D and X (from the name)
English
Let $D$ be a set. Let $X$ be an element of $C$. Then the constant composition evaluation object of $D$ and $X$ is an isomorphism of the composition of the constant of $C$ and the action of the evaluation of $C$ and $D$ and $X$ and the identity of $D$.
CategoryTheory.Functor.diagdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the diagonal functor of C (from the docstring)
English
Let $C$ be a set. Then the diagonal functor of $C$ is a functor of $C$ and $\mathrm{Prod}$ applied to $C$ and $C$ defined as the product of the identity of $C$ and the identity of $C$.
CategoryTheory.Functor.proddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of F and G (from the name)
English
Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $D$. Then the product of $F$ and $G$ is a functor of $\mathrm{Prod}$ applied to $A$ and $C$ and $\mathrm{Prod}$ applied to $B$ and $D$.
CategoryTheory.Functor.prod'defMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of F and G (from the name)
English
Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $A$ and $C$. Then the product of $F$ and $G$ is a functor of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.
CategoryTheory.Functor.prod'CompFstdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of F and G (from the docstring)
English
Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $A$ and $C$. Then the product of $F$ and $G$ is an isomorphism of the composition of the product of $F$ and $G$ and the first component of $B$ and $C$ and $F$.
CategoryTheory.Functor.prod'CompSnddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of F and G (from the docstring)
English
Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $A$ and $C$. Then the product of $F$ and $G$ is an isomorphism of the composition of the product of $F$ and $G$ and the second component of $B$ and $C$ and $G$.
CategoryTheory.Iso.proddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of f and g (from the name)
English
Let $f$ be an isomorphism of $P$ and $Q$. Let $g$ be an isomorphism of $S$ and $T$. Then the product of $f$ and $g$ is an isomorphism of $\ProdmkMACRoU {P}{S}$ and $\ProdmkMACRoU {Q}{T}$.
CategoryTheory.NatIso.proddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of x4 and x5 (from the name)
English
Let $x_{4}$ be an isomorphism of $F$ and $\mathrm{F'}$. Let $x_{5}$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the product of $x_{4}$ and $x_{5}$ is an isomorphism of the product of $F$ and $G$ and the product of $\mathrm{F'}$ and $\mathrm{G'}$.
CategoryTheory.NatTrans.proddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of x4 and x5 (from the name)
English
Let $x_{4}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $H$ and $I$. Then the product of $x_{4}$ and $x_{5}$ is a homomorphism of the product of $F$ and $H$ and the product of $G$ and $I$.
CategoryTheory.NatTrans.prod'defMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product of x3 and x4 (from the name)
English
Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $x_{4}$ be a homomorphism of $H$ and $K$. Then the product of $x_{3}$ and $x_{4}$ is a homomorphism of the product of $F$ and $H$ and the product of $G$ and $K$.
CategoryTheory.Prod.braidingdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the braiding of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the braiding of $C$ and $D$ is an equivalence of $\mathrm{Prod}$ applied to $C$ and $D$ and $\mathrm{Prod}$ applied to $D$ and $C$.
CategoryTheory.Prod.fstdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the first component of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the first component of $C$ and $D$ is a functor of $\mathrm{Prod}$ applied to $C$ and $D$ and $C$.
CategoryTheory.Prod.mkHomdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the homomorphism of f and g (from the name)
English
Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{4}$ and $x_{5}$. Then the homomorphism of $f$ and $g$ is a homomorphism of $\ProdmkMACRoU {x_{2}}{x_{4}}$ and $\ProdmkMACRoU {x_{3}}{x_{5}}$ defined as $\ProdmkMACRoU {f}{g}$.
CategoryTheory.Prod.sectLdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
no wording
English
Let $C$ be a set. Let $Z$ be an element of $D$. Then $\operatorname{sectL}$ applied to $C$ and $Z$ is a functor of $C$ and $\mathrm{Prod}$ applied to $C$ and $D$.
CategoryTheory.Prod.sectRdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
no wording
English
Let $Z$ be an element of $C$. Let $D$ be a set. Then $\operatorname{sectR}$ applied to $Z$ and $D$ is a functor of $D$ and $\mathrm{Prod}$ applied to $C$ and $D$.
CategoryTheory.Prod.snddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the second component of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the second component of $C$ and $D$ is a functor of $\mathrm{Prod}$ applied to $C$ and $D$ and $D$.
CategoryTheory.Prod.swapdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the swap of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the swap of $C$ and $D$ is a functor of $\mathrm{Prod}$ applied to $C$ and $D$ and $\mathrm{Prod}$ applied to $D$ and $C$.
CategoryTheory.Prod.symmetrydefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the symmetry of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the symmetry of $C$ and $D$ is an isomorphism of the composition of the swap of $C$ and $D$ and the swap of $D$ and $C$ and the identity of $\mathrm{Prod}$ applied to $C$ and $D$.
CategoryTheory.compEvaluationdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the composition evaluation of F and b (from the name)
English
Let $F$ be a functor of $A$ and the set of functors of $B$ and $C$. Let $b$ be an element of $B$. Then the composition evaluation of $F$ and $b$ is an isomorphism of the composition of $F$ and the action of the evaluation of $B$ and $C$ and $b$ and the action of the flip of $F$ and $b$.
CategoryTheory.evaluationdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the evaluation of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the evaluation of $C$ and $D$ is a functor of $C$ and the set of functors of the set of functors of $C$ and $D$ and $D$.
CategoryTheory.evaluationUncurrieddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
no wording
English
Let $C$ and $D$ be sets. Then $\operatorname{evaluationUncurried}$ applied to $C$ and $D$ is a functor of $\mathrm{Prod}$ applied to $C$ and the set of functors of $C$ and $D$ and $D$.
CategoryTheory.flipCompEvaluationdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the flip composition evaluation of F and a (from the name)
English
Let $F$ be a functor of $A$ and the set of functors of $B$ and $C$. Let $a$ be an element of $A$. Then the flip composition evaluation of $F$ and $a$ is an isomorphism of the composition of the flip of $F$ and the action of the evaluation of $A$ and $C$ and $a$ and the action of $F$ and $a$.
CategoryTheory.functorProdFunctorEquivdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the functor product functor equivalence of B and C (from the name)
English
Let $A$, $B$ and $C$ be sets. Then the functor product functor equivalence of $B$ and $C$ is an equivalence of $\mathrm{Prod}$ applied to the set of functors of $A$ and $B$ and the set of functors of $A$ and $C$ and the set of functors of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.
CategoryTheory.functorProdFunctorEquivCounitIsodefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the counit isomorphism for A (from the docstring)
English
Let $A$, $B$ and $C$ be sets. Then the counit isomorphism for $A$ is an isomorphism of the composition of the functor product to product functor of $B$ and $C$ and the product functor to functor product of $B$ and $C$ and the identity of the set of functors of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.
CategoryTheory.functorProdFunctorEquivUnitIsodefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the unit isomorphism for A (from the docstring)
English
Let $A$, $B$ and $C$ be sets. Then the unit isomorphism for $A$ is an isomorphism of the identity of $\mathrm{Prod}$ applied to the set of functors of $A$ and $B$ and the set of functors of $A$ and $C$ and the composition of the product functor to functor product of $B$ and $C$ and the functor product to product functor of $B$ and $C$.
CategoryTheory.functorProdToProdFunctordefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the functor product to product functor of B and C (from the name)
English
Let $A$, $B$ and $C$ be sets. Then the functor product to product functor of $B$ and $C$ is a functor of the set of functors of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$ and $\mathrm{Prod}$ applied to the set of functors of $A$ and $B$ and the set of functors of $A$ and $C$.
CategoryTheory.prod.etaIsodefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{Prod}$ applied to $C$ and $D$. Then $\operatorname{etaIso}$ applied to $X$ is an isomorphism of $\ProdmkMACRoU {\ProdfstMACRoZ {X}}{\ProdsndMACRoAA {X}}$ and $X$.
CategoryTheory.prodFunctordefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product functor (from the name)
English
The product functor is a functor of $\mathrm{Prod}$ applied to the set of functors of $A$ and $B$ and the set of functors of $C$ and $D$ and the set of functors of $\mathrm{Prod}$ applied to $A$ and $C$ and $\mathrm{Prod}$ applied to $B$ and $D$.
CategoryTheory.prodFunctorToFunctorProddefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the product functor to functor product of B and C (from the name)
English
Let $A$, $B$ and $C$ be sets. Then the product functor to functor product of $B$ and $C$ is a functor of $\mathrm{Prod}$ applied to the set of functors of $A$ and $B$ and the set of functors of $A$ and $C$ and the set of functors of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.
CategoryTheory.prodOpEquivdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the equivalence between the opposite of C (from the docstring)
English
Let $C$ be a set. Then the equivalence between the opposite of $C$ is an equivalence of the set of opposites of $\mathrm{Prod}$ applied to $C$ and $D$ and $\mathrm{Prod}$ applied to the set of opposites of $C$ and the set of opposites of $D$.
CategoryTheory.whiskeringLeftCompEvaluationdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the whiskering left composition evaluation of F and a (from the name)
English
Let $F$ be a functor of $A$ and $B$. Let $a$ be an element of $A$. Then the whiskering left composition evaluation of $F$ and $a$ is an isomorphism of the composition of the action of the left whiskering of $B$ and $C$ and $F$ and the action of the evaluation of $A$ and $C$ and $a$ and the action of the evaluation of $B$ and $C$ and the action of $F$ and $a$ defined as the identity of the composition of the action of the left whiskering of $B$ and $C$ and $F$ and the action of the evaluation of $A$ and $C$ and $a$.
CategoryTheory.whiskeringRightCompEvaluationdefMathlib.CategoryTheory.Products.Basic, function or constant
Wording
the whiskering right composition evaluation of F and a (from the name)
English
Let $F$ be a functor of $B$ and $C$. Let $a$ be an element of $A$. Then the whiskering right composition evaluation of $F$ and $a$ is an isomorphism of the composition of the action of the right whiskering of $B$ and $C$ and $F$ and the action of the evaluation of $A$ and $C$ and $a$ and the composition of the action of the evaluation of $A$ and $B$ and $a$ and $F$ defined as the identity of the composition of the action of the right whiskering of $B$ and $C$ and $F$ and the action of the evaluation of $A$ and $C$ and $a$.

Mathlib.CategoryTheory.Products.Unitor

CategoryTheory.prod.leftInverseUnitordefMathlib.CategoryTheory.Products.Unitor, function or constant
Wording
the left inverse unitor of C (from the docstring)
English
Let $C$ be a set. Then the left inverse unitor of $C$ is a functor of $C$ and $\mathrm{Prod}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$.
CategoryTheory.prod.leftUnitordefMathlib.CategoryTheory.Products.Unitor, function or constant
Wording
the left unitor functor of C (from the docstring)
English
Let $C$ be a set. Then the left unitor functor of $C$ is a functor of $\mathrm{Prod}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$ and $C$.
CategoryTheory.prod.leftUnitorEquivalencedefMathlib.CategoryTheory.Products.Unitor, function or constant
Wording
the left unitor equivalence of C (from the name)
English
Let $C$ be a set. Then the left unitor equivalence of $C$ is an equivalence of $\mathrm{Prod}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$ and $C$.
CategoryTheory.prod.rightInverseUnitordefMathlib.CategoryTheory.Products.Unitor, function or constant
Wording
the right inverse unitor of C (from the docstring)
English
Let $C$ be a set. Then the right inverse unitor of $C$ is a functor of $C$ and $\mathrm{Prod}$ applied to $C$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$.
CategoryTheory.prod.rightUnitordefMathlib.CategoryTheory.Products.Unitor, function or constant
Wording
the right unitor functor of C (from the docstring)
English
Let $C$ be a set. Then the right unitor functor of $C$ is a functor of $\mathrm{Prod}$ applied to $C$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$.
CategoryTheory.prod.rightUnitorEquivalencedefMathlib.CategoryTheory.Products.Unitor, function or constant
Wording
the right unitor equivalence of C (from the name)
English
Let $C$ be a set. Then the right unitor equivalence of $C$ is an equivalence of $\mathrm{Prod}$ applied to $C$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$.

Mathlib.CategoryTheory.Profunctor.Basic

CategoryTheory.Functor.profunctordefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the profunctor of F (from the name)
English
Let $F$ be a functor of $C$ and the set of functors of the set of opposites of $D$ and the set of sets. Then the profunctor of $F$ is a profunctor of $C$ and $D$ defined as $F$.
CategoryTheory.Functor.toProfunctordefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the profunctor of F (from the name)
English
Let $F$ be a functor of $C$ and $D$. Then the profunctor of $F$ is a profunctor of $C$ and $D$ defined as the left whisker of $F$ and the identity of $D$.
CategoryTheory.Functor.toProfunctorRevdefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
no wording
English
Let $F$ be a functor of $C$ and $D$. Then $\operatorname{toProfunctorRev}$ applied to $F$ is a profunctor of $D$ and $C$ defined as the left whisker of the identity of $D$ and $F$.
CategoryTheory.ProfunctordefMathlib.CategoryTheory.Profunctor.Basic, type
Wording
profunctor of C and D (from the name)
English
Let $C$ and $D$ be sets. Then a profunctor of $C$ and $D$ is an element of the function that maps $C$ and $D$ to the set of functors of $C$ and the set of functors of the set of opposites of $D$ and the set of sets.
CategoryTheory.Profunctor.iddefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the identity (from the name)
English
The identity is a profunctor of $C$ and $C$ defined as the Yoneda.
CategoryTheory.Profunctor.ofCoredefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the profunctor of P (from the name)
English
Let $P$ be a profunctor of $C$ and $D$. Then the profunctor of $P$ is a profunctor of $C$ and $D$.
CategoryTheory.Profunctor.ofHomdefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the profunctor of f (from the name)
English
Let $f$ be a homomorphism of $P$ and $Q$. Then the profunctor of $f$ is a homomorphism of the profunctor of $P$ and the profunctor of $Q$.
CategoryTheory.Profunctor.opdefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the opposite of P (from the docstring)
English
Let $P$ be a profunctor of $C$ and $D$. Then the opposite of $P$ is a profunctor of the set of opposites of $D$ and the set of opposites of $C$.
CategoryTheory.Profunctor.uliftdefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the lift of P (from the name)
English
Let $P$ be a profunctor of $C$ and $D$. Then the lift of $P$ is a profunctor of $C$ and $D$ defined as the action of the action of the postcomposition and the functor embedding and $P$.
CategoryTheory.Profunctor.ulift1defMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the lift of P (from the name)
English
Let $P$ be a profunctor of $C$ and $D$. Then the lift of $P$ is a profunctor of $C$ and $D$ defined as the lift of $P$.
CategoryTheory.Profunctor.whiskerLeft₂defMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the left whisker of F and G (from the name)
English
Let $P$ be a profunctor of $C$ and $D$. Let $F$ be a functor of $A$ and $C$. Let $G$ be a functor of $B$ and $D$. Then the left whisker of $F$ and $G$ is a profunctor of $A$ and $B$ defined as the action of the action of the action of the left whiskering of the set of sets and $F$ and the opposite of $G$ and $P$.
CategoryTheory.ProfunctorCorestructureMathlib.CategoryTheory.Profunctor.Basic, type
Wording
profunctor of C and D (from the name)
English
Let $C$ and $D$ be sets. Then the profunctors of $C$ and $D$ are a basic type.
CategoryTheory.ProfunctorCore.HomstructureMathlib.CategoryTheory.Profunctor.Basic, type
Wording
homomorphism of P and Q (from the name)
English
Let $P$ and $Q$ be profunctors of $C$ and $D$. Then the homomorphisms of $P$ and $Q$ are a basic type.
CategoryTheory.ProfunctorCore.Hom.appdefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the homomorphism of X and Y (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $P$ and $Q$. Let $X$ be an element of $C$. Let $Y$ be an element of $D$. Then the homomorphism of $X$ and $Y$ is a homomorphism of the set of objects of $X$ and $Y$ and the set of objects of $X$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $X$ and $Y$.
CategoryTheory.ProfunctorCore.mapdefMathlib.CategoryTheory.Profunctor.Basic, function or constant
Wording
the map of f and g (from the name)
English
Let $\mathrm{self}$ be a profunctor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $g$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Then the map of $f$ and $g$ is a homomorphism of the set of objects of $X$ and $\mathrm{Y'}$ and the set of objects of $\mathrm{X'}$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $f$ and $g$.
CategoryTheory.ProfunctorCore.objdefMathlib.CategoryTheory.Profunctor.Basic, type
Wording
object of x2 and x3 (from the name)
English
Let $\mathrm{self}$ be a profunctor of $C$ and $D$. Let $x_{2}$ be an element of $C$. Let $x_{3}$ be an element of $D$. Then an object of $x_{2}$ and $x_{3}$ is an element of the function that maps $\mathrm{self}$, $x_{2}$ and $x_{3}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

Mathlib.CategoryTheory.Profunctor.Bicategory

CategoryTheory.ProfCatstructureMathlib.CategoryTheory.Profunctor.Bicategory, type
Wording
no wording
English
The elements of $\operatorname{ProfCat}$ are a basic type.
CategoryTheory.ProfCat.objdefMathlib.CategoryTheory.Profunctor.Bicategory, type
Wording
object of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{ProfCat}$. Then an object of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

‹ previous next ›