Definitions: Mathlib.CategoryTheory, part 15 of 25

CategoryTheory.Limits.HasWidePullbackdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, predicate

Wording

no wording

English

Let $B$ be an element of $C$. Let $\mathrm{objs}$ be a function from elements of $J$ to elements of $C$. Let $\mathrm{arrows}$ be a function from elements $j$ of $J$ to homomorphisms of $\mathrm{objs}$ applied to $j$ and $B$. Then $\operatorname{HasWidePullback}$ holds for $B$, $\mathrm{objs}$, $j$ and $\mathrm{arrows}$, if the wide cospan of $\mathrm{objs}$ and $j$ has limits.

CategoryTheory.Limits.HasWidePullbacksdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, predicate

Wording

C has wide pullbacks (from the name)

English

Let $C$ be a set. Then $C$ has wide pullbacks, if for all sets $J$, $\operatorname{HasLimitsOfShape}$ holds for the set of wide pullback shapes of $J$ and $C$.

CategoryTheory.Limits.HasWidePushoutdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, predicate

Wording

no wording

English

Let $B$ be an element of $C$. Let $\mathrm{objs}$ be a function from elements of $J$ to elements of $C$. Let $\mathrm{arrows}$ be a function from elements $j$ of $J$ to homomorphisms of $B$ and $\mathrm{objs}$ applied to $j$. Then $\operatorname{HasWidePushout}$ holds for $B$, $\mathrm{objs}$, $j$ and $\mathrm{arrows}$, if the wide span of $\mathrm{objs}$ and $j$ has colimits.

CategoryTheory.Limits.HasWidePushoutsdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, predicate

Wording

C has wide pushouts (from the name)

English

Let $C$ be a set. Then $C$ has wide pushouts, if for all sets $J$, $\operatorname{HasColimitsOfShape}$ holds for the set of wide pushout shapes of $J$ and $C$.

CategoryTheory.Limits.WidePullback.basedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the unique map to the base from the pullback of arrows (from the docstring)

English

Let $\mathrm{arrows}$ be a function from elements $j$ of $J$ to homomorphisms of $\mathrm{objs}$ applied to $j$ and $B$. Then the unique map to the base from the pullback of $j$ is a homomorphism of the wide pullback of $\mathrm{objs}$ and $\mathrm{arrows}$ and $B$ defined as the function that maps $\mathrm{arrows}$ to the projection from the limit object to a value of the functor of the wide cospan of $\mathrm{objs}$ and $j$ and $\operatorname{none}$.

CategoryTheory.Limits.WidePullback.liftdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the lift of f and fs (from the name)

English

Let $f$ be a homomorphism of $X$ and $B$. Let $\mathrm{fs}$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $X$ and $\mathrm{objs}$ applied to $j_{1}$ such that for all elements $j$ of $J$, the composition of $\mathrm{fs}$ applied to $j$ and $\mathrm{arrows}$ applied to $j$ is equal to $f$. Then the lift of $f$ and $j_{1}$ is a homomorphism of $X$ and the wide pullback of $\mathrm{objs}$ and $\mathrm{arrows}$ defined as the function that maps $w$ to the lift of the wide cospan of $\mathrm{objs}$ and $\mathrm{arrows}$ and the cone of $f$ and $j_{1}$.

CategoryTheory.Limits.WidePullback.πdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the projection of arrows and j1 (from the name)

English

Let $\mathrm{arrows}$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $\mathrm{objs}$ applied to $j_{1}$ and $B$. Let $j$ be an element of $J$. Then the projection of $j_{1}$ and $\mathrm{arrows}$ is a homomorphism of the wide pullback of $\mathrm{objs}$ and $\mathrm{arrows}$ and $\mathrm{objs}$ applied to $j$ defined as the function that maps $j$ to the projection from the limit object to a value of the functor of the wide cospan of $\mathrm{objs}$ and $j_{1}$ and $\operatorname{some}$ applied to $\mathrm{arrows}$.

CategoryTheory.Limits.WidePullbackConedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, type

Wording

wide pullback cone of f (from the name)

English

Let $f$ be a function from elements $i$ of $x_{1}$ to homomorphisms of $Y$ applied to $i$ and $X$. Then a wide pullback cone of $i$ is an element of the function that maps $f$ and $f$ to the set of cones of the wide cospan of $Y$ and $i$.

CategoryTheory.Limits.WidePullbackCone.IsLimit.liftdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the lift of b and a (from the name)

English

Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $b$ be a homomorphism of $W$ and $X$. Let $a$ be a function from elements $i_{1}$ of $x_{1}$ to homomorphisms of $W$ and $Y$ applied to $i_{1}$ such that for all elements $i$ of $x_{1}$, the composition of $a$ applied to $i$ and $f$ applied to $i$ is equal to $b$. Then the lift of $b$ and $i_{1}$ is a homomorphism of $W$ and $\operatorname{pt}$ applied to $s$ defined as the function that maps $w$ to the lift of $\mathrm{hs}$ and $\operatorname{mk}$ applied to $b$, $i_{1}$ and $a$.

CategoryTheory.Limits.WidePullbackCone.IsLimit.mkdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

no wording

English

Let $s$ be a wide pullback cone of $f$. Let $\mathrm{lift}$ be a function from wide pullback cones $t_{3}$ of $f$ to homomorphisms of $\operatorname{pt}$ applied to $t_{3}$ and $\operatorname{pt}$ applied to $s$ such that for all wide pullback cones $t_{2}$ of $f$, the composition of $\mathrm{lift}$ applied to $t_{2}$ and the projection to the base of $s$ is equal to the projection to the base of $t_{2}$, for all wide pullback cones $t_{1}$ of $f$, for all elements $i_{1}$ of $x_{1}$, the composition of $\mathrm{lift}$ applied to $t_{1}$ and the projection on the components of $s$ and $i_{1}$ is equal to the projection on the components of $t_{1}$ and $i_{1}$ and for all wide pullback cones $t$ of $f$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s$, if the composition of $m$ and the projection to the base of $s$ is equal to the projection to the base of $t$, then if for all elements $i$ of $x_{1}$, the composition of $m$ and the projection on the components of $s$ and $i$ is equal to the projection on the components of $t$ and $i$, then $\EqtMACRoH {m}{\mathrm{lift} (t)}$. Then $\operatorname{mk}$ applied to $s$, $t_{3}$, $\mathrm{lift}$, $\mathrm{facbase}$, $h$ and $\mathrm{uniq}$ is an element of $\operatorname{IsLimit}$ applied to $s$.

CategoryTheory.Limits.WidePullbackCone.basedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the projection to the base of s (from the docstring)

English

Let $s$ be a wide pullback cone of $f$. Then the projection to the base of $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $X$ defined as the component of the projection of $s$ and $\operatorname{none}$.

CategoryTheory.Limits.WidePullbackCone.extdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the extension of e (from the name)

English

Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $e$ and the projection to the base of $t$ is equal to the projection to the base of $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_WidePullbackCone\_\_ext\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $x_{1}$, the composition of the homomorphism of $e$ and the projection on the components of $t$ and $i$ is equal to the projection on the components of $s$ and $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_WidePullbackCone\_\_ext\_\_\_auto\_3}$. Then the extension of $e$ is an isomorphism of $s$ and $t$.

CategoryTheory.Limits.WidePullbackCone.mkdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

no wording

English

Let $b$ be a homomorphism of $W$ and $X$. Let $x_{2}$ be a function from elements $i_{1}$ of $x_{1}$ to homomorphisms of $W$ and $Y$ applied to $i_{1}$ such that for all elements $i$ of $x_{1}$, the composition of $x_{2}$ applied to $i$ and $f$ applied to $i$ is equal to $b$. Then $\operatorname{mk}$ applied to $b$, $i_{1}$, $x_{2}$ and $h$ is a wide pullback cone of $f$ defined as the function that maps $h$ to the cone of $b$ and $i_{1}$.

CategoryTheory.Limits.WidePullbackCone.reindexdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the reindexing of s and e (from the name)

English

Let $s$ be a wide pullback cone of $f$. Let $e$ be an equivalence from $x_{2}$ to $x_{1}$. Then the reindexing of $s$ and $e$ is a wide pullback cone of the function that maps $i$ to $f$ applied to $e$ applied to $i$.

CategoryTheory.Limits.WidePullbackCone.reindexIsLimitEquivdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

no wording

English

Let $s$ be a wide pullback cone of $f$. Let $e$ be an equivalence from $x_{2}$ to $x_{1}$. Then $\operatorname{reindexIsLimitEquiv}$ applied to $s$ and $e$ is an equivalence from $\operatorname{IsLimit}$ applied to the reindexing of $s$ and $e$ to $\operatorname{IsLimit}$ applied to $s$.

CategoryTheory.Limits.WidePullbackCone.πdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the projection on the components of s and i (from the docstring)

English

Let $s$ be a wide pullback cone of $f$. Let $i$ be an element of $x_{1}$. Then the projection on the components of $s$ and $i$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $Y$ applied to $i$ defined as the component of the projection of $s$ and $\operatorname{some}$ applied to $i$.

CategoryTheory.Limits.WidePullbackShapedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, type

Wording

wide pullback shape of J (from the name)

English

Let $J$ be a set. Then a wide pullback shape of $J$ is an element of the function that maps $J$ to $\mathrm{Option}$ applied to $J$.

CategoryTheory.Limits.WidePullbackShape.HominductiveMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, type

Wording

homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be wide pullback shapes of $J$. Then the homomorphisms of $x$ and $x_{1}$ are a basic type.

CategoryTheory.Limits.WidePullbackShape.Hom.ctorElimTypedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from wide pullback shapes $X$ of $J$ to elements of $\mathrm{motive}$ applied to $X$, $X$ and the identity of $X$ and $\mathrm{PULift}$ applied to the set of functions from elements $j$ of $J$ to elements of $\mathrm{motive}$ applied to $\operatorname{some}$ applied to $j$, $\operatorname{none}$ and $\operatorname{term}$ applied to $j$.

CategoryTheory.Limits.WidePullbackShape.Hom.idconstructorMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the identity of X (from the name)

English

Let $X$ be a wide pullback shape of $J$. Then the identity of $X$ is a homomorphism of $X$ and $X$.

CategoryTheory.Limits.WidePullbackShape.diagramIsoWideCospandefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the diagram isomorphism wide cospan of F (from the name)

English

Let $F$ be a functor of the set of wide pullback shapes of $J$ and $C$. Then the diagram isomorphism wide cospan of $F$ is an isomorphism of $F$ and the wide cospan of the function that maps $j$ to the action of $F$ and $\operatorname{some}$ applied to $j$ and the function that maps $j_{1}$ to the map of $F$ and $\operatorname{term}$ applied to $j_{1}$.

CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquivdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the equivalence of h and #2 (from the name)

English

Let $\mathrm{J'}$ be a set. Let $h$ be an equivalence from $J$ to $\mathrm{J'}$. Then the equivalence of $\mathrm{J'}$ and $h$ is an equivalence of the set of wide pullback shapes of $J$ and the set of wide pullback shapes of $\mathrm{J'}$.

CategoryTheory.Limits.WidePullbackShape.functorExtdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the functor extension of base and comp (from the name)

English

Let $\mathrm{base}$ be an isomorphism of the action of $F$ and $\operatorname{none}$ and the action of $G$ and $\operatorname{none}$. Let $\mathrm{comp}$ be a function from elements $i_{1}$ of $x_{1}$ to isomorphisms of the action of $F$ and $\operatorname{some}$ applied to $i_{1}$ and the action of $G$ and $\operatorname{some}$ applied to $i_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $x_{1}$, the composition of the map of $F$ and $\operatorname{term}$ applied to $i$ and the homomorphism of $\mathrm{base}$ is equal to the composition of the homomorphism of $\mathrm{comp}$ applied to $i$ and the map of $G$ and $\operatorname{term}$ applied to $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_WidePullbackShape\_\_functorExt\_\_\_auto\_1}$. Then the functor extension of $\mathrm{base}$ and $i_{1}$ is an isomorphism of $F$ and $G$.

CategoryTheory.Limits.WidePullbackShape.mkConedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the cone of f and x1 (from the name)

English

Let $f$ be a homomorphism of $X$ and the action of $F$ and $\operatorname{none}$. Let $x_{1}$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $X$ and the action of $F$ and $\operatorname{some}$ applied to $j_{1}$ such that for all elements $j$ of $J$, the composition of $x_{1}$ applied to $j$ and the map of $F$ and $\operatorname{term}$ applied to $j$ is equal to $f$. Then the cone of $f$ and $j_{1}$ is a cone of $F$.

CategoryTheory.Limits.WidePullbackShape.uliftEquivalencedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the lift equivalence (from the name)

English

The lift equivalence is an equivalence of the set of lift homomorphisms of $\mathrm{ULift}$ applied to the set of wide pullback shapes of $J$ and the set of wide pullback shapes of $\mathrm{ULift}$ applied to $J$ defined as the composition of the inverse of the equivalence of the set of wide pullback shapes of $J$ and the equivalence of $\mathrm{ULift}$ applied to $J$ and the inverse of the lift.

CategoryTheory.Limits.WidePullbackShape.wideCospandefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide cospan of objs and arrows (from the name)

English

Let $B$ be an element of $C$. Let $\mathrm{objs}$ be a function from elements of $J$ to elements of $C$. Let $\mathrm{arrows}$ be a function from elements $j$ of $J$ to homomorphisms of $\mathrm{objs}$ applied to $j$ and $B$. Then the wide cospan of $\mathrm{objs}$ and $j$ is a functor of the set of wide pullback shapes of $J$ and $C$.

CategoryTheory.Limits.WidePushout.descdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $B$ and $X$. Let $\mathrm{fs}$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $\mathrm{objs}$ applied to $j_{1}$ and $X$ such that for all elements $j$ of $J$, the composition of $\mathrm{arrows}$ applied to $j$ and $\mathrm{fs}$ applied to $j$ is equal to $f$. Then $\operatorname{desc}$ applied to $f$, $j_{1}$, $\mathrm{fs}$ and $w$ is a homomorphism of the wide pushout of $\mathrm{objs}$ and $\mathrm{arrows}$ and $X$ defined as the function that maps $w$ to $\operatorname{desc}$ applied to the wide span of $\mathrm{objs}$ and $\mathrm{arrows}$, the cocone of $f$ and $j_{1}$ and $w$.

CategoryTheory.Limits.WidePushout.headdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the unique map from the head to the pushout of arrows (from the docstring)

English

Let $\mathrm{arrows}$ be a function from elements $j$ of $J$ to homomorphisms of $B$ and $\mathrm{objs}$ applied to $j$. Then the unique map from the head to the pushout of $j$ is a homomorphism of $B$ and the wide pushout of $\mathrm{objs}$ and $\mathrm{arrows}$ defined as the function that maps $\mathrm{arrows}$ to the inclusion of the wide span of $\mathrm{objs}$ and $j$ and $\operatorname{none}$.

CategoryTheory.Limits.WidePushout.ιdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the inclusion of arrows and j1 (from the name)

English

Let $\mathrm{arrows}$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $B$ and $\mathrm{objs}$ applied to $j_{1}$. Let $j$ be an element of $J$. Then the inclusion of $j_{1}$ and $\mathrm{arrows}$ is a homomorphism of $\mathrm{objs}$ applied to $j$ and the wide pushout of $\mathrm{objs}$ and $\mathrm{arrows}$ defined as the function that maps $j$ to the inclusion of the wide span of $\mathrm{objs}$ and $j_{1}$ and $\operatorname{some}$ applied to $\mathrm{arrows}$.

CategoryTheory.Limits.WidePushoutShapedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, type

Wording

wide pushout shape of J (from the name)

English

Let $J$ be a set. Then a wide pushout shape of $J$ is an element of the function that maps $J$ to $\mathrm{Option}$ applied to $J$.

CategoryTheory.Limits.WidePushoutShape.HominductiveMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, type

Wording

homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be wide pushout shapes of $J$. Then the homomorphisms of $x$ and $x_{1}$ are a basic type.

CategoryTheory.Limits.WidePushoutShape.Hom.ctorElimTypedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from wide pushout shapes $X$ of $J$ to elements of $\mathrm{motive}$ applied to $X$, $X$ and the identity of $X$ and $\mathrm{PULift}$ applied to the set of functions from elements $j$ of $J$ to elements of $\mathrm{motive}$ applied to $\operatorname{none}$, $\operatorname{some}$ applied to $j$ and $\operatorname{init}$ applied to $j$.

CategoryTheory.Limits.WidePushoutShape.Hom.idconstructorMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the identity of X (from the name)

English

Let $X$ be a wide pushout shape of $J$. Then the identity of $X$ is a homomorphism of $X$ and $X$.

CategoryTheory.Limits.WidePushoutShape.Hom.initconstructorMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

no wording

English

Let $j$ be an element of $J$. Then $\operatorname{init}$ applied to $j$ is a homomorphism of $\operatorname{none}$ and $\operatorname{some}$ applied to $j$.

CategoryTheory.Limits.WidePushoutShape.diagramIsoWideSpandefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the diagram isomorphism wide span of F (from the name)

English

Let $F$ be a functor of the set of wide pushout shapes of $J$ and $C$. Then the diagram isomorphism wide span of $F$ is an isomorphism of $F$ and the wide span of the function that maps $j$ to the action of $F$ and $\operatorname{some}$ applied to $j$ and the function that maps $j_{1}$ to the map of $F$ and $\operatorname{init}$ applied to $j_{1}$.

CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquivdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the equivalence of h and #2 (from the name)

English

Let $\mathrm{J'}$ be a set. Let $h$ be an equivalence from $J$ to $\mathrm{J'}$. Then the equivalence of $\mathrm{J'}$ and $h$ is an equivalence of the set of wide pushout shapes of $J$ and the set of wide pushout shapes of $\mathrm{J'}$.

CategoryTheory.Limits.WidePushoutShape.mkCoconedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the cocone of f and x1 (from the name)

English

Let $f$ be a homomorphism of the action of $F$ and $\operatorname{none}$ and $X$. Let $x_{1}$ be a function from elements $j_{1}$ of $J$ to homomorphisms of the action of $F$ and $\operatorname{some}$ applied to $j_{1}$ and $X$ such that for all elements $j$ of $J$, the composition of the map of $F$ and $\operatorname{init}$ applied to $j$ and $x_{1}$ applied to $j$ is equal to $f$. Then the cocone of $f$ and $j_{1}$ is a cocone of $F$.

CategoryTheory.Limits.WidePushoutShape.uliftEquivalencedefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the lift equivalence (from the name)

English

The lift equivalence is an equivalence of the set of lift homomorphisms of $\mathrm{ULift}$ applied to the set of wide pushout shapes of $J$ and the set of wide pushout shapes of $\mathrm{ULift}$ applied to $J$ defined as the composition of the inverse of the equivalence of the set of wide pushout shapes of $J$ and the equivalence of $\mathrm{ULift}$ applied to $J$ and the inverse of the lift.

CategoryTheory.Limits.WidePushoutShape.wideSpandefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide span of objs and arrows (from the name)

