Definitions: Mathlib.CategoryTheory, part 7 of 25

CategoryTheory.Functor.HomObjstructureMathlib.CategoryTheory.Functor.FunctorHom, type

Wording

homomorphism object of G and A (from the name)

English

Let $F$ and $G$ be functors of $C$ and $D$. Let $A$ be a functor of $C$ and the set of sets. Then the homomorphism objects of $G$ and $A$ are a basic type.

CategoryTheory.Functor.HomObj.appdefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the homomorphism object of c and a (from the name)

English

Let $\mathrm{self}$ be a homomorphism object of $G$ and $A$. Let $c$ be an element of $C$. Let $a$ be an element of the action of $A$ and $c$. Then the homomorphism object of $c$ and $a$ is a homomorphism of the action of $F$ and $c$ and the action of $G$ and $c$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $c$ and $a$.

CategoryTheory.Functor.HomObj.compdefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a homomorphism object of $G$ and $A$. Let $g$ be a homomorphism object of $M$ and $A$. Then the composition of $f$ and $g$ is a homomorphism object of $M$ and $A$.

CategoryTheory.Functor.HomObj.iddefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the identity of A (from the docstring)

English

Let $A$ be a functor of $C$ and the set of sets. Then the identity of $A$ is a homomorphism object of $F$ and $A$ defined as the homomorphism object of the identity morphism of $F$.

CategoryTheory.Functor.HomObj.mapdefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the map of f and x2 (from the name)

English

Let $f$ be a homomorphism of $\mathrm{A'}$ and $A$. Let $x_{2}$ be a homomorphism object of $G$ and $A$. Then the map of $f$ and $x_{2}$ is a homomorphism object of $G$ and $\mathrm{A'}$.

CategoryTheory.Functor.HomObj.ofNatTransdefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the homomorphism object of f (from the name)

English

Let $f$ be a homomorphism of $F$ and $G$. Then the homomorphism object of $f$ is a homomorphism object of $G$ and $A$.

CategoryTheory.Functor.functorHomdefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

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

English

Let $F$ and $G$ be functors of $C$ and $D$. Then the functor homomorphism of $F$ and $G$ is a functor of $C$ and the set of sets defined as the composition of the right opposite of the Coyoneda and the homomorphism object functor of $F$ and $G$.

CategoryTheory.Functor.functorHomEquivdefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the functor homomorphism equivalence of G and A (from the name)

English

Let $F$ and $G$ be functors of $C$ and $D$. Let $A$ be a functor of $C$ and the set of sets. Then the functor homomorphism equivalence of $G$ and $A$ is an equivalence from the set of homomorphisms of $A$ and the functor homomorphism of $F$ and $G$ to the set of homomorphism objects of $G$ and $A$.

CategoryTheory.Functor.homObjEquivdefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the homomorphism object equivalence of G and A (from the name)

English

Let $F$, $G$ and $A$ be functors of $C$ and the set of sets. Then the homomorphism object equivalence of $G$ and $A$ is an equivalence from the set of homomorphism objects of $G$ and $A$ to the set of homomorphisms of the tensor object of $F$ and $A$ and $G$.

CategoryTheory.Functor.homObjFunctordefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the homomorphism object functor of F and G (from the name)

English

Let $F$ and $G$ be functors of $C$ and $D$. Then the homomorphism object functor of $F$ and $G$ is a functor of the set of opposites of the set of functors of $C$ and the set of sets and the set of sets.

CategoryTheory.Functor.natTransEquivdefMathlib.CategoryTheory.Functor.FunctorHom, function or constant

Wording

the natural transformation equivalence (from the name)

English

The natural transformation equivalence is an equivalence from the set of homomorphisms of the tensor unity in the monoidal structure of the set of functors of $C$ and the set of sets and the functor homomorphism of $F$ and $G$ to the set of homomorphisms of $F$ and $G$.

Mathlib.CategoryTheory.Functor.Functorial

CategoryTheory.Functor.ofdefMathlib.CategoryTheory.Functor.Functorial, function or constant

Wording

no wording

English

Let $F$ be a function from elements of $C$ to elements of $D$. Then $\operatorname{of}$ applied to $F$ is a functor of $C$ and $D$ defined as $\operatorname{mk}$ applied to $F$, the function that maps $x_{2}$ and $x_{3}$ to $\operatorname{map}$ applied to $F$, $\mathrm{CategoryTheory\_\_Functorial\_\_map\_id}$ and $\mathrm{CategoryTheory\_\_Functorial\_\_map\_comp}$.

CategoryTheory.FunctorialclassMathlib.CategoryTheory.Functor.Functorial, predicate

Wording

F is functorial (from the name)

English

Let $F$ be a function from elements of $C$ to elements of $D$. Then we can say that $F$ is functorial.

CategoryTheory.Functorial.mapdefMathlib.CategoryTheory.Functor.Functorial, function or constant

Wording

the map of F and x2 (from the name)

English

Let $F$ be a function from elements of $C$ to elements of $D$. Let $x_{2}$ be a homomorphism of $X$ and $Y$. Then the map of $F$ and $x_{2}$ is a homomorphism of $F$ applied to $X$ and $F$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

Mathlib.CategoryTheory.Functor.Hom

CategoryTheory.Functor.homdefMathlib.CategoryTheory.Functor.Hom, function or constant

Wording

the homomorphism of C (from the name)

English

Let $C$ be a set. Then the homomorphism of $C$ is a functor of $\mathrm{Prod}$ applied to the set of opposites of $C$ and $C$ and the set of sets.

Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

CategoryTheory.Functor.colimitIsoColimitGrothendieckdefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $G$ be a functor of $C$ and $H$. Then $\operatorname{colimitIsoColimitGrothendieck}$ applied to $L$ and $G$ is an isomorphism of the colimit of $G$ and the colimit of the composition of the Grothendieck projection of $L$ and $G$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the colimit isomorphism of the left Kan extension of $L$ and $G$ and the unit of the chosen left Kan extension of $L$ and $G$ and the isomorphism of the left Kan extension isomorphism fiberwise colimit of $L$ and $G$ and the colimit fiberwise colimit isomorphism of the composition of the Grothendieck projection of $L$ and $G$.

CategoryTheory.Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnitdefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to the left Kan extension of $L$ and $F$ and the unit of the chosen left Kan extension of $L$ and $F$. Proof. Let $L$ be arbitrary. Let $F$ be arbitrary. By L. By F. By CategoryTheory__Functor__leftKanExtension. By L. By F. By CategoryTheory__Functor__leftKanExtensionUnit. By CategoryTheory__Functor__isPointwiseLeftKanExtensionOfIsLeftKanExtension.

CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounitdefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $\operatorname{mk}$ applied to the action of $\operatorname{ran}$ applied to $L$ and $F$ and the component of $\operatorname{ranCounit}$ applied to $L$ and $F$. Proof. Let $L$ be arbitrary. Let $F$ be arbitrary. By L. By CategoryTheory__Functor__ran. By F. By CategoryTheory__Functor__obj. By L. By CategoryTheory__Functor__ranCounit. By F. By CategoryTheory__NatTrans__app. By CategoryTheory__Functor__isPointwiseRightKanExtensionOfIsRightKanExtension.

CategoryTheory.Functor.landefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{lan}$ applied to $L$ is a functor of the set of functors of $C$ and $H$ and the set of functors of $D$ and $H$.

CategoryTheory.Functor.lanAdjunctiondefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $H$ be a set. Then $\operatorname{lanAdjunction}$ applied to $L$ and $H$ is an adjunction of $\operatorname{lan}$ applied to $L$ and the action of the left whiskering of $D$ and $H$ and $L$.

CategoryTheory.Functor.lanCompColimIsodefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{lanCompColimIso}$ applied to $L$ is an isomorphism of the composition of $\operatorname{lan}$ applied to $L$ and the colimit and the colimit.

CategoryTheory.Functor.lanUnitdefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{lanUnit}$ applied to $L$ is a homomorphism of the identity of the set of functors of $C$ and $H$ and the composition of $\operatorname{lan}$ applied to $L$ and the action of the left whiskering of $D$ and $H$ and $L$.

CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimitdefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

the left Kan extension isomorphism fiberwise colimit of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the left Kan extension isomorphism fiberwise colimit of $L$ and $F$ is an isomorphism of the left Kan extension of $L$ and $F$ and the fiberwise colimit of the composition of the Grothendieck projection of $L$ and $F$.

CategoryTheory.Functor.leftKanExtensionObjIsoColimitdefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