English

Let $B$ be an element of $C$. Let $\mathrm{objs}$ be a function from elements of $J$ to elements of $C$. Let $\mathrm{arrows}$ be a function from elements $j$ of $J$ to homomorphisms of $B$ and $\mathrm{objs}$ applied to $j$. Then the wide span of $\mathrm{objs}$ and $j$ is a functor of the set of wide pushout shapes of $J$ and $C$.

CategoryTheory.Limits.widePullbackdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pullback of objs and arrows (from the name)

English

Let $B$ be an element of $C$. Let $\mathrm{objs}$ be a function from elements of $J$ to elements of $C$. Let $\mathrm{arrows}$ be a function from elements $j$ of $J$ to homomorphisms of $\mathrm{objs}$ applied to $j$ and $B$. Then the wide pullback of $\mathrm{objs}$ and $j$ is an element of $C$ defined as the function that maps $\mathrm{arrows}$ to the limit of the wide cospan of $\mathrm{objs}$ and $j$.

CategoryTheory.Limits.widePullbackShapeOpdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pullback shape opposite of J (from the name)

English

Let $J$ be a set. Then the wide pullback shape opposite of $J$ is a functor of the set of wide pullback shapes of $J$ and the set of opposites of the set of wide pushout shapes of $J$.

CategoryTheory.Limits.widePullbackShapeOpEquivdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the duality equivalence of J (from the docstring)

English

Let $J$ be a set. Then the duality equivalence of $J$ is an equivalence of the set of opposites of the set of wide pullback shapes of $J$ and the set of wide pushout shapes of $J$.

CategoryTheory.Limits.widePullbackShapeOpMapdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pullback shape opposite map of Y and x (from the name)

English

Let $J$ be a set. Let $X$ and $Y$ be wide pullback shapes of $J$. Let $x$ be a homomorphism of $X$ and $Y$. Then the wide pullback shape opposite map of $Y$ and $x$ is a homomorphism of $\operatorname{op}$ applied to $X$ and $\operatorname{op}$ applied to $Y$.

CategoryTheory.Limits.widePullbackShapeOpUnopdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pullback shape opposite opposite of J (from the name)

English

Let $J$ be a set. Then the wide pullback shape opposite opposite of $J$ is an isomorphism of the composition of the wide pullback shape opposite of $J$ and the wide pushout shape opposite of $J$ and the identity of the set of opposites of the set of wide pullback shapes of $J$.

CategoryTheory.Limits.widePullbackShapeUnopdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pullback shape opposite of J (from the name)

English

Let $J$ be a set. Then the wide pullback shape opposite of $J$ is a functor of the set of opposites of the set of wide pullback shapes of $J$ and the set of wide pushout shapes of $J$ defined as the left opposite of the wide pullback shape opposite of $J$.

CategoryTheory.Limits.widePullbackShapeUnopOpdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pullback shape opposite opposite of J (from the name)

English

CategoryTheory.Limits.widePushoutdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pushout of objs and arrows (from the name)

English

Let $B$ be an element of $C$. Let $\mathrm{objs}$ be a function from elements of $J$ to elements of $C$. Let $\mathrm{arrows}$ be a function from elements $j$ of $J$ to homomorphisms of $B$ and $\mathrm{objs}$ applied to $j$. Then the wide pushout of $\mathrm{objs}$ and $j$ is an element of $C$ defined as the function that maps $\mathrm{arrows}$ to the colimit of the wide span of $\mathrm{objs}$ and $j$.

CategoryTheory.Limits.widePushoutShapeOpdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pushout shape opposite of J (from the name)

English

Let $J$ be a set. Then the wide pushout shape opposite of $J$ is a functor of the set of wide pushout shapes of $J$ and the set of opposites of the set of wide pullback shapes of $J$.

CategoryTheory.Limits.widePushoutShapeOpEquivdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the duality equivalence of J (from the docstring)

English

Let $J$ be a set. Then the duality equivalence of $J$ is an equivalence of the set of opposites of the set of wide pushout shapes of $J$ and the set of wide pullback shapes of $J$.

CategoryTheory.Limits.widePushoutShapeOpMapdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pushout shape opposite map of X and x (from the name)

English

Let $J$ be a set. Let $Y$ and $X$ be wide pushout shapes of $J$. Let $x$ be a homomorphism of $Y$ and $X$. Then the wide pushout shape opposite map of $X$ and $x$ is a homomorphism of $\operatorname{op}$ applied to $Y$ and $\operatorname{op}$ applied to $X$.

CategoryTheory.Limits.widePushoutShapeOpUnopdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pushout shape opposite opposite of J (from the name)

English

Let $J$ be a set. Then the wide pushout shape opposite opposite of $J$ is an isomorphism of the composition of the wide pushout shape opposite of $J$ and the wide pullback shape opposite of $J$ and the identity of the set of opposites of the set of wide pushout shapes of $J$.

CategoryTheory.Limits.widePushoutShapeUnopdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pushout shape opposite of J (from the name)

English

Let $J$ be a set. Then the wide pushout shape opposite of $J$ is a functor of the set of opposites of the set of wide pushout shapes of $J$ and the set of wide pullback shapes of $J$ defined as the left opposite of the wide pushout shape opposite of $J$.

CategoryTheory.Limits.widePushoutShapeUnopOpdefMathlib.CategoryTheory.Limits.Shapes.WidePullbacks, function or constant

Wording

the wide pushout shape opposite opposite of J (from the name)

English

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

CategoryTheory.Limits.HasZeroMorphismsclassMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, predicate

Wording

C has zero morphisms (from the name)

English

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

CategoryTheory.Limits.IsColimit.ofIsZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

no wording

English

Let $c$ be a cocone of $F$. Assume that $F$ is a zero. Assume that $\operatorname{pt}$ applied to $c$ is a zero. Then $\operatorname{ofIsZero}$ applied to $c$, $\mathrm{hF}$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$.

CategoryTheory.Limits.IsLimit.ofIsZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

no wording

English

Let $c$ be a cone of $F$. Assume that $F$ is a zero. Assume that $\operatorname{pt}$ applied to $c$ is a zero. Then $\operatorname{ofIsZero}$ applied to $c$, $\mathrm{hF}$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

CategoryTheory.Limits.Pi.ιdefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the inclusion of f and b (from the name)

English

Let $f$ be a function from elements of $x_{2}$ to elements of $C$. Let $b$ be an element of $x_{2}$. Then the inclusion of $f$ and $b$ is a homomorphism of $f$ applied to $b$ and the product object of $f$ defined as the lift of $\operatorname{update}$ applied to the function that maps $x_{4}$ to $0$, $b$ and the identity morphism of $f$ applied to $b$.

CategoryTheory.Limits.Sigma.πdefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the projection of f and b (from the name)

English

Let $f$ be a function from elements of $x_{2}$ to elements of $C$. Let $b$ be an element of $x_{2}$. Then the projection of $f$ and $b$ is a homomorphism of the sigma object of $f$ and $f$ applied to $b$ defined as $\operatorname{desc}$ applied to $\operatorname{update}$ applied to the function that maps $x_{4}$ to $0$, $b$ and the identity morphism of $f$ applied to $b$.

CategoryTheory.Limits.coprod.fstdefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the first component of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $C$. Then the first component of $X$ and $Y$ is a homomorphism of the coproduct of $X$ and $Y$ and $X$ defined as $\operatorname{desc}$ applied to the identity morphism of $X$ and $0$.

CategoryTheory.Limits.coprod.snddefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the second component of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $C$. Then the second component of $X$ and $Y$ is a homomorphism of the coproduct of $X$ and $Y$ and $Y$ defined as $\operatorname{desc}$ applied to $0$ and the identity morphism of $Y$.

CategoryTheory.Limits.idZeroEquivIsoZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the identity zero equivalence isomorphism zero of X (from the name)

English

Let $X$ be an element of $C$. Then the identity zero equivalence isomorphism zero of $X$ is an equivalence from the proposition that the identity morphism of $X$ is equal to $0$ to the set of isomorphisms of $X$ and $0$.

CategoryTheory.Limits.imageFactorisationZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the image factorisation zero of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $C$. Then the image factorisation zero of $X$ and $Y$ is an image factorisation of $0$.

CategoryTheory.Limits.imageZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the image (from the docstring)

English

The image is an isomorphism of the categorical image of $0$ and $0$ defined as the isomorphism extension of $\operatorname{isImage}$ applied to $0$ and $\operatorname{isImage}$ applied to the image factorisation zero of $X$ and $Y$.

CategoryTheory.Limits.imageZero'defMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the image of h1 (from the docstring)

English

Assume that $\EqtMACRoH {f}{0}$. Then the image of $h_{1}$ is an isomorphism of the categorical image of $f$ and $0$ defined as the composition of $\operatorname{eqToIso}$ applied to $h_{1}$ and the image.

CategoryTheory.Limits.isIsoZeroEquivdefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

no wording

English

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{isIsoZeroEquiv}$ applied to $X$ and $Y$ is an equivalence from the proposition that $0$ is an isomorphism to the proposition that the identity morphism of $X$ is equal to $0$ and the identity morphism of $Y$ is equal to $0$.

CategoryTheory.Limits.isIsoZeroEquivIsoZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

no wording

English

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{isIsoZeroEquivIsoZero}$ applied to $X$ and $Y$ is an equivalence from the proposition that $0$ is an isomorphism to $\mathrm{Prod}$ applied to the set of isomorphisms of $X$ and $0$ and the set of isomorphisms of $Y$ and $0$.

CategoryTheory.Limits.isIsoZeroSelfEquivdefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{isIsoZeroSelfEquiv}$ applied to $X$ is an equivalence from the proposition that $0$ is an isomorphism to the proposition that the identity morphism of $X$ is equal to $0$.

CategoryTheory.Limits.isIsoZeroSelfEquivIsoZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Then $\operatorname{isIsoZeroSelfEquivIsoZero}$ applied to $X$ is an equivalence from the proposition that $0$ is an isomorphism to the set of isomorphisms of $X$ and $0$ defined as the composition of $\operatorname{isIsoZeroEquivIsoZero}$ applied to $X$ and $X$ and the subsingleton product self equivalence.

CategoryTheory.Limits.isoOfIsIsomorphicZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the isomorphism of P (from the name)

English

Assume that $X$ is isomorphic to $0$. Then the isomorphism of $P$ is an isomorphism of $X$ and $0$.

CategoryTheory.Limits.isoZeroOfEpiEqZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the isomorphism zero of h2 (from the name)

English

Assume that $\EqtMACRoH {f}{0}$. Then the isomorphism zero of $h_{2}$ is an isomorphism of $Y$ and $0$.

CategoryTheory.Limits.isoZeroOfEpiZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the isomorphism zero of h1 (from the name)

English

Assume that $0$ is an epimorphism. Then the isomorphism zero of $h_{1}$ is an isomorphism of $Y$ and $0$.

CategoryTheory.Limits.isoZeroOfMonoEqZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the isomorphism zero of h2 (from the name)

English

Assume that $\EqtMACRoH {f}{0}$. Then the isomorphism zero of $h_{2}$ is an isomorphism of $Y$ and $0$.

CategoryTheory.Limits.isoZeroOfMonoZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the isomorphism zero of h1 (from the name)

English

Assume that $0$ is a monomorphism. Then the isomorphism zero of $h_{1}$ is an isomorphism of $Y$ and $0$.

CategoryTheory.Limits.monoFactorisationZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the monomorphism factorisation zero of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $C$. Then the monomorphism factorisation zero of $X$ and $Y$ is a monomorphism factorisation of $0$.

CategoryTheory.Limits.prod.inldefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the left injection of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $C$. Then the left injection of $X$ and $Y$ is a homomorphism of $X$ and the product of $X$ and $Y$ defined as the lift of the identity morphism of $X$ and $0$.

CategoryTheory.Limits.prod.inrdefMathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms, function or constant

Wording

the right injection of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $C$. Then the right injection of $X$ and $Y$ is a homomorphism of $Y$ and the product of $X$ and $Y$ defined as the lift of $0$ and the identity morphism of $Y$.

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

CategoryTheory.Limits.HasZeroObjectclassMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, predicate

Wording

C has zero objects (from the name)

English

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

CategoryTheory.Limits.HasZeroObject.zeroIsInitialdefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

$\operatorname{zeroIsInitial}$ is an element of $\operatorname{IsInitial}$ applied to $0$ defined as $\operatorname{isInitial}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_isZero\_zero}$ applied to $C$.

CategoryTheory.Limits.HasZeroObject.zeroIsTerminaldefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

$\operatorname{zeroIsTerminal}$ is an element of $\operatorname{IsTerminal}$ applied to $0$ defined as $\operatorname{isTerminal}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_isZero\_zero}$ applied to $C$.

CategoryTheory.Limits.HasZeroObject.zeroIsoInitialdefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

$\operatorname{zeroIsoInitial}$ is an isomorphism of $0$ and $\operatorname{initial}$ applied to $C$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{zeroIsInitial}$ and $\operatorname{initialIsInitial}$.

CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitialdefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

Let $t$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then $\operatorname{zeroIsoIsInitial}$ applied to $t$ is an isomorphism of $0$ and $X$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{zeroIsInitial}$ and $t$.

CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminaldefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

Let $t$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then $\operatorname{zeroIsoIsTerminal}$ applied to $t$ is an isomorphism of $0$ and $X$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{zeroIsTerminal}$ and $t$.

CategoryTheory.Limits.HasZeroObject.zeroIsoTerminaldefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

the zero isomorphism terminal (from the name)

English

The zero isomorphism terminal is an isomorphism of $0$ and $\operatorname{terminal}$ applied to $C$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{zeroIsTerminal}$ and $\operatorname{terminalIsTerminal}$.

CategoryTheory.Limits.IsZerostructureMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, predicate

Wording

X is a zero (from the name)

English

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

CategoryTheory.Limits.IsZero.from_defMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

Assume that $X$ is a zero. Let $Y$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_Limits\_\_IsZero\_\_from\_}$ applied to $h$ and $Y$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{default}$.

CategoryTheory.Limits.IsZero.isInitialdefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

Assume that $X$ is a zero. Then $\operatorname{isInitial}$ applied to $\mathrm{hX}$ is an element of $\operatorname{IsInitial}$ applied to $X$ defined as $\operatorname{ofUnique}$ applied to $X$.

CategoryTheory.Limits.IsZero.isTerminaldefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

Assume that $X$ is a zero. Then $\operatorname{isTerminal}$ applied to $\mathrm{hX}$ is an element of $\operatorname{IsTerminal}$ applied to $X$ defined as $\operatorname{ofUnique}$ applied to $X$.

CategoryTheory.Limits.IsZero.isodefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

the isomorphism of hX and hY (from the name)

English

Assume that $X$ is a zero. Assume that $Y$ is a zero. Then the isomorphism of $\mathrm{hX}$ and $\mathrm{hY}$ is an isomorphism of $X$ and $Y$.

CategoryTheory.Limits.IsZero.isoIsInitialdefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

Assume that $X$ is a zero. Let $\mathrm{hY}$ be an element of $\operatorname{IsInitial}$ applied to $Y$. Then $\operatorname{isoIsInitial}$ applied to $\mathrm{hX}$ and $\mathrm{hY}$ is an isomorphism of $X$ and $Y$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{isInitial}$ applied to $\mathrm{hX}$ and $\mathrm{hY}$.

CategoryTheory.Limits.IsZero.isoIsTerminaldefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

Assume that $X$ is a zero. Let $\mathrm{hY}$ be an element of $\operatorname{IsTerminal}$ applied to $Y$. Then $\operatorname{isoIsTerminal}$ applied to $\mathrm{hX}$ and $\mathrm{hY}$ is an isomorphism of $X$ and $Y$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{isTerminal}$ applied to $\mathrm{hX}$ and $\mathrm{hY}$.

CategoryTheory.Limits.IsZero.isoZerodefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

the isomorphism zero of hX (from the name)

English

Assume that $X$ is a zero. Then the isomorphism zero of $\mathrm{hX}$ is an isomorphism of $X$ and $0$ defined as the isomorphism of $\mathrm{hX}$ and $\mathrm{CategoryTheory\_\_Limits\_\_isZero\_zero}$ applied to $C$.

CategoryTheory.Limits.IsZero.retractdefMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

the retract of Y and h (from the name)

English

Let $Y$ be an element of $C$. Assume that $X$ is a zero. Then the retract of $Y$ and $h$ is a retract of $X$ and $Y$.

CategoryTheory.Limits.IsZero.to_defMathlib.CategoryTheory.Limits.Shapes.ZeroObjects, function or constant

Wording

no wording

English

Assume that $X$ is a zero. Let $Y$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_Limits\_\_IsZero\_\_to\_}$ applied to $h$ and $Y$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{default}$.

Mathlib.CategoryTheory.Limits.Sifted

CategoryTheory.IsSiftedclassMathlib.CategoryTheory.Limits.Sifted, predicate

Wording

C is sifted (from the name)

English

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

CategoryTheory.IsSiftedOrEmptydefMathlib.CategoryTheory.Limits.Sifted, predicate

Wording

C is sifted or empty (from the name)

English

Let $C$ be a set. Then $C$ is sifted or empty, if the diagonal functor of $C$ is final.

Mathlib.CategoryTheory.Limits.Types.Coequalizers

CategoryTheory.Limits.Types.coequalizerColimitdefMathlib.CategoryTheory.Limits.Types.Coequalizers, function or constant

Wording

the coequalizer colimit of f and g (from the name)

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the coequalizer colimit of $f$ and $g$ is a colimit cocone of the parallel pair of $f$ and $g$.

CategoryTheory.Limits.Types.coequalizerIsodefMathlib.CategoryTheory.Limits.Types.Coequalizers, function or constant

Wording

the coequalizer isomorphism of f and g (from the name)

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the coequalizer isomorphism of $f$ and $g$ is an isomorphism of the coequalizer of $f$ and $g$ and the set of coequalizers of $\operatorname{coe}$ applied to the homomorphism of $f$ and $\operatorname{coe}$ applied to the homomorphism of $g$ defined as the isomorphism colimit cocone of the coequalizer colimit of $f$ and $g$.

Mathlib.CategoryTheory.Limits.Types.ColimitType

CategoryTheory.Functor.CoconeTypesstructureMathlib.CategoryTheory.Limits.Types.ColimitType, type

Wording

cocone type of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the cocone types of $F$ are a basic type.

CategoryTheory.Functor.CoconeTypes.IsColimitstructureMathlib.CategoryTheory.Limits.Types.ColimitType, predicate

Wording

c is a colimit (from the name)

English

Let $c$ be a cocone type of $F$. Then we can say that $c$ is a colimit.

CategoryTheory.Functor.CoconeTypes.IsColimit.descdefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

no wording

English

Assume that $c$ is a colimit. Let $\mathrm{c'}$ be a cocone type of $F$. Let $x_{1}$ be an element of $\operatorname{pt}$ applied to $c$. Then $\operatorname{desc}$ applied to $\mathrm{hc}$, $\mathrm{c'}$ and $x_{1}$ is an element of $\operatorname{pt}$ applied to $\mathrm{c'}$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_CoconeTypes\_\_IsColimit\_\_exists\_desc}$ applied to $\mathrm{hc}$ and $\mathrm{c'}$ and $x_{1}$.

CategoryTheory.Functor.CoconeTypes.IsColimit.equivdefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

the equivalence of hc (from the name)

English

Assume that $c$ is a colimit. Then the equivalence of $\mathrm{hc}$ is an equivalence from the set of colimit types of $F$ to $\operatorname{pt}$ applied to $c$ defined as the equivalence of $\operatorname{descColimitType}$ applied to $F$ and $c$ and $\operatorname{bijective}$ applied to $\mathrm{hc}$.

CategoryTheory.Functor.CoconeTypes.IsColimit.isColimitCoredefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

no wording

English

Assume that $c$ is a colimit. Then $\operatorname{isColimitCore}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimitCore}$ applied to $c$.

CategoryTheory.Functor.CoconeTypes.IsColimitCorestructureMathlib.CategoryTheory.Limits.Types.ColimitType, type

Wording

no wording

English

Let $c$ be a cocone type of $F$. Then the elements of $\operatorname{IsColimitCore}$ applied to $c$ are a basic type.

CategoryTheory.Functor.CoconeTypes.IsColimitCore.descdefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{IsColimitCore}$ applied to $c$. Let $\mathrm{c'}$ be a cocone type of $F$. Let $x_{1}$ be an element of $\operatorname{pt}$ applied to $c$. Then $\operatorname{desc}$ applied to $\mathrm{self}$, $\mathrm{c'}$ and $x_{1}$ is an element of $\operatorname{pt}$ applied to $\mathrm{c'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $\mathrm{c'}$ and $x_{1}$.

CategoryTheory.Functor.CoconeTypes.IsColimitCore.downdefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

no wording

English

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimitCore}$ applied to $c$. Then $\operatorname{down}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimitCore}$ applied to $c$.

CategoryTheory.Functor.CoconeTypes.IsColimitCore.precomposedefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

the precomposition of hc and e (from the name)