the left Kan extension object isomorphism colimit of F and X (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $X$ be an element of $D$. Then the left Kan extension object isomorphism colimit of $F$ and $X$ is an isomorphism of the action of the left Kan extension of $L$ and $F$ and $X$ and the colimit of the composition of the projection of $L$ and $X$ and $F$ defined as the isomorphism colimit of $\operatorname{isPointwiseLeftKanExtensionLeftKanExtensionUnit}$ applied to $L$, $F$ and $X$.

CategoryTheory.Functor.randefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{ran}$ applied to $L$ is a functor of the set of functors of $C$ and $H$ and the set of functors of $D$ and $H$.

CategoryTheory.Functor.ranAdjunctiondefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $H$ be a set. Then $\operatorname{ranAdjunction}$ applied to $L$ and $H$ is an adjunction of the action of the left whiskering of $D$ and $H$ and $L$ and $\operatorname{ran}$ applied to $L$.

CategoryTheory.Functor.ranCompLimIsodefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{ranCompLimIso}$ applied to $L$ is an isomorphism of the composition of $\operatorname{ran}$ applied to $L$ and the limit and the limit.

CategoryTheory.Functor.ranCounitdefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{ranCounit}$ applied to $L$ is a homomorphism of the composition of $\operatorname{ran}$ applied to $L$ and the action of the left whiskering of $D$ and $H$ and $L$ and the identity of the set of functors of $C$ and $H$.

CategoryTheory.Functor.ranObjObjIsoLimitdefMathlib.CategoryTheory.Functor.KanExtension.Adjunction, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $X$ be an element of $D$. Then $\operatorname{ranObjObjIsoLimit}$ applied to $L$, $F$ and $X$ is an isomorphism of the action of the action of $\operatorname{ran}$ applied to $L$ and $F$ and $X$ and the limit of the composition of the projection of $X$ and $L$ and $F$ defined as the isomorphism limit of $\operatorname{isPointwiseRightKanExtensionRanCounit}$ applied to $L$, $F$ and $X$.

Mathlib.CategoryTheory.Functor.KanExtension.AdjunctionPreserves

CategoryTheory.Adjunction.leftExtensionPostCompose₂RightAdjointdefMathlib.CategoryTheory.Functor.KanExtension.AdjunctionPreserves, function or constant

Wording

the right adjoint of adj (from the docstring)

English

Let $\mathrm{adj}$ be an adjunction of $x_{6}$ and $x_{7}$. Let $F$ be a functor of $C$ and $x$. Let $L$ be a functor of $C$ and $D$. Then the right adjoint of $\mathrm{adj}$ is a functor of the set of left extensions of $L$ and the composition of $F$ and $x_{6}$ and the set of left extensions of $L$ and $F$.

CategoryTheory.Adjunction.leftExtensionPostcompose₂defMathlib.CategoryTheory.Functor.KanExtension.AdjunctionPreserves, function or constant

Wording

the left extension postcomposition of F and L (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $x_{6}$ and $x_{7}$. Let $F$ be a functor of $C$ and $x$. Let $L$ be a functor of $C$ and $D$. Then the left extension postcomposition of $F$ and $L$ is an adjunction of the postcomposition of $F$ and $x_{6}$ and the right adjoint of $\mathrm{adj}$.

CategoryTheory.Adjunction.rightExtensionPostCompose₂LeftAdjointdefMathlib.CategoryTheory.Functor.KanExtension.AdjunctionPreserves, function or constant

Wording

the left adjoint of adj (from the docstring)

English

Let $\mathrm{adj}$ be an adjunction of $x_{6}$ and $x_{7}$. Let $F$ be a functor of $C$ and $x_{1}$. Let $L$ be a functor of $C$ and $D$. Then the left adjoint of $\mathrm{adj}$ is a functor of the set of right extensions of $L$ and the composition of $F$ and $x_{7}$ and the set of right extensions of $L$ and $F$.

CategoryTheory.Adjunction.rightExtensionPostcompose₂defMathlib.CategoryTheory.Functor.KanExtension.AdjunctionPreserves, function or constant

Wording

the right extension postcomposition of F and L (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $x_{6}$ and $x_{7}$. Let $F$ be a functor of $C$ and $x_{1}$. Let $L$ be a functor of $C$ and $D$. Then the right extension postcomposition of $F$ and $L$ is an adjunction of the left adjoint of $\mathrm{adj}$ and the postcomposition of $F$ and $x_{7}$.

Mathlib.CategoryTheory.Functor.KanExtension.Basic

CategoryTheory.Functor.HasLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, predicate

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{HasLeftKanExtension}$ holds for $L$ and $F$, if $\operatorname{HasInitial}$ holds for the set of left extensions of $L$ and $F$.

CategoryTheory.Functor.HasRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, predicate

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{HasRightKanExtension}$ holds for $L$ and $F$, if the set of right extensions of $L$ and $F$ has terminals.

CategoryTheory.Functor.IsLeftKanExtensionclassMathlib.CategoryTheory.Functor.KanExtension.Basic, predicate

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Then we can say that $\operatorname{IsLeftKanExtension}$ holds for $\mathrm{F'}$ and $x_{3}$.

CategoryTheory.Functor.IsRightKanExtensionclassMathlib.CategoryTheory.Functor.KanExtension.Basic, predicate

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Then we can say that $\operatorname{IsRightKanExtension}$ holds for $\mathrm{F'}$ and $x_{3}$.

CategoryTheory.Functor.LeftExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, type

Wording

left extension of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then a left extension of $L$ and $F$ is an element of the function that maps $L$ and $F$ to the set of structured arrows of $F$ and the action of the left whiskering of $D$ and $H$ and $L$.

CategoryTheory.Functor.LeftExtension.isUniversalEquivOfIso₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $x_{5}$ be a left extension of $L$ and $x_{3}$. Let $x_{6}$ be a left extension of $L$ and $x_{4}$. Let $e$ be an isomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{e'}$ be an isomorphism of the right object of $x_{5}$ and the right object of $x_{6}$ such that the composition of the homomorphism of $x_{5}$ and the left whisker of $L$ and the homomorphism of $\mathrm{e'}$ is equal to the composition of the homomorphism of $e$ and the homomorphism of $x_{6}$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LeftExtension\_\_isUniversalEquivOfIso\_u2082\_}$ applied to $x_{5}$, $x_{6}$, $e$, $\mathrm{e'}$ and $h$ is an element of $\EquivMACRoAE {\operatorname{IsUniversal} (x_{5})}{\operatorname{IsUniversal} (x_{6})}$.

CategoryTheory.Functor.LeftExtension.isUniversalOfPrecomp₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $x_{6}$ be a homomorphism of $x_{4}$ and the composition of $L$ and $x_{5}$. Let $x_{7}$ be an element of $\operatorname{IsUniversal}$ applied to $\operatorname{mk}$ applied to $x_{5}$ and $x_{6}$. Let $\mathrm{hb}$ be an element of $\operatorname{IsUniversal}$ applied to the action of the precomposition of $\mathrm{L'}$ and $x_{6}$ and $b$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LeftExtension\_\_isUniversalOfPrecomp\_u2082\_}$ applied to $x_{6}$, $x_{7}$ and $\mathrm{hb}$ is an element of $\operatorname{IsUniversal}$ applied to $b$ defined as $\operatorname{ofUnique}$ applied to $b$.

CategoryTheory.Functor.LeftExtension.isUniversalPostcomp₁EquivdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $G$ be a functor of $D$ and $\mathrm{D'}$. Let $e$ be an isomorphism of the composition of $L$ and $G$ and $\mathrm{L'}$. Let $F$ be a functor of $C$ and $H$. Let $\mathrm{ex}$ be a left extension of $\mathrm{L'}$ and $F$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LeftExtension\_\_isUniversalPostcomp\_u2081\_Equiv}$ applied to $G$, $e$, $F$ and $\mathrm{ex}$ is an equivalence from $\operatorname{IsUniversal}$ applied to $\mathrm{ex}$ to $\operatorname{IsUniversal}$ applied to the action of the postcomposition of the inverse of $e$ and $F$ and $\mathrm{ex}$ defined as $\operatorname{isInitialIffObj}$ applied to the postcomposition of the inverse of $e$ and $F$ and $\mathrm{ex}$.

CategoryTheory.Functor.LeftExtension.isUniversalPrecompEquivdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $G$ be a functor of $\mathrm{C'}$ and $C$. Let $e$ be a left extension of $L$ and $F$. Then $\operatorname{isUniversalPrecompEquiv}$ applied to $L$, $F$, $G$ and $e$ is an equivalence from $\operatorname{IsUniversal}$ applied to $e$ to $\operatorname{IsUniversal}$ applied to the action of the precomposition of $F$ and $G$ and $e$ defined as $\operatorname{isInitialIffObj}$ applied to the precomposition of $F$ and $G$ and $e$.

CategoryTheory.Functor.LeftExtension.isUniversalPrecomp₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $x_{6}$ be a homomorphism of $x_{4}$ and the composition of $L$ and $x_{5}$. Let $x_{7}$ be an element of $\operatorname{IsUniversal}$ applied to $\operatorname{mk}$ applied to $x_{5}$ and $x_{6}$. Let $\mathrm{hb}$ be an element of $\operatorname{IsUniversal}$ applied to $b$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LeftExtension\_\_isUniversalPrecomp\_u2082\_}$ applied to $x_{6}$, $x_{7}$ and $\mathrm{hb}$ is an element of $\operatorname{IsUniversal}$ applied to the action of the precomposition of $\mathrm{L'}$ and $x_{6}$ and $b$ defined as $\operatorname{ofUnique}$ applied to the action of the precomposition of $\mathrm{L'}$ and $x_{6}$ and $b$.

CategoryTheory.Functor.LeftExtension.isUniversalPrecomp₂EquivdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $x_{6}$ be a homomorphism of $x_{4}$ and the composition of $L$ and $x_{5}$. Let $x_{7}$ be an element of $\operatorname{IsUniversal}$ applied to $\operatorname{mk}$ applied to $x_{5}$ and $x_{6}$. Let $b$ be a left extension of $\mathrm{L'}$ and $x_{5}$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LeftExtension\_\_isUniversalPrecomp\_u2082\_Equiv}$ applied to $x_{6}$, $x_{7}$ and $b$ is an equivalence from $\operatorname{IsUniversal}$ applied to $b$ to $\operatorname{IsUniversal}$ applied to the action of the precomposition of $\mathrm{L'}$ and $x_{6}$ and $b$.

CategoryTheory.Functor.LeftExtension.mkdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Then $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{3}$ is a left extension of $L$ and $F$ defined as $\operatorname{mk}$ applied to $x_{3}$.

CategoryTheory.Functor.LeftExtension.postcompose₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the postcomposition of F and G (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $G$ be a functor of $H$ and $\mathrm{D'}$. Then the postcomposition of $F$ and $G$ is a functor of the set of left extensions of $L$ and $F$ and the set of left extensions of $L$ and the composition of $F$ and $G$.

CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIsodefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the postcomposition object isomorphism of G and x4 (from the name)

English

Let $G$ be a functor of $H$ and $\mathrm{D'}$. Let $x_{4}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Then the postcomposition object isomorphism of $G$ and $x_{4}$ is an isomorphism of the action of the postcomposition of $F$ and $G$ and $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{4}$ and $\operatorname{mk}$ applied to the composition of $\mathrm{F'}$ and $G$ and the composition of the right whisker of $x_{4}$ and $G$ and the homomorphism of the associator of $\mathrm{F'}$ and $G$.

CategoryTheory.Functor.LeftExtension.postcomp₁defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the postcomposition of f and F (from the name)

English

Let $G$ be a functor of $D$ and $\mathrm{D'}$. Let $f$ be a homomorphism of $\mathrm{L'}$ and the composition of $L$ and $G$. Let $F$ be a functor of $C$ and $H$. Then the postcomposition of $f$ and $F$ is a functor of the set of left extensions of $\mathrm{L'}$ and $F$ and the set of left extensions of $L$ and $F$ defined as the map of the identity morphism of $F$ and the map of the left whiskering of $\mathrm{D'}$ and $H$ and $f$.

CategoryTheory.Functor.LeftExtension.precompdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the precomposition of F and G (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $G$ be a functor of $\mathrm{C'}$ and $C$. Then the precomposition of $F$ and $G$ is a functor of the set of left extensions of $L$ and $F$ and the set of left extensions of the composition of $G$ and $L$ and the composition of $G$ and $F$ defined as the map of the identity morphism of the composition of $G$ and $F$ and the identity morphism of the composition of the action of the left whiskering of $D$ and $H$ and $L$ and the action of the left whiskering of $C$ and $H$ and $G$.

CategoryTheory.Functor.LeftExtension.precomp₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the precomposition of x6 and #2 (from the name)

English

Let $\mathrm{L'}$ be a functor of $D$ and $\mathrm{D'}$. Let $x_{6}$ be a homomorphism of $x_{4}$ and the composition of $L$ and $x_{5}$. Then the precomposition of $\mathrm{L'}$ and $x_{6}$ is a functor of the set of left extensions of $\mathrm{L'}$ and $x_{5}$ and the set of left extensions of the composition of $L$ and $\mathrm{L'}$ and $x_{4}$ defined as the composition of the precomposition of $x_{5}$ and $L$ and the map of $x_{6}$.

CategoryTheory.Functor.RightExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, type

Wording

right extension of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then a right extension of $L$ and $F$ is an element of the function that maps $L$ and $F$ to the set of costructured arrows of the action of the left whiskering of $D$ and $H$ and $L$ and $F$.

CategoryTheory.Functor.RightExtension.isUniversalEquivOfIso₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $x_{5}$ be a right extension of $L$ and $x_{3}$. Let $x_{6}$ be a right extension of $L$ and $x_{4}$. Let $e$ be an isomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{e'}$ be an isomorphism of the left object of $x_{5}$ and the left object of $x_{6}$ such that the composition of the left whisker of $L$ and the homomorphism of $\mathrm{e'}$ and the homomorphism of $x_{6}$ is equal to the composition of the homomorphism of $x_{5}$ and the homomorphism of $e$. Then $\mathrm{CategoryTheory\_\_Functor\_\_RightExtension\_\_isUniversalEquivOfIso\_u2082\_}$ applied to $x_{5}$, $x_{6}$, $e$, $\mathrm{e'}$ and $h$ is an element of $\EquivMACRoAE {\operatorname{IsUniversal} (x_{5})}{\operatorname{IsUniversal} (x_{6})}$.

CategoryTheory.Functor.RightExtension.isUniversalPostcomp₁EquivdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $G$ be a functor of $D$ and $\mathrm{D'}$. Let $e$ be an isomorphism of the composition of $L$ and $G$ and $\mathrm{L'}$. Let $F$ be a functor of $C$ and $H$. Let $\mathrm{ex}$ be a right extension of $\mathrm{L'}$ and $F$. Then $\mathrm{CategoryTheory\_\_Functor\_\_RightExtension\_\_isUniversalPostcomp\_u2081\_Equiv}$ applied to $G$, $e$, $F$ and $\mathrm{ex}$ is an equivalence from $\operatorname{IsUniversal}$ applied to $\mathrm{ex}$ to $\operatorname{IsUniversal}$ applied to the action of the postcomposition of the homomorphism of $e$ and $F$ and $\mathrm{ex}$ defined as $\operatorname{isTerminalIffObj}$ applied to the postcomposition of the homomorphism of $e$ and $F$ and $\mathrm{ex}$.

CategoryTheory.Functor.RightExtension.isUniversalPrecompEquivdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $G$ be a functor of $\mathrm{C'}$ and $C$. Let $e$ be a right extension of $L$ and $F$. Then $\operatorname{isUniversalPrecompEquiv}$ applied to $L$, $F$, $G$ and $e$ is an equivalence from $\operatorname{IsUniversal}$ applied to $e$ to $\operatorname{IsUniversal}$ applied to the action of the precomposition of $F$ and $G$ and $e$ defined as $\operatorname{isTerminalIffObj}$ applied to the precomposition of $F$ and $G$ and $e$.

CategoryTheory.Functor.RightExtension.mkdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Then $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{3}$ is a right extension of $L$ and $F$ defined as $\operatorname{mk}$ applied to $x_{3}$.

CategoryTheory.Functor.RightExtension.postcompose₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the postcomposition of F and G (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $G$ be a functor of $H$ and $\mathrm{D'}$. Then the postcomposition of $F$ and $G$ is a functor of the set of right extensions of $L$ and $F$ and the set of right extensions of $L$ and the composition of $F$ and $G$.

CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIsodefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the postcomposition object isomorphism of G and x4 (from the name)

English

Let $G$ be a functor of $H$ and $\mathrm{D'}$. Let $x_{4}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Then the postcomposition object isomorphism of $G$ and $x_{4}$ is an isomorphism of the action of the postcomposition of $F$ and $G$ and $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{4}$ and $\operatorname{mk}$ applied to the composition of $\mathrm{F'}$ and $G$ and the composition of the inverse of the associator of $\mathrm{F'}$ and $G$ and the right whisker of $x_{4}$ and $G$.

CategoryTheory.Functor.RightExtension.postcomp₁defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the postcomposition of f and F (from the name)

English

Let $G$ be a functor of $D$ and $\mathrm{D'}$. Let $f$ be a homomorphism of the composition of $L$ and $G$ and $\mathrm{L'}$. Let $F$ be a functor of $C$ and $H$. Then the postcomposition of $f$ and $F$ is a functor of the set of right extensions of $\mathrm{L'}$ and $F$ and the set of right extensions of $L$ and $F$ defined as the map of the map of the left whiskering of $\mathrm{D'}$ and $H$ and $f$ and the identity morphism of the action of the identity of the set of functors of $C$ and $H$ and $F$.

CategoryTheory.Functor.RightExtension.precompdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the precomposition of F and G (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $G$ be a functor of $\mathrm{C'}$ and $C$. Then the precomposition of $F$ and $G$ is a functor of the set of right extensions of $L$ and $F$ and the set of right extensions of the composition of $G$ and $L$ and the composition of $G$ and $F$ defined as the map of the identity morphism of the composition of the identity of the set of functors of $D$ and $H$ and the action of the left whiskering of $D$ and $H$ and the composition of $G$ and $L$ and the identity morphism of the action of the action of the left whiskering of $C$ and $H$ and $G$ and $F$.

CategoryTheory.Functor.coconeOfIsLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the cocone of c and #3 (from the name)

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Let $c$ be a cocone of $F$. Then the cocone of $x_{3}$ and $c$ is a cocone of $\mathrm{F'}$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{descOfIsLeftKanExtension}$ applied to $\mathrm{F'}$, $x_{3}$, the action of the constant of $D$ and $\operatorname{pt}$ applied to $c$ and the inclusion of $c$.

CategoryTheory.Functor.colimitIsoOfIsLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the colimit isomorphism of x3 and #2 (from the name)

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Then the colimit isomorphism of $\mathrm{F'}$ and $x_{3}$ is an isomorphism of the colimit of $\mathrm{F'}$ and the colimit of $F$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to $\mathrm{F'}$ and $\operatorname{isColimitCoconeOfIsLeftKanExtension}$ applied to $\mathrm{F'}$, $x_{3}$ and $\operatorname{isColimit}$ applied to $F$.

CategoryTheory.Functor.coneOfIsRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the cone of c and #3 (from the name)

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Let $c$ be a cone of $F$. Then the cone of $x_{3}$ and $c$ is a cone of $\mathrm{F'}$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the lift of the action of the constant of $D$ and $\operatorname{pt}$ applied to $c$ and the projection of $c$.

CategoryTheory.Functor.descOfIsLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ and $G$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Let $x_{4}$ be a homomorphism of $F$ and the composition of $L$ and $G$. Then $\operatorname{descOfIsLeftKanExtension}$ applied to $\mathrm{F'}$, $x_{3}$, $G$ and $x_{4}$ is a homomorphism of $\mathrm{F'}$ and $G$ defined as $\operatorname{desc}$ applied to $\operatorname{isUniversalOfIsLeftKanExtension}$ applied to $\mathrm{F'}$ and $x_{3}$ and $\operatorname{mk}$ applied to $G$ and $x_{4}$.

CategoryTheory.Functor.homEquivOfIsLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the homomorphism equivalence of G and #3 (from the name)

English

Let $\mathrm{F'}$ and $G$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Then the homomorphism equivalence of $x_{3}$ and $G$ is an equivalence from the set of homomorphisms of $\mathrm{F'}$ and $G$ to the set of homomorphisms of $F$ and the composition of $L$ and $G$.

CategoryTheory.Functor.homEquivOfIsRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the homomorphism equivalence of G and #3 (from the name)

English

Let $\mathrm{F'}$ and $G$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Then the homomorphism equivalence of $x_{3}$ and $G$ is an equivalence from the set of homomorphisms of $G$ and $\mathrm{F'}$ to the set of homomorphisms of the composition of $L$ and $G$ and $F$.

CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCoconeOfIsLeftKanExtension}$ applied to $\mathrm{F'}$, $x_{3}$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $x_{3}$ and $c$.

CategoryTheory.Functor.isLimitConeOfIsRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitConeOfIsRightKanExtension}$ applied to $\mathrm{F'}$, $x_{3}$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $x_{3}$ and $c$.

CategoryTheory.Functor.isUniversalOfIsLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Then $\operatorname{isUniversalOfIsLeftKanExtension}$ applied to $\mathrm{F'}$ and $x_{3}$ is an element of $\operatorname{IsUniversal}$ applied to $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{3}$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsLeftKanExtension\_\_nonempty\_isUniversal}$.

CategoryTheory.Functor.isUniversalOfIsRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Then $\operatorname{isUniversalOfIsRightKanExtension}$ applied to $\mathrm{F'}$ and $x_{3}$ is an element of $\operatorname{IsUniversal}$ applied to $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{3}$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsRightKanExtension\_\_nonempty\_isUniversal}$.

CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the equivalence of x3 and F (from the docstring)

English

Let $x_{3}$ be an isomorphism of $L$ and $\mathrm{L'}$. Let $F$ be a functor of $C$ and $H$. Then the equivalence of $x_{3}$ and $F$ is an equivalence of the set of left extensions of $L$ and $F$ and the set of left extensions of $\mathrm{L'}$ and $F$ defined as the map natural isomorphism of the map isomorphism of the left whiskering of $D$ and $H$ and $x_{3}$.

CategoryTheory.Functor.leftExtensionEquivalenceOfIso₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the equivalence of L and x3 (from the docstring)

English

Let $L$ be a functor of $C$ and $D$. Let $x_{3}$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the equivalence of $L$ and $x_{3}$ is an equivalence of the set of left extensions of $L$ and $F$ and the set of left extensions of $L$ and $\mathrm{F'}$ defined as the map isomorphism of $x_{3}$.

CategoryTheory.Functor.leftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the left Kan extension of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the left Kan extension of $L$ and $F$ is a functor of $D$ and $H$ defined as the right object of $\operatorname{initial}$ applied to the set of left extensions of $L$ and $F$.

CategoryTheory.Functor.leftKanExtensionUniquedefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ and $\mathrm{F''}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Let $x_{4}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F''}$. Then $\operatorname{leftKanExtensionUnique}$ applied to $\mathrm{F'}$, $x_{3}$, $\mathrm{F''}$ and $x_{4}$ is an isomorphism of $\mathrm{F'}$ and $\mathrm{F''}$ defined as $\operatorname{leftKanExtensionUniqueOfIso}$ applied to $\mathrm{F'}$, $x_{3}$, the identity of $F$, $\mathrm{F''}$ and $x_{4}$.

CategoryTheory.Functor.leftKanExtensionUniqueOfIsodefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ and $\mathrm{G'}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Let $i$ be an isomorphism of $F$ and $G$. Let $x_{4}$ be a homomorphism of $G$ and the composition of $L$ and $\mathrm{G'}$. Then $\operatorname{leftKanExtensionUniqueOfIso}$ applied to $\mathrm{F'}$, $x_{3}$, $i$, $\mathrm{G'}$ and $x_{4}$ is an isomorphism of $\mathrm{F'}$ and $\mathrm{G'}$.

CategoryTheory.Functor.leftKanExtensionUnitdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the unit of the chosen left Kan extension of L and F (from the docstring)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the unit of the chosen left Kan extension of $L$ and $F$ is a homomorphism of $F$ and the composition of $L$ and the left Kan extension of $L$ and $F$ defined as the homomorphism of $\operatorname{initial}$ applied to the set of left extensions of $L$ and $F$.

CategoryTheory.Functor.liftOfIsRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the lift of x4 and #4 (from the name)

English

Let $\mathrm{F'}$ and $G$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Let $x_{4}$ be a homomorphism of the composition of $L$ and $G$ and $F$. Then the lift of $G$ and $x_{4}$ is a homomorphism of $G$ and $\mathrm{F'}$ defined as the lift of $\operatorname{isUniversalOfIsRightKanExtension}$ applied to $\mathrm{F'}$ and $x_{3}$ and $\operatorname{mk}$ applied to $G$ and $x_{4}$.

CategoryTheory.Functor.limitIsoOfIsRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the limit isomorphism of x3 and #2 (from the name)

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Then the limit isomorphism of $\mathrm{F'}$ and $x_{3}$ is an isomorphism of the limit of $\mathrm{F'}$ and the limit of $F$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to $\mathrm{F'}$ and $\operatorname{isLimitConeOfIsRightKanExtension}$ applied to $\mathrm{F'}$, $x_{3}$ and $\operatorname{isLimit}$ applied to $F$.

CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the equivalence of x3 and F (from the docstring)

English

Let $x_{3}$ be an isomorphism of $L$ and $\mathrm{L'}$. Let $F$ be a functor of $C$ and $H$. Then the equivalence of $x_{3}$ and $F$ is an equivalence of the set of right extensions of $L$ and $F$ and the set of right extensions of $\mathrm{L'}$ and $F$ defined as the map natural isomorphism of the map isomorphism of the left whiskering of $D$ and $H$ and $x_{3}$.

CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂defMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the equivalence of L and x3 (from the docstring)

English

Let $L$ be a functor of $C$ and $D$. Let $x_{3}$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the equivalence of $L$ and $x_{3}$ is an equivalence of the set of right extensions of $L$ and $F$ and the set of right extensions of $L$ and $\mathrm{F'}$ defined as the map isomorphism of $x_{3}$.

CategoryTheory.Functor.rightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the right Kan extension of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the right Kan extension of $L$ and $F$ is a functor of $D$ and $H$ defined as the left object of $\operatorname{terminal}$ applied to the set of right extensions of $L$ and $F$.

CategoryTheory.Functor.rightKanExtensionCounitdefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

the counit of the chosen right Kan extension of L and F (from the docstring)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the counit of the chosen right Kan extension of $L$ and $F$ is a homomorphism of the composition of $L$ and the right Kan extension of $L$ and $F$ and $F$ defined as the homomorphism of $\operatorname{terminal}$ applied to the set of right extensions of $L$ and $F$.

CategoryTheory.Functor.rightKanExtensionUniquedefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ and $\mathrm{F''}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Let $x_{4}$ be a homomorphism of the composition of $L$ and $\mathrm{F''}$ and $F$. Then $\operatorname{rightKanExtensionUnique}$ applied to $\mathrm{F'}$, $x_{3}$, $\mathrm{F''}$ and $x_{4}$ is an isomorphism of $\mathrm{F'}$ and $\mathrm{F''}$ defined as $\operatorname{rightKanExtensionUniqueOfIso}$ applied to $\mathrm{F'}$, $x_{3}$, the identity of $F$, $\mathrm{F''}$ and $x_{4}$.

CategoryTheory.Functor.rightKanExtensionUniqueOfIsodefMathlib.CategoryTheory.Functor.KanExtension.Basic, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ and $\mathrm{G'}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Let $i$ be an isomorphism of $F$ and $G$. Let $x_{4}$ be a homomorphism of the composition of $L$ and $\mathrm{G'}$ and $G$. Then $\operatorname{rightKanExtensionUniqueOfIso}$ applied to $\mathrm{F'}$, $x_{3}$, $i$, $\mathrm{G'}$ and $x_{4}$ is an isomorphism of $\mathrm{F'}$ and $\mathrm{G'}$.

Mathlib.CategoryTheory.Functor.KanExtension.Dense

CategoryTheory.Functor.IsDenseclassMathlib.CategoryTheory.Functor.KanExtension.Dense, predicate

Wording

F is dense (from the name)

English

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

CategoryTheory.Functor.IsDense.leftKanExtensionIsodefMathlib.CategoryTheory.Functor.KanExtension.Dense, function or constant

Wording

the left Kan extension isomorphism of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the left Kan extension isomorphism of $F$ is an isomorphism of the left Kan extension of $F$ and $F$ and the identity of $D$ defined as $\operatorname{leftKanExtensionUnique}$ applied to the left Kan extension of $F$ and $F$, the unit of the chosen left Kan extension of $F$ and $F$, the identity of $D$ and the inverse of the right unitor of $F$.

CategoryTheory.Functor.denseAtdefMathlib.CategoryTheory.Functor.KanExtension.Dense, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Let $Y$ be an element of $D$. Then $\operatorname{denseAt}$ applied to $F$ and $Y$ is an element of $\operatorname{DenseAt}$ applied to $F$ and $Y$ defined as $\operatorname{some}$ applied to $\operatorname{isDenseAt}$ applied to $F$ and $Y$.

CategoryTheory.denseAtUliftYonedadefMathlib.CategoryTheory.Functor.KanExtension.Dense, function or constant

Wording

no wording

English

Let $X$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{denseAtUliftYoneda}$ applied to $X$ is an element of $\operatorname{DenseAt}$ applied to the lift Yoneda and $X$ defined as $\operatorname{isColimitTautologicalCocone'}$ applied to $X$.

CategoryTheory.denseAtYonedadefMathlib.CategoryTheory.Functor.KanExtension.Dense, function or constant

Wording

no wording

English

Let $X$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{denseAtYoneda}$ applied to $X$ is an element of $\operatorname{DenseAt}$ applied to the Yoneda and $X$ defined as $\operatorname{isColimitTautologicalCocone}$ applied to $X$.

Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

CategoryTheory.Functor.DenseAtdefMathlib.CategoryTheory.Functor.KanExtension.DenseAt, type

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Let $Y$ be an element of $D$. Then an element of $\operatorname{DenseAt}$ applied to $F$ and $Y$ is an element of the function that maps $F$ and $Y$ to $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $\operatorname{mk}$ applied to the identity of $D$ and the inverse of the right unitor of $F$ and $Y$.

CategoryTheory.Functor.DenseAt.ofIsodefMathlib.CategoryTheory.Functor.KanExtension.DenseAt, function or constant

Wording

no wording

English

Let $\mathrm{hY}$ be an element of $\operatorname{DenseAt}$ applied to $F$ and $Y$. Let $e$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Then $\operatorname{ofIso}$ applied to $\mathrm{hY}$ and $e$ is an element of $\operatorname{DenseAt}$ applied to $F$ and $\mathrm{Y'}$ defined as $\operatorname{isPointwiseLeftKanExtensionAtOfIso'}$ applied to $\operatorname{mk}$ applied to the identity of $D$ and the inverse of the right unitor of $F$, $\mathrm{hY}$ and $e$.

CategoryTheory.Functor.DenseAt.ofNatIsodefMathlib.CategoryTheory.Functor.KanExtension.DenseAt, function or constant

Wording

no wording

English

Let $\mathrm{hY}$ be an element of $\operatorname{DenseAt}$ applied to $F$ and $Y$. Let $e$ be an isomorphism of $F$ and $G$. Then $\operatorname{ofNatIso}$ applied to $\mathrm{hY}$ and $e$ is an element of $\operatorname{DenseAt}$ applied to $G$ and $Y$.

CategoryTheory.Functor.DenseAt.postcompEquivalencedefMathlib.CategoryTheory.Functor.KanExtension.DenseAt, function or constant

Wording

the postcomposition equivalence of hY and G (from the name)

English

Let $\mathrm{hY}$ be an element of $\operatorname{DenseAt}$ applied to $F$ and $Y$. Let $G$ be a functor of $D$ and $\mathrm{D'}$. Then the postcomposition equivalence of $\mathrm{hY}$ and $G$ is an element of $\operatorname{DenseAt}$ applied to the composition of $F$ and $G$ and the action of $G$ and $Y$.

CategoryTheory.Functor.DenseAt.precompEquivOfFinaldefMathlib.CategoryTheory.Functor.KanExtension.DenseAt, function or constant

Wording

the precomposition equivalence of G (from the name)

English

Let $G$ be a functor of $\mathrm{C'}$ and $C$. Then the precomposition equivalence of $G$ is an equivalence from $\operatorname{DenseAt}$ applied to the composition of $G$ and $F$ and $Y$ to $\operatorname{DenseAt}$ applied to $F$ and $Y$ defined as $\operatorname{isColimitWhiskerEquiv}$ applied to $\operatorname{pre}$ applied to $G$, $F$ and $Y$ and $\operatorname{coconeAt}$ applied to $\operatorname{mk}$ applied to the identity of $D$ and the inverse of the right unitor of $F$ and $Y$.

CategoryTheory.Functor.DenseAt.precompOfFinaldefMathlib.CategoryTheory.Functor.KanExtension.DenseAt, function or constant

Wording

the precomposition of hY and G (from the name)

English

Let $\mathrm{hY}$ be an element of $\operatorname{DenseAt}$ applied to $F$ and $Y$. Let $G$ be a functor of $\mathrm{C'}$ and $C$. Then the precomposition of $\mathrm{hY}$ and $G$ is an element of $\operatorname{DenseAt}$ applied to the composition of $G$ and $F$ and $Y$ defined as $\operatorname{symm}$ applied to the precomposition equivalence of $G$ and $\mathrm{hY}$.

CategoryTheory.Functor.denseAtEquivdefMathlib.CategoryTheory.Functor.KanExtension.DenseAt, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Let $Y$ be an element of $D$. Then $\operatorname{denseAtEquiv}$ applied to $F$ and $Y$ is an equivalence from $\operatorname{DenseAt}$ applied to $F$ and $Y$ to $\operatorname{IsColimit}$ applied to $\operatorname{coconeAt}$ applied to $\operatorname{mk}$ applied to the identity of $D$ and the inverse of the right unitor of $F$ and $Y$ defined as the identity of $\operatorname{DenseAt}$ applied to $F$ and $Y$.

CategoryTheory.Functor.isDenseAtdefMathlib.CategoryTheory.Functor.KanExtension.DenseAt, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then there is an object property of $D$. Proof. Let $F$ be arbitrary. Let $Y$ be arbitrary. By F. By Y. By CategoryTheory__Functor__DenseAt. By Nonempty.

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

CategoryTheory.Functor.HasPointwiseLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, predicate

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{HasPointwiseLeftKanExtension}$ holds for $L$ and $F$, if for all elements $Y$ of $D$, $\operatorname{HasPointwiseLeftKanExtensionAt}$ holds for $L$, $F$ and $Y$.

CategoryTheory.Functor.HasPointwiseLeftKanExtensionAtdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, predicate

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $Y$ be an element of $D$. Then $\operatorname{HasPointwiseLeftKanExtensionAt}$ holds for $L$, $F$ and $Y$, if the composition of the projection of $L$ and $Y$ and $F$ has colimits.

CategoryTheory.Functor.HasPointwiseRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, predicate

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{HasPointwiseRightKanExtension}$ holds for $L$ and $F$, if for all elements $Y$ of $D$, $\operatorname{HasPointwiseRightKanExtensionAt}$ holds for $L$, $F$ and $Y$.

CategoryTheory.Functor.HasPointwiseRightKanExtensionAtdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, predicate

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $Y$ be an element of $D$. Then $\operatorname{HasPointwiseRightKanExtensionAt}$ holds for $L$, $F$ and $Y$, if the composition of the projection of $Y$ and $L$ and $F$ has limits.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, type

Wording

no wording

English

Let $E$ be a left extension of $L$ and $F$. Then an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $E$ is an element of the function that maps $E$ to the set of functions from elements $Y$ of $D$ to elements of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $E$ and $Y$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.homFromdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $E$. Let $G$ be a left extension of $L$ and $F$. Then $\operatorname{homFrom}$ applied to $h$ and $G$ is a homomorphism of $E$ and $G$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isUniversaldefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $E$. Then $\operatorname{isUniversal}$ applied to $h$ is an element of $\operatorname{IsUniversal}$ applied to $E$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAtdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, type

Wording

no wording

English

Let $E$ be a left extension of $L$ and $F$. Let $Y$ be an element of $D$. Then an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $E$ and $Y$ is an element of the function that maps $E$ and $Y$ to $\operatorname{IsColimit}$ applied to $\operatorname{coconeAt}$ applied to $E$ and $Y$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimitdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

the isomorphism colimit of h (from the name)

English

Let $h$ be an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $E$ and $Y$. Then the isomorphism colimit of $h$ is an isomorphism of the action of the right object of $E$ and $Y$ and the colimit of the composition of the projection of $L$ and $Y$ and $F$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $h$ and $\operatorname{isColimit}$ applied to the composition of the projection of $L$ and $Y$ and $F$.

CategoryTheory.Functor.LeftExtension.coconeAtdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $E$ be a left extension of $L$ and $F$. Let $Y$ be an element of $D$. Then $\operatorname{coconeAt}$ applied to $E$ and $Y$ is a cocone of the composition of the projection of $L$ and $Y$ and $F$.

CategoryTheory.Functor.LeftExtension.coconeAtFunctordefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

the cocone at functor of F and Y (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $Y$ be an element of $D$. Then the cocone at functor of $F$ and $Y$ is a functor of the set of left extensions of $L$ and $F$ and the set of cocones of the composition of the projection of $L$ and $Y$ and $F$.

CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $E$ be a left extension of $L$ and $F$. Then there is an object property of $D$. Proof. Let $E$ be arbitrary. Let $Y$ be arbitrary. By E. By Y. By CategoryTheory__Functor__LeftExtension__IsPointwiseLeftKanExtensionAt. By Nonempty.

CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIsodefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $e$ be an isomorphism of $E$ and $\mathrm{E'}$. Let $Y$ be an element of $D$. Then $\operatorname{isPointwiseLeftKanExtensionAtEquivOfIso}$ applied to $e$ and $Y$ is an element of $\EquivMACRoAE {\operatorname{IsPointwiseLeftKanExtensionAt} (E , Y)}{\operatorname{IsPointwiseLeftKanExtensionAt} (\mathrm{E'} , Y)}$ defined as the equivalence isomorphism colimit of the map isomorphism of the cocone at functor of $F$ and $Y$ and $e$.

CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIso'defMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $E$ be a left extension of $L$ and $F$. Let $e$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Then $\operatorname{isPointwiseLeftKanExtensionAtEquivOfIso'}$ applied to $E$ and $e$ is an element of $\EquivMACRoAE {\operatorname{IsPointwiseLeftKanExtensionAt} (E , Y)}{\operatorname{IsPointwiseLeftKanExtensionAt} (E , \mathrm{Y'})}$.

CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtOfIso'defMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $E$ be a left extension of $L$ and $F$. Let $\mathrm{hY}$ be an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $E$ and $Y$. Let $e$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Then $\operatorname{isPointwiseLeftKanExtensionAtOfIso'}$ applied to $E$, $\mathrm{hY}$ and $e$ is an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $E$ and $\mathrm{Y'}$.

CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIsodefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $e$ be an isomorphism of $E$ and $\mathrm{E'}$. Then $\operatorname{isPointwiseLeftKanExtensionEquivOfIso}$ applied to $e$ is an element of $\EquivMACRoAE {\operatorname{IsPointwiseLeftKanExtension} (E)}{\operatorname{IsPointwiseLeftKanExtension} (\mathrm{E'})}$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, type

Wording

no wording

English

Let $E$ be a right extension of $L$ and $F$. Then an element of $\operatorname{IsPointwiseRightKanExtension}$ applied to $E$ is an element of the function that maps $E$ to the set of functions from elements $Y$ of $D$ to elements of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $E$ and $Y$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.homTodefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{IsPointwiseRightKanExtension}$ applied to $E$. Let $G$ be a right extension of $L$ and $F$. Then $\operatorname{homTo}$ applied to $h$ and $G$ is a homomorphism of $G$ and $E$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isUniversaldefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{IsPointwiseRightKanExtension}$ applied to $E$. Then $\operatorname{isUniversal}$ applied to $h$ is an element of $\operatorname{IsUniversal}$ applied to $E$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAtdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, type

Wording

no wording

English

Let $E$ be a right extension of $L$ and $F$. Let $Y$ be an element of $D$. Then an element of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $E$ and $Y$ is an element of the function that maps $E$ and $Y$ to $\operatorname{IsLimit}$ applied to $\operatorname{coneAt}$ applied to $E$ and $Y$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimitdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

the isomorphism limit of h (from the name)

English

Let $h$ be an element of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $E$ and $Y$. Then the isomorphism limit of $h$ is an isomorphism of the action of the left object of $E$ and $Y$ and the limit of the composition of the projection of $Y$ and $L$ and $F$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $h$ and $\operatorname{isLimit}$ applied to the composition of the projection of $Y$ and $L$ and $F$.

CategoryTheory.Functor.RightExtension.coneAtdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $E$ be a right extension of $L$ and $F$. Let $Y$ be an element of $D$. Then $\operatorname{coneAt}$ applied to $E$ and $Y$ is a cone of the composition of the projection of $Y$ and $L$ and $F$.

CategoryTheory.Functor.RightExtension.coneAtFunctordefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

the cone at functor of F and Y (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Let $Y$ be an element of $D$. Then the cone at functor of $F$ and $Y$ is a functor of the set of right extensions of $L$ and $F$ and the set of cones of the composition of the projection of $Y$ and $L$ and $F$.

CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $E$ be a right extension of $L$ and $F$. Then there is an object property of $D$. Proof. Let $E$ be arbitrary. Let $Y$ be arbitrary. By E. By Y. By CategoryTheory__Functor__RightExtension__IsPointwiseRightKanExtensionAt. By Nonempty.

CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtEquivOfIsodefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $e$ be an isomorphism of $E$ and $\mathrm{E'}$. Let $Y$ be an element of $D$. Then $\operatorname{isPointwiseRightKanExtensionAtEquivOfIso}$ applied to $e$ and $Y$ is an element of $\EquivMACRoAE {\operatorname{IsPointwiseRightKanExtensionAt} (E , Y)}{\operatorname{IsPointwiseRightKanExtensionAt} (\mathrm{E'} , Y)}$ defined as the equivalence isomorphism limit of the map isomorphism of the cone at functor of $F$ and $Y$ and $e$.

CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtEquivOfIso'defMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $E$ be a right extension of $L$ and $F$. Let $e$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Then $\operatorname{isPointwiseRightKanExtensionAtEquivOfIso'}$ applied to $E$ and $e$ is an element of $\EquivMACRoAE {\operatorname{IsPointwiseRightKanExtensionAt} (E , Y)}{\operatorname{IsPointwiseRightKanExtensionAt} (E , \mathrm{Y'})}$.

CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtOfIso'defMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $E$ be a right extension of $L$ and $F$. Let $\mathrm{hY}$ be an element of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $E$ and $Y$. Let $e$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Then $\operatorname{isPointwiseRightKanExtensionAtOfIso'}$ applied to $E$, $\mathrm{hY}$ and $e$ is an element of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $E$ and $\mathrm{Y'}$.

CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionEquivOfIsodefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $e$ be an isomorphism of $E$ and $\mathrm{E'}$. Then $\operatorname{isPointwiseRightKanExtensionEquivOfIso}$ applied to $e$ is an element of $\EquivMACRoAE {\operatorname{IsPointwiseRightKanExtension} (E)}{\operatorname{IsPointwiseRightKanExtension} (\mathrm{E'})}$.

CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{3}$. Proof. Let $\mathrm{F'}$ be arbitrary. Let $x_{3}$ be arbitrary. By L. By F. By CategoryTheory__Functor__pointwiseLeftKanExtensionIsUniversal. By F'. By x3. By CategoryTheory__Functor__isUniversalOfIsLeftKanExtension. By CategoryTheory__Limits__IsColimit__coconePointUniqueUpToIso. By L. By F. By CategoryTheory__Functor__pointwiseLeftKanExtensionIsPointwiseLeftKanExtension. By CategoryTheory__Functor__LeftExtension__isPointwiseLeftKanExtensionEquivOfIso__app.

CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{3}$. Proof. Let $\mathrm{F'}$ be arbitrary. Let $x_{3}$ be arbitrary. By L. By F. By CategoryTheory__Functor__pointwiseRightKanExtensionIsUniversal. By F'. By x3. By CategoryTheory__Functor__isUniversalOfIsRightKanExtension. By CategoryTheory__Limits__IsLimit__conePointUniqueUpToIso. By L. By F. By CategoryTheory__Functor__pointwiseRightKanExtensionIsPointwiseRightKanExtension. By CategoryTheory__Functor__RightExtension__isPointwiseRightKanExtensionEquivOfIso__app.

CategoryTheory.Functor.pointwiseLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

the pointwise left Kan extension of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the pointwise left Kan extension of $L$ and $F$ is a functor of $D$ and $H$.

CategoryTheory.Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to the pointwise left Kan extension of $L$ and $F$ and the pointwise left Kan extension unit of $L$ and $F$.

CategoryTheory.Functor.pointwiseLeftKanExtensionIsUniversaldefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{pointwiseLeftKanExtensionIsUniversal}$ applied to $L$ and $F$ is an element of $\operatorname{IsUniversal}$ applied to $\operatorname{mk}$ applied to the pointwise left Kan extension of $L$ and $F$ and the pointwise left Kan extension unit of $L$ and $F$ defined as $\operatorname{isUniversal}$ applied to $\operatorname{pointwiseLeftKanExtensionIsPointwiseLeftKanExtension}$ applied to $L$ and $F$.

CategoryTheory.Functor.pointwiseLeftKanExtensionUnitdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

the pointwise left Kan extension unit of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the pointwise left Kan extension unit of $L$ and $F$ is a homomorphism of $F$ and the composition of $L$ and the pointwise left Kan extension of $L$ and $F$.

CategoryTheory.Functor.pointwiseRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

the pointwise right Kan extension of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the pointwise right Kan extension of $L$ and $F$ is a functor of $D$ and $H$.

CategoryTheory.Functor.pointwiseRightKanExtensionCounitdefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

the pointwise right Kan extension counit of L and F (from the name)

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then the pointwise right Kan extension counit of $L$ and $F$ is a homomorphism of the composition of $L$ and the pointwise right Kan extension of $L$ and $F$ and $F$.

CategoryTheory.Functor.pointwiseRightKanExtensionIsPointwiseRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $\operatorname{mk}$ applied to the pointwise right Kan extension of $L$ and $F$ and the pointwise right Kan extension counit of $L$ and $F$.

CategoryTheory.Functor.pointwiseRightKanExtensionIsUniversaldefMathlib.CategoryTheory.Functor.KanExtension.Pointwise, function or constant

Wording

no wording

English

Let $L$ be a functor of $C$ and $D$. Let $F$ be a functor of $C$ and $H$. Then $\operatorname{pointwiseRightKanExtensionIsUniversal}$ applied to $L$ and $F$ is an element of $\operatorname{IsUniversal}$ applied to $\operatorname{mk}$ applied to the pointwise right Kan extension of $L$ and $F$ and the pointwise right Kan extension counit of $L$ and $F$ defined as $\operatorname{isUniversal}$ applied to $\operatorname{pointwiseRightKanExtensionIsPointwiseRightKanExtension}$ applied to $L$ and $F$.

Mathlib.CategoryTheory.Functor.KanExtension.Preserves

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.postcomposedefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the postcomposition of G and hE (from the name)

English

Let $G$ be a functor of $B$ and $D$. Let $\mathrm{hE}$ be an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $E$. Then the postcomposition of $G$ and $\mathrm{hE}$ is an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to the action of the postcomposition of $F$ and $G$ and $E$ defined as the function that maps $c$ to the postcomposition of $G$ and $\mathrm{hE}$ applied to $c$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.postcomposedefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the postcomposition of G and hE (from the name)

English

Let $G$ be a functor of $B$ and $D$. Let $\mathrm{hE}$ be an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $E$ and $c$. Then the postcomposition of $G$ and $\mathrm{hE}$ is an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to the action of the postcomposition of $F$ and $G$ and $E$ and $c$ defined as $\operatorname{some}$ applied to $\operatorname{preserves}$ applied to $E$ and $\mathrm{hE}$.

CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIsodefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the cocone at a point of the whiskering right by G (from the docstring)

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Let $E$ be a left extension of $L$ and $F$. Let $c$ be an element of $C$. Then the cocone at a point of the whiskering right by $G$ is an isomorphism of $\operatorname{coconeAt}$ applied to the action of the postcomposition of $F$ and $G$ and $E$ and $c$ and the map cocone of $G$ and $\operatorname{coconeAt}$ applied to $E$ and $c$.

CategoryTheory.Functor.PreservesLeftKanExtensionclassMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Then we can say that $\operatorname{PreservesLeftKanExtension}$ holds for $G$, $F$ and $L$.

CategoryTheory.Functor.PreservesLeftKanExtensionsdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $L$ be a functor of $A$ and $C$. Then $\operatorname{PreservesLeftKanExtensions}$ holds for $G$ and $L$, if for all functors $F$ of $A$ and $B$, $\operatorname{PreservesLeftKanExtension}$ holds for $G$, $F$ and $L$.

CategoryTheory.Functor.PreservesPointwiseLeftKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Then $\operatorname{PreservesPointwiseLeftKanExtension}$ holds for $G$, $F$ and $L$, if for all elements $c$ of $C$, $\operatorname{PreservesPointwiseLeftKanExtensionAt}$ holds for $G$, $F$, $L$ and $c$.

CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAtclassMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Let $c$ be an element of $C$. Then we can say that $\operatorname{PreservesPointwiseLeftKanExtensionAt}$ holds for $G$, $F$, $L$ and $c$.

CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionsdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $L$ be a functor of $A$ and $C$. Then $\operatorname{PreservesPointwiseLeftKanExtensions}$ holds for $G$ and $L$, if for all functors $F$ of $A$ and $B$, $\operatorname{PreservesPointwiseLeftKanExtension}$ holds for $G$, $F$ and $L$.

CategoryTheory.Functor.PreservesPointwiseRightKanExtensiondefMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Then $\operatorname{PreservesPointwiseRightKanExtension}$ holds for $G$, $F$ and $L$, if for all elements $c$ of $C$, $\operatorname{PreservesPointwiseRightKanExtensionAt}$ holds for $G$, $F$, $L$ and $c$.

CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAtclassMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Let $c$ be an element of $C$. Then we can say that $\operatorname{PreservesPointwiseRightKanExtensionAt}$ holds for $G$, $F$, $L$ and $c$.

CategoryTheory.Functor.PreservesPointwiseRightKanExtensionsdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $L$ be a functor of $A$ and $C$. Then $\operatorname{PreservesPointwiseRightKanExtensions}$ holds for $G$ and $L$, if for all functors $F$ of $A$ and $B$, $\operatorname{PreservesPointwiseRightKanExtension}$ holds for $G$, $F$ and $L$.

CategoryTheory.Functor.PreservesRightKanExtensionclassMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Then we can say that $\operatorname{PreservesRightKanExtension}$ holds for $G$, $F$ and $L$.

CategoryTheory.Functor.PreservesRightKanExtensionsdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, predicate

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $L$ be a functor of $A$ and $C$. Then $\operatorname{PreservesRightKanExtensions}$ holds for $G$ and $L$, if for all functors $F$ of $A$ and $B$, $\operatorname{PreservesRightKanExtension}$ holds for $G$, $F$ and $L$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.postcomposedefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the postcomposition of G and hE (from the name)

English

Let $G$ be a functor of $B$ and $D$. Let $\mathrm{hE}$ be an element of $\operatorname{IsPointwiseRightKanExtension}$ applied to $E$. Then the postcomposition of $G$ and $\mathrm{hE}$ is an element of $\operatorname{IsPointwiseRightKanExtension}$ applied to the action of the postcomposition of $F$ and $G$ and $E$ defined as the function that maps $c$ to the postcomposition of $G$ and $\mathrm{hE}$ applied to $c$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.postcomposedefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the postcomposition of G and hE (from the name)

English

Let $G$ be a functor of $B$ and $D$. Let $\mathrm{hE}$ be an element of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $E$ and $c$. Then the postcomposition of $G$ and $\mathrm{hE}$ is an element of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to the action of the postcomposition of $F$ and $G$ and $E$ and $c$ defined as $\operatorname{some}$ applied to $\operatorname{preserves}$ applied to $E$ and $\mathrm{hE}$.

CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIsodefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the cone at a point of the whiskering right by G (from the docstring)

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Let $E$ be a right extension of $L$ and $F$. Let $c$ be an element of $C$. Then the cone at a point of the whiskering right by $G$ is an isomorphism of $\operatorname{coneAt}$ applied to the action of the postcomposition of $F$ and $G$ and $E$ and $c$ and the map cone of $G$ and $\operatorname{coneAt}$ applied to $E$ and $c$.

CategoryTheory.Functor.lanCompIsoOfPreservesdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $L$ be a functor of $A$ and $C$. Then $\operatorname{lanCompIsoOfPreserves}$ applied to $G$ and $L$ is an isomorphism of the composition of $\operatorname{lan}$ applied to $L$ and the action of the right whiskering of $B$ and $D$ and $G$ and the composition of the action of the right whiskering of $B$ and $D$ and $G$ and $\operatorname{lan}$ applied to $L$.

CategoryTheory.Functor.leftKanExtensionCompIsoOfPreservesdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the left Kan extension composition isomorphism of F and L (from the name)

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Then the left Kan extension composition isomorphism of $F$ and $L$ is an isomorphism of the composition of the left Kan extension of $L$ and $F$ and $G$ and the left Kan extension of $L$ and the composition of $F$ and $G$ defined as $\operatorname{leftKanExtensionUnique}$ applied to the composition of the left Kan extension of $L$ and $F$ and $G$, the composition of the right whisker of the unit of the chosen left Kan extension of $L$ and $F$ and $G$ and the homomorphism of the associator of the left Kan extension of $L$ and $F$ and $G$, the left Kan extension of $L$ and the composition of $F$ and $G$ and the unit of the chosen left Kan extension of $L$ and the composition of $F$ and $G$.

CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreservesdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the pointwise left Kan extension composition isomorphism of F and L (from the name)

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Then the pointwise left Kan extension composition isomorphism of $F$ and $L$ is an isomorphism of the composition of the pointwise left Kan extension of $L$ and $F$ and $G$ and the pointwise left Kan extension of $L$ and the composition of $F$ and $G$ defined as $\operatorname{leftKanExtensionUnique}$ applied to the composition of the pointwise left Kan extension of $L$ and $F$ and $G$, the composition of the right whisker of the pointwise left Kan extension unit of $L$ and $F$ and $G$ and the homomorphism of the associator of the pointwise left Kan extension of $L$ and $F$ and $G$, the pointwise left Kan extension of $L$ and the composition of $F$ and $G$ and the pointwise left Kan extension unit of $L$ and the composition of $F$ and $G$.

CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreservesdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the pointwise right Kan extension composition isomorphism of F and L (from the name)

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Then the pointwise right Kan extension composition isomorphism of $F$ and $L$ is an isomorphism of the composition of the pointwise right Kan extension of $L$ and $F$ and $G$ and the pointwise right Kan extension of $L$ and the composition of $F$ and $G$ defined as $\operatorname{rightKanExtensionUnique}$ applied to the composition of the pointwise right Kan extension of $L$ and $F$ and $G$, the composition of the inverse of the associator of the pointwise right Kan extension of $L$ and $F$ and $G$ and the right whisker of the pointwise right Kan extension counit of $L$ and $F$ and $G$, the pointwise right Kan extension of $L$ and the composition of $F$ and $G$ and the pointwise right Kan extension counit of $L$ and the composition of $F$ and $G$.

CategoryTheory.Functor.ranCompIsoOfPreservesdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

no wording

English

Let $G$ be a functor of $B$ and $D$. Let $L$ be a functor of $A$ and $C$. Then $\operatorname{ranCompIsoOfPreserves}$ applied to $G$ and $L$ is an isomorphism of the composition of $\operatorname{ran}$ applied to $L$ and the action of the right whiskering of $B$ and $D$ and $G$ and the composition of the action of the right whiskering of $B$ and $D$ and $G$ and $\operatorname{ran}$ applied to $L$.

CategoryTheory.Functor.rightKanExtensionCompIsoOfPreservesdefMathlib.CategoryTheory.Functor.KanExtension.Preserves, function or constant

Wording

the right Kan extension composition isomorphism of F and L (from the name)

English

Let $G$ be a functor of $B$ and $D$. Let $F$ be a functor of $A$ and $B$. Let $L$ be a functor of $A$ and $C$. Then the right Kan extension composition isomorphism of $F$ and $L$ is an isomorphism of the composition of the right Kan extension of $L$ and $F$ and $G$ and the right Kan extension of $L$ and the composition of $F$ and $G$ defined as $\operatorname{rightKanExtensionUnique}$ applied to the composition of the right Kan extension of $L$ and $F$ and $G$, the composition of the inverse of the associator of the right Kan extension of $L$ and $F$ and $G$ and the right whisker of the counit of the chosen right Kan extension of $L$ and $F$ and $G$, the right Kan extension of $L$ and the composition of $F$ and $G$ and the counit of the chosen right Kan extension of $L$ and the composition of $F$ and $G$.

Mathlib.CategoryTheory.Functor.OfSequence

CategoryTheory.Functor.OfSequence.mapdefMathlib.CategoryTheory.Functor.OfSequence, function or constant

Wording

the map of n and i (from the name)

English

Let $x_{1}$ be a function from natural numbers $n$ to homomorphisms of $X$ applied to $n$ and $X$ applied to $n + 1$. Let $i$ and $j$ be natural numbers such that $i \leq j$. Then the map of $x_{1}$ and $i$ is a homomorphism of $X$ applied to $i$ and $X$ applied to $j$ defined as the function that maps $h$ to $\operatorname{brecOn}$ applied to $i$, $\mathrm{CategoryTheory\_\_Functor\_\_OfSequence\_\_map\_\_\_f}$, $X$, $n$, $x_{1}$, $j$ and $h$.

CategoryTheory.Functor.ofOpSequencedefMathlib.CategoryTheory.Functor.OfSequence, function or constant

Wording

the functor of f (from the docstring)

English

Let $f$ be a function from natural numbers $n$ to homomorphisms of $X$ applied to $n + 1$ and $X$ applied to $n$. Then the functor of $n$ is a functor of the set of opposites of $\Natural$ and $C$ defined as the function that maps $f$ to the left opposite of the functor of the function that maps $n$ to the opposite in $n$ applied to $n$.

CategoryTheory.Functor.ofSequencedefMathlib.CategoryTheory.Functor.OfSequence, function or constant

Wording

the functor of f (from the docstring)

English

Let $f$ be a function from natural numbers $n$ to homomorphisms of $X$ applied to $n$ and $X$ applied to $n + 1$. Then the functor of $n$ is a functor of $\Natural$ and $C$.

CategoryTheory.NatTrans.ofOpSequencedefMathlib.CategoryTheory.Functor.OfSequence, function or constant

Wording

the natural transformation of app and n1 (from the name)

English

Let $\mathrm{app}$ be a function from natural numbers $n_{1}$ to homomorphisms of the action of $F$ and $\operatorname{op}$ applied to $n_{1}$ and the action of $G$ and $\operatorname{op}$ applied to $n_{1}$ such that for all natural numbers $n$, the composition of the map of $F$ and the opposite in the homomorphism of $\mathrm{Nat\_\_le\_add\_right}$ applied to $n$ and $1$ and $\mathrm{app}$ applied to $n$ is equal to the composition of $\mathrm{app}$ applied to $n + 1$ and the map of $G$ and the opposite in the homomorphism of $\mathrm{Nat\_\_le\_add\_right}$ applied to $n$ and $1$. Then the natural transformation of $n_{1}$ and $\mathrm{app}$ is a homomorphism of $F$ and $G$.

CategoryTheory.NatTrans.ofSequencedefMathlib.CategoryTheory.Functor.OfSequence, function or constant

Wording

the natural transformation of app and n1 (from the name)

English

Let $\mathrm{app}$ be a function from natural numbers $n_{1}$ to homomorphisms of the action of $F$ and $n_{1}$ and the action of $G$ and $n_{1}$ such that for all natural numbers $n$, the composition of the map of $F$ and the homomorphism of $\mathrm{Nat\_\_le\_add\_right}$ applied to $n$ and $1$ and $\mathrm{app}$ applied to $n + 1$ is equal to the composition of $\mathrm{app}$ applied to $n$ and the map of $G$ and the homomorphism of $\mathrm{Nat\_\_le\_add\_right}$ applied to $n$ and $1$. Then the natural transformation of $n_{1}$ and $\mathrm{app}$ is a homomorphism of $F$ and $G$.

Mathlib.CategoryTheory.Functor.Quadrifunctor

CategoryTheory.trifunctorComp₂₃₄defMathlib.CategoryTheory.Functor.Quadrifunctor, function or constant

Wording

the trifunctor composition of F and G (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{4}$ and $E$. Let $G$ be a functor of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $x_{4}$. Then the trifunctor composition of $F$ and $G$ is a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$.

CategoryTheory.trifunctorComp₂₃₄FunctordefMathlib.CategoryTheory.Functor.Quadrifunctor, function or constant

Wording

the functor (from the docstring)

English

The functor is a functor of the set of functors of $x$ and the set of functors of $x_{4}$ and $E$ and the set of functors of the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $x_{4}$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$.

CategoryTheory.trifunctorComp₃₄defMathlib.CategoryTheory.Functor.Quadrifunctor, function or constant

Wording

the trifunctor composition of F and G (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{4}$ and $E$. Let $G$ be a functor of $x_{2}$ and the set of functors of $x_{3}$ and $x_{4}$. Then the trifunctor composition of $F$ and $G$ is a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$.

CategoryTheory.trifunctorComp₃₄FunctordefMathlib.CategoryTheory.Functor.Quadrifunctor, function or constant

Wording

the functor (from the docstring)

English

The functor is a functor of the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{4}$ and $E$ and the set of functors of the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $x_{4}$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$.

Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

CategoryTheory.Functor.ReflectsIsomorphismsclassMathlib.CategoryTheory.Functor.ReflectsIso.Basic, predicate

Wording

F reflects isomorphisms (from the name)

English

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

Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

CategoryTheory.JointlyFaithfulstructureMathlib.CategoryTheory.Functor.ReflectsIso.Jointly, predicate

Wording

F is jointly faithful (from the docstring)

English

generation took over the time limit

CategoryTheory.JointlyReflectEpimorphismsstructureMathlib.CategoryTheory.Functor.ReflectsIso.Jointly, predicate

Wording

no wording

English

Let $F$ be a function from elements $i$ of $I$ to functors of $C$ and $D$ applied to $i$. Then we can say that $\operatorname{JointlyReflectEpimorphisms}$ holds for $i$ and $F$.

CategoryTheory.JointlyReflectIsomorphismsstructureMathlib.CategoryTheory.Functor.ReflectsIso.Jointly, predicate

Wording

no wording

English

Let $F$ be a function from elements $i$ of $I$ to functors of $C$ and $D$ applied to $i$. Then we can say that $\operatorname{JointlyReflectIsomorphisms}$ holds for $i$ and $F$.

CategoryTheory.JointlyReflectMonomorphismsstructureMathlib.CategoryTheory.Functor.ReflectsIso.Jointly, predicate

Wording

no wording

English

Let $F$ be a function from elements $i$ of $I$ to functors of $C$ and $D$ applied to $i$. Then we can say that $\operatorname{JointlyReflectMonomorphisms}$ holds for $i$ and $F$.

Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectsColimitdefMathlib.CategoryTheory.Functor.ReflectsIso.Limits, function or constant

Wording

no wording

English

Assume that $\operatorname{JointlyReflectIsomorphisms}$ holds for $F$. Let $\mathrm{hc}$ be a function from elements $i$ of $I$ to elements of $\operatorname{IsColimit}$ applied to the map cocone of $F$ applied to $i$ and $c$. Then $\operatorname{jointlyReflectsColimit}$ applied to $\mathrm{hF}$, $i$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$.

CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectsLimitdefMathlib.CategoryTheory.Functor.ReflectsIso.Limits, function or constant

Wording

no wording

English

Assume that $\operatorname{JointlyReflectIsomorphisms}$ holds for $F$. Let $\mathrm{hc}$ be a function from elements $i$ of $I$ to elements of $\operatorname{IsLimit}$ applied to the map cone of $F$ applied to $i$ and $c$. Then $\operatorname{jointlyReflectsLimit}$ applied to $\mathrm{hF}$, $i$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

Mathlib.CategoryTheory.Functor.Trifunctor

CategoryTheory.bifunctorComp₁₂defMathlib.CategoryTheory.Functor.Trifunctor, function or constant

Wording

the bifunctor composition of x10 and G (from the name)

English

Let $x_{10}$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{4}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{2}$ and $x_{3}$. Then the bifunctor composition of $x_{10}$ and $G$ is a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $x_{3}$.

CategoryTheory.bifunctorComp₁₂FunctordefMathlib.CategoryTheory.Functor.Trifunctor, function or constant

Wording

the functor (from the docstring)

English

The functor is a functor of the set of functors of $x$ and the set of functors of $x_{1}$ and $x_{4}$ and the set of functors of the set of functors of $x_{4}$ and the set of functors of $x_{2}$ and $x_{3}$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $x_{3}$.

CategoryTheory.bifunctorComp₂₃defMathlib.CategoryTheory.Functor.Trifunctor, function or constant

Wording

the bifunctor composition of F and x10 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{4}$ and $x_{3}$. Let $x_{10}$ be a functor of $x_{1}$ and the set of functors of $x_{2}$ and $x_{4}$. Then the bifunctor composition of $F$ and $x_{10}$ is a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $x_{3}$.

CategoryTheory.bifunctorComp₂₃FunctordefMathlib.CategoryTheory.Functor.Trifunctor, function or constant

Wording

the functor (from the docstring)

English

The functor is a functor of the set of functors of $x$ and the set of functors of $x_{4}$ and $x_{3}$ and the set of functors of the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $x_{4}$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $x_{3}$.

Mathlib.CategoryTheory.Functor.TwoSquare

CategoryTheory.TwoSquaredefMathlib.CategoryTheory.Functor.TwoSquare, type

Wording

no wording

English

Let $T$ be a functor of $x$ and $x_{1}$. Let $L$ be a functor of $x$ and $x_{2}$. Let $R$ be a functor of $x_{1}$ and $x_{3}$. Let $B$ be a functor of $x_{2}$ and $x_{3}$. Then an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$ is an element of the function that maps $T$, $L$, $R$ and $B$ to the set of homomorphisms of the composition of $T$ and $R$ and the composition of $L$ and $B$.

CategoryTheory.TwoSquare.hCompdefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

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

English

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $\mathrm{w'}$ be an element of $\operatorname{TwoSquare}$ applied to $\mathrm{T'}$, $R$, $\mathrm{R'}$ and $\mathrm{B'}$. Then the composition of $w$ and $\mathrm{w'}$ is an element of $\operatorname{TwoSquare}$ applied to the composition of $T$ and $\mathrm{T'}$, $L$, $\mathrm{R'}$ and the composition of $B$ and $\mathrm{B'}$ defined as the composition of the homomorphism of the associator of $\mathrm{T'}$ and $\mathrm{R'}$ and the composition of the left whisker of $T$ and $\mathrm{w'}$ and the composition of the inverse of the associator of $R$ and $\mathrm{B'}$ and the composition of the right whisker of $w$ and $\mathrm{B'}$ and the homomorphism of the associator of $B$ and $\mathrm{B'}$.

CategoryTheory.TwoSquare.hIddefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

the identity of L (from the name)

English

Let $L$ be a functor of $x$ and $x_{1}$. Then the identity of $L$ is an element of $\operatorname{TwoSquare}$ applied to the identity of $x$, $L$, $L$ and the identity of $x_{1}$ defined as the composition of the homomorphism of the left unitor of $L$ and the inverse of the right unitor of $L$.

CategoryTheory.TwoSquare.mkdefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

no wording

English

Let $T$ be a functor of $x$ and $x_{1}$. Let $L$ be a functor of $x$ and $x_{2}$. Let $R$ be a functor of $x_{1}$ and $x_{3}$. Let $B$ be a functor of $x_{2}$ and $x_{3}$. Let $x_{8}$ be a homomorphism of the composition of $T$ and $R$ and the composition of $L$ and $B$. Then $\operatorname{mk}$ applied to $T$, $L$, $R$, $B$ and $x_{8}$ is an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$ defined as $x_{8}$.

CategoryTheory.TwoSquare.opdefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

the opposite of x8 (from the docstring)

English

Let $x_{8}$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then the opposite of $x_{8}$ is an element of $\operatorname{TwoSquare}$ applied to the opposite of $L$, the opposite of $T$, the opposite of $B$ and the opposite of $R$ defined as the opposite of $x_{8}$.

CategoryTheory.TwoSquare.proddefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

the external product of two of w and #2 (from the docstring)

English

CategoryTheory.TwoSquare.vCompdefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

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

English

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $\mathrm{w'}$ be an element of $\operatorname{TwoSquare}$ applied to $B$, $\mathrm{L'}$, $\mathrm{R''}$ and $\mathrm{B''}$. Then the composition of $w$ and $\mathrm{w'}$ is an element of $\operatorname{TwoSquare}$ applied to $T$, the composition of $L$ and $\mathrm{L'}$, the composition of $R$ and $\mathrm{R''}$ and $\mathrm{B''}$ defined as the composition of the inverse of the associator of $R$ and $\mathrm{R''}$ and the composition of the right whisker of $w$ and $\mathrm{R''}$ and the composition of the homomorphism of the associator of $B$ and $\mathrm{R''}$ and the composition of the left whisker of $L$ and $\mathrm{w'}$ and the inverse of the associator of $\mathrm{L'}$ and $\mathrm{B''}$.

CategoryTheory.TwoSquare.vIddefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

the identity of T (from the name)

English

Let $T$ be a functor of $x$ and $x_{1}$. Then the identity of $T$ is an element of $\operatorname{TwoSquare}$ applied to $T$, the identity of $x$, the identity of $x_{1}$ and $T$ defined as the composition of the homomorphism of the right unitor of $T$ and the inverse of the left unitor of $T$.

CategoryTheory.TwoSquare.whiskerBottomdefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

the whisker bottom of w and x8 (from the name)

English

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $x_{8}$ be a homomorphism of $B$ and $\mathrm{B'}$. Then the whisker bottom of $w$ and $x_{8}$ is an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $\mathrm{B'}$ defined as the composition of $w$ and the left whisker of $L$ and $x_{8}$.

CategoryTheory.TwoSquare.whiskerLeftdefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

the left whisker of w and x8 (from the name)

English

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $x_{8}$ be a homomorphism of $L$ and $\mathrm{L'}$. Then the left whisker of $w$ and $x_{8}$ is an element of $\operatorname{TwoSquare}$ applied to $T$, $\mathrm{L'}$, $R$ and $B$ defined as the composition of $w$ and the right whisker of $x_{8}$ and $B$.

CategoryTheory.TwoSquare.whiskerRightdefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

the right whisker of w and x8 (from the name)

English

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $\mathrm{R'}$ and $B$. Let $x_{8}$ be a homomorphism of $R$ and $\mathrm{R'}$. Then the right whisker of $w$ and $x_{8}$ is an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$ defined as the composition of the left whisker of $T$ and $x_{8}$ and $w$.

CategoryTheory.TwoSquare.whiskerTopdefMathlib.CategoryTheory.Functor.TwoSquare, function or constant

Wording

the whisker top of w and x8 (from the name)

English

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $\mathrm{T'}$, $L$, $R$ and $B$. Let $x_{8}$ be a homomorphism of $T$ and $\mathrm{T'}$. Then the whisker top of $w$ and $x_{8}$ is an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$ defined as the composition of the right whisker of $x_{8}$ and $R$ and $w$.

Mathlib.CategoryTheory.Functor.TypeValuedFlat

CategoryTheory.FunctorToTypes.fromOverFunctordefMathlib.CategoryTheory.Functor.TypeValuedFlat, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of sets. Let $x_{1}$ be an element of the action of $F$ and $X$. Then $\operatorname{fromOverFunctor}$ applied to $F$ and $x_{1}$ is a functor of $\operatorname{Over}$ applied to $X$ and the set of sets defined as the subfunctor as a functor of $\operatorname{fromOverSubfunctor}$ applied to $F$ and $x_{1}$.

CategoryTheory.FunctorToTypes.fromOverFunctorElementsEquivalencedefMathlib.CategoryTheory.Functor.TypeValuedFlat, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of sets. Let $x_{1}$ be an element of the action of $F$ and $X$. Then $\operatorname{fromOverFunctorElementsEquivalence}$ applied to $F$ and $x_{1}$ is an equivalence of the set of elements of $\operatorname{fromOverFunctor}$ applied to $F$ and $x_{1}$ and $\operatorname{Over}$ applied to the element of $X$ and $x_{1}$.

CategoryTheory.FunctorToTypes.fromOverSubfunctordefMathlib.CategoryTheory.Functor.TypeValuedFlat, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of sets. Let $x_{1}$ be an element of the action of $F$ and $X$. Then $\operatorname{fromOverSubfunctor}$ applied to $F$ and $x_{1}$ is a subfunctor of the composition of $\operatorname{forget}$ applied to $X$ and $F$.

Mathlib.CategoryTheory.Galois.Action

CategoryTheory.PreGaloisCategory.functorToActiondefMathlib.CategoryTheory.Galois.Action, function or constant

Wording

the functor to action of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the functor to action of $F$ is a functor of $C$ and the set of actions of the set of finite type categories and the set of automorphisms of $F$.

Mathlib.CategoryTheory.Galois.Basic

CategoryTheory.GaloisCategoryclassMathlib.CategoryTheory.Galois.Basic, predicate

Wording

C is a Galois category (from the name)

English

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

CategoryTheory.GaloisCategory.getFiberFunctordefMathlib.CategoryTheory.Galois.Basic, function or constant

Wording

no wording

English

Let $C$ be a set. Then $\operatorname{getFiberFunctor}$ applied to $C$ is a functor of $C$ and the set of finite type categories defined as $\operatorname{choose}$ applied to $\operatorname{hasFiberFunctor}$ applied to $C$.

CategoryTheory.PreGaloisCategoryclassMathlib.CategoryTheory.Galois.Basic, predicate

Wording

C is a Galois category (from the name)

English

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

CategoryTheory.PreGaloisCategory.FiberFunctorclassMathlib.CategoryTheory.Galois.Basic, predicate

Wording

F is a fiber functor (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then we can say that $F$ is a fiber functor.

CategoryTheory.PreGaloisCategory.IsConnectedclassMathlib.CategoryTheory.Galois.Basic, predicate

Wording

X is connected (from the name)

English

Let $X$ be an element of $C$. Then we can say that $X$ is connected.

CategoryTheory.PreGaloisCategory.PreservesIsConnectedclassMathlib.CategoryTheory.Galois.Basic, predicate

Wording

no wording

English

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

CategoryTheory.PreGaloisCategory.fiberBinaryProductEquivdefMathlib.CategoryTheory.Galois.Basic, function or constant

Wording

the fiber binary product equivalence of X and Y (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $X$ and $Y$ be elements of $C$. Then the fiber binary product equivalence of $X$ and $Y$ is an equivalence from the object of the action of $F$ and the product of $X$ and $Y$ to $\mathrm{Prod}$ applied to the object of the action of $F$ and $X$ and the object of the action of $F$ and $Y$ defined as the equivalence of the composition of the isomorphism of $X$ and $Y$ and the binary product isomorphism of the object of the action of $F$ and $X$ and the object of the action of $F$ and $Y$.

CategoryTheory.PreGaloisCategory.fiberEqualizerEquivdefMathlib.CategoryTheory.Galois.Basic, function or constant

Wording

the fiber of the equalizer of F (from the docstring)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the fiber of the equalizer of $F$ is an element of $\EquivMACRoAE {\operatorname{obj} (\operatorname{obj} (F , \operatorname{equalizer} (f , g)))}{(\SubtypeSet {x_{1}}{(\EqtMACRoH {\operatorname{hom} (\operatorname{map} (F , f), x_{1})}{\operatorname{hom} (\operatorname{map} (F , g), x_{1})})})}$ defined as the equivalence of the composition of the isomorphism of $f$ and $g$ and the equalizer isomorphism of the homomorphism of the map of $F$ and $f$ and the homomorphism of the map of $F$ and $g$.

CategoryTheory.PreGaloisCategory.fiberPullbackEquivdefMathlib.CategoryTheory.Galois.Basic, function or constant

Wording

the fiber pullback equivalence of f and g (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $f$ be a homomorphism of $A$ and $X$. Let $g$ be a homomorphism of $B$ and $X$. Then the fiber pullback equivalence of $f$ and $g$ is an element of $\EquivMACRoAE {\operatorname{obj} (\operatorname{obj} (F , \operatorname{pullback} (f , g)))}{(\SubtypeSet {p}{(\EqtMACRoH {\operatorname{hom} (\operatorname{map} (F , f), \ProdfstMACRoZ {p})}{\operatorname{hom} (\operatorname{map} (F , g), \ProdsndMACRoAA {p})})})}$ defined as the equivalence of the composition of the isomorphism of $f$ and $g$ and the pullback isomorphism pullback of the homomorphism of the map of $F$ and $f$ and the homomorphism of the map of $F$ and $g$.

Mathlib.CategoryTheory.Galois.ContAction

Action.trivialOnSetdefMathlib.CategoryTheory.Galois.ContAction, function or constant

Wording

no wording

English

Let $V$ be a set. Let $S$ be an element of $\wp G$. Then there is an object property of the set of actions of $V$ and $G$. Proof. Let $V$ be arbitrary. Let $S$ be arbitrary. Let $X$ be arbitrary. By G. Let $s$ be arbitrary. By S. By s. By Membership__mem. By X. By s. By Action___u3c1___app. By 1. By Eqt. By if. By forall.

Mathlib.CategoryTheory.Galois.Equivalence

CategoryTheory.PreGaloisCategory.functorToContActiondefMathlib.CategoryTheory.Galois.Equivalence, function or constant

Wording

the functor to continuous action of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the functor to continuous action of $F$ is a functor of $C$ and the set of continuous actions of the set of finite type categories and the set of automorphisms of $F$ defined as the lift of $\operatorname{isContinuous}$ applied to the set of finite type categories and the set of automorphisms of $F$ and the functor to action of $F$.

Mathlib.CategoryTheory.Galois.EssSurj

CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizerdefMathlib.CategoryTheory.Galois.EssSurj, function or constant

Wording

the fiber isomorphism quotient stabilizer of X and x1 (from the name)

English

Let $X$ be an element of $C$. Let $x_{1}$ be an element of the object of the action of $F$ and $X$. Then the fiber isomorphism quotient stabilizer of $X$ and $x_{1}$ is an isomorphism of the action of the functor to action of $F$ and $X$ and the finite type category of the set of automorphisms of $F$ and $\operatorname{of}$ applied to the set of quotients of the set of automorphisms of $F$ and the stabilizer of the set of automorphisms of $F$ and $x_{1}$ defined as the isomorphism quotient stabilizer of the action of the functor to action of $F$ and $X$ and $x_{1}$.

Mathlib.CategoryTheory.Galois.Examples

CategoryTheory.FintypeCat.Action.imageComplementdefMathlib.CategoryTheory.Galois.Examples, function or constant

Wording

the image complement of G and f (from the name)

English

Let $G$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the image complement of $G$ and $f$ is an action of the set of finite type categories and $G$.

CategoryTheory.FintypeCat.Action.imageComplementIncldefMathlib.CategoryTheory.Galois.Examples, function or constant

Wording

the image complement inclusion of G and f (from the name)

English

Let $G$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the image complement inclusion of $G$ and $f$ is a homomorphism of the image complement of $G$ and $f$ and $Y$.

CategoryTheory.FintypeCat.imageComplementdefMathlib.CategoryTheory.Galois.Examples, function or constant

Wording

the image complement of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the image complement of $f$ is a finite type category defined as $\operatorname{of}$ applied to the set of elements of the complement of the range of $\operatorname{coe}$ applied to the homomorphism of $f$.

CategoryTheory.FintypeCat.imageComplementIncldefMathlib.CategoryTheory.Galois.Examples, function or constant

Wording

the inclusion from the complement of the image of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the inclusion from the complement of the image of $f$ is a homomorphism of the image complement of $f$ and $Y$ defined as the homomorphism of the function that maps $x$ to the proposition that $x$ is an element of the complement of the range of $\operatorname{coe}$ applied to the homomorphism of $f$.

CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnecteddefMathlib.CategoryTheory.Galois.Examples, function or constant

Wording

the isomorphism quotient stabilizer of X and x1 (from the name)

English

Let $X$ be an action of the set of finite type categories and $G$. Let $x_{1}$ be an element of the object of $\operatorname{V}$ applied to $X$. Then the isomorphism quotient stabilizer of $X$ and $x_{1}$ is an isomorphism of $X$ and the finite type category of $G$ and $\operatorname{of}$ applied to the set of quotients of $G$ and the stabilizer of $G$ and $x_{1}$.

Mathlib.CategoryTheory.Galois.FullSubcategory

CategoryTheory.ObjectProperty.IsGaloisSubcategoryclassMathlib.CategoryTheory.Galois.FullSubcategory, predicate

Wording

P is a Galois subcategory (from the name)

English

Let $P$ be an object property of $C$. Then we can say that $P$ is a Galois subcategory.

Mathlib.CategoryTheory.Galois.GaloisObjects

CategoryTheory.PreGaloisCategory.IsGaloisclassMathlib.CategoryTheory.Galois.GaloisObjects, predicate

Wording

no wording

English

Let $X$ be an element of $C$. Then we can say that $\operatorname{IsGalois}$ holds for $X$.

CategoryTheory.PreGaloisCategory.autMapdefMathlib.CategoryTheory.Galois.GaloisObjects, function or constant

Wording

the automorphism map of f and x1 (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Let $x_{1}$ be an automorphism of $A$. Then the automorphism map of $f$ and $x_{1}$ is an automorphism of $B$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_PreGaloisCategory\_\_exists\_autMap}$ applied to $f$ and $x_{1}$.

CategoryTheory.PreGaloisCategory.autMapHomdefMathlib.CategoryTheory.Galois.GaloisObjects, function or constant

Wording

the automorphism map homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Then the automorphism map homomorphism of $f$ is a monoid homomorphism of the set of automorphisms of $A$ and the set of automorphisms of $B$ defined as $\operatorname{mk'}$ applied to $\operatorname{autMap}$ applied to $f$ and $\mathrm{CategoryTheory\_\_PreGaloisCategory\_\_autMap\_apply\_mul}$ applied to $f$.

CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGaloisdefMathlib.CategoryTheory.Galois.GaloisObjects, function or constant

Wording

the evaluation equivalence of A and a (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $A$ be an element of $C$. Let $a$ be an element of the object of the action of $F$ and $A$. Then the evaluation equivalence of $A$ and $a$ is an equivalence from the set of automorphisms of $A$ to the object of the action of $F$ and $A$ defined as the equivalence of the function that maps $f$ to $\operatorname{hom}$ applied to the map of $F$ and the homomorphism of the underlying isomorphism of $f$ and $a$ and $\mathrm{CategoryTheory\_\_PreGaloisCategory\_\_evaluation\_aut\_bijective\_of\_isGalois}$ applied to $F$, $A$ and $a$.

CategoryTheory.PreGaloisCategory.isTerminalQuotientOfIsGaloisdefMathlib.CategoryTheory.Galois.GaloisObjects, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{isTerminalQuotientOfIsGalois}$ applied to $X$ is an element of $\operatorname{IsTerminal}$ applied to the colimit of the functor of the end defined as $\operatorname{some}$ applied to $\operatorname{quotientByAutTerminal}$.

CategoryTheory.PreGaloisCategory.quotientByAutTerminalEquivUniqueQuotientdefMathlib.CategoryTheory.Galois.GaloisObjects, function or constant

Wording

the quotient by automorphism terminal equivalence unique quotient of F and X (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $X$ be an element of $C$. Then the quotient by automorphism terminal equivalence unique quotient of $F$ and $X$ is an equivalence from $\operatorname{IsTerminal}$ applied to the colimit of the functor of the end to the proposition that the set of quotients of the set of automorphisms of $X$ and the object of the action of $F$ and $X$ is unique defined as the composition of the composition of $\operatorname{isTerminalIffObj}$ applied to the composition of $F$ and the inclusion and the colimit of the functor of the end and $\operatorname{isLimitEmptyConeEquiv}$ applied to the set of sets, $\operatorname{asEmptyCone}$ applied to the action of the composition of $F$ and the inclusion and the colimit of the functor of the end, $\operatorname{asEmptyCone}$ applied to $\mathrm{Quot}$ applied to $\operatorname{r}$ and the composition of $\operatorname{preservesColimitIso}$ applied to the composition of $F$ and the inclusion and the functor of the end and the isomorphism of the colimit of the composition of the functor of the end and the composition of $F$ and the inclusion and $\operatorname{isTerminalEquivUnique}$ applied to $\mathrm{Quot}$ applied to $\operatorname{r}$.

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

CategoryTheory.PreGaloisCategory.IsFundamentalGroupclassMathlib.CategoryTheory.Galois.IsFundamentalgroup, predicate

Wording

F is a fundamental group (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $G$ be a set. Then we can say that $F$ is a fundamental group.

CategoryTheory.PreGaloisCategory.IsNaturalSMulclassMathlib.CategoryTheory.Galois.IsFundamentalgroup, predicate

Wording

F is a natural product (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $G$ be a set. Then we can say that $F$ is a natural product.

CategoryTheory.PreGaloisCategory.toAutdefMathlib.CategoryTheory.Galois.IsFundamentalgroup, function or constant

Wording

the automorphism of F and G (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $G$ be a set. Then the automorphism of $F$ and $G$ is a monoid homomorphism of $G$ and the set of automorphisms of $F$.

CategoryTheory.PreGaloisCategory.toAutHomeodefMathlib.CategoryTheory.Galois.IsFundamentalgroup, function or constant

Wording

the automorphism homeomorphism of F and G (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $G$ be a set. Then the automorphism homeomorphism of $F$ and $G$ is a homeomorphism of $G$ and the set of automorphisms of $F$ defined as the homeomorphism of $\operatorname{coe}$ applied to the automorphism of $F$ and $G$ and $\mathrm{CategoryTheory\_\_PreGaloisCategory\_\_toAut\_isHomeomorph}$ applied to $F$ and $G$.

CategoryTheory.PreGaloisCategory.toAutMulEquivdefMathlib.CategoryTheory.Galois.IsFundamentalgroup, function or constant

Wording

the automorphism multiplicative equivalence of F and G (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $G$ be a set. Then the automorphism multiplicative equivalence of $F$ and $G$ is a multiplicative equivalence of $G$ and the set of automorphisms of $F$ defined as the multiplicative equivalence of the automorphism of $F$ and $G$ and $\mathrm{CategoryTheory\_\_PreGaloisCategory\_\_toAut\_bijective}$ applied to $F$ and $G$.

Mathlib.CategoryTheory.Galois.Prorepresentability

CategoryTheory.PreGaloisCategory.AutGaloisdefMathlib.CategoryTheory.Galois.Prorepresentability, type

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then an element of $\operatorname{AutGalois}$ applied to $F$ is an element of the function that maps $F$ to the set of elements of the section of the composition of the automorphism Galois system of $F$ and the forgetful functor of the set of group categories.

CategoryTheory.PreGaloisCategory.AutGalois.πdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the projection of F and A (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $A$ be a pointed Galois object of $F$. Then the projection of $F$ and $A$ is a monoid homomorphism of $\operatorname{AutGalois}$ applied to $F$ and the set of automorphisms of the underlying object of $A$ defined as the section projection monoid homomorphism of the automorphism Galois system of $F$ and $A$.

CategoryTheory.PreGaloisCategory.PointedGaloisObjectstructureMathlib.CategoryTheory.Galois.Prorepresentability, type

Wording

pointed Galois object of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the pointed Galois objects of $F$ are a basic type.

CategoryTheory.PreGaloisCategory.PointedGaloisObject.HomstructureMathlib.CategoryTheory.Galois.Prorepresentability, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be pointed Galois objects of $F$. Then the homomorphisms of $A$ and $B$ are a basic type.

CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.valdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the value of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the value of $\mathrm{self}$ is a homomorphism of the underlying object of $A$ and the underlying object of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.PreGaloisCategory.PointedGaloisObject.coconedefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the cocone of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the cocone of $F$ is a cocone of the composition of the opposite of the inclusion of $F$ and the Coyoneda.

CategoryTheory.PreGaloisCategory.PointedGaloisObject.incldefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the inclusion of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the inclusion of $F$ is a functor of the set of pointed Galois objects of $F$ and $C$.

CategoryTheory.PreGaloisCategory.PointedGaloisObject.isColimitdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the colimit cocone of F (from the docstring)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the colimit cocone of $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $F$.

CategoryTheory.PreGaloisCategory.PointedGaloisObject.objdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the underlying object of self (from the docstring)

English

Let $\mathrm{self}$ be a pointed Galois object of $F$. Then the underlying object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.PreGaloisCategory.PointedGaloisObject.ptdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a pointed Galois object of $F$. Then $\operatorname{pt}$ applied to $\mathrm{self}$ is an element of the object of the action of $F$ and the underlying object of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.PreGaloisCategory.autGaloisSystemdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the automorphism Galois system of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the automorphism Galois system of $F$ is a functor of the set of pointed Galois objects of $F$ and the set of group categories.

CategoryTheory.PreGaloisCategory.autIsoFibersdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the automorphism isomorphism fiber of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the automorphism isomorphism fiber of $F$ is an isomorphism of the composition of the automorphism Galois system of $F$ and the forgetful functor of the set of group categories and the composition of the inclusion of $F$ and the composition of $F$ and the inclusion.

CategoryTheory.PreGaloisCategory.autMulEquivAutGaloisdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the automorphism group of F (from the docstring)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the automorphism group of $F$ is a multiplicative equivalence of the set of automorphisms of $F$ and the set of multiplicative opposites of $\operatorname{AutGalois}$ applied to $F$.

CategoryTheory.PreGaloisCategory.endEquivAutGaloisdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then $\operatorname{endEquivAutGalois}$ applied to $F$ is an equivalence from the set of ends of $F$ to $\operatorname{AutGalois}$ applied to $F$ defined as the composition of the end equivalence section fiber of $F$ and the equivalence of the map isomorphism of the section functor of the set of pointed Galois objects of $F$ and the inverse of the automorphism isomorphism fiber of $F$.

CategoryTheory.PreGaloisCategory.endEquivSectionsFibersdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

the end equivalence section fiber of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the end equivalence section fiber of $F$ is an equivalence from the set of ends of $F$ to the set of elements of the section of the composition of the inclusion of $F$ and the composition of $F$ and the inclusion defined as the composition of $\operatorname{toEquiv}$ applied to the multiplicative equivalence end of the right whiskering of $\operatorname{ofFullyFaithful}$ applied to the inclusion and $C$ and $F$ and the composition of the equivalence of the composition of the isomorphism of the homomorphism equivalence and the map isomorphism of the action of the Yoneda and the composition of $F$ and the inclusion and the opposite isomorphism of the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cocone of $F$ and the colimit cocone of $F$ and the composition of the equivalence of the colimit Coyoneda homomorphism isomorphism limit of the inclusion of $F$ and the composition of $F$ and the inclusion and the composition of the limit equivalence section of the composition of the inclusion of $F$ and the composition of the composition of $F$ and the inclusion and the functor embedding and the inverse of the section equivalence of the composition of the inclusion of $F$ and the composition of $F$ and the inclusion.

CategoryTheory.PreGaloisCategory.endMulEquivAutGaloisdefMathlib.CategoryTheory.Galois.Prorepresentability, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then $\operatorname{endMulEquivAutGalois}$ applied to $F$ is a multiplicative equivalence of the set of ends of $F$ and the set of multiplicative opposites of $\operatorname{AutGalois}$ applied to $F$.

Mathlib.CategoryTheory.Galois.Topology

CategoryTheory.PreGaloisCategory.autEmbeddingdefMathlib.CategoryTheory.Galois.Topology, function or constant

Wording

the automorphism embedding of F (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Then the automorphism embedding of $F$ is a monoid homomorphism of the set of automorphisms of $F$ and the set of functions from elements $X$ of $C$ to automorphisms of the action of $F$ and $X$.

CategoryTheory.PreGaloisCategory.autEquivAutWhiskerRightdefMathlib.CategoryTheory.Galois.Topology, function or constant

Wording

the right automorphism equivalence automorphism whisker of F and h (from the name)

English

Let $F$ be a functor of $C$ and the set of finite type categories. Let $h$ be an element of $\operatorname{FullyFaithful}$ applied to $G$. Then the right automorphism equivalence automorphism whisker of $F$ and $h$ is a continuous multiplicative equivalence of the set of automorphisms of $F$ and the set of automorphisms of the composition of $F$ and $G$.

Mathlib.CategoryTheory.Generator.Basic

CategoryTheory.HasCodetectorclassMathlib.CategoryTheory.Generator.Basic, predicate

Wording

C has codetectors (from the name)

English

Let $C$ be a set. Then we can say that $C$ has codetectors.

CategoryTheory.HasCoseparatorclassMathlib.CategoryTheory.Generator.Basic, predicate

Wording

C has coseparators (from the name)

English

Let $C$ be a set. Then we can say that $C$ has coseparators.

CategoryTheory.HasDetectorclassMathlib.CategoryTheory.Generator.Basic, predicate

Wording

C has detectors (from the name)

English

Let $C$ be a set. Then we can say that $C$ has detectors.

CategoryTheory.HasSeparatorclassMathlib.CategoryTheory.Generator.Basic, predicate

Wording

C has separators (from the name)

English

Let $C$ be a set. Then we can say that $C$ has separators.

CategoryTheory.IsCodetectordefMathlib.CategoryTheory.Generator.Basic, predicate

Wording

G is a codetector (from the name)

English

Let $G$ be an element of $C$. Then $G$ is a codetector, if $\operatorname{IsCodetecting}$ holds for the singleton of $G$.

CategoryTheory.IsCoseparatordefMathlib.CategoryTheory.Generator.Basic, predicate

Wording

G is a coseparator (from the name)

English

Let $G$ be an element of $C$. Then $G$ is a coseparator, if $\operatorname{IsCoseparating}$ holds for the singleton of $G$.

CategoryTheory.IsDetectordefMathlib.CategoryTheory.Generator.Basic, predicate

Wording

G is a detector (from the name)

English

Let $G$ be an element of $C$. Then $G$ is a detector, if $\operatorname{IsDetecting}$ holds for the singleton of $G$.

CategoryTheory.IsSeparatordefMathlib.CategoryTheory.Generator.Basic, predicate

Wording

G is a separator (from the name)

English

Let $G$ be an element of $C$. Then $G$ is a separator, if the singleton of $G$ is a separating.

CategoryTheory.ObjectProperty.IsCodetectingdefMathlib.CategoryTheory.Generator.Basic, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then $\operatorname{IsCodetecting}$ holds for $P$, if for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, if for all elements $G$ of $C$, if $P$ holds for $G$, then for all homomorphisms $h_{2}$ of $X$ and $G$, $\mathrm{ExistsUnique}$ holds for the function that maps $\mathrm{h'}$ to the proposition that the composition of $f$ and $\mathrm{h'}$ is equal to $h_{2}$, then $f$ is an isomorphism.

CategoryTheory.ObjectProperty.IsCoseparatingdefMathlib.CategoryTheory.Generator.Basic, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then $\operatorname{IsCoseparating}$ holds for $P$, if for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ and $g$ of $X$ and $Y$, if for all elements $G$ of $C$, if $P$ holds for $G$, then for all homomorphisms $h_{2}$ of $Y$ and $G$, the composition of $f$ and $h_{2}$ is equal to the composition of $g$ and $h_{2}$, then $\EqtMACRoH {f}{g}$.

CategoryTheory.ObjectProperty.IsDetectingdefMathlib.CategoryTheory.Generator.Basic, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then $\operatorname{IsDetecting}$ holds for $P$, if for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, if for all elements $G$ of $C$, if $P$ holds for $G$, then for all homomorphisms $h_{2}$ of $G$ and $Y$, $\mathrm{ExistsUnique}$ holds for the function that maps $\mathrm{h'}$ to the proposition that the composition of $\mathrm{h'}$ and $f$ is equal to $h_{2}$, then $f$ is an isomorphism.

CategoryTheory.ObjectProperty.IsSeparatingdefMathlib.CategoryTheory.Generator.Basic, predicate

Wording

P is a separating (from the name)

English

Let $P$ be an object property of $C$. Then $P$ is a separating, if for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ and $g$ of $X$ and $Y$, if for all elements $G$ of $C$, if $P$ holds for $G$, then for all homomorphisms $h_{2}$ of $G$ and $X$, the composition of $h_{2}$ and $f$ is equal to the composition of $h_{2}$ and $g$, then $\EqtMACRoH {f}{g}$.

CategoryTheory.ObjectProperty.coproductFromdefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Let $X$ be an element of $C$. Then $\operatorname{coproductFrom}$ applied to $P$ and $X$ is a homomorphism of the sigma object of $\operatorname{coproductFromFamily}$ applied to $X$ and $X$ defined as $\operatorname{desc}$ applied to the function that maps $i$ to the homomorphism of $i$.

CategoryTheory.ObjectProperty.coproductFromFamilydefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

the coproduct from family of X and i (from the name)

English

Let $P$ be an object property of $C$. Let $X$ be an element of $C$. Let $i$ be a costructured arrow of the inclusion of $P$ and $X$. Then the coproduct from family of $X$ and $i$ is an element of $C$ defined as the object of the left object of $i$.

CategoryTheory.ObjectProperty.productTodefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Let $X$ be an element of $C$. Then $\operatorname{productTo}$ applied to $P$ and $X$ is a homomorphism of $X$ and the product object of $\operatorname{productToFamily}$ applied to $X$ defined as the lift of the function that maps $i$ to the homomorphism of $i$.

CategoryTheory.ObjectProperty.productToFamilydefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

the product to family of X and i (from the name)

English

Let $P$ be an object property of $C$. Let $X$ be an element of $C$. Let $i$ be a structured arrow of $X$ and the inclusion of $P$. Then the product to family of $X$ and $i$ is an element of $C$ defined as the object of the right object of $i$.

CategoryTheory.ObjectProperty.ιCoproductFromdefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Let $f$ be a homomorphism of $Y$ and $X$. Assume that $P$ holds for $Y$. Then $\mathrm{CategoryTheory\_\_ObjectProperty\_\_\_u3b9\_CoproductFrom}$ applied to $P$, $f$ and $\mathrm{hY}$ is a homomorphism of $Y$ and the sigma object of $\operatorname{coproductFromFamily}$ applied to $X$ defined as the inclusion of $\operatorname{coproductFromFamily}$ applied to $X$ and $\operatorname{mk}$ applied to $f$.

CategoryTheory.ObjectProperty.πProductTodefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Assume that $P$ holds for $Y$. Then $\mathrm{CategoryTheory\_\_ObjectProperty\_\_\_u3c0\_ProductTo}$ applied to $P$, $f$ and $\mathrm{hY}$ is a homomorphism of the product object of $\operatorname{productToFamily}$ applied to $X$ and $Y$ defined as the projection of $\operatorname{productToFamily}$ applied to $X$ and $\operatorname{mk}$ applied to $f$.

CategoryTheory.codetectordefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

the codetector of C (from the name)

English

Let $C$ be a set. Then the codetector of $C$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\operatorname{hasCodetector}$.

CategoryTheory.coseparatordefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

the coseparator of C (from the name)

English

Let $C$ be a set. Then the coseparator of $C$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\operatorname{hasCoseparator}$.

CategoryTheory.detectordefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

the detector of C (from the name)

English

Let $C$ be a set. Then the detector of $C$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\operatorname{hasDetector}$.

CategoryTheory.separatordefMathlib.CategoryTheory.Generator.Basic, function or constant

Wording

the separator of C (from the name)

English

Let $C$ be a set. Then the separator of $C$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\operatorname{hasSeparator}$.

Mathlib.CategoryTheory.Generator.HomologicalComplex

HomologicalComplex.separatingFamilydefMathlib.CategoryTheory.Generator.HomologicalComplex, function or constant

Wording

the separating family of X and j (from the name)

English

Let $c$ be a complex shape of $x_{1}$. Let $X$ be a function from elements of $x_{3}$ to elements of $C$. Let $j$ be an element of $\mathrm{Prod}$ applied to $x_{3}$ and $x_{1}$. Then the separating family of $X$ and $j$ is a homological complex of $C$ and $c$ defined as $\operatorname{evalCompCoyonedaCorepresentative}$ applied to $c$, $X$ applied to $\ProdfstMACRoZ {j}$ and $\ProdsndMACRoAA {j}$.

Mathlib.CategoryTheory.Generator.Presheaf

CategoryTheory.Presheaf.freeYonedadefMathlib.CategoryTheory.Generator.Presheaf, function or constant

Wording

the free Yoneda of X and M (from the name)

English

Let $X$ be an element of $C$. Let $M$ be an element of $A$. Then the free Yoneda of $X$ and $M$ is a functor of the set of opposites of $C$ and $A$.

CategoryTheory.Presheaf.freeYonedaHomEquivdefMathlib.CategoryTheory.Generator.Presheaf, function or constant

Wording

the free Yoneda homomorphism equivalence (from the name)

English

Mathlib.CategoryTheory.Generator.Sheaf

CategoryTheory.Sheaf.freeYonedadefMathlib.CategoryTheory.Generator.Sheaf, function or constant

Wording

the free Yoneda of X and M (from the name)

English

Let $J$ be a Grothendieck topology of $C$. Let $X$ be an element of $C$. Let $M$ be an element of $A$. Then the free Yoneda of $X$ and $M$ is a sheaf of $J$ and $A$ defined as the action of the presheaf to sheaf of $J$ and $A$ and the free Yoneda of $X$ and $M$.

CategoryTheory.Sheaf.freeYonedaHomEquivdefMathlib.CategoryTheory.Generator.Sheaf, function or constant

Wording

the free Yoneda homomorphism equivalence (from the name)

English

The free Yoneda homomorphism equivalence is an equivalence from the set of homomorphisms of the free Yoneda of $X$ and $M$ and $F$ to the set of homomorphisms of $M$ and the action of the object of $F$ and $\operatorname{op}$ applied to $X$ defined as the composition of the homomorphism equivalence of the free Yoneda of $X$ and $M$ and $F$ and the free Yoneda homomorphism equivalence.

Mathlib.CategoryTheory.Generator.StrongGenerator

CategoryTheory.ObjectProperty.IsStrongGeneratordefMathlib.CategoryTheory.Generator.StrongGenerator, predicate

Wording

P is a strong generator (from the name)

English

Let $P$ be an object property of $C$. Then $P$ is a strong generator, if $P$ is a separating and for all elements $X$ of $C$, for all subobjects $A$ of $X$, if for all elements $G$ of $C$, if $P$ holds for $G$, then for all homomorphisms $f$ of $G$ and $X$, $\operatorname{Factors}$ holds for $A$ and $f$, then $A$ is equal to the top.

Mathlib.CategoryTheory.GlueData

CategoryTheory.GlueDatastructureMathlib.CategoryTheory.GlueData, type

Wording

glue data of C (from the name)

English

Let $C$ be a set. Then the glue data of $C$ are a basic type.

CategoryTheory.GlueData'structureMathlib.CategoryTheory.GlueData, type

Wording

glue data of C (from the name)

English

Let $C$ be a set. Then the glue data of $C$ are a basic type.

CategoryTheory.GlueData'.JdefMathlib.CategoryTheory.GlueData, type

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Then an element of $\operatorname{J}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.GlueData'.UdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $x_{1}$ be an element of $\operatorname{J}$ applied to $\mathrm{self}$. Then $\operatorname{U}$ applied to $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

CategoryTheory.GlueData'.VdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$ such that $i \neq j$. Then $\operatorname{V}$ applied to $\mathrm{self}$, $i$, $j$ and $h$ is an element of $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $i$, $j$ and $h$.

CategoryTheory.GlueData'.fdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$ such that $i \neq j$. Then $\operatorname{f}$ applied to $\mathrm{self}$, $i$, $j$ and $h$ is a homomorphism of $\operatorname{V}$ applied to $\mathrm{self}$, $i$, $j$ and $h$ and $\operatorname{U}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $i$, $j$ and $h$.

CategoryTheory.GlueData'.f'defMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $D$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $D$. Then $\operatorname{f'}$ applied to $D$, $i$ and $j$ is a homomorphism of $\mathrm{dite}$ applied to $\EqtMACRoH {i}{j}$, the function that maps $h$ to $\operatorname{U}$ applied to $D$ and $i$ and the function that maps $h_{1}$ to $\operatorname{V}$ applied to $D$, $i$, $j$ and $h_{1}$ and $\operatorname{U}$ applied to $D$ and $i$.

CategoryTheory.GlueData'.tdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$ such that $i \neq j$. Then $\operatorname{t}$ applied to $\mathrm{self}$, $i$, $j$ and $h$ is a homomorphism of $\operatorname{V}$ applied to $\mathrm{self}$, $i$, $j$ and $h$ and $\operatorname{V}$ applied to $\mathrm{self}$, $j$, $i$ and $\operatorname{symm}$ applied to $h$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$, $i$, $j$ and $h$.

CategoryTheory.GlueData'.t'defMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $i$, $j$ and $k$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$ such that $i \neq j$, $i \neq k$ and $j \neq k$. Then $\operatorname{t'}$ applied to $\mathrm{self}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hik}$ and $\mathrm{hjk}$ is a homomorphism of the pullback of $\operatorname{f}$ applied to $\mathrm{self}$, $i$, $j$ and $\mathrm{hij}$ and $\operatorname{f}$ applied to $\mathrm{self}$, $i$, $k$ and $\mathrm{hik}$ and the pullback of $\operatorname{f}$ applied to $\mathrm{self}$, $j$, $k$ and $\mathrm{hjk}$ and $\operatorname{f}$ applied to $\mathrm{self}$, $j$, $i$ and $\operatorname{symm}$ applied to $\mathrm{hij}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$, $i$, $j$, $k$, $\mathrm{hij}$, $\mathrm{hik}$ and $\mathrm{hjk}$.

CategoryTheory.GlueData'.t''defMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $D$ be a glue data of $C$. Let $i$, $j$ and $k$ be elements of $\operatorname{J}$ applied to $D$. Then $\operatorname{t''}$ applied to $D$, $i$, $j$ and $k$ is a homomorphism of the pullback of $\operatorname{f'}$ applied to $D$, $i$ and $j$ and $\operatorname{f'}$ applied to $D$, $i$ and $k$ and the pullback of $\operatorname{f'}$ applied to $D$, $j$ and $k$ and $\operatorname{f'}$ applied to $D$, $j$ and $i$.

CategoryTheory.GlueData.JdefMathlib.CategoryTheory.GlueData, type

Wording

no wording

English

CategoryTheory.GlueData.UdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

CategoryTheory.GlueData.VdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $\operatorname{J}$ applied to $\mathrm{self}$ and $\operatorname{J}$ applied to $\mathrm{self}$. Then $\operatorname{V}$ applied to $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{1}$.

CategoryTheory.GlueData.diagramdefMathlib.CategoryTheory.GlueData, function or constant

Wording

the diagram of D (from the name)

English

Let $D$ be a glue data of $C$. Then the diagram of $D$ is a multispan index of the product of $\operatorname{J}$ applied to $D$ and $C$.

CategoryTheory.GlueData.diagramIsodefMathlib.CategoryTheory.GlueData, function or constant

Wording

the diagram of the image of D and F (from the docstring)

English

Let $D$ be a glue data of $C$. Let $F$ be a functor of $C$ and $\mathrm{C'}$. Then the diagram of the image of $D$ and $F$ is an isomorphism of the composition of the multispan of the diagram of $D$ and $F$ and the multispan of the diagram of the map glue data of $D$ and $F$.

CategoryTheory.GlueData.fdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$. Then $\operatorname{f}$ applied to $\mathrm{self}$, $i$ and $j$ is a homomorphism of $\operatorname{V}$ applied to $\mathrm{self}$ and $\ProdmkMACRoU {i}{j}$ and $\operatorname{U}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $i$ and $j$.

CategoryTheory.GlueData.glueddefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $D$ be a glue data of $C$. Then $\operatorname{glued}$ applied to $D$ is an element of $C$ defined as the multicoequalizer of the diagram of $D$.

CategoryTheory.GlueData.gluedIsodefMathlib.CategoryTheory.GlueData, function or constant

Wording

the glued isomorphism of D and F (from the name)

English

Let $D$ be a glue data of $C$. Let $F$ be a functor of $C$ and $\mathrm{C'}$. Then the glued isomorphism of $D$ and $F$ is an isomorphism of the action of $F$ and $\operatorname{glued}$ applied to $D$ and $\operatorname{glued}$ applied to the map glue data of $D$ and $F$ defined as the composition of $\operatorname{preservesColimitIso}$ applied to $F$ and the multispan of the diagram of $D$ and the isomorphism of the diagram of the image of $D$ and $F$.

CategoryTheory.GlueData.mapGlueDatadefMathlib.CategoryTheory.GlueData, function or constant

Wording

the map glue data of D and F (from the name)

English

Let $D$ be a glue data of $C$. Let $F$ be a functor of $C$ and $\mathrm{C'}$. Then the map glue data of $D$ and $F$ is a glue data of $\mathrm{C'}$.

CategoryTheory.GlueData.ofGlueData'defMathlib.CategoryTheory.GlueData, function or constant

Wording

the glue data of D (from the name)

English

Let $D$ be a glue data of $C$. Then the glue data of $D$ is a glue data of $C$.

CategoryTheory.GlueData.sigmaOpensdefMathlib.CategoryTheory.GlueData, function or constant

Wording

the sigma open of D (from the name)

English

Let $D$ be a glue data of $C$. Then the sigma open of $D$ is an element of $C$ defined as the sigma object of $\operatorname{U}$ applied to $D$.

CategoryTheory.GlueData.tdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$. Then $\operatorname{t}$ applied to $\mathrm{self}$, $i$ and $j$ is a homomorphism of $\operatorname{V}$ applied to $\mathrm{self}$ and $\ProdmkMACRoU {i}{j}$ and $\operatorname{V}$ applied to $\mathrm{self}$ and $\ProdmkMACRoU {j}{i}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$, $i$ and $j$.

CategoryTheory.GlueData.t'defMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a glue data of $C$. Let $i$, $j$ and $k$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$. Then $\operatorname{t'}$ applied to $\mathrm{self}$, $i$, $j$ and $k$ is a homomorphism of the pullback of $\operatorname{f}$ applied to $\mathrm{self}$, $i$ and $j$ and $\operatorname{f}$ applied to $\mathrm{self}$, $i$ and $k$ and the pullback of $\operatorname{f}$ applied to $\mathrm{self}$, $j$ and $k$ and $\operatorname{f}$ applied to $\mathrm{self}$, $j$ and $i$ defined as $\operatorname{proj9}$ applied to $\mathrm{self}$, $i$, $j$ and $k$.

CategoryTheory.GlueData.vPullbackConedefMathlib.CategoryTheory.GlueData, function or constant

Wording

the pullback cone of i and j (from the name)

English

Let $D$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $D$. Then the pullback cone of $i$ and $j$ is a pullback cone of the inclusion of $D$ and $i$ and the inclusion of $D$ and $j$.

CategoryTheory.GlueData.vPullbackConeIsLimitOfMapdefMathlib.CategoryTheory.GlueData, function or constant

Wording

no wording

English

Let $D$ be a glue data of $C$. Let $F$ be a functor of $C$ and $\mathrm{C'}$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $D$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to the pullback cone of $i$ and $j$. Then $\operatorname{vPullbackConeIsLimitOfMap}$ applied to $D$, $F$, $i$, $j$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $i$ and $j$.

CategoryTheory.GlueData.ιdefMathlib.CategoryTheory.GlueData, function or constant

Wording

the inclusion of D and i (from the name)

English

Let $D$ be a glue data of $C$. Let $i$ be an element of $\operatorname{J}$ applied to $D$. Then the inclusion of $D$ and $i$ is a homomorphism of $\operatorname{U}$ applied to $D$ and $i$ and $\operatorname{glued}$ applied to $D$ defined as the projection of the diagram of $D$ and $i$.

CategoryTheory.GlueData.πdefMathlib.CategoryTheory.GlueData, function or constant

Wording

the projection of D (from the docstring)

English

Let $D$ be a glue data of $C$. Then the projection of $D$ is a homomorphism of the sigma open of $D$ and $\operatorname{glued}$ applied to $D$ defined as the canonical projection of the diagram of $D$.

Mathlib.CategoryTheory.GradedObject

CategoryTheory.GradedObjectdefMathlib.CategoryTheory.GradedObject, type

Wording

graded object of x and C (from the name)

English

Let $x$ and $C$ be sets. Then a graded object of $x$ and $C$ is an element of the function that maps $x$ and $C$ to the set of functions from elements of $x$ to elements of $C$.

CategoryTheory.GradedObject.CofanMapObjFundefMathlib.CategoryTheory.GradedObject, type

Wording

cofan map object function of p and j (from the name)

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $j$ be an element of $J$. Then a cofan map object function of $p$ and $j$ is an element of the function that maps $X$, $p$ and $j$ to the set of cofans of $\operatorname{mapObjFun}$ applied to $j$.

CategoryTheory.GradedObject.CofanMapObjFun.isodefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the isomorphism of hc (from the name)

English

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the isomorphism of $\mathrm{hc}$ is an isomorphism of $\operatorname{pt}$ applied to $c$ and the map object of $X$ and $p$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\mathrm{hc}$ and $\operatorname{isColimitCofanMapObj}$ applied to $X$, $p$ and $j$.

CategoryTheory.GradedObject.CofanMapObjFun.mkdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

no wording

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $j$ be an element of $J$. Let $\mathrm{pt}$ be an element of $C$. Let $x_{1}$ be a function from elements $i$ of $I$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {p (i)}{j}$ to homomorphisms of $X$ applied to $i$ and $\mathrm{pt}$. Then $\operatorname{mk}$ applied to $X$, $p$, $j$, $\mathrm{pt}$, $i$ and $x_{1}$ is a cofan map object function of $p$ and $j$.

CategoryTheory.GradedObject.HasMapdefMathlib.CategoryTheory.GradedObject, predicate

Wording

no wording

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Then $\operatorname{HasMap}$ holds for $X$ and $p$, if for all elements $j$ of $J$, $\operatorname{mapObjFun}$ applied to $j$ has coproducts.

CategoryTheory.GradedObject.cofanMapObjdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the tautological cofan corresponding to the coproduct decomposition of X (from the docstring)

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $j$ be an element of $J$. Then the tautological cofan corresponding to the coproduct decomposition of $X$ is a cofan map object function of $p$ and $j$ defined as $\operatorname{mk}$ applied to $X$, $p$, $j$, the map object of $X$ and $p$ and the function that maps $i$ and $\mathrm{hi}$ to the inclusion map object of $i$ and $j$.

CategoryTheory.GradedObject.cofanMapObjCompdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the cofan map object composition of c and j1 (from the name)

English

CategoryTheory.GradedObject.comapdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the preimage of C and h (from the name)

English

Let $C$ be a set. 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 graded objects of $I$ and $C$ and the set of graded objects of $J$ and $C$ defined as the preimage of the function that maps $x_{1}$ to $C$ and $h$.

CategoryTheory.GradedObject.comapEqdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

no wording

English

Let $C$ be a set. Assume that $\EqtMACRoH {f}{g}$. Then $\operatorname{comapEq}$ applied to $C$ and $h$ is an isomorphism of the preimage of $C$ and $f$ and the preimage of $C$ and $g$.

CategoryTheory.GradedObject.comapEquivdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the preimage equivalence of C and e (from the name)

English

Let $C$ be a set. Let $e$ be an equivalence from $x_{1}$ to $x_{2}$. Then the preimage equivalence of $C$ and $e$ is an equivalence of the set of graded objects of $x_{1}$ and $C$ and the set of graded objects of $x_{2}$ and $C$.

CategoryTheory.GradedObject.descMapObjdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

no wording

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $x_{1}$ be a function from elements $i$ of $I$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {p (i)}{j}$ to homomorphisms of $X$ applied to $i$ and $A$. Then $\operatorname{descMapObj}$ applied to $X$, $p$, $i$ and $x_{1}$ is a homomorphism of the map object of $X$ and $p$ and $A$.

CategoryTheory.GradedObject.evaldefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the evaluation of b (from the name)

English

Let $b$ be an element of $x_{1}$. Then the evaluation of $b$ is a functor of the set of graded objects of $x_{1}$ and $C$ and $C$.

CategoryTheory.GradedObject.isColimitCofanMapObjdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

no wording

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $j$ be an element of $J$. Then $\operatorname{isColimitCofanMapObj}$ applied to $X$, $p$ and $j$ is an element of $\operatorname{IsColimit}$ applied to the tautological cofan corresponding to the coproduct decomposition of $X$ defined as $\operatorname{isColimit}$ applied to the functor of $\operatorname{mapObjFun}$ applied to $j$.

CategoryTheory.GradedObject.isColimitCofanMapObjCompdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

no wording

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $q$ be a function from elements of $J$ to elements of $K$. Let $r$ be a function from elements of $I$ to elements of $K$ such that for all elements $i$ of $I$, $\EqtMACRoH {q (p (i))}{r (i)}$. Let $k$ be an element of $K$. Let $c$ be a function from elements $j_{2}$ of $J$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {q (j_{2})}{k}$ to cofan map object functions of $p$ and $j_{2}$. Let $\mathrm{hc}$ be a function from elements $j_{1}$ of $J$ and elements $\mathrm{hj}$ of $\mathrm{Proof}$ applied to $\EqtMACRoH {q (j_{1})}{k}$ to elements of $\operatorname{IsColimit}$ applied to $c$ applied to $j_{1}$ and $\mathrm{hj}$. Let $\mathrm{c'}$ be a cofan of the function that maps $j$ to $\operatorname{pt}$ applied to $c$ applied to $j$ and $\operatorname{property}$ applied to $j$. Let $\mathrm{hc'}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{c'}$. Then $\operatorname{isColimitCofanMapObjComp}$ applied to $X$, $p$, $q$, $r$, $\mathrm{hpqr}$, $k$, $j_{2}$, $c$, $j_{1}$, $\mathrm{hj}$, $\mathrm{hc}$, $\mathrm{c'}$ and $\mathrm{hc'}$ is an element of $\operatorname{IsColimit}$ applied to the cofan map object composition of $c$ and $\mathrm{c'}$.

CategoryTheory.GradedObject.isoMkdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the isomorphism of Y and e (from the name)

English

Let $X$ and $Y$ be graded objects of $x_{1}$ and $C$. Let $e$ be a function from elements $i$ of $x_{1}$ to isomorphisms of $X$ applied to $i$ and $Y$ applied to $i$. Then the isomorphism of $Y$ and $i$ is an isomorphism of $X$ and $Y$.

CategoryTheory.GradedObject.mapdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the map of C and p (from the name)

English

Let $C$ be a set. Let $p$ be a function from elements of $I$ to elements of $J$. Then the map of $C$ and $p$ is a functor of the set of graded objects of $I$ and $C$ and the set of graded objects of $J$ and $C$.

CategoryTheory.GradedObject.mapIsodefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the map isomorphism of e and p (from the name)

English

Let $e$ be an isomorphism of $X$ and $Y$. Let $p$ be a function from elements of $I$ to elements of $J$. Then the map isomorphism of $e$ and $p$ is an isomorphism of the map object of $X$ and $p$ and the map object of $Y$ and $p$.

CategoryTheory.GradedObject.mapMapdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the map map of x1 and p (from the name)

English

Let $x_{1}$ be a homomorphism of $X$ and $Y$. Let $p$ be a function from elements of $I$ to elements of $J$. Then the map map of $x_{1}$ and $p$ is a homomorphism of the map object of $X$ and $p$ and the map object of $Y$ and $p$ defined as the function that maps $j$ to $\operatorname{descMapObj}$ applied to $X$, $p$ and the function that maps $i$ and $\mathrm{hi}$ to the composition of $x_{1}$ applied to $i$ and the inclusion map object of $i$ and $j$.

CategoryTheory.GradedObject.mapObjdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the map object of X and p (from the name)

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Then the map object of $X$ and $p$ is a graded object of $J$ and $C$ defined as the function that maps $j$ to the sigma object of $\operatorname{mapObjFun}$ applied to $j$.

CategoryTheory.GradedObject.mapObjFundefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the map object function of j and i (from the name)

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $j$ be an element of $J$. Let $i$ be an element of the preimage of $p$ and $\operatorname{singleton}$ applied to $j$. Then the map object function of $j$ and $i$ is an element of $C$ defined as $X$ applied to $i$.

CategoryTheory.GradedObject.totaldefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the total object of x and C (from the docstring)

English

Let $x$ and $C$ be sets. Then the total object of $x$ and $C$ is a functor of the set of graded objects of $x$ and $C$ and $C$.

CategoryTheory.GradedObject.ιMapObjdefMathlib.CategoryTheory.GradedObject, function or constant

Wording

the inclusion map object of i and j (from the name)

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $i$ be an element of $I$. Let $j$ be an element of $J$ such that $\EqtMACRoH {p (i)}{j}$. Then the inclusion map object of $i$ and $j$ is a homomorphism of $X$ applied to $i$ and the map object of $X$ and $p$ defined as the inclusion of $\operatorname{mapObjFun}$ applied to $j$ and $i$.

CategoryTheory.GradedObject.ιMapObjOrZerodefMathlib.CategoryTheory.GradedObject, function or constant

Wording

no wording

English

Let $X$ be a graded object of $I$ and $C$. Let $p$ be a function from elements of $I$ to elements of $J$. Let $i$ be an element of $I$. Let $j$ be an element of $J$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_\_u3b9\_MapObjOrZero}$ applied to $X$, $p$, $i$ and $j$ is a homomorphism of $X$ applied to $i$ and the map object of $X$ and $p$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {p (i)}{j}$, the function that maps $h_{1}$ to the inclusion map object of $i$ and $j$ and the function that maps $h_{2}$ to $0$.

CategoryTheory.GradedObjectWithShiftdefMathlib.CategoryTheory.GradedObject, type

Wording

graded object with shift of x2 and C (from the name)

English

Let $x_{2}$ be an element of $x$. Let $C$ be a set. Then a graded object with shift of $x_{2}$ and $C$ is an element of the function that maps $x_{2}$ and $C$ to the set of graded objects of $x$ and $C$.

Mathlib.CategoryTheory.GradedObject.Associator

CategoryTheory.GradedObject.mapBifunctorAssociatordefMathlib.CategoryTheory.GradedObject.Associator, function or constant

Wording

the map bifunctor associator of x20 and x21 (from the name)

English

Let $\mathrm{associator}$ be an isomorphism of the bifunctor composition of $x_{12}$ and $G$ and the bifunctor composition of $F$ and $x_{13}$. Let $x_{17}$ and $x_{18}$ be bifunctor composition index data of $r$. Let $x_{19}$ be a graded object of $x_{14}$ and $x$. Let $x_{20}$ be a graded object of $x_{15}$ and $x_{1}$. Let $x_{21}$ be a graded object of $x_{16}$ and $x_{4}$. Then the map bifunctor associator of $x_{20}$ and $x_{21}$ is an isomorphism of the map bifunctor map object of the map bifunctor map object of $x_{19}$ and $x_{20}$ and $x_{21}$ and the map bifunctor map object of $x_{19}$ and the map bifunctor map object of $x_{20}$ and $x_{21}$ defined as the composition of the inverse of the map bifunctor composition map object isomorphism of $x_{20}$ and $x_{21}$ and the composition of the map isomorphism of the application of the application of the application of the map trifunctor map isomorphism of $\mathrm{associator}$ and $x_{19}$ and $x_{20}$ and $x_{21}$ and $r$ and the map bifunctor composition map object isomorphism of $x_{20}$ and $x_{21}$.

Mathlib.CategoryTheory.GradedObject.Bifunctor

CategoryTheory.GradedObject.mapBifunctordefMathlib.CategoryTheory.GradedObject.Bifunctor, function or constant

Wording

the map bifunctor of F (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $I$ and $J$ be sets. Then the map bifunctor of $F$ is a functor of the set of graded objects of $I$ and $x$ and the set of functors of the set of graded objects of $J$ and $x_{1}$ and the set of graded objects of $\mathrm{Prod}$ applied to $I$ and $J$ and $x_{2}$.

CategoryTheory.GradedObject.mapBifunctorMapdefMathlib.CategoryTheory.GradedObject.Bifunctor, function or constant

Wording

the map bifunctor map of F and p (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $I$ and $J$ to elements of $K$. Then the map bifunctor map of $F$ and $p$ is a functor of the set of graded objects of $I$ and $x$ and the set of functors of the set of graded objects of $J$ and $x_{1}$ and the set of graded objects of $K$ and $x_{2}$.

CategoryTheory.GradedObject.mapBifunctorMapMapdefMathlib.CategoryTheory.GradedObject.Bifunctor, function or constant

Wording

the map bifunctor map map of f and g (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $I$ and $J$ to elements of $K$. Let $f$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $g$ be a homomorphism of $x_{8}$ and $x_{9}$. Then the map bifunctor map map of $f$ and $g$ is a homomorphism of the map bifunctor map object of $x_{6}$ and $x_{8}$ and the map bifunctor map object of $x_{7}$ and $x_{9}$ defined as the map map of the composition of the component of the map of the map bifunctor of $F$ and $f$ and $x_{8}$ and the map of the action of the map bifunctor of $F$ and $x_{7}$ and $g$ and $p$.

CategoryTheory.GradedObject.mapBifunctorMapMapIsodefMathlib.CategoryTheory.GradedObject.Bifunctor, function or constant

Wording

the map bifunctor map map isomorphism of e and #4 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $I$ and $J$ to elements of $K$. Let $e$ be an isomorphism of $x_{6}$ and $x_{7}$. Let $\mathrm{e'}$ be an isomorphism of $x_{8}$ and $x_{9}$. Then the map bifunctor map map isomorphism of $e$ and $\mathrm{e'}$ is an isomorphism of the map bifunctor map object of $x_{6}$ and $x_{8}$ and the map bifunctor map object of $x_{7}$ and $x_{9}$.

CategoryTheory.GradedObject.mapBifunctorMapObjdefMathlib.CategoryTheory.GradedObject.Bifunctor, function or constant

Wording

the map bifunctor map object of X and Y (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $I$ and $J$ to elements of $K$. Let $X$ be a graded object of $I$ and $x$. Let $Y$ be a graded object of $J$ and $x_{1}$. Then the map bifunctor map object of $X$ and $Y$ is a graded object of $K$ and $x_{2}$ defined as the map object of the action of the action of the map bifunctor of $F$ and $X$ and $Y$ and $p$.

CategoryTheory.GradedObject.mapBifunctorMapObjDescdefMathlib.CategoryTheory.GradedObject.Bifunctor, function or constant

Wording

no wording

English

Let $f$ be a function from elements $i$ of $I$ and elements $j$ of $J$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {p (\ProdmkMACRoU {i}{j})}{k}$ to homomorphisms of the action of the action of $F$ and $X$ applied to $i$ and $Y$ applied to $j$ and $A$. Then $\operatorname{mapBifunctorMapObjDesc}$ applied to $i$, $j$ and $f$ is a homomorphism of the map bifunctor map object of $X$ and $Y$ and $A$.

CategoryTheory.GradedObject.ιMapBifunctorMapObjdefMathlib.CategoryTheory.GradedObject.Bifunctor, function or constant

Wording

the inclusion of F (from the docstring)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $I$ and $J$ to elements of $K$. Let $X$ be a graded object of $I$ and $x$. Let $Y$ be a graded object of $J$ and $x_{1}$. Let $i$ be an element of $I$. Let $j$ be an element of $J$. Let $k$ be an element of $K$ such that $\EqtMACRoH {p (\ProdmkMACRoU {i}{j})}{k}$. Then the inclusion of $F$ is a homomorphism of the action of the action of $F$ and $X$ applied to $i$ and $Y$ applied to $j$ and the map bifunctor map object of $X$ and $Y$ defined as the inclusion map object of $\ProdmkMACRoU {i}{j}$ and $k$.

Mathlib.CategoryTheory.GradedObject.Braiding

CategoryTheory.GradedObject.Monoidal.braidingdefMathlib.CategoryTheory.GradedObject.Braiding, function or constant

Wording

the braiding of X and Y (from the docstring)

English

Let $X$ and $Y$ be graded objects of $I$ and $C$. Then the braiding of $X$ and $Y$ is an isomorphism of the tensor object of $X$ and $Y$ and the tensor object of $Y$ and $X$.

Mathlib.CategoryTheory.GradedObject.Monoidal

CategoryTheory.GradedObject.HasGoodTensorTensor₂₃defMathlib.CategoryTheory.GradedObject.Monoidal, predicate

Wording

no wording

English

Let $x_{3}$, $x_{4}$ and $x_{5}$ be graded objects of $I$ and $C$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_HasGoodTensorTensor\_u2082\_\_u2083\_}$ holds for $x_{3}$, $x_{4}$ and $x_{5}$, if $\mathrm{CategoryTheory\_\_GradedObject\_\_HasGoodTrifunctor\_u2082\_\_u2083\_Obj}$ holds for the tensor product bifunctor of $C$, the tensor product bifunctor of $C$, $\mathrm{CategoryTheory\_\_GradedObject\_\_Monoidal\_\_\_u3c1\_\_u2082\_\_u2083\_}$, $x_{3}$, $x_{4}$ and $x_{5}$.

CategoryTheory.GradedObject.HasGoodTensor₁₂TensordefMathlib.CategoryTheory.GradedObject.Monoidal, predicate

Wording

no wording

English

Let $x_{3}$, $x_{4}$ and $x_{5}$ be graded objects of $I$ and $C$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_HasGoodTensor\_u2081\_\_u2082\_Tensor}$ holds for $x_{3}$, $x_{4}$ and $x_{5}$, if $\mathrm{CategoryTheory\_\_GradedObject\_\_HasGoodTrifunctor\_u2081\_\_u2082\_Obj}$ holds for the tensor product bifunctor of $C$, the tensor product bifunctor of $C$, $\mathrm{CategoryTheory\_\_GradedObject\_\_Monoidal\_\_\_u3c1\_\_u2081\_\_u2082\_}$, $x_{3}$, $x_{4}$ and $x_{5}$.

CategoryTheory.GradedObject.HasLeftTensor₃ObjExtdefMathlib.CategoryTheory.GradedObject.Monoidal, predicate

Wording

no wording

English

Let $Z$ be an element of $C$. Let $x_{3}$, $x_{4}$ and $x_{5}$ be graded objects of $I$ and $C$. Let $j$ be an element of $I$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_HasLeftTensor\_u2083\_ObjExt}$ holds for $Z$, $x_{3}$, $x_{4}$, $x_{5}$ and $j$, if $\operatorname{PreservesColimit}$ holds for the functor of the function that maps $i$ to the action of the action of the action of the map trifunctor of the bifunctor composition of the tensor product bifunctor of $C$ and the tensor product bifunctor of $C$ and $x_{3}$ and $x_{4}$ and $x_{5}$ and the action of the tensor product bifunctor of $C$ and $Z$.

CategoryTheory.GradedObject.HasTensordefMathlib.CategoryTheory.GradedObject.Monoidal, predicate

Wording

no wording

English

Let $x_{3}$ and $x_{4}$ be graded objects of $I$ and $C$. Then we can say that $\operatorname{HasTensor}$ holds for $x_{3}$ and $x_{4}$.

CategoryTheory.GradedObject.HasTensor₄ObjExtdefMathlib.CategoryTheory.GradedObject.Monoidal, predicate

Wording

no wording

English

Let $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ be graded objects of $I$ and $C$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_HasTensor\_u2084\_ObjExt}$ holds for $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$, if for all elements $x_{7}$ and $x_{8}$ of $I$, $\mathrm{CategoryTheory\_\_GradedObject\_\_HasLeftTensor\_u2083\_ObjExt}$ holds for $x_{3}$ applied to $x_{7}$, $x_{4}$, $x_{5}$, $x_{6}$ and $x_{8}$.

CategoryTheory.GradedObject.Monoidal.associatordefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the associator of x4 and x5 (from the name)

English

Let $x_{3}$, $x_{4}$ and $x_{5}$ be graded objects of $I$ and $C$. Then the associator of $x_{4}$ and $x_{5}$ is an isomorphism of the tensor object of the tensor object of $x_{3}$ and $x_{4}$ and $x_{5}$ and the tensor object of $x_{3}$ and the tensor object of $x_{4}$ and $x_{5}$ defined as the map bifunctor associator of $x_{4}$ and $x_{5}$.

CategoryTheory.GradedObject.Monoidal.isInitialTensorUnitApplydefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

no wording

English

Let $i$ be an element of $I$ such that $i \neq 0$. Then $\operatorname{isInitialTensorUnitApply}$ applied to $i$ and $\mathrm{hi}$ is an element of $\operatorname{IsInitial}$ applied to the tensor unit defined as $\operatorname{isInitialSingleObjApply}$ applied to $0$, the tensor unity in the monoidal structure of $C$, $i$ and $\mathrm{hi}$.

CategoryTheory.GradedObject.Monoidal.leftUnitordefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the left unitor of X (from the name)

English

Let $X$ be a graded object of $I$ and $C$. Then the left unitor of $X$ is an isomorphism of the tensor object of the tensor unit and $X$ and $X$.

CategoryTheory.GradedObject.Monoidal.rightUnitordefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the right unitor of X (from the name)

English

Let $X$ be a graded object of $I$ and $C$. Then the right unitor of $X$ is an isomorphism of the tensor object of $X$ and the tensor unit and $X$.

CategoryTheory.GradedObject.Monoidal.r₁₂₃defMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $I$ and $\mathrm{Prod}$ applied to $I$ and $I$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_Monoidal\_\_r\_u2081\_\_u2082\_\_u2083\_}$ applied to $x_{1}$ is an element of $I$.

CategoryTheory.GradedObject.Monoidal.tensorHomdefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

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

English

Let $f$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $g$ be a homomorphism of $x_{5}$ and $x_{6}$. Then the tensor homomorphism of $f$ and $g$ is a homomorphism of the tensor object of $x_{3}$ and $x_{5}$ and the tensor object of $x_{4}$ and $x_{6}$.

CategoryTheory.GradedObject.Monoidal.tensorIsodefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the isomorphism of e and #2 (from the docstring)

English

Let $e$ be an isomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{e'}$ be an isomorphism of $x_{5}$ and $x_{6}$. Then the isomorphism of $e$ and $\mathrm{e'}$ is an isomorphism of the tensor object of $x_{3}$ and $x_{5}$ and the tensor object of $x_{4}$ and $x_{6}$.

CategoryTheory.GradedObject.Monoidal.tensorObjdefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the tensor object of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be graded objects of $I$ and $C$. Then the tensor object of $x_{3}$ and $x_{4}$ is a graded object of $I$ and $C$.

CategoryTheory.GradedObject.Monoidal.tensorObjDescdefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

no wording

English

Let $f$ be a function from elements $x_{5}$ of $I$ and elements $x_{6}$ of $I$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {(x_{5} + x_{6})}{k}$ to homomorphisms of the tensor object of $x_{3}$ applied to $x_{5}$ and $x_{4}$ applied to $x_{6}$ and $A$. Then $\operatorname{tensorObjDesc}$ applied to $x_{5}$, $x_{6}$ and $f$ is a homomorphism of the tensor object of $x_{3}$ and $x_{4}$ and $A$ defined as the function that maps $x_{6}$ and $f$ to $\operatorname{mapBifunctorMapObjDesc}$ applied to $x_{5}$, $x_{6}$ and $f$.

CategoryTheory.GradedObject.Monoidal.tensorUnitdefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the tensor unit (from the name)

English

The tensor unit is a graded object of $I$ and $C$ defined as the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and the tensor unity in the monoidal structure of $C$.

CategoryTheory.GradedObject.Monoidal.tensorUnit₀defMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the tensor unit (from the name)

English

The tensor unit is an isomorphism of the tensor unit and the tensor unity in the monoidal structure of $C$ defined as the canonical isomorphism of $0$ and the tensor unity in the monoidal structure of $C$.

CategoryTheory.GradedObject.Monoidal.whiskerLeftdefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the left whisker of X and x5 (from the name)

English

Let $X$ be a graded object of $I$ and $C$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the left whisker of $X$ and $x_{5}$ is a homomorphism of the tensor object of $X$ and $x_{3}$ and the tensor object of $X$ and $x_{4}$ defined as the tensor homomorphism of the identity morphism of $X$ and $x_{5}$.

CategoryTheory.GradedObject.Monoidal.whiskerRightdefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

the right whisker of x5 and Y (from the name)

English

Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $Y$ be a graded object of $I$ and $C$. Then the right whisker of $x_{5}$ and $Y$ is a homomorphism of the tensor object of $x_{3}$ and $Y$ and the tensor object of $x_{4}$ and $Y$ defined as the tensor homomorphism of $x_{5}$ and the identity morphism of $Y$.

CategoryTheory.GradedObject.Monoidal.ιTensorObjdefMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

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

English

Let $x_{3}$ and $x_{4}$ be graded objects of $I$ and $C$. Let $x_{5}$, $x_{6}$ and $x_{7}$ be elements of $I$ such that $\EqtMACRoH {x_{5} + x_{6}}{x_{7}}$. Then the inclusion tensor object of $x_{6}$ and $x_{7}$ is a homomorphism of the tensor object of $x_{3}$ applied to $x_{5}$ and $x_{4}$ applied to $x_{6}$ and the tensor object of $x_{3}$ and $x_{4}$.

CategoryTheory.GradedObject.Monoidal.ιTensorObj₃defMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

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

English

Let $x_{3}$, $x_{4}$ and $x_{5}$ be graded objects of $I$ and $C$. Let $x_{6}$, $x_{7}$, $x_{8}$ and $j$ be elements of $I$ such that $\EqtMACRoH {x_{6} + x_{7} + x_{8}}{j}$. Then the inclusion tensor object of $x_{8}$ and $j$ is a homomorphism of the tensor object of $x_{3}$ applied to $x_{6}$ and the tensor object of $x_{4}$ applied to $x_{7}$ and $x_{5}$ applied to $x_{8}$ and the tensor object of $x_{3}$ and the tensor object of $x_{4}$ and $x_{5}$.

CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'defMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

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

English

Let $x_{3}$, $x_{4}$ and $x_{5}$ be graded objects of $I$ and $C$. Let $x_{6}$, $x_{7}$, $x_{8}$ and $j$ be elements of $I$ such that $\EqtMACRoH {x_{6} + x_{7} + x_{8}}{j}$. Then the inclusion tensor object of $x_{8}$ and $j$ is a homomorphism of the tensor object of the tensor object of $x_{3}$ applied to $x_{6}$ and $x_{4}$ applied to $x_{7}$ and $x_{5}$ applied to $x_{8}$ and the tensor object of the tensor object of $x_{3}$ and $x_{4}$ and $x_{5}$.

CategoryTheory.GradedObject.Monoidal.ιTensorObj₄defMathlib.CategoryTheory.GradedObject.Monoidal, function or constant

Wording

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

English

Let $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ be graded objects of $I$ and $C$. Let $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$ and $j$ be elements of $I$ such that $\EqtMACRoH {x_{7} + x_{8} + x_{9} + x_{10}}{j}$. Then the inclusion tensor object of $x_{10}$ and $j$ is a homomorphism of the tensor object of $x_{3}$ applied to $x_{7}$ and the tensor object of $x_{4}$ applied to $x_{8}$ and the tensor object of $x_{5}$ applied to $x_{9}$ and $x_{6}$ applied to $x_{10}$ and the tensor object of $x_{3}$ and the tensor object of $x_{4}$ and the tensor object of $x_{5}$ and $x_{6}$.

Mathlib.CategoryTheory.GradedObject.Single

CategoryTheory.GradedObject.isInitialSingleObjApplydefMathlib.CategoryTheory.GradedObject.Single, function or constant

Wording

no wording

English

Let $j$ and $i$ be elements of $J$. Let $X$ be an element of $C$. Assume that $i \neq j$. Then $\operatorname{isInitialSingleObjApply}$ applied to $j$, $X$, $i$ and $h_{1}$ is an element of $\operatorname{IsInitial}$ applied to the action of $\operatorname{single}$ applied to $j$ and $X$.

CategoryTheory.GradedObject.singledefMathlib.CategoryTheory.GradedObject.Single, function or constant

Wording

no wording

English

Let $j$ be an element of $J$. Then $\operatorname{single}$ applied to $j$ is a functor of $C$ and the set of graded objects of $J$ and $C$.

CategoryTheory.GradedObject.singleCompEvaldefMathlib.CategoryTheory.GradedObject.Single, function or constant

Wording

the composition of the single functor of C and j (from the docstring)

English

Let $C$ be a set. Let $j$ be an element of $J$. Then the composition of the single functor of $C$ and $j$ is an isomorphism of the composition of $\operatorname{single}$ applied to $j$ and the evaluation of $j$ and the identity of $C$.

CategoryTheory.GradedObject.singleObjApplyIsodefMathlib.CategoryTheory.GradedObject.Single, function or constant

Wording

the canonical isomorphism of j and X (from the docstring)

English

Let $j$ be an element of $J$. Let $X$ be an element of $C$. Then the canonical isomorphism of $j$ and $X$ is an isomorphism of the action of $\operatorname{single}$ applied to $j$ and $X$ and $X$ defined as $\operatorname{singleObjApplyIsoOfEq}$ applied to $j$, $X$, $j$ and $\mathrm{rfl}$.

CategoryTheory.GradedObject.singleObjApplyIsoOfEqdefMathlib.CategoryTheory.GradedObject.Single, function or constant

Wording

no wording

English

Let $j$ and $i$ be elements of $J$. Let $X$ be an element of $C$. Assume that $\EqtMACRoH {i}{j}$. Then $\operatorname{singleObjApplyIsoOfEq}$ applied to $j$, $X$, $i$ and $h_{1}$ is an isomorphism of the action of $\operatorname{single}$ applied to $j$ and $X$ and $X$.

CategoryTheory.GradedObject.single₀defMathlib.CategoryTheory.GradedObject.Single, function or constant

Wording

no wording

English

Let $J$ be a set. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $J$ is a functor of $C$ and the set of graded objects of $J$ and $C$ defined as $\operatorname{single}$ applied to $0$.

Mathlib.CategoryTheory.GradedObject.Trifunctor

CategoryTheory.GradedObject.BifunctorComp₁₂IndexDatastructureMathlib.CategoryTheory.GradedObject.Trifunctor, type

Wording

bifunctor composition index data of r (from the name)

English

Let $r$ be a function from elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ to elements of $J$. Then the bifunctor composition index data of $r$ are a basic type.

CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.I₁₂defMathlib.CategoryTheory.GradedObject.Trifunctor, type

Wording

no wording

English

Let $\mathrm{self}$ be a bifunctor composition index data of $r$. Then an element of $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_I\_u2081\_\_u2082\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.pdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a bifunctor composition index data of $r$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_p}$ applied to $\mathrm{self}$ and $x_{3}$ is an element of $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_I\_u2081\_\_u2082\_}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_proj1}$ applied to $\mathrm{self}$ and $x_{3}$.

CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.qdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a bifunctor composition index data of $r$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_I\_u2081\_\_u2082\_}$ applied to $\mathrm{self}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_q}$ applied to $\mathrm{self}$ and $x_{3}$ is an element of $J$ defined as $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_proj2}$ applied to $\mathrm{self}$ and $x_{3}$.

CategoryTheory.GradedObject.BifunctorComp₂₃IndexDatastructureMathlib.CategoryTheory.GradedObject.Trifunctor, type

Wording

bifunctor composition index data of r (from the name)

English

CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.I₂₃defMathlib.CategoryTheory.GradedObject.Trifunctor, type

Wording

no wording

English

Let $\mathrm{self}$ be a bifunctor composition index data of $r$. Then an element of $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_I\_u2082\_\_u2083\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.pdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a bifunctor composition index data of $r$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_p}$ applied to $\mathrm{self}$ and $x_{3}$ is an element of $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_I\_u2082\_\_u2083\_}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_proj1}$ applied to $\mathrm{self}$ and $x_{3}$.

CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.qdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a bifunctor composition index data of $r$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to $x$ and $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_I\_u2082\_\_u2083\_}$ applied to $\mathrm{self}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_q}$ applied to $\mathrm{self}$ and $x_{3}$ is an element of $J$ defined as $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_proj2}$ applied to $\mathrm{self}$ and $x_{3}$.

CategoryTheory.GradedObject.HasGoodTrifunctor₁₂ObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, predicate

Wording

no wording

English

Let $x_{10}$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{4}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{2}$ and $x_{3}$. Let $x_{14}$ be a bifunctor composition index data of $r$. Let $x_{15}$ be a graded object of $x_{11}$ and $x$. Let $x_{16}$ be a graded object of $x_{12}$ and $x_{1}$. Let $x_{17}$ be a graded object of $x_{13}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_HasGoodTrifunctor\_u2081\_\_u2082\_Obj}$ holds for $x_{10}$, $G$, $x_{14}$, $x_{15}$, $x_{16}$ and $x_{17}$, if for all elements $x_{18}$ of $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_I\_u2081\_\_u2082\_}$ applied to $x_{14}$, for all elements $x_{19}$ of $x_{13}$, $\operatorname{PreservesColimit}$ holds for the functor of $\operatorname{mapObjFun}$ applied to $x_{18}$ and the action of the flip of $G$ and $x_{17}$ applied to $x_{19}$.

CategoryTheory.GradedObject.HasGoodTrifunctor₂₃ObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, predicate

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{4}$ and $x_{3}$. Let $x_{10}$ be a functor of $x_{1}$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{14}$ be a bifunctor composition index data of $r$. Let $x_{15}$ be a graded object of $x_{11}$ and $x$. Let $x_{16}$ be a graded object of $x_{12}$ and $x_{1}$. Let $x_{17}$ be a graded object of $x_{13}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_HasGoodTrifunctor\_u2082\_\_u2083\_Obj}$ holds for $F$, $x_{10}$, $x_{14}$, $x_{15}$, $x_{16}$ and $x_{17}$, if for all elements $x_{18}$ of $x_{11}$, for all elements $x_{19}$ of $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_I\_u2082\_\_u2083\_}$ applied to $x_{14}$, $\operatorname{PreservesColimit}$ holds for the functor of $\operatorname{mapObjFun}$ applied to $x_{19}$ and the action of $F$ and $x_{15}$ applied to $x_{18}$.

CategoryTheory.GradedObject.cofan₃MapBifunctorBifunctor₂₃MapObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the cofan map bifunctor bifunctor map object of x17 and j (from the name)

English

CategoryTheory.GradedObject.cofan₃MapBifunctor₁₂BifunctorMapObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the cofan map bifunctor bifunctor map object of x17 and j (from the name)

English

CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{4}$ and $x_{3}$. Let $x_{10}$ be a functor of $x_{1}$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{14}$ be a bifunctor composition index data of $r$. Let $x_{15}$ be a graded object of $x_{11}$ and $x$. Let $x_{16}$ be a graded object of $x_{12}$ and $x_{1}$. Let $x_{17}$ be a graded object of $x_{13}$ and $x_{2}$. Let $j$ be an element of $J$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_isColimitCofan\_u2083\_MapBifunctorBifunctor\_u2082\_\_u2083\_MapObj}$ applied to $F$, $x_{10}$, $x_{14}$, $x_{15}$, $x_{16}$, $x_{17}$ and $j$ is an element of $\operatorname{IsColimit}$ applied to the cofan map bifunctor bifunctor map object of $x_{17}$ and $j$.

CategoryTheory.GradedObject.isColimitCofan₃MapBifunctor₁₂BifunctorMapObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

no wording

English

Let $x_{10}$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{4}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{2}$ and $x_{3}$. Let $x_{14}$ be a bifunctor composition index data of $r$. Let $x_{15}$ be a graded object of $x_{11}$ and $x$. Let $x_{16}$ be a graded object of $x_{12}$ and $x_{1}$. Let $x_{17}$ be a graded object of $x_{13}$ and $x_{2}$. Let $j$ be an element of $J$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_isColimitCofan\_u2083\_MapBifunctor\_u2081\_\_u2082\_BifunctorMapObj}$ applied to $x_{10}$, $G$, $x_{14}$, $x_{15}$, $x_{16}$, $x_{17}$ and $j$ is an element of $\operatorname{IsColimit}$ applied to the cofan map bifunctor bifunctor map object of $x_{17}$ and $j$.

CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃DescdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

no wording

English

Let $f$ be a function from elements $x_{18}$ of $x_{11}$ and elements $x_{19}$ of $x_{12}$ and elements $x_{20}$ of $x_{13}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {r (\ProdmkMACRoU {x_{18}}{(\ProdmkMACRoU {x_{19}}{x_{20}})})}{j}$ to homomorphisms of the action of the action of $F$ and $x_{15}$ applied to $x_{18}$ and the action of the action of $x_{10}$ and $x_{16}$ applied to $x_{19}$ and $x_{17}$ applied to $x_{20}$ and $A$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_mapBifunctorBifunctor\_u2082\_\_u2083\_Desc}$ applied to $x_{18}$, $x_{19}$, $x_{20}$ and $f$ is a homomorphism of the map bifunctor map object of $x_{15}$ and the map bifunctor map object of $x_{16}$ and $x_{17}$ and $A$.

CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIsodefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map bifunctor composition map object isomorphism of x16 and x17 (from the name)

English

Let $x_{10}$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{4}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{2}$ and $x_{3}$. Let $x_{14}$ be a bifunctor composition index data of $r$. Let $x_{15}$ be a graded object of $x_{11}$ and $x$. Let $x_{16}$ be a graded object of $x_{12}$ and $x_{1}$. Let $x_{17}$ be a graded object of $x_{13}$ and $x_{2}$. Then the map bifunctor composition map object isomorphism of $x_{16}$ and $x_{17}$ is an isomorphism of the map trifunctor map object of $x_{16}$ and $x_{17}$ and the map bifunctor map object of the map bifunctor map object of $x_{15}$ and $x_{16}$ and $x_{17}$ defined as the isomorphism of the map bifunctor map object of the map bifunctor map object of $x_{15}$ and $x_{16}$ and $x_{17}$ and the function that maps $j$ to the inverse of the isomorphism of $\mathrm{CategoryTheory\_\_GradedObject\_\_isColimitCofan\_u2083\_MapBifunctor\_u2081\_\_u2082\_BifunctorMapObj}$ applied to $x_{10}$, $G$, $x_{14}$, $x_{15}$, $x_{16}$, $x_{17}$ and $j$.

CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIsodefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map bifunctor composition map object isomorphism of x16 and x17 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{4}$ and $x_{3}$. Let $x_{10}$ be a functor of $x_{1}$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{14}$ be a bifunctor composition index data of $r$. Let $x_{15}$ be a graded object of $x_{11}$ and $x$. Let $x_{16}$ be a graded object of $x_{12}$ and $x_{1}$. Let $x_{17}$ be a graded object of $x_{13}$ and $x_{2}$. Then the map bifunctor composition map object isomorphism of $x_{16}$ and $x_{17}$ is an isomorphism of the map trifunctor map object of $x_{16}$ and $x_{17}$ and the map bifunctor map object of $x_{15}$ and the map bifunctor map object of $x_{16}$ and $x_{17}$ defined as the isomorphism of the map bifunctor map object of $x_{15}$ and the map bifunctor map object of $x_{16}$ and $x_{17}$ and the function that maps $j$ to the inverse of the isomorphism of $\mathrm{CategoryTheory\_\_GradedObject\_\_isColimitCofan\_u2083\_MapBifunctorBifunctor\_u2082\_\_u2083\_MapObj}$ applied to $F$, $x_{10}$, $x_{14}$, $x_{15}$, $x_{16}$, $x_{17}$ and $j$.

CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDescdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

no wording

English

Let $f$ be a function from elements $x_{18}$ of $x_{11}$ and elements $x_{19}$ of $x_{12}$ and elements $x_{20}$ of $x_{13}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {r (\ProdmkMACRoU {x_{18}}{(\ProdmkMACRoU {x_{19}}{x_{20}})})}{j}$ to homomorphisms of the action of the action of $G$ and the action of the action of $x_{10}$ and $x_{15}$ applied to $x_{18}$ and $x_{16}$ applied to $x_{19}$ and $x_{17}$ applied to $x_{20}$ and $A$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_mapBifunctor\_u2081\_\_u2082\_BifunctorDesc}$ applied to $x_{18}$, $x_{19}$, $x_{20}$ and $f$ is a homomorphism of the map bifunctor map object of the map bifunctor map object of $x_{15}$ and $x_{16}$ and $x_{17}$ and $A$.

CategoryTheory.GradedObject.mapTrifunctordefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map trifunctor of F (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $x_{3}$. Let $x_{8}$, $x_{9}$ and $x_{10}$ be sets. Then the map trifunctor of $F$ is a functor of the set of graded objects of $x_{8}$ and $x$ and the set of functors of the set of graded objects of $x_{9}$ and $x_{1}$ and the set of functors of the set of graded objects of $x_{10}$ and $x_{2}$ and the set of graded objects of $\mathrm{Prod}$ applied to $x_{8}$ and $\mathrm{Prod}$ applied to $x_{9}$ and $x_{10}$ and $x_{3}$.

CategoryTheory.GradedObject.mapTrifunctorMapdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map trifunctor map of F and p (from the name)

English

CategoryTheory.GradedObject.mapTrifunctorMapFunctorObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map trifunctor map functor object of p and x11 (from the name)

English

CategoryTheory.GradedObject.mapTrifunctorMapIsodefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map trifunctor map isomorphism of e (from the name)

English

Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Let $x_{8}$, $x_{9}$ and $x_{10}$ be sets. Then the map trifunctor map isomorphism of $e$ is an isomorphism of the map trifunctor of $F$ and the map trifunctor of $\mathrm{F'}$.

CategoryTheory.GradedObject.mapTrifunctorMapMapdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map trifunctor map map of x16 and x19 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $x_{3}$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $x_{8}$ and $\mathrm{Prod}$ applied to $x_{9}$ and $x_{10}$ to elements of $J$. Let $x_{13}$ be a homomorphism of $x_{11}$ and $x_{12}$. Let $x_{16}$ be a homomorphism of $x_{14}$ and $x_{15}$. Let $x_{19}$ be a homomorphism of $x_{17}$ and $x_{18}$. Then the map trifunctor map map of $x_{16}$ and $x_{19}$ is a homomorphism of the map trifunctor map object of $x_{14}$ and $x_{17}$ and the map trifunctor map object of $x_{15}$ and $x_{18}$ defined as the map map of the composition of the component of the component of the map of the map trifunctor of $F$ and $x_{13}$ and $x_{14}$ and $x_{17}$ and the composition of the component of the map of the action of the map trifunctor of $F$ and $x_{12}$ and $x_{16}$ and $x_{17}$ and the map of the action of the action of the map trifunctor of $F$ and $x_{12}$ and $x_{15}$ and $x_{19}$ and $p$.

CategoryTheory.GradedObject.mapTrifunctorMapNatTransdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map trifunctor map natural transformation of x8 (from the name)

English

Let $x_{8}$ be a homomorphism of $F$ and $\mathrm{F'}$. Let $x_{9}$, $x_{10}$ and $x_{11}$ be sets. Then the map trifunctor map natural transformation of $x_{8}$ is a homomorphism of the map trifunctor of $F$ and the map trifunctor of $\mathrm{F'}$.

CategoryTheory.GradedObject.mapTrifunctorMapObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the map trifunctor map object of x12 and x13 (from the name)

English

CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the inclusion of F (from the docstring)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{4}$ and $x_{3}$. Let $x_{10}$ be a functor of $x_{1}$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{14}$ be a bifunctor composition index data of $r$. Let $x_{15}$ be a graded object of $x_{11}$ and $x$. Let $x_{16}$ be a graded object of $x_{12}$ and $x_{1}$. Let $x_{17}$ be a graded object of $x_{13}$ and $x_{2}$. Let $x_{18}$ be an element of $x_{11}$. Let $x_{19}$ be an element of $x_{12}$. Let $x_{20}$ be an element of $x_{13}$. Let $j$ be an element of $J$ such that $\EqtMACRoH {r (\ProdmkMACRoU {x_{18}}{(\ProdmkMACRoU {x_{19}}{x_{20}})})}{j}$. Then the inclusion of $F$ is a homomorphism of the action of the action of $F$ and $x_{15}$ applied to $x_{18}$ and the action of the action of $x_{10}$ and $x_{16}$ applied to $x_{19}$ and $x_{17}$ applied to $x_{20}$ and the map bifunctor map object of $x_{15}$ and the map bifunctor map object of $x_{16}$ and $x_{17}$.

CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the inclusion of x10 (from the docstring)

English

Let $x_{10}$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{4}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{2}$ and $x_{3}$. Let $x_{14}$ be a bifunctor composition index data of $r$. Let $x_{15}$ be a graded object of $x_{11}$ and $x$. Let $x_{16}$ be a graded object of $x_{12}$ and $x_{1}$. Let $x_{17}$ be a graded object of $x_{13}$ and $x_{2}$. Let $x_{18}$ be an element of $x_{11}$. Let $x_{19}$ be an element of $x_{12}$. Let $x_{20}$ be an element of $x_{13}$. Let $j$ be an element of $J$ such that $\EqtMACRoH {r (\ProdmkMACRoU {x_{18}}{(\ProdmkMACRoU {x_{19}}{x_{20}})})}{j}$. Then the inclusion of $x_{10}$ is a homomorphism of the action of the action of $G$ and the action of the action of $x_{10}$ and $x_{15}$ applied to $x_{18}$ and $x_{16}$ applied to $x_{19}$ and $x_{17}$ applied to $x_{20}$ and the map bifunctor map object of the map bifunctor map object of $x_{15}$ and $x_{16}$ and $x_{17}$.

CategoryTheory.GradedObject.ιMapTrifunctorMapObjdefMathlib.CategoryTheory.GradedObject.Trifunctor, function or constant

Wording

the inclusion map trifunctor map object of x16 and j (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $x_{3}$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $x_{8}$ and $\mathrm{Prod}$ applied to $x_{9}$ and $x_{10}$ to elements of $J$. Let $x_{11}$ be a graded object of $x_{8}$ and $x$. Let $x_{12}$ be a graded object of $x_{9}$ and $x_{1}$. Let $x_{13}$ be a graded object of $x_{10}$ and $x_{2}$. Let $x_{14}$ be an element of $x_{8}$. Let $x_{15}$ be an element of $x_{9}$. Let $x_{16}$ be an element of $x_{10}$. Let $j$ be an element of $J$ such that $\EqtMACRoH {p (\ProdmkMACRoU {x_{14}}{(\ProdmkMACRoU {x_{15}}{x_{16}})})}{j}$. Then the inclusion map trifunctor map object of $x_{16}$ and $j$ is a homomorphism of the action of the action of the action of $F$ and $x_{11}$ applied to $x_{14}$ and $x_{12}$ applied to $x_{15}$ and $x_{13}$ applied to $x_{16}$ and the map trifunctor map object of $x_{12}$ and $x_{13}$ defined as the inclusion map object of $\ProdmkMACRoU {x_{14}}{(\ProdmkMACRoU {x_{15}}{x_{16}})}$ and $j$.

Mathlib.CategoryTheory.GradedObject.Unitor

CategoryTheory.GradedObject.TriangleIndexDatastructureMathlib.CategoryTheory.GradedObject.Unitor, type

Wording

triangle index data of r and x4 (from the name)

English

Let $r$ be a function from elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ to elements of $J$. Let $x_{4}$ be a function from elements of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ to elements of $J$. Then the triangle index data of $r$ and $x_{4}$ are a basic type.

CategoryTheory.GradedObject.TriangleIndexData.p₁₂defMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a triangle index data of $r$ and $x_{4}$. Let $x_{5}$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_TriangleIndexData\_\_p\_u2081\_\_u2082\_}$ applied to $\mathrm{self}$ and $x_{5}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{5}$.

CategoryTheory.GradedObject.TriangleIndexData.p₂₃defMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a triangle index data of $r$ and $x_{4}$. Let $x_{5}$ be an element of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_TriangleIndexData\_\_p\_u2082\_\_u2083\_}$ applied to $\mathrm{self}$ and $x_{5}$ is an element of $x_{2}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{5}$.

CategoryTheory.GradedObject.TriangleIndexData.ρ₁₂defMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

no wording

English

Let $x_{5}$ be a triangle index data of $r$ and $x_{4}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_TriangleIndexData\_\_\_u3c1\_\_u2081\_\_u2082\_}$ applied to $x_{5}$ is a bifunctor composition index data of $r$ defined as $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2081\_\_u2082\_IndexData\_\_mk}$ applied to $x$, $\mathrm{CategoryTheory\_\_GradedObject\_\_TriangleIndexData\_\_p\_u2081\_\_u2082\_}$ applied to $x_{5}$, $x_{4}$ and $\mathrm{CategoryTheory\_\_GradedObject\_\_TriangleIndexData\_\_hp\_u2081\_\_u2082\_}$ applied to $x_{5}$.

CategoryTheory.GradedObject.TriangleIndexData.ρ₂₃defMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

no wording

English

Let $x_{5}$ be a triangle index data of $r$ and $x_{4}$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_TriangleIndexData\_\_\_u3c1\_\_u2082\_\_u2083\_}$ applied to $x_{5}$ is a bifunctor composition index data of $r$ defined as $\mathrm{CategoryTheory\_\_GradedObject\_\_BifunctorComp\_u2082\_\_u2083\_IndexData\_\_mk}$ applied to $x_{2}$, $\mathrm{CategoryTheory\_\_GradedObject\_\_TriangleIndexData\_\_p\_u2082\_\_u2083\_}$ applied to $x_{5}$, $x_{4}$ and $\mathrm{CategoryTheory\_\_GradedObject\_\_TriangleIndexData\_\_hp\_u2082\_\_u2083\_}$ applied to $x_{5}$.

CategoryTheory.GradedObject.mapBifunctorLeftUnitordefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

the map bifunctor left unitor of p and Y (from the name)

English

Let $F$ be a functor of $C$ and the set of functors of $D$ and $D$. Let $X$ be an element of $C$. Let $e$ be an isomorphism of the action of $F$ and $X$ and the identity of $D$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $I$ and $J$ to elements of $J$ such that for all elements $j$ of $J$, $\EqtMACRoH {p (\ProdmkMACRoU {0}{j})}{j}$. Let $Y$ be a graded object of $J$ and $D$. Then the map bifunctor left unitor of $p$ and $Y$ is an isomorphism of the map bifunctor map object of the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and $X$ and $Y$ and $Y$ defined as the isomorphism of $Y$ and the function that maps $j$ to the inverse of the isomorphism of $\operatorname{mapBifunctorLeftUnitorCofanIsColimit}$ applied to $F$, $X$, $e$, $p$, $\mathrm{hp}$, $Y$ and $j$.

CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofandefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

the map bifunctor left unitor cofan of Y and j (from the name)

English

CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofanIsColimitdefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of functors of $D$ and $D$. Let $X$ be an element of $C$. Let $e$ be an isomorphism of the action of $F$ and $X$ and the identity of $D$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $I$ and $J$ to elements of $J$ such that for all elements $j_{1}$ of $J$, $\EqtMACRoH {p (\ProdmkMACRoU {0}{j_{1}})}{j_{1}}$. Let $Y$ be a graded object of $J$ and $D$. Let $j$ be an element of $J$. Then $\operatorname{mapBifunctorLeftUnitorCofanIsColimit}$ applied to $F$, $X$, $e$, $p$, $\mathrm{hp}$, $Y$ and $j$ is an element of $\operatorname{IsColimit}$ applied to the map bifunctor left unitor cofan of $Y$ and $j$.

CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀IsInitialdefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

no wording

English

Let $F$ be a functor of $D$ and the set of functors of $C$ and $D$. Let $Y$ be an element of $C$. Let $X$ be a graded object of $J$ and $D$. Let $a$ be an element of $\mathrm{Prod}$ applied to $J$ and $I$ such that $\ProdsndMACRoAA {a}\neq 0$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_mapBifunctorObjObjSingle\_u2080\_IsInitial}$ applied to $F$, $Y$, $X$, $a$ and $\mathrm{ha}$ is an element of $\operatorname{IsInitial}$ applied to the action of the action of the map bifunctor of $F$ and $X$ and the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and $Y$ defined as $\operatorname{isInitialObj}$ applied to the action of $F$ and $X$ applied to $\ProdfstMACRoZ {a}$, the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and $Y$ and $\operatorname{isInitialSingleObjApply}$ applied to $0$, $Y$, $\ProdsndMACRoAA {a}$ and $\mathrm{ha}$.

CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀IsodefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

the map bifunctor object object single isomorphism of X and a (from the name)

English

Let $F$ be a functor of $D$ and the set of functors of $C$ and $D$. Let $Y$ be an element of $C$. Let $e$ be an isomorphism of the action of the flip of $F$ and $Y$ and the identity of $D$. Let $X$ be a graded object of $J$ and $D$. Let $a$ be an element of $\mathrm{Prod}$ applied to $J$ and $I$ such that $\EqtMACRoH {\ProdsndMACRoAA {a}}{0}$. Then the map bifunctor object object single isomorphism of $X$ and $a$ is an isomorphism of the action of the action of the map bifunctor of $F$ and $X$ and the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and $Y$ and $X$ applied to $\ProdfstMACRoZ {a}$ defined as the composition of the map isomorphism of the action of $F$ and $X$ applied to $\ProdfstMACRoZ {a}$ and $\operatorname{singleObjApplyIsoOfEq}$ applied to $0$, $Y$, $\ProdsndMACRoAA {a}$ and $\mathrm{ha}$ and the application of $e$ and $X$ applied to $\ProdfstMACRoZ {a}$.

CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsInitialdefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of functors of $D$ and $D$. Let $X$ be an element of $C$. Let $Y$ be a graded object of $J$ and $D$. Let $a$ be an element of $\mathrm{Prod}$ applied to $I$ and $J$ such that $\ProdfstMACRoZ {a}\neq 0$. Then $\mathrm{CategoryTheory\_\_GradedObject\_\_mapBifunctorObjSingle\_u2080\_ObjIsInitial}$ applied to $F$, $X$, $Y$, $a$ and $\mathrm{ha}$ is an element of $\operatorname{IsInitial}$ applied to the action of the action of the map bifunctor of $F$ and the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and $X$ and $Y$ defined as $\operatorname{isInitialObj}$ applied to the action of the flip of $F$ and $Y$ applied to $\ProdsndMACRoAA {a}$, the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and $X$ and $\operatorname{isInitialSingleObjApply}$ applied to $0$, $X$, $\ProdfstMACRoZ {a}$ and $\mathrm{ha}$.

CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsodefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

the map bifunctor object single object isomorphism of Y and a (from the name)

English

Let $F$ be a functor of $C$ and the set of functors of $D$ and $D$. Let $X$ be an element of $C$. Let $e$ be an isomorphism of the action of $F$ and $X$ and the identity of $D$. Let $Y$ be a graded object of $J$ and $D$. Let $a$ be an element of $\mathrm{Prod}$ applied to $I$ and $J$ such that $\EqtMACRoH {\ProdfstMACRoZ {a}}{0}$. Then the map bifunctor object single object isomorphism of $Y$ and $a$ is an isomorphism of the action of the action of the map bifunctor of $F$ and the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and $X$ and $Y$ and $Y$ applied to $\ProdsndMACRoAA {a}$ defined as the composition of the application of the map isomorphism of $F$ and $\operatorname{singleObjApplyIsoOfEq}$ applied to $0$, $X$, $\ProdfstMACRoZ {a}$ and $\mathrm{ha}$ and $Y$ applied to $\ProdsndMACRoAA {a}$ and the application of $e$ and $Y$ applied to $\ProdsndMACRoAA {a}$.

CategoryTheory.GradedObject.mapBifunctorRightUnitordefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

the map bifunctor right unitor of p and X (from the name)

English

Let $F$ be a functor of $D$ and the set of functors of $C$ and $D$. Let $Y$ be an element of $C$. Let $e$ be an isomorphism of the action of the flip of $F$ and $Y$ and the identity of $D$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $J$ and $I$ to elements of $J$ such that for all elements $j$ of $J$, $\EqtMACRoH {p (\ProdmkMACRoU {j}{0})}{j}$. Let $X$ be a graded object of $J$ and $D$. Then the map bifunctor right unitor of $p$ and $X$ is an isomorphism of the map bifunctor map object of $X$ and the action of $\mathrm{CategoryTheory\_\_GradedObject\_\_single\_u2080\_}$ applied to $I$ and $Y$ and $X$ defined as the isomorphism of $X$ and the function that maps $j$ to the inverse of the isomorphism of $\operatorname{mapBifunctorRightUnitorCofanIsColimit}$ applied to $F$, $Y$, $e$, $p$, $\mathrm{hp}$, $X$ and $j$.

CategoryTheory.GradedObject.mapBifunctorRightUnitorCofandefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

the map bifunctor right unitor cofan of X and j (from the name)

English

Let $F$ be a functor of $D$ and the set of functors of $C$ and $D$. Let $Y$ be an element of $C$. Let $e$ be an isomorphism of the action of the flip of $F$ and $Y$ and the identity of $D$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $J$ and $I$ to elements of $J$ such that for all elements $j_{1}$ of $J$, $\EqtMACRoH {p (\ProdmkMACRoU {j_{1}}{0})}{j_{1}}$. Let $X$ be a graded object of $J$ and $D$. Let $j$ be an element of $J$. Then the map bifunctor right unitor cofan of $X$ and $j$ is a cofan map object function of $p$ and $j$.

CategoryTheory.GradedObject.mapBifunctorRightUnitorCofanIsColimitdefMathlib.CategoryTheory.GradedObject.Unitor, function or constant

Wording

no wording

English

Let $F$ be a functor of $D$ and the set of functors of $C$ and $D$. Let $Y$ be an element of $C$. Let $e$ be an isomorphism of the action of the flip of $F$ and $Y$ and the identity of $D$. Let $p$ be a function from elements of $\mathrm{Prod}$ applied to $J$ and $I$ to elements of $J$ such that for all elements $j_{1}$ of $J$, $\EqtMACRoH {p (\ProdmkMACRoU {j_{1}}{0})}{j_{1}}$. Let $X$ be a graded object of $J$ and $D$. Let $j$ be an element of $J$. Then $\operatorname{mapBifunctorRightUnitorCofanIsColimit}$ applied to $F$, $Y$, $e$, $p$, $\mathrm{hp}$, $X$ and $j$ is an element of $\operatorname{IsColimit}$ applied to the map bifunctor right unitor cofan of $X$ and $j$.