English

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimitCore}$ applied to $c$. Let $e$ be a function from elements $j_{1}$ of $J$ to equivalences from the action of $G$ and $j_{1}$ to the action of $F$ and $j_{1}$ such that for all elements $j$ and $\mathrm{j'}$ of $J$, for all homomorphisms $f$ of $j$ and $\mathrm{j'}$, $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $e$ applied to $\mathrm{j'}$ and $\operatorname{coe}$ applied to the homomorphism of the map of $G$ and $f$ is equal to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the homomorphism of the map of $F$ and $f$ and $\operatorname{coe}$ applied to $e$ applied to $j$. Then the precomposition of $\mathrm{hc}$ and $j_{1}$ is an element of $\operatorname{IsColimitCore}$ applied to the precomposition of $c$ and the function that maps $x_{1}$ to $\operatorname{coe}$ applied to $e$ applied to $x_{1}$.

CategoryTheory.Functor.CoconeTypes.postcompdefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

the postcomposition of c and x1 (from the name)

English

Let $c$ be a cocone type of $F$. Let $x_{1}$ be a function from elements of $\operatorname{pt}$ applied to $c$ to elements of $T$. Then the postcomposition of $c$ and $x_{1}$ is a cocone type of $F$.

CategoryTheory.Functor.CoconeTypes.precompdefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

the precomposition of c and G (from the name)

English

Let $c$ be a cocone type of $F$. Let $G$ be a functor of $\mathrm{J'}$ and $J$. Then the precomposition of $c$ and $G$ is a cocone type of the composition of $G$ and $F$.

CategoryTheory.Functor.CoconeTypes.precomposedefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

the precomposition of c and app (from the name)

English

Let $c$ be a cocone type of $F$. Let $\mathrm{app}$ be a function from elements $j_{1}$ of $J$ and elements of the action of $G$ and $j_{1}$ to elements of the action of $F$ and $j_{1}$ such that for all elements $j$ and $\mathrm{j'}$ of $J$, for all homomorphisms $f$ of $j$ and $\mathrm{j'}$, $\operatorname{comp}$ applied to $\mathrm{app}$ applied to $\mathrm{j'}$ and $\operatorname{coe}$ applied to the homomorphism of the map of $G$ and $f$ is equal to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the homomorphism of the map of $F$ and $f$ and $\mathrm{app}$ applied to $j$. Then the precomposition of $c$ and $j_{1}$ is a cocone type of $G$.

CategoryTheory.Functor.CoconeTypes.ptdefMathlib.CategoryTheory.Limits.Types.ColimitType, type

Wording

no wording

English

Let $\mathrm{self}$ be a cocone type of $F$. Then an element of $\operatorname{pt}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Functor.CoconeTypes.ιdefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

the inclusion of j and x1 (from the name)

English

Let $\mathrm{self}$ be a cocone type of $F$. Let $j$ be an element of $J$. Let $x_{1}$ be an element of the action of $F$ and $j$. Then the inclusion of $j$ and $x_{1}$ is an element of $\operatorname{pt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $j$ and $x_{1}$.

CategoryTheory.Functor.ColimitTypedefMathlib.CategoryTheory.Limits.Types.ColimitType, type

Wording

colimit type of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then a colimit type of $F$ is an element of the function that maps $F$ to $\mathrm{Quot}$ applied to $\operatorname{ColimitTypeRel}$ applied to $F$.

CategoryTheory.Functor.ColimitTypeReldefMathlib.CategoryTheory.Limits.Types.ColimitType, predicate

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of sets. Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $j_{1}$ to the action of $F$ and $j_{1}$. Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $j$ to the action of $F$ and $j$. Then $\operatorname{ColimitTypeRel}$ holds for $F$, $x_{1}$ and $x_{2}$, if there exists a homomorphism $f$ of $\operatorname{fst}$ applied to $x_{1}$ and $\operatorname{fst}$ applied to $x_{2}$, such that $\operatorname{snd}$ applied to $x_{2}$ is equal to $\operatorname{hom}$ applied to the map of $F$ and $f$ and $\operatorname{snd}$ applied to $x_{1}$.

CategoryTheory.Functor.coconeTypesdefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

the cocone type of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the cocone type of $F$ is a cocone type of $F$.

CategoryTheory.Functor.descColimitTypedefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of sets. Let $c$ be a cocone type of $F$. Let $x_{1}$ be a colimit type of $F$. Then $\operatorname{descColimitType}$ applied to $F$, $c$ and $x_{1}$ is an element of $\operatorname{pt}$ applied to $c$.

CategoryTheory.Functor.ιColimitTypedefMathlib.CategoryTheory.Limits.Types.ColimitType, function or constant

Wording

the inclusion colimit type of j and x1 (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Let $j$ be an element of $J$. Let $x_{1}$ be an element of the action of $F$ and $j$. Then the inclusion colimit type of $j$ and $x_{1}$ is a colimit type of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{ColimitTypeRel}$ applied to $F$ and $\operatorname{mk}$ applied to $j$ and $x_{1}$.

Mathlib.CategoryTheory.Limits.Types.Colimits

CategoryTheory.Functor.coconeTypesEquivdefMathlib.CategoryTheory.Limits.Types.Colimits, function or constant

Wording

the cocone type equivalence of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the cocone type equivalence of $F$ is an equivalence from the set of cocone types of $F$ to the set of cocones of $F$.

CategoryTheory.Limits.Types.TypeMax.colimitCoconedefMathlib.CategoryTheory.Limits.Types.Colimits, function or constant

Wording

the colimit cocone of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the colimit cocone of $F$ is a cocone of $F$ defined as $\operatorname{coconeTypesEquiv}$ applied to $F$ and the cocone type of $F$.

CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimitdefMathlib.CategoryTheory.Limits.Types.Colimits, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of sets. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.

CategoryTheory.Limits.Types.colimitCoconedefMathlib.CategoryTheory.Limits.Types.Colimits, function or constant

Wording

the colimit cocone of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the colimit cocone of $F$ is a cocone of $F$ defined as $\operatorname{coconeTypesEquiv}$ applied to $F$ and the postcomposition of the cocone type of $F$ and $\operatorname{coe}$ applied to the equivalence shrink of the set of colimit types of $F$.

CategoryTheory.Limits.Types.colimitCoconeIsColimitdefMathlib.CategoryTheory.Limits.Types.Colimits, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of sets. Then $\operatorname{colimitCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $F$.

CategoryTheory.Limits.Types.colimitEquivColimitTypedefMathlib.CategoryTheory.Limits.Types.Colimits, function or constant

Wording

the colimit equivalence colimit type of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the colimit equivalence colimit type of $F$ is an equivalence from the colimit of $F$ to the set of colimit types of $F$ defined as the composition of the equivalence of $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to $F$ and $\operatorname{colimitCoconeIsColimit}$ applied to $F$ and the inverse of the equivalence shrink of the set of colimit types of $F$.

Mathlib.CategoryTheory.Limits.Types.Coproducts

CategoryTheory.Limits.Cofan.cofanTypesdefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the cofan type of c (from the name)

English

Let $c$ be a cofan of $F$. Then the cofan type of $c$ is a cofan type of $F$.

CategoryTheory.Limits.CofanTypesdefMathlib.CategoryTheory.Limits.Types.Coproducts, type

Wording

cofan type of F (from the name)

English

Let $F$ be a function from elements of $C$ to sets. Then a cofan type of $F$ is an element of the function that maps $F$ to the set of cocone types of the functor of $F$.

CategoryTheory.Limits.CofanTypes.equivOfIsColimitdefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the equivalence of hc (from the name)

English

Assume that $c$ is a colimit. Then the equivalence of $\mathrm{hc}$ is an element of $\EquivMACRoAE {\Sigma (\lambda i . F (i))}{\operatorname{pt} (c)}$ defined as the equivalence of $\operatorname{fromSigma}$ applied to $F$ and $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_CofanTypes\_\_bijective\_fromSigma\_of\_isColimit}$ applied to $\mathrm{hc}$.

CategoryTheory.Limits.CofanTypes.fromSigmadefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

no wording

English

Let $F$ be a function from elements of $C$ to sets. Let $c$ be a cofan type of $F$. Let $x$ be an element of $\Sigma$ applied to the function that maps $i$ to $F$ applied to $i$. Then $\operatorname{fromSigma}$ applied to $F$, $c$ and $x$ is an element of $\operatorname{pt}$ applied to $c$ defined as the injection of $\operatorname{fst}$ applied to $x$ and $\operatorname{snd}$ applied to $x$.

CategoryTheory.Limits.CofanTypes.injdefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the injection of i and x (from the name)

English

Let $c$ be a cofan type of $F$. Let $i$ be an element of $C$. Let $x$ be an element of $F$ applied to $i$. Then the injection of $i$ and $x$ is an element of $\operatorname{pt}$ applied to $c$ defined as the inclusion of $\operatorname{mk}$ applied to $i$ and $x$.

CategoryTheory.Limits.CofanTypes.sigmadefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the sigma of F (from the name)

English

Let $F$ be a function from elements of $C$ to sets. Then the sigma of $F$ is a cofan type of $F$.

CategoryTheory.Limits.Types.binaryCoproductCoconedefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the binary coproduct cocone of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the binary coproduct cocone of $X$ and $Y$ is a cocone of the pair of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the type category of $\operatorname{inl}$ and the type category of $\operatorname{inr}$.

CategoryTheory.Limits.Types.binaryCoproductColimitdefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the binary coproduct colimit of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the binary coproduct colimit of $X$ and $Y$ is an element of $\operatorname{IsColimit}$ applied to the binary coproduct cocone of $X$ and $Y$.

CategoryTheory.Limits.Types.binaryCoproductColimitCoconedefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the binary coproduct colimit cocone of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the binary coproduct colimit cocone of $X$ and $Y$ is a colimit cocone of the pair of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the binary coproduct cocone of $X$ and $Y$ and the binary coproduct colimit of $X$ and $Y$.

CategoryTheory.Limits.Types.binaryCoproductIsodefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the binary coproduct isomorphism of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the binary coproduct isomorphism of $X$ and $Y$ is an isomorphism of the coproduct of $X$ and $Y$ and $\mathrm{Sum}$ applied to $X$ and $Y$ defined as the isomorphism colimit cocone of the binary coproduct colimit cocone of $X$ and $Y$.

CategoryTheory.Limits.Types.coproductColimitCoconedefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the coproduct colimit cocone of F (from the name)

English

Let $F$ be a function from elements of $J$ to sets. Then the coproduct colimit cocone of $F$ is a colimit cocone of the functor of $F$.

CategoryTheory.Limits.Types.coproductIsodefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the categorical coproduct in F (from the docstring)

English

Let $F$ be a function from elements of $J$ to sets. Then the categorical coproduct in $F$ is an isomorphism of the sigma object of $F$ and $\Sigma$ applied to the function that maps $j$ to $F$ applied to $j$ defined as the isomorphism colimit cocone of the coproduct colimit cocone of $F$.

CategoryTheory.Limits.Types.initialColimitCoconedefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the initial colimit cocone (from the name)

English

The initial colimit cocone is a colimit cocone of $\operatorname{empty}$ applied to the set of sets.

CategoryTheory.Limits.Types.initialIsodefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

the initial isomorphism (from the name)

English

The initial isomorphism is an isomorphism of $\operatorname{initial}$ applied to the set of sets and $\mathrm{PEmpty}$ defined as the isomorphism colimit cocone of the initial colimit cocone.

CategoryTheory.Limits.Types.isCoprodOfMonodefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isCoprodOfMono}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $f$ and the type category 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.Limits.Types.isInitialPEmptydefMathlib.CategoryTheory.Limits.Types.Coproducts, function or constant

Wording

no wording

English

$\operatorname{isInitialPEmpty}$ is an element of $\operatorname{IsInitial}$ applied to $\mathrm{PEmpty}$ defined as $\operatorname{ofIso}$ applied to $\operatorname{initialIsInitial}$ and the initial isomorphism.

Mathlib.CategoryTheory.Limits.Types.End

CategoryTheory.Limits.Types.coenddefMathlib.CategoryTheory.Limits.Types.End, type

Wording

coend in F (from the docstring)

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Then a coend in $F$ is an element of the function that maps $F$ to $\mathrm{Quot}$ applied to $\operatorname{coendRel}$ applied to $F$.

CategoryTheory.Limits.Types.coend.ιdefMathlib.CategoryTheory.Limits.Types.End, function or constant

Wording

the inclusion of F and j (from the name)

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Let $j$ be an element of $J$. Then the inclusion of $F$ and $j$ is a homomorphism of the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$ and the set of coends in $F$ defined as the type category of the function that maps $x_{1}$ to $\operatorname{mk}$ applied to $\operatorname{coendRel}$ applied to $F$ and $\operatorname{mk}$ applied to $j$ and $x_{1}$.

CategoryTheory.Limits.Types.coendRelinductiveMathlib.CategoryTheory.Limits.Types.End, predicate

Wording

no wording

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $j_{1}$ to the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$. Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $j$ to the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$. Then we can say that $\operatorname{coendRel}$ holds for $F$, $x_{1}$ and $x_{2}$.

CategoryTheory.Limits.Types.cowedgedefMathlib.CategoryTheory.Limits.Types.End, function or constant

Wording

the cowedge corresponding to the explicit coend in F (from the docstring)

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Then the cowedge corresponding to the explicit coend in $F$ is a cowedge of $F$.

CategoryTheory.Limits.Types.cowedgeIsColimitdefMathlib.CategoryTheory.Limits.Types.End, function or constant

Wording

the cowedge corresponding to the explicit coend in F (from the docstring)

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Then the cowedge corresponding to the explicit coend in $F$ is an element of $\operatorname{IsColimit}$ applied to the cowedge corresponding to the explicit coend in $F$.

CategoryTheory.Limits.Types.end_defMathlib.CategoryTheory.Limits.Types.End, type

Wording

end in F (from the docstring)

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Then an end in $F$ is an element of the function that maps $F$ to $\SubtypeSet {x_{1}}{\mathrm{forall} (J , \lambda i . \mathrm{forall} (J , \lambda j . \mathrm{forall} (\operatorname{Hom} (i , j), \lambda f . \EqtMACRoH {\operatorname{hom} (\operatorname{map} (\operatorname{obj} (F , \operatorname{op} (i)), f), x_{1} (i))}{\operatorname{hom} (\operatorname{NatTrans} (\operatorname{map} (F , \operatorname{op} (f)), j), x_{1} (j))})))}$.

CategoryTheory.Limits.Types.end_.πdefMathlib.CategoryTheory.Limits.Types.End, function or constant

Wording

the projection of F and j (from the name)

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Let $j$ be an element of $J$. Then the projection of $F$ and $j$ is a homomorphism of the set of ends in $F$ and the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$ defined as the type category of the function that maps $x_{1}$ to $j$.

CategoryTheory.Limits.Types.wedgedefMathlib.CategoryTheory.Limits.Types.End, function or constant

Wording

the wedge corresponding to the explicit end in F (from the docstring)

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Then the wedge corresponding to the explicit end in $F$ is a wedge of $F$.

CategoryTheory.Limits.Types.wedgeIsLimitdefMathlib.CategoryTheory.Limits.Types.End, function or constant

Wording

the wedge corresponding to the explicit end in F (from the docstring)

English

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and the set of sets. Then the wedge corresponding to the explicit end in $F$ is an element of $\operatorname{IsLimit}$ applied to the wedge corresponding to the explicit end in $F$.

Mathlib.CategoryTheory.Limits.Types.Equalizers

CategoryTheory.Limits.Types.equalizerIsodefMathlib.CategoryTheory.Limits.Types.Equalizers, function or constant

Wording

the equalizer isomorphism of g and h (from the name)

English

Let $g$ and $h$ be homomorphisms of $Y$ and $Z$. Then the equalizer isomorphism of $g$ and $h$ is an isomorphism of the equalizer of $g$ and $h$ and $\SubtypeSet {x}{(\EqtMACRoH {\operatorname{hom} (g , x)}{\operatorname{hom} (h , x)})}$ defined as the isomorphism limit cone of the equalizer limit.

CategoryTheory.Limits.Types.equalizerLimitdefMathlib.CategoryTheory.Limits.Types.Equalizers, function or constant

Wording

the equalizer limit (from the name)

English

The equalizer limit is a limit cone of the parallel pair of $g$ and $h$.

CategoryTheory.Limits.Types.typeEqualizerOfUniquedefMathlib.CategoryTheory.Limits.Types.Equalizers, function or constant

Wording

the type equalizer of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$ such that the composition of $f$ and $g$ is equal to the composition of $f$ and $h$ and for all elements $y$ of $Y$, if $\EqtMACRoH {\operatorname{hom} (g , y)}{\operatorname{hom} (h , y)}$, then $\mathrm{ExistsUnique}$ holds for the function that maps $x$ to $\EqtMACRoH {\operatorname{hom} (f , x)}{y}$. Then the type equalizer of $f$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $w$.

Mathlib.CategoryTheory.Limits.Types.Filtered

CategoryTheory.Limits.Types.FilteredColimit.ReldefMathlib.CategoryTheory.Limits.Types.Filtered, predicate

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of sets. Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $j_{1}$ to the action of $F$ and $j_{1}$. Let $y$ be an element of $\Sigma$ applied to the function that maps $j$ to the action of $F$ and $j$. Then $\operatorname{Rel}$ holds for $F$, $x_{1}$ and $y$, if there exists an element $k$ of $J$, such that there exists a homomorphism $f$ of $\operatorname{fst}$ applied to $x_{1}$ and $k$, such that there exists a homomorphism $g$ of $\operatorname{fst}$ applied to $y$ and $k$, such that $\operatorname{hom}$ applied to the map of $F$ and $f$ and $\operatorname{snd}$ applied to $x_{1}$ is equal to $\operatorname{hom}$ applied to the map of $F$ and $g$ and $\operatorname{snd}$ applied to $y$.

CategoryTheory.Limits.Types.FilteredColimit.isColimitOfdefMathlib.CategoryTheory.Limits.Types.Filtered, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.Limits.Types.FilteredColimit.isColimitOf'defMathlib.CategoryTheory.Limits.Types.Filtered, function or constant

Wording

no wording

English

generation took over the time limit

Mathlib.CategoryTheory.Limits.Types.Images

CategoryTheory.Limits.Types.ImagedefMathlib.CategoryTheory.Limits.Types.Images, type

Wording

image of f (from the name)

English

Let $f$ be a homomorphism of $x$ and $x_{1}$. Then an image of $f$ is an element of the function that maps $f$ to the set of elements of the range of $\operatorname{coe}$ applied to the homomorphism of $f$.

CategoryTheory.Limits.Types.Image.liftdefMathlib.CategoryTheory.Limits.Types.Images, function or constant

Wording

the lift of #1 (from the name)

English

Let $\mathrm{F'}$ be a monomorphism factorisation of $f$. Then the lift of $\mathrm{F'}$ is a homomorphism of the set of images of $f$ and $\operatorname{I}$ applied to $\mathrm{F'}$.

CategoryTheory.Limits.Types.Image.ιdefMathlib.CategoryTheory.Limits.Types.Images, function or constant

Wording

the inclusion of f (from the docstring)

English

Let $f$ be a homomorphism of $x$ and $x_{1}$. Then the inclusion of $f$ is a homomorphism of the set of images of $f$ and $x_{1}$ defined as the type category of the function that maps $x_{2}$ to the proposition that $x_{2}$ is an element of the range of $\operatorname{coe}$ applied to the homomorphism of $f$.

CategoryTheory.Limits.Types.isImagedefMathlib.CategoryTheory.Limits.Types.Images, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $x$ and $x_{1}$. Then $\operatorname{isImage}$ applied to $f$ is an element of $\operatorname{IsImage}$ applied to the monomorphism factorisation of $f$ defined as $\operatorname{mk}$ applied to $\operatorname{lift}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Types\_\_Image\_\_lift\_fac}$.

CategoryTheory.Limits.Types.monoFactorisationdefMathlib.CategoryTheory.Limits.Types.Images, function or constant

Wording

the monomorphism factorisation of f (from the name)

English

Let $f$ be a homomorphism of $x$ and $x_{1}$. Then the monomorphism factorisation of $f$ is a monomorphism factorisation of $f$.

Mathlib.CategoryTheory.Limits.Types.Limits

CategoryTheory.Limits.Types.Limit.mkdefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of sets. Let $x_{1}$ be a function from elements $j_{1}$ of $J$ to elements of the action of $F$ and $j_{1}$ such that for all elements $j$ and $\mathrm{j'}$ of $J$, for all homomorphisms $f$ of $j$ and $\mathrm{j'}$, $\operatorname{hom}$ applied to the map of $F$ and $f$ and $x_{1}$ applied to $j$ is equal to $x_{1}$ applied to $\mathrm{j'}$. Then $\operatorname{mk}$ applied to $F$, $j_{1}$, $x_{1}$ and $h_{1}$ is an element of the limit of $F$ defined as the function that maps $h_{1}$ to $\operatorname{symm}$ applied to the limit equivalence section of $F$, $j_{1}$ and $h_{1}$.

CategoryTheory.Limits.Types.Small.limitConedefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

the limit cone of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the limit cone of $F$ is a cone of $F$.

CategoryTheory.Limits.Types.Small.limitConeIsLimitdefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of sets. Then $\operatorname{limitConeIsLimit}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$.

CategoryTheory.Limits.Types.coneOfSectiondefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

the cone of hs (from the name)

English

Assume that $s$ is an element of the section of $F$. Then the cone of $\mathrm{hs}$ is a cone of $F$.

CategoryTheory.Limits.Types.isLimitEquivSectionsdefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

the equivalence between a limiting cone of t (from the docstring)

English

Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the equivalence between a limiting cone of $t$ is an equivalence from $\operatorname{pt}$ applied to $c$ to the set of elements of the section of $F$.

CategoryTheory.Limits.Types.limNatIsoSectionsFunctordefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

the limit (from the docstring)

English

The limit is an isomorphism of the limit and the section functor of $J$.

CategoryTheory.Limits.Types.limitConedefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

the limit cone of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the limit cone of $F$ is a cone of $F$.

CategoryTheory.Limits.Types.limitConeIsLimitdefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of sets. Then $\operatorname{limitConeIsLimit}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$.

CategoryTheory.Limits.Types.limitEquivSectionsdefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

the limit equivalence section of F (from the name)

English

Let $F$ be a functor of $J$ and the set of sets. Then the limit equivalence section of $F$ is an equivalence from the limit of $F$ to the set of elements of the section of $F$ defined as the equivalence between a limiting cone of $\operatorname{isLimit}$ applied to $F$.

CategoryTheory.Limits.Types.sectionOfConedefMathlib.CategoryTheory.Limits.Types.Limits, function or constant

Wording

the section of c and x1 (from the name)

English

Let $c$ be a cone of $F$. Let $x_{1}$ be an element of $\operatorname{pt}$ applied to $c$. Then the section of $c$ and $x_{1}$ is an element of the section of $F$ defined as the function that maps $j$ to $\operatorname{hom}$ applied to the component of the projection of $c$ and $j$ and $x_{1}$.

Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagramdefMathlib.CategoryTheory.Limits.Types.Multicoequalizer, function or constant

Wording

no wording

English

Assume that $\operatorname{MulticoequalizerDiagram}$ holds for $A$, $U$ and $V$. Then $\operatorname{isColimitOfMulticoequalizerDiagram}$ applied to $c$ is an element of $\operatorname{IsColimit}$ applied to the map of the multicofork of $c$ and the functor to type.

CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram'defMathlib.CategoryTheory.Limits.Types.Multicoequalizer, function or constant

Wording

no wording

English

Assume that $\operatorname{MulticoequalizerDiagram}$ holds for $A$, $U$ and $V$. Then $\operatorname{isColimitOfMulticoequalizerDiagram'}$ applied to $c$ is an element of $\operatorname{IsColimit}$ applied to the map of the linear order of the multicofork of $c$ and the functor to type.

Mathlib.CategoryTheory.Limits.Types.Multiequalizer

CategoryTheory.Limits.MulticospanIndex.sectionsstructureMathlib.CategoryTheory.Limits.Types.Multiequalizer, type

Wording

section of I (from the name)

English

Let $I$ be a multicospan index of $J$ and the set of sets. Then the sections of $I$ are a basic type.

CategoryTheory.Limits.MulticospanIndex.sections.valdefMathlib.CategoryTheory.Limits.Types.Multiequalizer, function or constant

Wording

the value of self and i (from the name)

English

Let $\mathrm{self}$ be a section of $I$. Let $i$ be an element of $\operatorname{L}$ applied to $J$. Then the value of $\mathrm{self}$ and $i$ is an element of the left of $I$ and $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

CategoryTheory.Limits.MulticospanIndex.sectionsEquivdefMathlib.CategoryTheory.Limits.Types.Multiequalizer, function or constant

Wording

the section equivalence of I (from the name)

English

Let $I$ be a multicospan index of $J$ and the set of sets. Then the section equivalence of $I$ is an equivalence from the set of sections of $I$ to the set of elements of the section of the multicospan of $I$.

CategoryTheory.Limits.Multifork.IsLimit.sectionsEquivdefMathlib.CategoryTheory.Limits.Types.Multiequalizer, function or constant

Wording

the section equivalence of hc (from the name)

English

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the section equivalence of $\mathrm{hc}$ is an equivalence from the set of sections of $I$ to $\operatorname{pt}$ applied to $c$.

CategoryTheory.Limits.Multifork.toSectionsdefMathlib.CategoryTheory.Limits.Types.Multiequalizer, function or constant

Wording

the section of c and x (from the name)

English

Let $c$ be a multifork of $I$. Let $x$ be an element of $\operatorname{pt}$ applied to $c$. Then the section of $c$ and $x$ is a section of $I$.

Mathlib.CategoryTheory.Limits.Types.PreservesLimit

CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquivdefMathlib.CategoryTheory.Limits.Types.PreservesLimit, function or constant

Wording

the cocone composition shrink Yoneda homomorphism equivalence of #1 (from the name)

English

Let $\mathrm{hc'}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{c'}$. Then the cocone composition shrink Yoneda homomorphism equivalence of $\mathrm{hc'}$ is an equivalence from the set of homomorphisms of $\operatorname{pt}$ applied to $\mathrm{c'}$ and $P$ to the set of elements of the section of the composition of $F$ and $P$.

CategoryTheory.Presheaf.coconePtToShrinkYonedadefMathlib.CategoryTheory.Limits.Types.PreservesLimit, function or constant

Wording

no wording

English

Let $c$ be a cone of $F$. Let $\mathrm{hc'}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{c'}$. Then $\operatorname{coconePtToShrinkYoneda}$ applied to $c$ and $\mathrm{hc'}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{c'}$ and the action of the Yoneda embedding and the opposite of $\operatorname{pt}$ applied to $c$ defined as $\operatorname{desc}$ applied to $\mathrm{hc'}$ and the map cocone of the Yoneda embedding and the cocone left opposite of $c$.

CategoryTheory.Presheaf.preservesLimitHomFamilydefMathlib.CategoryTheory.Limits.Types.PreservesLimit, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $h_{2}$ be an element of $\mathrm{PLift}$ applied to the proposition that $F$ has limits. Then $\operatorname{preservesLimitHomFamily}$ applied to $F$ and $h_{2}$ is a homomorphism of $\operatorname{preservesLimitHomFamilySrc}$ applied to $F$ and $\operatorname{preservesLimitHomFamilyTgt}$ applied to $F$ and $h_{2}$ defined as $\operatorname{coconePtToShrinkYoneda}$ applied to the cone of $F$ and $\operatorname{isColimit}$ applied to the composition of the left opposite of $F$ and the Yoneda embedding.

Mathlib.CategoryTheory.Limits.Types.Products

CategoryTheory.Limits.Types.Small.productIsodefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the categorical product in F (from the docstring)

English

Let $F$ be a function from elements of $J$ to sets. Then the categorical product in $F$ is an isomorphism of the product object of $F$ and the set of shrinks of the set of functions from elements $j$ of $J$ to elements of $F$ applied to $j$ defined as the isomorphism limit cone of the product limit cone of $F$.

CategoryTheory.Limits.Types.Small.productLimitConedefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the product limit cone of F (from the name)

English

Let $F$ be a function from elements of $J$ to sets. Then the product limit cone of $F$ is a limit cone of the functor of $F$.

CategoryTheory.Limits.Types.binaryProductConedefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the product type of X and Y (from the docstring)

English

Let $X$ and $Y$ be sets. Then the product type of $X$ and $Y$ is an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$ defined as $\operatorname{mk}$ applied to the type category of $\ProdfstMACRoZ$ and the type category of $\ProdsndMACRoAA$.

CategoryTheory.Limits.Types.binaryProductFunctordefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the binary product functor (from the name)

English

The binary product functor is a functor of the set of sets and the set of functors of the set of sets and the set of sets.

CategoryTheory.Limits.Types.binaryProductIsodefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the binary product isomorphism of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the binary product isomorphism of $X$ and $Y$ is an isomorphism of the product of $X$ and $Y$ and $\mathrm{Prod}$ applied to $X$ and $Y$ defined as the isomorphism limit cone of the binary product limit cone of $X$ and $Y$.

CategoryTheory.Limits.Types.binaryProductIsoProddefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the binary product isomorphism product (from the name)

English

The binary product isomorphism product is an isomorphism of the binary product functor and the binary product functor.

CategoryTheory.Limits.Types.binaryProductLimitdefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the product type of X and Y (from the docstring)

English

Let $X$ and $Y$ be sets. Then the product type of $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to the product type of $X$ and $Y$.

CategoryTheory.Limits.Types.binaryProductLimitConedefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the binary product limit cone of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the binary product limit cone of $X$ and $Y$ is a limit cone of the pair of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the product type of $X$ and $Y$ and the product type of $X$ and $Y$.

CategoryTheory.Limits.Types.isTerminalEquivIsoPUnitdefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\operatorname{isTerminalEquivIsoPUnit}$ applied to $X$ is an equivalence from $\operatorname{IsTerminal}$ applied to $X$ to the set of isomorphisms of $X$ and $\mathrm{PUnit}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{isTerminalEquivUnique}$ applied to $X$ and $\mathrm{uniqueEquivEquivUnique}$ applied to $X$ and $\mathrm{PUnit}$ and the equivalence equivalence isomorphism.

CategoryTheory.Limits.Types.isTerminalEquivUniquedefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\operatorname{isTerminalEquivUnique}$ applied to $X$ is an equivalence from $\operatorname{IsTerminal}$ applied to $X$ to the proposition that $X$ is unique defined as the equivalence of the function that maps $h$ to $\operatorname{unique}$ applied to the equivalence of $\operatorname{uniqueUpToIso}$ applied to $h$ and $\operatorname{isTerminalPUnit}$ and the function that maps $x$ to $\operatorname{ofIso}$ applied to $\operatorname{isTerminalPUnit}$ and the isomorphism of the equivalence of $\mathrm{PUnit}$ and $X$.

CategoryTheory.Limits.Types.isTerminalPUnitdefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

no wording

English

$\operatorname{isTerminalPUnit}$ is an element of $\operatorname{IsTerminal}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{ofUnique}$ applied to $\mathrm{PUnit}$.

CategoryTheory.Limits.Types.productIsodefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the categorical product in F (from the docstring)

English

Let $F$ be a function from elements of $J$ to sets. Then the categorical product in $F$ is an isomorphism of the product object of $F$ and the set of functions from elements $j$ of $J$ to elements of $F$ applied to $j$ defined as the isomorphism limit cone of the product limit cone of $F$.

CategoryTheory.Limits.Types.productLimitConedefMathlib.CategoryTheory.Limits.Types.Products, function or constant

Wording

the product limit cone of F (from the name)

English

Let $F$ be a function from elements of $J$ to sets. Then the product limit cone of $F$ is a limit cone of the functor of $F$.

Mathlib.CategoryTheory.Limits.Types.Pullbacks

CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObjdefMathlib.CategoryTheory.Limits.Types.Pullbacks, function or constant

Wording

the equivalence pullback object of hc (from the name)

English

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the equivalence pullback object of $\mathrm{hc}$ is an equivalence from $\operatorname{pt}$ applied to $c$ to the set of pullback objects of $f$ and $g$ defined as the equivalence of $\operatorname{conePointUniqueUpToIso}$ applied to $\mathrm{hc}$ and $\operatorname{isLimit}$ applied to the pullback limit cone of $f$ and $g$.

CategoryTheory.Limits.PullbackCone.isLimitEquivBijectivedefMathlib.CategoryTheory.Limits.Types.Pullbacks, function or constant

Wording

no wording

English

Let $c$ be a pullback cone of $f$ and $g$. Then $\operatorname{isLimitEquivBijective}$ applied to $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to the proposition that $\operatorname{toPullbackObj}$ applied to $c$ is bijective.

CategoryTheory.Limits.PullbackCone.toPullbackObjdefMathlib.CategoryTheory.Limits.Types.Pullbacks, function or constant

Wording

the pullback object of c and x (from the name)

English

Let $c$ be a pullback cone of $f$ and $g$. Let $x$ be an element of $\operatorname{pt}$ applied to $c$. Then the pullback object of $c$ and $x$ is a pullback object of $f$ and $g$ defined as $\ProdmkMACRoU {\operatorname{hom} (\operatorname{fst} (c), x)}{\operatorname{hom} (\operatorname{snd} (c), x)}$.

CategoryTheory.Limits.Types.PullbackObjdefMathlib.CategoryTheory.Limits.Types.Pullbacks, type

Wording

pullback object of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then a pullback object of $f$ and $g$ is an element of the function that maps $f$ and $g$ to $\SubtypeSet {p}{(\EqtMACRoH {\operatorname{hom} (f , \ProdfstMACRoZ {p})}{\operatorname{hom} (g , \ProdsndMACRoAA {p})})}$.

CategoryTheory.Limits.Types.pullbackConedefMathlib.CategoryTheory.Limits.Types.Pullbacks, function or constant

Wording

the pullback cone of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cone of $f$ and $g$ is a pullback cone of $f$ and $g$.

CategoryTheory.Limits.Types.pullbackIsoPullbackdefMathlib.CategoryTheory.Limits.Types.Pullbacks, function or constant

Wording

the pullback isomorphism pullback of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback isomorphism pullback of $f$ and $g$ is an isomorphism of the pullback of $f$ and $g$ and the set of pullback objects of $f$ and $g$ defined as the isomorphism of the equivalence pullback object of $\operatorname{pullbackIsPullback}$ applied to $f$ and $g$.

CategoryTheory.Limits.Types.pullbackLimitConedefMathlib.CategoryTheory.Limits.Types.Pullbacks, function or constant

Wording

the pullback limit cone of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback limit cone of $f$ and $g$ is a limit cone of the cospan of $f$ and $g$.

Mathlib.CategoryTheory.Limits.Types.Pushouts

CategoryTheory.Limits.Types.PushoutdefMathlib.CategoryTheory.Limits.Types.Pushouts, type

Wording

pushout of f and g (from the name)

English

Let $f$ be a homomorphism of $S$ and $x$. Let $g$ be a homomorphism of $S$ and $x_{1}$. Then a pushout of $f$ and $g$ is an element of the function that maps $f$ and $g$ to $\mathrm{Quot}$ applied to $\operatorname{Rel}$ applied to $f$ and $g$.

CategoryTheory.Limits.Types.Pushout'defMathlib.CategoryTheory.Limits.Types.Pushouts, type

Wording

pushout of f and g (from the name)

English

CategoryTheory.Limits.Types.Pushout.RelinductiveMathlib.CategoryTheory.Limits.Types.Pushouts, predicate

Wording

no wording

English

Let $f$ be a homomorphism of $S$ and $x$. Let $g$ be a homomorphism of $S$ and $x_{1}$. Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then we can say that $\operatorname{Rel}$ holds for $f$, $g$, $x_{2}$ and $x_{3}$.

CategoryTheory.Limits.Types.Pushout.Rel'inductiveMathlib.CategoryTheory.Limits.Types.Pushouts, predicate

Wording

no wording

English

CategoryTheory.Limits.Types.Pushout.coconedefMathlib.CategoryTheory.Limits.Types.Pushouts, function or constant

Wording

the cocone of f and g (from the name)

English

Let $f$ be a homomorphism of $S$ and $x$. Let $g$ be a homomorphism of $S$ and $x_{1}$. Then the cocone of $f$ and $g$ is a pushout cocone of $f$ and $g$ defined as $\operatorname{mk}$ applied to the left injection of $f$ and $g$, the right injection of $f$ and $g$ and $\operatorname{condition}$ applied to $f$ and $g$.

CategoryTheory.Limits.Types.Pushout.equivPushout'defMathlib.CategoryTheory.Limits.Types.Pushouts, function or constant

Wording

the obvious equivalence of f and g (from the docstring)

English

Let $f$ be a homomorphism of $S$ and $x$. Let $g$ be a homomorphism of $S$ and $x_{1}$. Then the obvious equivalence of $f$ and $g$ is an equivalence from the set of pushouts of $f$ and $g$ to the set of pushouts of $f$ and $g$.

CategoryTheory.Limits.Types.Pushout.inldefMathlib.CategoryTheory.Limits.Types.Pushouts, function or constant

Wording

the left injection of f and g (from the name)

English

Let $f$ be a homomorphism of $S$ and $x$. Let $g$ be a homomorphism of $S$ and $x_{1}$. Then the left injection of $f$ and $g$ is a homomorphism of $x$ and the set of pushouts of $f$ and $g$ defined as the type category of the function that maps $x_{2}$ to $\operatorname{mk}$ applied to $\operatorname{Rel}$ applied to $f$ and $g$ and $\operatorname{inl}$ applied to $x_{2}$.

CategoryTheory.Limits.Types.Pushout.inrdefMathlib.CategoryTheory.Limits.Types.Pushouts, function or constant

Wording

the right injection of f and g (from the name)

English

Let $f$ be a homomorphism of $S$ and $x$. Let $g$ be a homomorphism of $S$ and $x_{1}$. Then the right injection of $f$ and $g$ is a homomorphism of $x_{1}$ and the set of pushouts of $f$ and $g$ defined as the type category of the function that maps $x_{2}$ to $\operatorname{mk}$ applied to $\operatorname{Rel}$ applied to $f$ and $g$ and $\operatorname{inr}$ applied to $x_{2}$.

CategoryTheory.Limits.Types.Pushout.isColimitCoconedefMathlib.CategoryTheory.Limits.Types.Pushouts, function or constant

Wording

the cocone of f and g (from the docstring)

English

Let $f$ be a homomorphism of $S$ and $x$. Let $g$ be a homomorphism of $S$ and $x_{1}$. Then the cocone of $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $f$ and $g$.

Mathlib.CategoryTheory.Limits.Types.Yoneda

CategoryTheory.Limits.compCoyonedaSectionsEquivdefMathlib.CategoryTheory.Limits.Types.Yoneda, function or constant

Wording

the composition Coyoneda section equivalence of F and X (from the name)

English

Let $F$ be a functor of $J$ and $C$. Let $X$ be an element of $C$. Then the composition Coyoneda section equivalence of $F$ and $X$ is an equivalence from the set of elements of the section of the composition of $F$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$ to the set of homomorphisms of the action of the constant of $J$ and $X$ and $F$.

CategoryTheory.Limits.compYonedaSectionsEquivdefMathlib.CategoryTheory.Limits.Types.Yoneda, function or constant

Wording

the composition Yoneda section equivalence of F and X (from the name)

English

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $X$ be an element of $C$. Then the composition Yoneda section equivalence of $F$ and $X$ is an equivalence from the set of elements of the section of the composition of $F$ and the action of the Yoneda and $X$ to the set of homomorphisms of the action of the constant of $J$ and $\operatorname{op}$ applied to $X$ and $F$.

CategoryTheory.Limits.limitCompCoyonedaIsoConedefMathlib.CategoryTheory.Limits.Types.Yoneda, function or constant

Wording

the limit composition Coyoneda isomorphism cone of F and X (from the name)

English

Let $F$ be a functor of $J$ and $C$. Let $X$ be an element of $C$. Then the limit composition Coyoneda isomorphism cone of $F$ and $X$ is an isomorphism of the limit of the composition of $F$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and the set of homomorphisms of the action of the constant of $J$ and $X$ and $F$.

CategoryTheory.Limits.limitCompYonedaIsoCoconedefMathlib.CategoryTheory.Limits.Types.Yoneda, function or constant

Wording

the limit composition Yoneda isomorphism cocone of F and X (from the name)

English

Let $F$ be a functor of $J$ and $C$. Let $X$ be an element of $C$. Then the limit composition Yoneda isomorphism cocone of $F$ and $X$ is an isomorphism of the limit of the composition of the opposite of $F$ and the action of the Yoneda and $X$ and the set of homomorphisms of $F$ and the action of the constant of $J$ and $X$.

CategoryTheory.Limits.opCompYonedaSectionsEquivdefMathlib.CategoryTheory.Limits.Types.Yoneda, function or constant

Wording

the opposite composition Yoneda section equivalence of F and X (from the name)

English

Let $F$ be a functor of $J$ and $C$. Let $X$ be an element of $C$. Then the opposite composition Yoneda section equivalence of $F$ and $X$ is an equivalence from the set of elements of the section of the composition of the opposite of $F$ and the action of the Yoneda and $X$ to the set of homomorphisms of $F$ and the action of the constant of $J$ and $X$.

CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCoconesdefMathlib.CategoryTheory.Limits.Types.Yoneda, function or constant

Wording

the opposite homomorphism composition whiskering limit Yoneda isomorphism cocone of J and C (from the name)

English

Let $J$ and $C$ be sets. Then the opposite homomorphism composition whiskering limit Yoneda isomorphism cocone of $J$ and $C$ is an isomorphism of the composition of the opposite homomorphism of $J$ and $C$ and the composition of the left whiskering of the set of opposites of $C$ and the set of sets and the composition of the action of the right whiskering of the set of functors of the set of opposites of $J$ and the set of sets and the set of sets and the limit and the action of the left whiskering of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and the Yoneda and the cocone of $J$ and $C$.

CategoryTheory.Limits.whiskeringLimYonedaIsoConesdefMathlib.CategoryTheory.Limits.Types.Yoneda, function or constant

Wording

the whiskering limit Yoneda isomorphism cone of J and C (from the name)

English

Let $J$ and $C$ be sets. Then the whiskering limit Yoneda isomorphism cone of $J$ and $C$ is an isomorphism of the composition of the left whiskering of $C$ and the set of sets and the composition of the action of the right whiskering of the set of functors of $J$ and the set of sets and the set of sets and the limit and the action of the left whiskering of the set of functors of $C$ and the set of sets and the set of sets and the Coyoneda and the cone of $J$ and $C$.

Mathlib.CategoryTheory.Limits.Unit

CategoryTheory.Limits.punitCoconedefMathlib.CategoryTheory.Limits.Unit, function or constant

Wording

no wording

English

$\operatorname{punitCocone}$ is a cocone of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{unit}$ and the homomorphism of $\operatorname{punitExt}$ applied to $F$ and the action of the constant of $J$ and $\operatorname{mk}$ applied to $\operatorname{unit}$.

CategoryTheory.Limits.punitCoconeIsColimitdefMathlib.CategoryTheory.Limits.Unit, function or constant

Wording

no wording

English

$\operatorname{punitCoconeIsColimit}$ is an element of $\operatorname{IsColimit}$ applied to $c$.

CategoryTheory.Limits.punitConedefMathlib.CategoryTheory.Limits.Unit, function or constant

Wording

no wording

English

$\operatorname{punitCone}$ is a cone of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{unit}$ and the homomorphism of $\operatorname{punitExt}$ applied to the action of the constant of $J$ and $\operatorname{mk}$ applied to $\operatorname{unit}$ and $F$.

CategoryTheory.Limits.punitConeIsLimitdefMathlib.CategoryTheory.Limits.Unit, function or constant

Wording

no wording

English

$\operatorname{punitConeIsLimit}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

Mathlib.CategoryTheory.Limits.VanKampen

CategoryTheory.IsUniversalColimitdefMathlib.CategoryTheory.Limits.VanKampen, predicate

Wording

c is a universal colimit (from the name)

English

Let $c$ be a cocone of $F$. Then $c$ is a universal colimit, if for all functors $\mathrm{F'}$ of $J$ and $C$, for all cocones $\mathrm{c'}$ of $\mathrm{F'}$, for all homomorphisms $x_{2}$ of $\mathrm{F'}$ and $F$, for all homomorphisms $f$ of $\operatorname{pt}$ applied to $\mathrm{c'}$ and $\operatorname{pt}$ applied to $c$, if the composition of $x_{2}$ and the inclusion of $c$ is equal to the composition of the inclusion of $\mathrm{c'}$ and the map of the constant of $J$ and $f$, then if $\operatorname{Equifibered}$ holds for $\mathrm{F'}$, $F$ and $x_{2}$, then if for all elements $j$ of $J$, $\operatorname{IsPullback}$ holds for the component of the inclusion of $\mathrm{c'}$ and $j$, the component of $x_{2}$ and $j$, $f$ and the component of the inclusion of $c$ and $j$, then $\mathrm{Nonempty}$ holds for $\operatorname{IsColimit}$ applied to $\mathrm{c'}$.

CategoryTheory.IsUniversalColimit.isColimitdefMathlib.CategoryTheory.Limits.VanKampen, function or constant

Wording

no wording

English

Assume that $c$ is a universal colimit. Then $\operatorname{isColimit}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to $c$.

CategoryTheory.IsVanKampenColimitdefMathlib.CategoryTheory.Limits.VanKampen, predicate

Wording

no wording

English

Let $c$ be a cocone of $F$. Then $\operatorname{IsVanKampenColimit}$ holds for $c$, if for all functors $\mathrm{F'}$ of $J$ and $C$, for all cocones $\mathrm{c'}$ of $\mathrm{F'}$, for all homomorphisms $x_{2}$ of $\mathrm{F'}$ and $F$, for all homomorphisms $f$ of $\operatorname{pt}$ applied to $\mathrm{c'}$ and $\operatorname{pt}$ applied to $c$, if the composition of $x_{2}$ and the inclusion of $c$ is equal to the composition of the inclusion of $\mathrm{c'}$ and the map of the constant of $J$ and $f$, then if $\operatorname{Equifibered}$ holds for $\mathrm{F'}$, $F$ and $x_{2}$, then $\mathrm{Nonempty}$ holds for $\operatorname{IsColimit}$ applied to $\mathrm{c'}$, if and only if for all elements $j$ of $J$, $\operatorname{IsPullback}$ holds for the component of the inclusion of $\mathrm{c'}$ and $j$, the component of $x_{2}$ and $j$, $f$ and the component of the inclusion of $c$ and $j$.

CategoryTheory.IsVanKampenColimit.isColimitdefMathlib.CategoryTheory.Limits.VanKampen, function or constant

Wording

no wording

English

Assume that $\operatorname{IsVanKampenColimit}$ holds for $c$. Then $\operatorname{isColimit}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{isColimit}$ applied to $\operatorname{isUniversal}$ applied to $h$.

Mathlib.CategoryTheory.Limits.WeakLimits.Basic

CategoryTheory.Limits.HasWeakLimitclassMathlib.CategoryTheory.Limits.WeakLimits.Basic, predicate

Wording

F has weak limits (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then we can say that $F$ has weak limits.

CategoryTheory.Limits.HasWeakLimitsOfShapeclassMathlib.CategoryTheory.Limits.WeakLimits.Basic, predicate

Wording

no wording

English

Let $J$ and $C$ be sets. Then we can say that $\operatorname{HasWeakLimitsOfShape}$ holds for $J$ and $C$.

CategoryTheory.Limits.IsLimit.isWeakLimitdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

no wording

English

Let $l$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then $\operatorname{isWeakLimit}$ applied to $l$ is an element of $\operatorname{IsWeakLimit}$ applied to $t$ defined as $\operatorname{mk}$ applied to $\operatorname{lift}$ applied to $l$ and $\operatorname{fac}$ applied to $l$.

CategoryTheory.Limits.IsWeakLimitstructureMathlib.CategoryTheory.Limits.WeakLimits.Basic, type

Wording

no wording

English

Let $t$ be a cone of $F$. Then the elements of $\operatorname{IsWeakLimit}$ applied to $t$ are a basic type.

CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimitdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the equivalence isomorphism weak limit of i (from the name)

English

Let $i$ be an isomorphism of $r$ and $t$. Then the equivalence isomorphism weak limit of $i$ is an element of $\EquivMACRoAE {\operatorname{IsWeakLimit} (r)}{\operatorname{IsWeakLimit} (t)}$.

CategoryTheory.Limits.IsWeakLimit.liftdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the lift of self and s (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{IsWeakLimit}$ applied to $t$. Let $s$ be a cone of $F$. Then the lift of $\mathrm{self}$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $s$.

CategoryTheory.Limits.IsWeakLimit.liftConeMorphismdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the lift cone morphism of h and s (from the name)

English

Let $h$ be an element of $\operatorname{IsWeakLimit}$ applied to $t$. Let $s$ be a cone of $F$. Then the lift cone morphism of $h$ and $s$ is a homomorphism of $s$ and $t$.

CategoryTheory.Limits.IsWeakLimit.mkOfConeMorphismdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

no wording

English

Let $\mathrm{lift}$ be a function from cones $s$ of $F$ to homomorphisms of $s$ and $t$. Then $\operatorname{mkOfConeMorphism}$ applied to $s$ and $\mathrm{lift}$ is an element of $\operatorname{IsWeakLimit}$ applied to $t$.

CategoryTheory.Limits.IsWeakLimit.ofIsoWeakLimitdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

no wording

English

Let $P$ be an element of $\operatorname{IsWeakLimit}$ applied to $r$. Let $i$ be an isomorphism of $r$ and $t$. Then $\operatorname{ofIsoWeakLimit}$ applied to $P$ and $i$ is an element of $\operatorname{IsWeakLimit}$ applied to $t$.

CategoryTheory.Limits.IsWeakLimit.ofRightAdjointdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $\mathrm{left}$ and $\mathrm{right}$. Let $t$ be an element of $\operatorname{IsWeakLimit}$ applied to $c$. Then $\operatorname{ofRightAdjoint}$ applied to $\mathrm{adj}$ and $t$ is an element of $\operatorname{IsWeakLimit}$ applied to the action of $\mathrm{right}$ and $c$ defined as $\operatorname{mkOfConeMorphism}$ applied to the function that maps $s$ to $\operatorname{homEquiv}$ applied to $\mathrm{adj}$, $s$, $c$ and the lift cone morphism of $t$ and the action of $\mathrm{left}$ and $s$.

CategoryTheory.Limits.IsWeakLimit.retractOfIsLimitdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the retract of l and #2 (from the name)

English

Let $l$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $\mathrm{l'}$ be an element of $\operatorname{IsWeakLimit}$ applied to $\mathrm{t'}$. Then the retract of $l$ and $\mathrm{l'}$ is a retract of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $\mathrm{t'}$.

CategoryTheory.Limits.WeakLimitConestructureMathlib.CategoryTheory.Limits.WeakLimits.Basic, type

Wording

weak limit cone of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the weak limit cones of $F$ are a basic type.

CategoryTheory.Limits.WeakLimitCone.conedefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the cone of self (from the name)

English

Let $\mathrm{self}$ be a weak limit cone of $F$. Then the cone of $\mathrm{self}$ is a cone of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Limits.WeakLimitCone.isWeakLimitdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a weak limit cone of $F$. Then $\operatorname{isWeakLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsWeakLimit}$ applied to the cone of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Limits.WeakLimitCone.ofLimitConedefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the weak limit cone of c (from the name)

English

Let $c$ be a limit cone of $F$. Then the weak limit cone of $c$ is a weak limit cone of $F$ defined as $\operatorname{mk}$ applied to the cone of $c$ and $\operatorname{isWeakLimit}$ applied to $\operatorname{isLimit}$ applied to $c$.

CategoryTheory.Limits.getWeakLimitConedefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{getWeakLimitCone}$ applied to $F$ is a weak limit cone of $F$ defined as $\operatorname{choice}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_HasWeakLimit\_\_exists\_weakLimitCone}$.

CategoryTheory.Limits.weakLimitdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the weak limit of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the weak limit of $F$ is an element of $C$ defined as $\operatorname{pt}$ applied to the cone of $F$.

CategoryTheory.Limits.weakLimit.conedefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the cone of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the cone of $F$ is a cone of $F$ defined as the cone of $\operatorname{getWeakLimitCone}$ applied to $F$.

CategoryTheory.Limits.weakLimit.isWeakLimitdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{isWeakLimit}$ applied to $F$ is an element of $\operatorname{IsWeakLimit}$ applied to the cone of $F$ defined as $\operatorname{isWeakLimit}$ applied to $\operatorname{getWeakLimitCone}$ applied to $F$.

CategoryTheory.Limits.weakLimit.liftdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the lift of F and c (from the name)

English

Let $F$ be a functor of $J$ and $C$. Let $c$ be a cone of $F$. Then the lift of $F$ and $c$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and the weak limit of $F$ defined as the lift of $\operatorname{isWeakLimit}$ applied to $F$ and $c$.

CategoryTheory.Limits.weakLimit.πdefMathlib.CategoryTheory.Limits.WeakLimits.Basic, function or constant

Wording

the projection of F and j (from the name)

English

Let $F$ be a functor of $J$ and $C$. Let $j$ be an element of $J$. Then the projection of $F$ and $j$ is a homomorphism of the weak limit of $F$ and the action of $F$ and $j$ defined as the component of the projection of the cone of $F$ and $j$.

Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers

CategoryTheory.Limits.Fork.IsWeakLimit.mkdefMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, function or constant

Wording

no wording

English

Let $t$ be a fork of $f$ and $g$. Let $\mathrm{lift}$ be a function from forks $s_{1}$ of $f$ and $g$ to homomorphisms of $\operatorname{pt}$ applied to $s_{1}$ and $\operatorname{pt}$ applied to $t$ such that for all forks $s$ of $f$ and $g$, the composition of $\mathrm{lift}$ applied to $s$ and the inclusion of $t$ is equal to the inclusion of $s$. Then $\operatorname{mk}$ applied to $t$, $s_{1}$, $\mathrm{lift}$ and $\mathrm{fac}$ is an element of $\operatorname{IsWeakLimit}$ applied to $t$.

CategoryTheory.Limits.Fork.IsWeakLimit.mk'defMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, function or constant

Wording

no wording

English

Let $t$ be a fork of $f$ and $g$. Let $\mathrm{create}$ be a function from forks $s$ of $f$ and $g$ to elements of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_\_u3b9\_} (t))}{\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_\_u3b9\_} (s)})}$. Then $\operatorname{mk'}$ applied to $t$, $s$ and $\mathrm{create}$ is an element of $\operatorname{IsWeakLimit}$ applied to $t$.

CategoryTheory.Limits.HasWeakEqualizerdefMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, predicate

Wording

no wording

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{HasWeakEqualizer}$ holds for $f$ and $g$, if the parallel pair of $f$ and $g$ has weak limits.

CategoryTheory.Limits.HasWeakEqualizersdefMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, predicate

Wording

C has weak equalizers (from the name)

English

Let $C$ be a set. Then $C$ has weak equalizers, if $\operatorname{HasWeakLimitsOfShape}$ holds for the set of walking parallel pairs and $C$.

CategoryTheory.Limits.weakEqualizerdefMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, function or constant

Wording

the weak equalizer of f and g (from the name)

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the weak equalizer of $f$ and $g$ is an element of $C$ defined as the weak limit of the parallel pair of $f$ and $g$.

CategoryTheory.Limits.weakEqualizer.forkdefMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, function or constant

Wording

the fork of f and g (from the name)

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the fork of $f$ and $g$ is a fork of $f$ and $g$ defined as the cone of the parallel pair of $f$ and $g$.

CategoryTheory.Limits.weakEqualizer.liftdefMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, function or constant

Wording

the lift of k and h1 (from the name)

English

Let $k$ be a homomorphism of $W$ and $X$ such that the composition of $k$ and $f$ is equal to the composition of $k$ and $g$. Then the lift of $k$ and $h_{1}$ is a homomorphism of $W$ and the weak equalizer of $f$ and $g$ defined as the lift of the parallel pair of $f$ and $g$ and the inclusion of $k$ and $h_{1}$.

CategoryTheory.Limits.weakEqualizer.lift'defMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, function or constant

Wording

the lift of k and h1 (from the name)

English

Let $k$ be a homomorphism of $W$ and $X$ such that $\EqtMACRoH {\operatorname{comp} (k , f)}{\operatorname{comp} (k , g)}$. Then the lift of $k$ and $h_{1}$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_weakEqualizer\_\_\_u3b9\_} (f , g))}{k})}$ defined as the lift of $k$ and $h_{1}$.

CategoryTheory.Limits.weakEqualizer.ιdefMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, function or constant

Wording

the inclusion of f and g (from the name)

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the inclusion of $f$ and $g$ is a homomorphism of the weak equalizer of $f$ and $g$ and $X$ defined as the projection of the parallel pair of $f$ and $g$ and the zero.

CategoryTheory.Limits.weakEqualizerIsWeakEqualizerdefMathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers, function or constant

Wording

no wording

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{weakEqualizerIsWeakEqualizer}$ applied to $f$ and $g$ is an element of $\operatorname{IsWeakLimit}$ applied to the inclusion of the inclusion of $f$ and $g$ and $\operatorname{condition}$ applied to $f$ and $g$.

Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels

CategoryTheory.Limits.HasWeakKerneldefMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, predicate

Wording

f has weak kernels (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $f$ has weak kernels, if the parallel pair of $f$ and $0$ has weak limits.

CategoryTheory.Limits.HasWeakKernelsclassMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, predicate

Wording

C has weak kernels (from the name)

English

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

CategoryTheory.Limits.weakKerneldefMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, function or constant

Wording

the weak kernel of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the weak kernel of $f$ is an element of $C$ defined as the weak equalizer of $f$ and $0$.

CategoryTheory.Limits.weakKernel.liftdefMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, function or constant

Wording

the lift of f and k (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $k$ be a homomorphism of $W$ and $X$ such that the composition of $k$ and $f$ is equal to $0$. Then the lift of $f$ and $k$ is a homomorphism of $W$ and the weak kernel of $f$ defined as the lift of $\operatorname{weakKernelIsWeakKernel}$ applied to $f$ and the inclusion of $k$ and $h_{1}$.

CategoryTheory.Limits.weakKernel.lift'defMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, function or constant

Wording

the lift of f and k (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $k$ be a homomorphism of $W$ and $X$ such that $\EqtMACRoH {\operatorname{comp} (k , f)}{0}$. Then the lift of $f$ and $k$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_weakKernel\_\_\_u3b9\_} (f))}{k})}$ defined as the lift of $f$ and $k$.

CategoryTheory.Limits.weakKernel.ιdefMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, function or constant

Wording

the inclusion of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the inclusion of $f$ is a homomorphism of the weak kernel of $f$ and $X$ defined as the inclusion of $f$ and $0$.

CategoryTheory.Limits.weakKernelIsWeakKerneldefMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{weakKernelIsWeakKernel}$ applied to $f$ is an element of $\operatorname{IsWeakLimit}$ applied to the inclusion of the inclusion of $f$ and $\operatorname{trans}$ applied to $\operatorname{condition}$ applied to $f$ and $\operatorname{symm}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_comp\_zero}$.

CategoryTheory.Preadditive.isWeakLimitForkOfKernelForkdefMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, function or constant

Wording

no wording

English

Let $i$ be an element of $\operatorname{IsWeakLimit}$ applied to $c$. Then $\operatorname{isWeakLimitForkOfKernelFork}$ applied to $i$ is an element of $\operatorname{IsWeakLimit}$ applied to the fork of $c$ defined as $\operatorname{mk'}$ applied to the fork of $c$ and the function that maps $s$ to the lift of $i$ and the kernel fork of $s$.

CategoryTheory.Preadditive.isWeakLimitKernelForkOfForkdefMathlib.CategoryTheory.Limits.WeakLimits.WeakKernels, function or constant

Wording

no wording

English

Let $i$ be an element of $\operatorname{IsWeakLimit}$ applied to $c$. Then $\operatorname{isWeakLimitKernelForkOfFork}$ applied to $i$ is an element of $\operatorname{IsWeakLimit}$ applied to the kernel fork of $c$ defined as $\operatorname{mk'}$ applied to the kernel fork of $c$ and the function that maps $s$ to the lift of $i$ and the fork of $s$.

Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

CategoryTheory.Limits.HasWeakPullbackdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, predicate

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{HasWeakPullback}$ holds for $f$ and $g$, if the cospan of $f$ and $g$ has weak limits.

CategoryTheory.Limits.HasWeakPullbacksdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, predicate

Wording

C has weak pullbacks (from the name)

English

Let $C$ be a set. Then $C$ has weak pullbacks, if $\operatorname{HasWeakLimitsOfShape}$ holds for the set of walking cospans and $C$.

CategoryTheory.Limits.PullbackCone.IsWeakLimit.liftdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the lift of h and k (from the name)

English

Let $\mathrm{ht}$ be an element of $\operatorname{IsWeakLimit}$ applied to $t$. Let $h$ be a homomorphism of $W$ and $X$. Let $k$ be a homomorphism of $W$ and $Y$ such that the composition of $h$ and $f$ is equal to the composition of $k$ and $g$. Then the lift of $h$ and $k$ is a homomorphism of $W$ and $\operatorname{pt}$ applied to $t$ defined as the lift of $\mathrm{ht}$ and $\operatorname{mk}$ applied to $h$, $k$ and $w$.

CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift'defMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the lift of h and k (from the name)

English

Let $\mathrm{ht}$ be an element of $\operatorname{IsWeakLimit}$ applied to $t$. Let $h$ be a homomorphism of $W$ and $X$. Let $k$ be a homomorphism of $W$ and $Y$ such that $\EqtMACRoH {\operatorname{comp} (h , f)}{\operatorname{comp} (k , g)}$. Then the lift of $h$ and $k$ is an element of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (l , \operatorname{fst} (t))}{h}, \EqtMACRoH {\operatorname{comp} (l , \operatorname{snd} (t))}{k})}$ defined as the lift of $h$ and $k$.

CategoryTheory.Limits.PullbackCone.IsWeakLimit.mkdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

no wording

English

Assume that the composition of $\mathrm{fst}$ and $f$ is equal to the composition of $\mathrm{snd}$ and $g$. Let $\mathrm{lift}$ be a function from pullback cones $s_{2}$ of $f$ and $g$ to homomorphisms of $\operatorname{pt}$ applied to $s_{2}$ and $W$ such that for all pullback cones $s_{1}$ of $f$ and $g$, the composition of $\mathrm{lift}$ applied to $s_{1}$ and $\mathrm{fst}$ is equal to the first projection of $s_{1}$ and for all pullback cones $s$ of $f$ and $g$, the composition of $\mathrm{lift}$ applied to $s$ and $\mathrm{snd}$ is equal to the second projection of $s$. Then $\operatorname{mk}$ applied to $\mathrm{eq}$, $s_{2}$, $\mathrm{lift}$, $\mathrm{fac\_left}$ and $\mathrm{fac\_right}$ is an element of $\operatorname{IsWeakLimit}$ applied to $\operatorname{mk}$ applied to $\mathrm{fst}$, $\mathrm{snd}$ and $\mathrm{eq}$ defined as the function that maps $\mathrm{fac\_right}$ to $\operatorname{isWeakLimitAux}$ applied to $\operatorname{mk}$ applied to $\mathrm{fst}$, $\mathrm{snd}$ and $\mathrm{eq}$, $s_{2}$, $\mathrm{lift}$, $\mathrm{fac\_left}$ and $\mathrm{fac\_right}$.

CategoryTheory.Limits.PullbackCone.isWeakLimitAux'defMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

no wording

English

Let $t$ be a pullback cone of $f$ and $g$. Let $\mathrm{create}$ be a function from pullback cones $s$ of $f$ and $g$ to elements of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (l , \operatorname{fst} (t))}{\operatorname{fst} (s)}, \EqtMACRoH {\operatorname{comp} (l , \operatorname{snd} (t))}{\operatorname{snd} (s)})}$. Then $\operatorname{isWeakLimitAux'}$ applied to $t$, $s$ and $\mathrm{create}$ is an element of $\operatorname{IsWeakLimit}$ applied to $t$.

CategoryTheory.Limits.PullbackCone.mkSelfIsWeakLimitdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

no wording

English

Let $\mathrm{ht}$ be an element of $\operatorname{IsWeakLimit}$ applied to $t$. Then $\operatorname{mkSelfIsWeakLimit}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsWeakLimit}$ applied to $\operatorname{mk}$ applied to the first projection of $t$, the second projection of $t$ and $\operatorname{condition}$ applied to $t$ defined as $\operatorname{ofIsoWeakLimit}$ applied to $\mathrm{ht}$ and $\operatorname{eta}$ applied to $t$.

CategoryTheory.Limits.weakPullbackdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the weak pullback of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the weak pullback of $f$ and $g$ is an element of $C$ defined as the weak limit of the cospan of $f$ and $g$.

CategoryTheory.Limits.weakPullback.conedefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the cone of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the cone of $f$ and $g$ is a pullback cone of $f$ and $g$ defined as the cone of the cospan of $f$ and $g$.

CategoryTheory.Limits.weakPullback.fstdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the first projection of the weak pullback of f and g (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the first projection of the weak pullback of $f$ and $g$ is a homomorphism of the weak pullback of $f$ and $g$ and $X$ defined as the projection of the cospan of $f$ and $g$ and the left point of the walking cospan.

CategoryTheory.Limits.weakPullback.isWeakLimitdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{isWeakLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsWeakLimit}$ applied to the cone of $f$ and $g$ defined as $\operatorname{isWeakLimit}$ applied to the cospan of $f$ and $g$.

CategoryTheory.Limits.weakPullback.liftdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the lift of h1 and k (from the name)

English

Let $h_{1}$ be a homomorphism of $W$ and $X$. Let $k$ be a homomorphism of $W$ and $Y$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $h_{1}$ and $f$ is equal to the composition of $k$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_weakPullback\_\_lift\_\_\_auto\_1}$. Then the lift of $h_{1}$ and $k$ is a homomorphism of $W$ and the weak pullback of $f$ and $g$ defined as the lift of the cospan of $f$ and $g$ and $\operatorname{mk}$ applied to $h_{1}$, $k$ and $w$.

CategoryTheory.Limits.weakPullback.lift'defMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the lift of h1 and k (from the name)

English

Let $h_{1}$ be a homomorphism of $W$ and $X$. Let $k$ be a homomorphism of $W$ and $Y$ such that $\EqtMACRoH {\operatorname{comp} (h_{1} , f)}{\operatorname{comp} (k , g)}$. Then the lift of $h_{1}$ and $k$ is an element of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (l , \operatorname{fst} (f , g))}{h_{1}}, \EqtMACRoH {\operatorname{comp} (l , \operatorname{snd} (f , g))}{k})}$ defined as the lift of $h_{1}$ and $k$.

CategoryTheory.Limits.weakPullback.mapdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the map of x6 and x7 (from the name)

English

Let $x_{1}$ be a homomorphism of $W$ and $S$. Let $x_{2}$ be a homomorphism of $X$ and $S$. Let $x_{3}$ be a homomorphism of $Y$ and $T$. Let $x_{4}$ be a homomorphism of $Z$ and $T$. Let $x_{5}$ be a homomorphism of $W$ and $Y$. Let $x_{6}$ be a homomorphism of $X$ and $Z$. Let $x_{7}$ be a homomorphism of $S$ and $T$ such that the composition of $x_{1}$ and $x_{7}$ is equal to the composition of $x_{5}$ and $x_{3}$ and the composition of $x_{2}$ and $x_{7}$ is equal to the composition of $x_{6}$ and $x_{4}$. Then the map of $x_{6}$ and $x_{7}$ is a homomorphism of the weak pullback of $x_{1}$ and $x_{2}$ and the weak pullback of $x_{3}$ and $x_{4}$.

CategoryTheory.Limits.weakPullback.mapDescdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $S$. Let $g$ be a homomorphism of $Y$ and $S$. Let $i$ be a homomorphism of $S$ and $T$. Then $\operatorname{mapDesc}$ applied to $f$, $g$ and $i$ is a homomorphism of the weak pullback of $f$ and $g$ and the weak pullback of the composition of $f$ and $i$ and the composition of $g$ and $i$.

CategoryTheory.Limits.weakPullback.snddefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

the second projection of the weak pullback of f and g (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the second projection of the weak pullback of $f$ and $g$ is a homomorphism of the weak pullback of $f$ and $g$ and $Y$ defined as the projection of the cospan of $f$ and $g$ and the right point of the walking cospan.

CategoryTheory.Limits.weakPullbackIsWeakPullbackdefMathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{weakPullbackIsWeakPullback}$ applied to $f$ and $g$ is an element of $\operatorname{IsWeakLimit}$ applied to $\operatorname{mk}$ applied to the first projection of the weak pullback of $f$ and $g$, the second projection of the weak pullback of $f$ and $g$ and $\operatorname{condition}$ defined as $\operatorname{mkSelfIsWeakLimit}$ applied to $\operatorname{isWeakLimit}$ applied to $f$ and $g$.

Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

CategoryTheory.Functor.HasWeightedLimFlipObjdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, predicate

Wording

F has weighted limit flip objects (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then $F$ has weighted limit flip objects, if for all functors $W$ of $J$ and the set of sets, $\operatorname{HasWeightedLimit}$ holds for $W$ and $F$.

CategoryTheory.Functor.HasWeightedLimObjdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, predicate

Wording

W has weighted limit objects (from the name)

English

Let $W$ be a functor of $J$ and the set of sets. Let $C$ be a set. Then $W$ has weighted limit objects, if for all functors $F$ of $J$ and $C$, $\operatorname{HasWeightedLimit}$ holds for $W$ and $F$.

CategoryTheory.Functor.hasWeightedLimitdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and $C$. Then there is an object property of the set of functors of $J$ and the set of sets. Proof. Let $F$ be arbitrary. Let $W$ be arbitrary. By W. By F. By CategoryTheory__Limits__HasWeightedLimit.

CategoryTheory.Functor.isLimitWeightedLimConedefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted cone of W and F (from the docstring)

English

Let $W$ be a functor of $J$ and the set of sets. Let $F$ be a functor of $J$ and $C$. Then the weighted cone of $W$ and $F$ is an element of $\operatorname{IsLimit}$ applied to the weighted limit cone of $W$ and $F$ defined as $\operatorname{isLimit}$ applied to the composition of the projection of $W$ and $F$.

CategoryTheory.Functor.weightedLimConedefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit cone of W and F (from the name)

English

Let $W$ be a functor of $J$ and the set of sets. Let $F$ be a functor of $J$ and $C$. Then the weighted limit cone of $W$ and $F$ is a weighted cone of $W$ and $F$.

CategoryTheory.Functor.weightedLimFlipObjdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit flip object of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the weighted limit flip object of $F$ is a functor of the set of opposites of the set of functors of $J$ and the set of sets and $C$.

CategoryTheory.Functor.weightedLimFlipObj'defMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit flip object of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the weighted limit flip object of $F$ is a functor of the set of opposites of the set of full subcategories of $\operatorname{hasWeightedLimit}$ applied to $F$ and $C$.

CategoryTheory.Functor.weightedLimFlipObjIsodefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit flip object isomorphism of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the weighted limit flip object isomorphism of $F$ is an isomorphism of the composition of the opposite of the inverse of the inclusion of $\operatorname{hasWeightedLimit}$ applied to $F$ and the weighted limit flip object of $F$ and the weighted limit flip object of $F$ defined as the composition of the left isomorphism whisker of the opposite of the inverse of the inclusion of $\operatorname{hasWeightedLimit}$ applied to $F$ and the inverse of the weighted limit flip object isomorphism of $F$ and the composition of the inverse of the associator of the opposite of the inclusion of $\operatorname{hasWeightedLimit}$ applied to $F$ and the weighted limit flip object of $F$ and the composition of the right isomorphism whisker of the counit isomorphism of the opposite of $\operatorname{asEquivalence}$ applied to the inclusion of $\operatorname{hasWeightedLimit}$ applied to $F$ and the weighted limit flip object of $F$ and the left unitor of the weighted limit flip object of $F$.

CategoryTheory.Functor.weightedLimFlipObjIso'defMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit flip object isomorphism of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the weighted limit flip object isomorphism of $F$ is an isomorphism of the composition of the opposite of the inclusion of $\operatorname{hasWeightedLimit}$ applied to $F$ and the weighted limit flip object of $F$ and the weighted limit flip object of $F$ defined as the identity of the composition of the opposite of the inclusion of $\operatorname{hasWeightedLimit}$ applied to $F$ and the weighted limit flip object of $F$.

CategoryTheory.Functor.weightedLimFlipObjMapdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit flip object map of g and F (from the name)

English

Let $g$ be a homomorphism of $W$ and $\mathrm{W'}$. Let $F$ be a functor of $J$ and $C$. Then the weighted limit flip object map of $g$ and $F$ is a homomorphism of the weighted limit object object of $\mathrm{W'}$ and $F$ and the weighted limit object object of $W$ and $F$.

CategoryTheory.Functor.weightedLimObjdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit object of W (from the name)

English

Let $W$ be a functor of $J$ and the set of sets. Then the weighted limit object of $W$ is a functor of the set of functors of $J$ and $C$ and $C$.

CategoryTheory.Functor.weightedLimObjMapdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit object map of W and f (from the name)

English

Let $W$ be a functor of $J$ and the set of sets. Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the weighted limit object map of $W$ and $f$ is a homomorphism of the weighted limit object object of $W$ and $x_{2}$ and the weighted limit object object of $W$ and $x_{3}$ defined as the limit map of the left whisker of the projection of $W$ and $f$.

CategoryTheory.Functor.weightedLimObjObjdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit object object of W and F (from the name)

English

Let $W$ be a functor of $J$ and the set of sets. Let $F$ be a functor of $J$ and $C$. Then the weighted limit object object of $W$ and $F$ is an element of $C$ defined as the limit of the composition of the projection of $W$ and $F$.

CategoryTheory.Functor.weightedLimObjObjπdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit object object projection of F and x2 (from the name)

English

Let $W$ be a functor of $J$ and the set of sets. Let $F$ be a functor of $J$ and $C$. Let $x_{2}$ be an element of the action of $W$ and $j$. Then the weighted limit object object projection of $F$ and $x_{2}$ is a homomorphism of the weighted limit object object of $W$ and $F$ and the action of $F$ and $j$ defined as the projection from the limit object to a value of the functor of the composition of the projection of $W$ and $F$ and the element of $j$ and $x_{2}$.

CategoryTheory.Limits.HasWeightedLimitdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, predicate

Wording

no wording

English

Let $W$ be a functor of $J$ and the set of sets. Let $F$ be a functor of $J$ and $C$. Then $\operatorname{HasWeightedLimit}$ holds for $W$ and $F$, if the composition of the projection of $W$ and $F$ has limits.

CategoryTheory.Limits.WeightedConedefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, type

Wording

weighted cone of W and F (from the name)

English

Let $W$ be a functor of $J$ and the set of sets. Let $F$ be a functor of $J$ and $C$. Then a weighted cone of $W$ and $F$ is an element of the function that maps $W$ and $F$ to the set of cones of the composition of the projection of $W$ and $F$.

CategoryTheory.Limits.WeightedCone.IsLimitdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, type

Wording

no wording

English

Let $c$ be a weighted cone of $W$ and $F$. Then an element of $\operatorname{IsLimit}$ applied to $c$ is an element of the function that maps $c$ to $\operatorname{IsLimit}$ applied to $c$.

CategoryTheory.Limits.WeightedCone.IsLimit.isodefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the isomorphism of hc (from the docstring)

English

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the isomorphism of $\mathrm{hc}$ is an isomorphism of the weighted limit object object of $W$ and $F$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the composition of the projection of $W$ and $F$ and $\mathrm{hc}$.

CategoryTheory.Limits.WeightedCone.IsLimit.liftdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the lift of hc and x2 (from the name)

English

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $x_{2}$ be a function from elements $j$ of $J$ and elements of the action of $W$ and $j$ to homomorphisms of $Z$ and the action of $F$ and $j$ such that for all elements $x_{3}$ and $x_{4}$ of $J$, for all elements $x_{5}$ of the action of $W$ and $x_{3}$, for all homomorphisms $f$ of $x_{3}$ and $x_{4}$, the composition of $x_{2}$ applied to $x_{3}$ and $x_{5}$ and the map of $F$ and $f$ is equal to $x_{2}$ applied to $x_{4}$ and $\operatorname{hom}$ applied to the map of $W$ and $f$ and $x_{5}$. Then the lift of $\mathrm{hc}$ and $j$ is a homomorphism of $Z$ and $\operatorname{pt}$ applied to $c$ defined as the function that maps $h$ to the lift of $\mathrm{hc}$ and $\operatorname{mk}$ applied to $Z$, $j$ and $x_{2}$.

CategoryTheory.Limits.WeightedCone.IsLimit.mkdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

no wording

English

Let $\mathrm{lift}$ be a function from weighted cones $s_{2}$ of $W$ and $F$ to homomorphisms of $\operatorname{pt}$ applied to $s_{2}$ and $\operatorname{pt}$ applied to $c$ such that for all weighted cones $s_{1}$ of $W$ and $F$, for all elements $j_{1}$ of $J$, for all elements $x_{3}$ of the action of $W$ and $j_{1}$, the composition of $\mathrm{lift}$ applied to $s_{1}$ and the projection of $c$ and $x_{3}$ is equal to the projection of $s_{1}$ and $x_{3}$ and for all weighted cones $s$ of $W$ and $F$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $c$, if for all elements $j$ of $J$, for all elements $x_{2}$ of the action of $W$ and $j$, the composition of $m$ and the projection of $c$ and $x_{2}$ is equal to the projection of $s$ and $x_{2}$, then $\EqtMACRoH {m}{\mathrm{lift} (s)}$. Then $\operatorname{mk}$ applied to $s_{2}$, $\mathrm{lift}$, $\mathrm{fac}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

CategoryTheory.Limits.WeightedCone.coyonedadefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the Coyoneda of F and j (from the name)

English

Let $F$ be a functor of $J$ and $C$. Let $j$ be an element of $J$. Then the Coyoneda of $F$ and $j$ is a weighted cone of the action of the Coyoneda and $\operatorname{op}$ applied to $j$ and $F$.

CategoryTheory.Limits.WeightedCone.isLimitCoyonedadefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and $C$. Let $j$ be an element of $J$. Then $\operatorname{isLimitCoyoneda}$ applied to $F$ and $j$ is an element of $\operatorname{IsLimit}$ applied to the Coyoneda of $F$ and $j$.

CategoryTheory.Limits.WeightedCone.mkdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

no wording

English

Let $\mathrm{pt}$ be an element of $C$. Let $x_{2}$ be a function from elements $j$ of $J$ and elements of the action of $W$ and $j$ to homomorphisms of $\mathrm{pt}$ and the action of $F$ and $j$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{3}$ and $x_{4}$ of $J$, for all elements $x_{5}$ of the action of $W$ and $x_{3}$, for all homomorphisms $f$ of $x_{3}$ and $x_{4}$, the composition of $x_{2}$ applied to $x_{3}$ and $x_{5}$ and the map of $F$ and $f$ is equal to $x_{2}$ applied to $x_{4}$ and $\operatorname{hom}$ applied to the map of $W$ and $f$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_Limits\_\_WeightedCone\_\_mk\_\_\_auto\_1}$. Then $\operatorname{mk}$ applied to $\mathrm{pt}$, $j$, $x_{2}$ and $h$ is a weighted cone of $W$ and $F$.

CategoryTheory.Limits.WeightedCone.πdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the projection of c and x2 (from the docstring)

English

Let $c$ be a weighted cone of $W$ and $F$. Let $x_{2}$ be an element of the action of $W$ and $j$. Then the projection of $c$ and $x_{2}$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and the action of $F$ and $j$ defined as the component of the projection of $c$ and the element of $j$ and $x_{2}$.

CategoryTheory.Limits.weightedLimdefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit (from the name)

English

The weighted limit is a functor of the set of opposites of the set of functors of $J$ and the set of sets and the set of functors of the set of functors of $J$ and $C$ and $C$.

CategoryTheory.Limits.weightedLimObjCoyonedaObjIsodefMathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit, function or constant

Wording

the weighted limit object Coyoneda object isomorphism of j (from the name)

English

Let $j$ be an element of $J$. Then the weighted limit object Coyoneda object isomorphism of $j$ is an isomorphism of the weighted limit object of the action of the Coyoneda and $\operatorname{op}$ applied to $j$ and the action of the evaluation of $J$ and $C$ and $j$.

Mathlib.CategoryTheory.Limits.Yoneda

CategoryTheory.Coyoneda.colimitCoconedefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

the colimit cocone of X (from the name)

English

Let $X$ be an opposite of $C$. Then the colimit cocone of $X$ is a cocone of the action of the Coyoneda and $X$.

CategoryTheory.Coyoneda.colimitCoconeIsColimitdefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

no wording

English

Let $X$ be an opposite of $C$. Then $\operatorname{colimitCoconeIsColimit}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $X$.

CategoryTheory.Coyoneda.colimitCoyonedaIsodefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

the colimit of X (from the docstring)

English

Let $X$ be an opposite of $C$. Then the colimit of $X$ is an isomorphism of the colimit of the action of the Coyoneda and $X$ and $\mathrm{PUnit}$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the colimit cocone of $X$ and $\operatorname{colimitCoconeIsColimit}$ applied to $X$.

CategoryTheory.Limits.Cocone.isColimitYonedaEquivdefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

no wording

English

Let $c$ be a cocone of $F$. Then $\operatorname{isColimitYonedaEquiv}$ applied to $c$ is an equivalence from $\operatorname{IsColimit}$ applied to $c$ to the set of functions from elements $X$ of $C$ to elements of $\operatorname{IsLimit}$ applied to the map cone of the action of the Yoneda and $X$ and the opposite of $c$.

CategoryTheory.Limits.Cone.isLimitCoyonedaEquivdefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

no wording

English

Let $c$ be a cone of $F$. Then $\operatorname{isLimitCoyonedaEquiv}$ applied to $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to the set of functions from opposites $X$ of $C$ to elements of $\operatorname{IsLimit}$ applied to the map cone of the action of the Coyoneda and $X$ and $c$.

CategoryTheory.Limits.coneOfSectionCompCoyonedadefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

the cone of X and s (from the name)

English

Let $F$ be a functor of $J$ and $C$. Let $X$ be an opposite of $C$. Let $s$ be an element of the section of the composition of $F$ and the action of the Coyoneda and $X$. Then the cone of $X$ and $s$ is a cone of $F$.

CategoryTheory.Limits.coneOfSectionCompYonedadefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

the cone of X and s (from the name)

English

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $X$ be an element of $C$. Let $s$ be an element of the section of the composition of $F$ and the action of the Yoneda and $X$. Then the cone of $X$ and $s$ is a cone of $F$.

CategoryTheory.coyonedaJointlyReflectsLimitsdefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and $C$. Let $c$ be a cone of $F$. Let $\mathrm{hc}$ be a function from opposites $X$ of $C$ to elements of $\operatorname{IsLimit}$ applied to the map cone of the action of the Coyoneda and $X$ and $c$. Then $\operatorname{coyonedaJointlyReflectsLimits}$ applied to $F$, $c$, $X$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

CategoryTheory.yonedaJointlyReflectsLimitsdefMathlib.CategoryTheory.Limits.Yoneda, function or constant

Wording

no wording

English

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $c$ be a cone of $F$. Let $\mathrm{hc}$ be a function from elements $X$ of $C$ to elements of $\operatorname{IsLimit}$ applied to the map cone of the action of the Yoneda and $X$ and $c$. Then $\operatorname{yonedaJointlyReflectsLimits}$ applied to $F$, $c$, $X$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

Mathlib.CategoryTheory.Linear.Basic

CategoryTheory.End.linearEquivdefMathlib.CategoryTheory.Linear.Basic, function or constant

Wording

the linear equivalence (from the docstring)

English

The linear equivalence is a linear equivalence of the set of ends of $X$ and the set of homomorphisms of $X$ and $X$.

CategoryTheory.InducedCategory.homLinearEquivdefMathlib.CategoryTheory.Linear.Basic, function or constant

Wording

the linear equivalence (from the docstring)

English

The linear equivalence is a linear equivalence of the set of homomorphisms of $X$ and $Y$ and the set of homomorphisms of $F$ applied to $X$ and $F$ applied to $Y$.

CategoryTheory.LinearclassMathlib.CategoryTheory.Linear.Basic, predicate

Wording

no wording

English

Let $R$ and $C$ be sets. Then we can say that $\operatorname{Linear}$ holds for $R$ and $C$.

CategoryTheory.Linear.compdefMathlib.CategoryTheory.Linear.Basic, function or constant

Wording

the composition of Y and Z (from the name)

English

Let $X$, $Y$ and $Z$ be elements of $C$. Then the composition of $Y$ and $Z$ is a linear map of the set of homomorphisms of $X$ and $Y$ and the set of linear maps of the set of homomorphisms of $Y$ and $Z$ and the set of homomorphisms of $X$ and $Z$.

CategoryTheory.Linear.homCongrdefMathlib.CategoryTheory.Linear.Basic, function or constant

Wording

the homomorphism congruence of x4 and x5 (from the name)

English

Let $k$ be a set. Let $x_{4}$ be an isomorphism of $X$ and $Y$. Let $x_{5}$ be an isomorphism of $W$ and $Z$. Then the homomorphism congruence of $x_{4}$ and $x_{5}$ is a linear equivalence of the set of homomorphisms of $X$ and $W$ and the set of homomorphisms of $Y$ and $Z$.

CategoryTheory.Linear.leftCompdefMathlib.CategoryTheory.Linear.Basic, function or constant

Wording

the left composition of Z and f (from the name)

English

Let $R$ be a set. Let $Z$ be an element of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then the left composition of $Z$ and $f$ is a linear map of the set of homomorphisms of $Y$ and $Z$ and the set of homomorphisms of $X$ and $Z$.

CategoryTheory.Linear.rightCompdefMathlib.CategoryTheory.Linear.Basic, function or constant

Wording

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

English

Let $R$ be a set. Let $X$ be an element of $C$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the right composition of $X$ and $g$ is a linear map of the set of homomorphisms of $X$ and $Y$ and the set of homomorphisms of $X$ and $Z$.

Mathlib.CategoryTheory.Linear.FunctorCategory

CategoryTheory.NatTrans.appLinearMapdefMathlib.CategoryTheory.Linear.FunctorCategory, function or constant

Wording

the application linear map of X (from the name)

English

Let $X$ be an element of $C$. Then the application linear map of $X$ is a linear map of the set of homomorphisms of $F$ and $G$ and the set of homomorphisms of the action of $F$ and $X$ and the action of $G$ and $X$.

Mathlib.CategoryTheory.Linear.LinearFunctor

CategoryTheory.Functor.LinearclassMathlib.CategoryTheory.Linear.LinearFunctor, predicate

Wording

F is linear (from the name)

English

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

CategoryTheory.Functor.mapLinearMapdefMathlib.CategoryTheory.Linear.LinearFunctor, function or constant

Wording

the map linear map of R and F (from the name)

English

Let $R$ be a set. Let $F$ be a functor of $C$ and $D$. Then the map linear map of $R$ and $F$ is a linear map of the set of homomorphisms of $X$ and $Y$ and the set of homomorphisms of the action of $F$ and $X$ and the action of $F$ and $Y$.

Mathlib.CategoryTheory.Linear.Yoneda

CategoryTheory.linearCoyonedadefMathlib.CategoryTheory.Linear.Yoneda, function or constant

Wording

the linear Coyoneda of R and C (from the name)

English

Let $R$ and $C$ be sets. Then the linear Coyoneda of $R$ and $C$ is a functor of the set of opposites of $C$ and the set of functors of $C$ and the set of module categories of $R$.

CategoryTheory.linearYonedadefMathlib.CategoryTheory.Linear.Yoneda, function or constant

Wording

the linear Yoneda of R and C (from the name)

English

Let $R$ and $C$ be sets. Then the linear Yoneda of $R$ and $C$ is a functor of $C$ and the set of functors of the set of opposites of $C$ and the set of module categories of $R$.

Mathlib.CategoryTheory.Localization.Adjunction

CategoryTheory.Adjunction.localizationdefMathlib.CategoryTheory.Localization.Adjunction, function or constant

Wording

the localization of #6 and #7 (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $G$ and $F$. Let $x_{8}$ be a functor of $x$ and $x_{2}$. Let $x_{9}$ be a morphism property of $x$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{3}$. Let $x_{11}$ be a morphism property of $x_{1}$. Let $\mathrm{G'}$ be a functor of $x_{2}$ and $x_{3}$. Let $\mathrm{F'}$ be a functor of $x_{3}$ and $x_{2}$. Then the localization of $\mathrm{G'}$ and $\mathrm{F'}$ is an adjunction of $\mathrm{G'}$ and $\mathrm{F'}$.

Mathlib.CategoryTheory.Localization.Bifunctor

CategoryTheory.Localization.Lifting₂classMathlib.CategoryTheory.Localization.Bifunctor, predicate

Wording

no wording

English

CategoryTheory.Localization.Lifting₂.isodefMathlib.CategoryTheory.Localization.Bifunctor, function or constant

Wording

the isomorphism of F and #6 (from the name)

English

Let $x_{9}$ be a functor of $x$ and $x_{2}$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{3}$. Let $x_{11}$ be a morphism property of $x$. Let $x_{12}$ be a morphism property of $x_{1}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $E$. Let $\mathrm{F'}$ be a functor of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Then the isomorphism of $F$ and $\mathrm{F'}$ is an isomorphism of the action of the action of the action of the left whiskering of $E$ and $x_{9}$ and $x_{10}$ and $\mathrm{F'}$ and $F$ defined as $\mathrm{CategoryTheory\_\_Localization\_\_Lifting\_u2082\_\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Localization.lift₂defMathlib.CategoryTheory.Localization.Bifunctor, function or constant

Wording

the lift of x11 and x12 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $E$ such that $\mathrm{CategoryTheory\_\_MorphismProperty\_\_IsInvertedBy\_u2082\_}$ holds for $x_{9}$, $x_{10}$ and $F$. Let $x_{11}$ be a functor of $x$ and $x_{2}$. Let $x_{12}$ be a functor of $x_{1}$ and $x_{3}$. Then the lift of $x_{11}$ and $x_{12}$ is a functor of $x_{2}$ and the set of functors of $x_{3}$ and $E$ defined as the action of the curry and the lift of the action of $\operatorname{uncurry}$ and $F$ and the product of $x_{11}$ and $x_{12}$.

CategoryTheory.Localization.lift₂NatIsodefMathlib.CategoryTheory.Localization.Bifunctor, function or constant

Wording

the lift natural isomorphism of x16 and e (from the name)

English

Let $x_{9}$ be a functor of $x$ and $x_{2}$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{3}$. Let $x_{11}$ be a morphism property of $x$. Let $x_{12}$ be a morphism property of $x_{1}$. Let $x_{13}$ and $x_{14}$ be functors of $x$ and the set of functors of $x_{1}$ and $E$. Let $x_{15}$ and $x_{16}$ be functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Let $e$ be an isomorphism of $x_{13}$ and $x_{14}$. Then the lift natural isomorphism of $x_{16}$ and $e$ is an isomorphism of $x_{15}$ and $x_{16}$.

CategoryTheory.Localization.lift₂NatTransdefMathlib.CategoryTheory.Localization.Bifunctor, function or constant

Wording

the lift natural transformation of x16 and x19 (from the name)

English

Let $x_{9}$ be a functor of $x$ and $x_{2}$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{3}$. Let $x_{11}$ be a morphism property of $x$. Let $x_{12}$ be a morphism property of $x_{1}$. Let $x_{13}$ and $x_{14}$ be functors of $x$ and the set of functors of $x_{1}$ and $E$. Let $x_{15}$ and $x_{16}$ be functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Let $x_{19}$ be a homomorphism of $x_{13}$ and $x_{14}$. Then the lift natural transformation of $x_{16}$ and $x_{19}$ is a homomorphism of $x_{15}$ and $x_{16}$ defined as the preimage of $\operatorname{fullyFaithfulUncurry}$ and the lift natural transformation of the action of $\operatorname{uncurry}$ and $x_{16}$ and the map of $\operatorname{uncurry}$ and $x_{19}$.

CategoryTheory.MorphismProperty.IsInvertedBy₂defMathlib.CategoryTheory.Localization.Bifunctor, predicate

Wording

no wording

English

Let $x_{5}$ be a morphism property of $x$. Let $x_{6}$ be a morphism property of $x_{1}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $E$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_IsInvertedBy\_u2082\_}$ holds for $x_{5}$, $x_{6}$ and $F$, if $\operatorname{IsInvertedBy}$ holds for the product of $x_{5}$ and $x_{6}$ and the action of $\operatorname{uncurry}$ and $F$.

Mathlib.CategoryTheory.Localization.Bousfield

CategoryTheory.ObjectProperty.isColocaldefMathlib.CategoryTheory.Localization.Bousfield, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Then there is a morphism property of $C$. Proof. Let $P$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $g$ be arbitrary. By C. Let $X$ be arbitrary. By X. By P. Let $f$ be arbitrary. By f. By g. By CategoryTheory__CategoryStruct__comp. By Function__Bijective. By if. By forall.

CategoryTheory.ObjectProperty.isColocal.homEquivdefMathlib.CategoryTheory.Localization.Bousfield, function or constant

Wording

the homomorphism equivalence of X (from the name)

English

Assume that $\operatorname{isColocal}$ holds for $P$, $Y$, $Z$ and $g$. Let $X$ be an element of $C$ such that $P$ holds for $X$. Then the homomorphism equivalence of $X$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of $X$ and $Z$ defined as the equivalence of the function that maps $f$ to the composition of $f$ and $g$ and $\mathrm{hg}$ applied to $X$ and $\mathrm{hX}$.

CategoryTheory.ObjectProperty.isLocaldefMathlib.CategoryTheory.Localization.Bousfield, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Then there is a morphism property of $C$. Proof. Let $P$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $f$ be arbitrary. By C. Let $Z$ be arbitrary. By Z. By P. Let $g$ be arbitrary. By f. By g. By CategoryTheory__CategoryStruct__comp. By Function__Bijective. By if. By forall.

CategoryTheory.ObjectProperty.isLocal.homEquivdefMathlib.CategoryTheory.Localization.Bousfield, function or constant

Wording

the homomorphism equivalence of Z (from the name)

English

Assume that $\operatorname{isLocal}$ holds for $P$, $X$, $Y$ and $f$. Let $Z$ be an element of $C$ such that $P$ holds for $Z$. Then the homomorphism equivalence of $Z$ is an equivalence from the set of homomorphisms of $Y$ and $Z$ to the set of homomorphisms of $X$ and $Z$ defined as the equivalence of the function that maps $g$ to the composition of $f$ and $g$ and $\mathrm{hf}$ applied to $Z$ and $\mathrm{hZ}$.

Mathlib.CategoryTheory.Localization.CalculusOfFractions

CategoryTheory.MorphismProperty.HasLeftCalculusOfFractionsclassMathlib.CategoryTheory.Localization.CalculusOfFractions, predicate

Wording

W has a left calculus of fraction (from the name)

English

Let $W$ be a morphism property of $C$. Then we can say that $W$ has a left calculus of fraction.

CategoryTheory.MorphismProperty.HasRightCalculusOfFractionsclassMathlib.CategoryTheory.Localization.CalculusOfFractions, predicate

Wording

W has a right calculus of fraction (from the name)

English

Let $W$ be a morphism property of $C$. Then we can say that $W$ has a right calculus of fraction.

CategoryTheory.MorphismProperty.LeftFractionstructureMathlib.CategoryTheory.Localization.CalculusOfFractions, type

Wording

left fraction of X and Y (from the name)

English

Let $W$ be a morphism property of $C$. Let $X$ and $Y$ be elements of $C$. Then the left fractions of $X$ and $Y$ are a basic type.

CategoryTheory.MorphismProperty.LeftFraction.LocalizationdefMathlib.CategoryTheory.Localization.CalculusOfFractions, type

Wording

localization of x1 (from the name)

English

Let $x_{1}$ be a morphism property of $C$. Then a localization of $x_{1}$ is an element of the function that maps $x_{1}$ to $C$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.HomdefMathlib.CategoryTheory.Localization.CalculusOfFractions, type

Wording

homomorphism of X and Y (from the name)

English

Let $W$ be a morphism property of $C$. Let $X$ and $Y$ be elements of $C$. Then a homomorphism of $X$ and $Y$ is an element of the function that maps $W$, $X$ and $Y$ to $\mathrm{Quot}$ applied to $\operatorname{LeftFractionRel}$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.compdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the composition of x1 and x2 (from the name)

English

Let $x_{1}$ be a homomorphism of $X$ and $Y$. Let $x_{2}$ be a homomorphism of $Y$ and $Z$. Then the composition of $x_{1}$ and $x_{2}$ is a homomorphism of $X$ and $Z$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mapdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the map of f and F (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $F$ be a functor of $C$ and $E$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $F$. Then the map of $f$ and $F$ is a homomorphism of the action of $F$ and $X$ and the action of $F$ and $Y$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mkdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $z$ be a left fraction of $X$ and $Y$. Then $\operatorname{mk}$ applied to $z$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{LeftFractionRel}$ and $z$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.QdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then $\operatorname{Q}$ applied to $W$ is a functor of $C$ and the set of localizations of $W$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.QinvdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $s$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $s$. Then $\operatorname{Qinv}$ applied to $s$ and $\mathrm{hs}$ is a homomorphism of the action of $\operatorname{Q}$ applied to $W$ and $Y$ and the action of $\operatorname{Q}$ applied to $W$ and $X$ defined as the homomorphism of the left fraction of $s$ and $\mathrm{hs}$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.QisodefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $s$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $s$. Then $\operatorname{Qiso}$ applied to $s$ and $\mathrm{hs}$ is an isomorphism of the action of $\operatorname{Q}$ applied to $W$ and $X$ and the action of $\operatorname{Q}$ applied to $W$ and $Y$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.liftdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the lift of F and hF (from the name)

English

Let $F$ be a functor of $C$ and $E$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $F$. Then the lift of $F$ and $\mathrm{hF}$ is a functor of the set of localizations of $W$ and $E$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.homMkdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a left fraction of $X$ and $Y$. Then the homomorphism of $f$ is a homomorphism of the action of $\operatorname{Q}$ applied to $W$ and $X$ and the action of $\operatorname{Q}$ applied to $W$ and $Y$ defined as $\operatorname{mk}$ applied to $f$.

CategoryTheory.MorphismProperty.LeftFraction.Localization.strictUniversalPropertyFixedTargetdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the strict universal property fixed target of W and E (from the name)

English

Let $W$ be a morphism property of $C$. Let $E$ be a set. Then the strict universal property fixed target of $W$ and $E$ is a strict universal property fixed target of $W$ and $E$ defined as $\operatorname{mk}$ applied to $\operatorname{inverts}$ applied to $W$, $\operatorname{lift}$, $\operatorname{fac}$ and $\operatorname{uniq}$.

CategoryTheory.MorphismProperty.LeftFraction.Y'defMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\operatorname{Y'}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction.fdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\operatorname{Y'}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction.mapdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the map of x2 and L (from the name)

English

Let $x_{2}$ be a left fraction of $X$ and $Y$. Let $L$ be a functor of $C$ and $D$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $L$. Then the map of $x_{2}$ and $L$ is a homomorphism of the action of $L$ and $X$ and the action of $L$ and $Y$ defined as the composition of the map of $L$ and $\operatorname{f}$ applied to $x_{2}$ and the inverse of the map of $L$ and $\operatorname{s}$ applied to $x_{2}$.

CategoryTheory.MorphismProperty.LeftFraction.ofHomdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the left fraction of W and f (from the name)

English

Let $W$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then the left fraction of $W$ and $f$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $f$, the identity morphism of $Y$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_id\_mem}$ applied to $W$ and $Y$.

CategoryTheory.MorphismProperty.LeftFraction.ofInvdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the left fraction of s and hs (from the name)

English

Let $s$ be a homomorphism of $Y$ and $X$ such that $W$ holds for $Y$, $X$ and $s$. Then the left fraction of $s$ and $\mathrm{hs}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the identity morphism of $X$, $s$ and $\mathrm{hs}$.

CategoryTheory.MorphismProperty.LeftFraction.opdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then the opposite of $x_{1}$ is a right fraction of $\operatorname{op}$ applied to $Y$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{mk}$ applied to the opposite in $\operatorname{s}$ applied to $x_{1}$, $\operatorname{hs}$ applied to $x_{1}$ and the opposite in $\operatorname{f}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction.rightFractiondefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the right fraction of x1 (from the name)

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then the right fraction of $x_{1}$ is a right fraction of $X$ and $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_\_exists\_rightFraction}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction.sdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a homomorphism of $Y$ and $\operatorname{Y'}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction.unopdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then the opposite of $x_{1}$ is a right fraction of the opposite of $Y$ and the opposite of $X$.

CategoryTheory.MorphismProperty.LeftFractionReldefMathlib.CategoryTheory.Localization.CalculusOfFractions, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be left fractions of $X$ and $Y$. Then $\operatorname{LeftFractionRel}$ holds for $x_{1}$ and $x_{2}$, if there exists an element $Z$ of $C$, such that there exists a homomorphism $x_{3}$ of $\operatorname{Y'}$ applied to $x_{1}$ and $Z$, such that there exists a homomorphism $x_{4}$ of $\operatorname{Y'}$ applied to $x_{2}$ and $Z$, such that there exists an element $h$ of $\mathrm{Eqt}$ applied to the composition of $\operatorname{s}$ applied to $x_{1}$ and $x_{3}$ and the composition of $\operatorname{s}$ applied to $x_{2}$ and $x_{4}$, such that there exists an element $h_{1}$ of $\mathrm{Eqt}$ applied to the composition of $\operatorname{f}$ applied to $x_{1}$ and $x_{3}$ and the composition of $\operatorname{f}$ applied to $x_{2}$ and $x_{4}$, such that $W$ holds for $Y$, $Z$ and the composition of $\operatorname{s}$ applied to $x_{1}$ and $x_{3}$.

CategoryTheory.MorphismProperty.RightFractionstructureMathlib.CategoryTheory.Localization.CalculusOfFractions, type

Wording

right fraction of X and Y (from the name)

English

Let $W$ be a morphism property of $C$. Let $X$ and $Y$ be elements of $C$. Then the right fractions of $X$ and $Y$ are a basic type.

CategoryTheory.MorphismProperty.RightFraction.X'defMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right fraction of $X$ and $Y$. Then $\operatorname{X'}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.RightFraction.fdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right fraction of $X$ and $Y$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{X'}$ applied to $\mathrm{self}$ and $Y$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.RightFraction.leftFractiondefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the left fraction of x1 (from the name)

English

Let $x_{1}$ be a right fraction of $X$ and $Y$. Then the left fraction of $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_\_exists\_leftFraction}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.RightFraction.mapdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the map of x2 and L (from the name)

English

Let $x_{2}$ be a right fraction of $X$ and $Y$. Let $L$ be a functor of $C$ and $D$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $L$. Then the map of $x_{2}$ and $L$ is a homomorphism of the action of $L$ and $X$ and the action of $L$ and $Y$ defined as the composition of the inverse of the map of $L$ and $\operatorname{s}$ applied to $x_{2}$ and the map of $L$ and $\operatorname{f}$ applied to $x_{2}$.

CategoryTheory.MorphismProperty.RightFraction.ofHomdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the right fraction of W and f (from the name)

English

Let $W$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then the right fraction of $W$ and $f$ is a right fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the identity morphism of $X$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_id\_mem}$ applied to $W$ and $X$ and $f$.

CategoryTheory.MorphismProperty.RightFraction.ofInvdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the right fraction of s and hs (from the name)

English

Let $s$ be a homomorphism of $Y$ and $X$ such that $W$ holds for $Y$, $X$ and $s$. Then the right fraction of $s$ and $\mathrm{hs}$ is a right fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $s$, $\mathrm{hs}$ and the identity morphism of $Y$.

CategoryTheory.MorphismProperty.RightFraction.opdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a right fraction of $X$ and $Y$. Then the opposite of $x_{1}$ is a left fraction of $\operatorname{op}$ applied to $Y$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{mk}$ applied to the opposite in $\operatorname{f}$ applied to $x_{1}$, the opposite in $\operatorname{s}$ applied to $x_{1}$ and $\operatorname{hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.RightFraction.sdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right fraction of $X$ and $Y$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{X'}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.RightFraction.unopdefMathlib.CategoryTheory.Localization.CalculusOfFractions, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a right fraction of $X$ and $Y$. Then the opposite of $x_{1}$ is a left fraction of the opposite of $Y$ and the opposite of $X$.

CategoryTheory.MorphismProperty.RightFractionReldefMathlib.CategoryTheory.Localization.CalculusOfFractions, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be right fractions of $X$ and $Y$. Then $\operatorname{RightFractionRel}$ holds for $x_{1}$ and $x_{2}$, if there exists an element $Z$ of $C$, such that there exists a homomorphism $x_{3}$ of $Z$ and $\operatorname{X'}$ applied to $x_{1}$, such that there exists a homomorphism $x_{4}$ of $Z$ and $\operatorname{X'}$ applied to $x_{2}$, such that there exists an element $h$ of $\mathrm{Eqt}$ applied to the composition of $x_{3}$ and $\operatorname{s}$ applied to $x_{1}$ and the composition of $x_{4}$ and $\operatorname{s}$ applied to $x_{2}$, such that there exists an element $h_{1}$ of $\mathrm{Eqt}$ applied to the composition of $x_{3}$ and $\operatorname{f}$ applied to $x_{1}$ and the composition of $x_{4}$ and $\operatorname{f}$ applied to $x_{2}$, such that $W$ holds for $Z$, $X$ and the composition of $x_{3}$ and $\operatorname{s}$ applied to $x_{1}$.

Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

CategoryTheory.MorphismProperty.LeftFraction₂structureMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, type

Wording

left fraction of X and Y (from the name)

English

Let $W$ be a morphism property of $C$. Let $X$ and $Y$ be elements of $C$. Then the left fractions of $X$ and $Y$ are a basic type.

CategoryTheory.MorphismProperty.LeftFraction₂.Y'defMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_Y'}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₂.fdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_Y'}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_proj1}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₂.f'defMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f'}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_Y'}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_proj2}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₂.fstdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

the first left fraction of x1 (from the docstring)

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then the first left fraction of $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction₂.sdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_s}$ applied to $\mathrm{self}$ is a homomorphism of $Y$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_Y'}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_proj3}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₂.snddefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

the second left fraction of x1 (from the docstring)

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then the second left fraction of $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f'}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction₂.symmdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

the inverse of x1 (from the name)

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then the inverse of $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f'}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction₂ReldefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be left fractions of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_Rel}$ holds for $x_{1}$ and $x_{2}$, if there exists an element $Z$ of $C$, such that there exists a homomorphism $x_{3}$ of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_Y'}$ applied to $x_{1}$ and $Z$, such that there exists a homomorphism $x_{4}$ of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_Y'}$ applied to $x_{2}$ and $Z$, such that there exists an element $h$ of $\mathrm{Eqt}$ applied to the composition of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_s}$ applied to $x_{1}$ and $x_{3}$ and the composition of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_s}$ applied to $x_{2}$ and $x_{4}$, such that there exists an element $h_{1}$ of $\mathrm{Eqt}$ applied to the composition of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f}$ applied to $x_{1}$ and $x_{3}$ and the composition of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f}$ applied to $x_{2}$ and $x_{4}$, such that there exists an element $h_{2}$ of $\mathrm{Eqt}$ applied to the composition of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f'}$ applied to $x_{1}$ and $x_{3}$ and the composition of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_f'}$ applied to $x_{2}$ and $x_{4}$, such that $W$ holds for $Y$, $Z$ and the composition of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_s}$ applied to $x_{1}$ and $x_{3}$.

CategoryTheory.MorphismProperty.LeftFraction₃structureMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, type

Wording

left fraction of X and Y (from the name)

English

Let $W$ be a morphism property of $C$. Let $X$ and $Y$ be elements of $C$. Then the left fractions of $X$ and $Y$ are a basic type.

CategoryTheory.MorphismProperty.LeftFraction₃.Y'defMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_Y'}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₃.fdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_Y'}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_proj1}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₃.f'defMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f'}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_Y'}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_proj2}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₃.f''defMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f''}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_Y'}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_proj3}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₃.forgetFstdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_forgetFst}$ applied to $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f'}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f''}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction₃.forgetSnddefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_forgetSnd}$ applied to $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f''}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction₃.forgetThddefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_forgetThd}$ applied to $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2082\_\_\_mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f'}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction₃.fstdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

the first left fraction of x1 (from the docstring)

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then the first left fraction of $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction₃.sdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_s}$ applied to $\mathrm{self}$ is a homomorphism of $Y$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_Y'}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_proj4}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.LeftFraction₃.snddefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

the second left fraction of x1 (from the docstring)

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then the second left fraction of $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f'}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.LeftFraction₃.thddefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $x_{1}$ be a left fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_thd}$ applied to $x_{1}$ is a left fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_f''}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_s}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_LeftFraction\_u2083\_\_\_hs}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.RightFraction₂structureMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, type

Wording

right fraction of X and Y (from the name)

English

Let $W$ be a morphism property of $C$. Let $X$ and $Y$ be elements of $C$. Then the right fractions of $X$ and $Y$ are a basic type.

CategoryTheory.MorphismProperty.RightFraction₂.X'defMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_X'}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.RightFraction₂.fdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_f}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_X'}$ applied to $\mathrm{self}$ and $Y$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_proj3}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.RightFraction₂.f'defMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_f'}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_X'}$ applied to $\mathrm{self}$ and $Y$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_proj4}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.RightFraction₂.fstdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

the first right fraction of x1 (from the docstring)

English

Let $x_{1}$ be a right fraction of $X$ and $Y$. Then the first right fraction of $x_{1}$ is a right fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_s}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_hs}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_f}$ applied to $x_{1}$.

CategoryTheory.MorphismProperty.RightFraction₂.sdefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a right fraction of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_s}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_X'}$ applied to $\mathrm{self}$ and $X$ defined as $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_proj1}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.RightFraction₂.snddefMathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions, function or constant

Wording

the second right fraction of x1 (from the docstring)

English

Let $x_{1}$ be a right fraction of $X$ and $Y$. Then the second right fraction of $x_{1}$ is a right fraction of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_s}$ applied to $x_{1}$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_hs}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_RightFraction\_u2082\_\_\_f'}$ applied to $x_{1}$.