Definitions: Mathlib.CategoryTheory, part 19 of 25

CategoryTheory.Monoidal.InducingFunctorData.εIsodefMathlib.CategoryTheory.Monoidal.Transport, function or constant

Wording

the isomorphism of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{InducingFunctorData}$ applied to $F$. Then the isomorphism of $\mathrm{self}$ is an isomorphism of the tensor unity in the monoidal structure of $C$ and the action of $F$ and the tensor unity in the monoidal structure of $D$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

CategoryTheory.Monoidal.InducingFunctorData.μIsodefMathlib.CategoryTheory.Monoidal.Transport, function or constant

Wording

the isomorphism of X and Y (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{InducingFunctorData}$ applied to $F$. Let $X$ and $Y$ be elements of $D$. Then the isomorphism of $X$ and $Y$ is an isomorphism of the tensor object of the action of $F$ and $X$ and the action of $F$ and $Y$ and the action of $F$ and the tensor object of $X$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $X$ and $Y$.

CategoryTheory.Monoidal.TransporteddefMathlib.CategoryTheory.Monoidal.Transport, type

Wording

no wording

English

Let $x_{2}$ be an equivalence of $C$ and $D$. Then an element of $\operatorname{Transported}$ applied to $x_{2}$ is an element of the function that maps $x_{2}$ to $D$.

CategoryTheory.Monoidal.equivalenceTransporteddefMathlib.CategoryTheory.Monoidal.Transport, function or constant

Wording

no wording

English

Let $e$ be an equivalence of $C$ and $D$. Then $\operatorname{equivalenceTransported}$ applied to $e$ is an equivalence of $C$ and $\operatorname{Transported}$ applied to $e$ defined as $e$.

CategoryTheory.Monoidal.fromInducedCoreMonoidaldefMathlib.CategoryTheory.Monoidal.Transport, function or constant

Wording

no wording

English

Let $F$ be a functor of $D$ and $C$. Let $\mathrm{fData}$ be an element of $\operatorname{InducingFunctorData}$ applied to $F$. Then $\operatorname{fromInducedCoreMonoidal}$ applied to $F$ and $\mathrm{fData}$ is an element of $\operatorname{CoreMonoidal}$ applied to $F$.

Mathlib.CategoryTheory.Monoidal.Types.Basic

CategoryTheory.MonoidalFunctor.mapPidefMathlib.CategoryTheory.Monoidal.Types.Basic, function or constant

Wording

the map product of F and n (from the name)

English

Let $F$ be a functor of the set of sets and $C$. Let $n$ be a natural number. Let $x_{3}$ be a set. Then the map product of $F$ and $n$ is an isomorphism of the action of $F$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x_{3}$ and the tensor object of the action of $F$ and $x_{3}$ and the action of $F$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x_{3}$ defined as the composition of the map isomorphism of $F$ and the isomorphism of the inverse of $\operatorname{consEquiv}$ applied to the function that maps $x_{4}$ to $x_{3}$ and the inverse of the isomorphism of $x_{3}$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x_{3}$.

Mathlib.CategoryTheory.Monoidal.Widesubcategory

CategoryTheory.MorphismProperty.IsMonoidalStableclassMathlib.CategoryTheory.Monoidal.Widesubcategory, predicate

Wording

P is a monoidal stable (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ is a monoidal stable.

CategoryTheory.MorphismProperty.IsStableUnderAssociatorclassMathlib.CategoryTheory.Monoidal.Widesubcategory, predicate

Wording

P is a stable under associator (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ is a stable under associator.

CategoryTheory.MorphismProperty.IsStableUnderBraidingclassMathlib.CategoryTheory.Monoidal.Widesubcategory, predicate

Wording

P is a stable under braiding (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ is a stable under braiding.

CategoryTheory.MorphismProperty.IsStableUnderUnitorclassMathlib.CategoryTheory.Monoidal.Widesubcategory, predicate

Wording

P is a stable under unitor (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ is a stable under unitor.

Mathlib.CategoryTheory.MorphismProperty.Basic

CategoryTheory.MorphismPropertydefMathlib.CategoryTheory.MorphismProperty.Basic, type

Wording

morphism property of C (from the name)

English

Let $C$ be a set. Then a morphism property of $C$ is an element of the function that maps $C$ to the set of functions from elements $X$ of $C$ and elements $Y$ of $C$ and homomorphisms of $X$ and $Y$ to propositions.

CategoryTheory.MorphismProperty.RespectsclassMathlib.CategoryTheory.MorphismProperty.Basic, predicate

Wording

no wording

English

Let $P$ and $Q$ be morphism properties of $C$. Then we can say that $\operatorname{Respects}$ holds for $P$ and $Q$.

CategoryTheory.MorphismProperty.RespectsIsodefMathlib.CategoryTheory.MorphismProperty.Basic, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Then $\operatorname{RespectsIso}$ holds for $P$, if $\operatorname{Respects}$ holds for $P$ and the isomorphism of $C$.

CategoryTheory.MorphismProperty.RespectsLeftclassMathlib.CategoryTheory.MorphismProperty.Basic, predicate

Wording

no wording

English

Let $P$ and $Q$ be morphism properties of $C$. Then we can say that $\operatorname{RespectsLeft}$ holds for $P$ and $Q$.

CategoryTheory.MorphismProperty.RespectsRightclassMathlib.CategoryTheory.MorphismProperty.Basic, predicate

Wording

no wording

English

Let $P$ and $Q$ be morphism properties of $C$. Then we can say that $\operatorname{RespectsRight}$ holds for $P$ and $Q$.

CategoryTheory.MorphismProperty.arrowdefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the arrow of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the arrow of $W$ is a morphism property of the set of arrows of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that $W$ holds for the left object of $x_{1}$, the left object of $x_{2}$ and the left part of $f$ and $W$ holds for the right object of $x_{1}$, the right object of $x_{2}$ and the right part of $f$.

CategoryTheory.MorphismProperty.epimorphismsdefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the epimorphism of C (from the name)

English

Let $C$ be a set. Then the epimorphism of $C$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that $f$ is an epimorphism.

CategoryTheory.MorphismProperty.functorCategorydefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the functor category of W and J (from the name)

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then the functor category of $W$ and $J$ is a morphism property of the set of functors of $J$ and $C$ defined as the function that maps $x_{2}$, $x_{3}$ and $f$ to the proposition that for all elements $j$ of $J$, $W$ holds for the action of $x_{2}$ and $j$, the action of $x_{3}$ and $j$ and the component of $f$ and $j$.

CategoryTheory.MorphismProperty.homFamilydefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the homomorphism family of P and f (from the name)

English

Let $P$ be a morphism property of $C$. Let $f$ be an element of the set in $P$. Then the homomorphism family of $P$ and $f$ is a homomorphism of the left object of $f$ and the right object of $f$ defined as the homomorphism of $f$.

CategoryTheory.MorphismProperty.inverseImagedefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the inverse image of P and F (from the docstring)

English

Let $P$ be a morphism property of $D$. Let $F$ be a functor of $C$ and $D$. Then the inverse image of $P$ and $F$ is a morphism property of $C$ defined as the function that maps $x_{2}$, $x_{3}$ and $f$ to $P$ applied to the action of $F$ and $x_{2}$, the action of $F$ and $x_{3}$ and the map of $F$ and $f$.

CategoryTheory.MorphismProperty.isoClosuredefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the isomorphism closure of P (from the name)

English

Let $P$ be a morphism property of $C$. Then the isomorphism closure of $P$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that there exist elements $x_{3}$ and $x_{4}$ of $C$, such that there exists a homomorphism $\mathrm{f'}$ of $x_{3}$ and $x_{4}$, such that there exists an element $h$ of $P$ applied to $x_{3}$, $x_{4}$ and $\mathrm{f'}$, such that $\mathrm{Nonempty}$ holds for the set of isomorphisms of $\operatorname{mk}$ applied to $\mathrm{f'}$ and $\operatorname{mk}$ applied to $f$.

CategoryTheory.MorphismProperty.isomorphismsdefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the isomorphism of C (from the name)

English

Let $C$ be a set. Then the isomorphism of $C$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that $f$ is an isomorphism.

CategoryTheory.MorphismProperty.mapdefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the map of P and F (from the name)

English

Let $P$ be a morphism property of $C$. Let $F$ be a functor of $C$ and $D$. Then the map of $P$ and $F$ is a morphism property of $D$ defined as the function that maps $x_{2}$, $x_{3}$ and $f$ to the proposition that there exist elements $\mathrm{X'}$ and $\mathrm{Y'}$ of $C$, such that there exists a homomorphism $\mathrm{f'}$ of $\mathrm{X'}$ and $\mathrm{Y'}$, such that there exists an element $h$ of $P$ applied to $\mathrm{X'}$, $\mathrm{Y'}$ and $\mathrm{f'}$, such that $\mathrm{Nonempty}$ holds for the set of isomorphisms of $\operatorname{mk}$ applied to the map of $F$ and $\mathrm{f'}$ and $\operatorname{mk}$ applied to $f$.

CategoryTheory.MorphismProperty.monomorphismsdefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the monomorphism of C (from the name)

English

Let $C$ be a set. Then the monomorphism of $C$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that $f$ is a monomorphism.

CategoryTheory.MorphismProperty.ofHomsinductiveMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the morphism property of f (from the name)

English

Let $f$ be a function from elements $i$ of $x_{1}$ to homomorphisms of $X$ applied to $i$ and $Y$ applied to $i$. Then the morphism property of $i$ is a morphism property of $C$.

CategoryTheory.MorphismProperty.opdefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the opposite of P (from the name)

English

Let $P$ be a morphism property of $C$. Then the opposite of $P$ is a morphism property of the set of opposites of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to $P$ applied to the opposite of $x_{2}$, the opposite of $x_{1}$ and the opposite of $f$.

CategoryTheory.MorphismProperty.pidefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the product of W (from the name)

English

Let $W$ be a function from elements $j_{1}$ of $J$ to morphism properties of $C$ applied to $j_{1}$. Then the product of $j_{1}$ is a morphism property of the set of functions from elements $j$ of $J$ to elements of $C$ applied to $j$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that for all elements $j$ of $J$, $j_{1}$ holds for $j$, $W$ applied to $j$, $x_{2}$ applied to $j$ and $f$ applied to $j$.

CategoryTheory.MorphismProperty.proddefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the product of x4 and x5 (from the name)

English

Let $x_{4}$ be a morphism property of $x$. Let $x_{5}$ be a morphism property of $x_{1}$. Then the product of $x_{4}$ and $x_{5}$ is a morphism property of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as the function that maps $x_{6}$, $x_{7}$ and $f$ to the proposition that $x_{4}$ holds for $\ProdfstMACRoZ {x_{6}}$, $\ProdfstMACRoZ {x_{7}}$ and $\ProdfstMACRoZ {f}$ and $x_{5}$ holds for $\ProdsndMACRoAA {x_{6}}$, $\ProdsndMACRoAA {x_{7}}$ and $\ProdsndMACRoAA {f}$.

CategoryTheory.MorphismProperty.singledefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then there is a morphism property of $C$. Proof. Let $f$ be arbitrary. Let $x_{1}$ be arbitrary. By f. By CategoryTheory__MorphismProperty__ofHoms.

CategoryTheory.MorphismProperty.strictMapinductiveMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the strict map of P and F (from the name)

English

Let $P$ be a morphism property of $C$. Let $F$ be a functor of $C$ and $D$. Then the strict map of $P$ and $F$ is a morphism property of $D$.

CategoryTheory.MorphismProperty.toSetdefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the set in P (from the docstring)

English

Let $P$ be a morphism property of $C$. Then the set in $P$ is an element of the power set of the set of arrows of $C$ defined as $\operatorname{ofPred}$ applied to the function that maps $f$ to $P$ applied to the left object of $f$, the right object of $f$ and the homomorphism of $f$.

CategoryTheory.MorphismProperty.unopdefMathlib.CategoryTheory.MorphismProperty.Basic, function or constant

Wording

the opposite of P (from the name)

English

Let $P$ be a morphism property of the set of opposites of $C$. Then the opposite of $P$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to $P$ applied to $\operatorname{op}$ applied to $x_{2}$, $\operatorname{op}$ applied to $x_{1}$ and the opposite in $f$.

Mathlib.CategoryTheory.MorphismProperty.Comma

CategoryTheory.MorphismProperty.ArrowdefMathlib.CategoryTheory.MorphismProperty.Comma, type

Wording

arrow of Q and W (from the name)

English

Let $P$, $Q$ and $W$ be morphism properties of $T$. Then an arrow of $Q$ and $W$ is an element of the function that maps $P$, $Q$ and $W$ to the set of commas of $Q$ and $W$.

CategoryTheory.MorphismProperty.Arrow.Hom.mkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of the action of the forgetful functor from the full subcategory of $P$ and $A$ and the action of the forgetful functor from the full subcategory of $P$ and $B$ such that $Q$ holds for the left object of the action of the forgetful functor from the full subcategory of $P$ and $A$, the left object of the action of the forgetful functor from the full subcategory of $P$ and $B$ and the left part of $f$ and $W$ holds for the right object of the action of the forgetful functor from the full subcategory of $P$ and $A$, the right object of the action of the forgetful functor from the full subcategory of $P$ and $B$ and the right part of $f$. Then $\operatorname{mk}$ applied to $f$, $\mathrm{hfl}$ and $\mathrm{hfr}$ is a homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $f$, $\mathrm{hfl}$ and $\mathrm{hfr}$.

CategoryTheory.MorphismProperty.Arrow.changePropdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Assume that $P \leq \mathrm{P'}$. Assume that $Q \leq \mathrm{Q'}$. Assume that $W \leq \mathrm{W'}$. Then $\operatorname{changeProp}$ applied to $\mathrm{hPP'}$, $\mathrm{hQQ'}$ and $\mathrm{hWW'}$ is a functor of the set of arrows of $Q$ and $W$ and the set of arrows of $\mathrm{Q'}$ and $\mathrm{W'}$ defined as $\operatorname{changeProp}$ applied to the identity of $T$, the identity of $T$, $\mathrm{hPP'}$, $\mathrm{hQQ'}$ and $\mathrm{hWW'}$.

CategoryTheory.MorphismProperty.Arrow.forgetdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the forgetful functor from the full subcategory of P (from the docstring)

English

Let $P$, $Q$ and $W$ be morphism properties of $T$. Then the forgetful functor from the full subcategory of $P$ is a functor of the set of arrows of $Q$ and $W$ and the set of arrows of $T$ defined as $\operatorname{forget}$ applied to the identity of $T$, the identity of $T$, $P$, $Q$ and $W$.

CategoryTheory.MorphismProperty.Arrow.homMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the homomorphism of f and g (from the name)

English

Let $f$ be a homomorphism of the left subobject of $\operatorname{toComma}$ applied to $A$ and the left subobject of $\operatorname{toComma}$ applied to $B$. Let $g$ be a homomorphism of the right subobject of $\operatorname{toComma}$ applied to $A$ and the right subobject of $\operatorname{toComma}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and the homomorphism of $\operatorname{toComma}$ applied to $B$ is equal to the composition of the homomorphism of $\operatorname{toComma}$ applied to $A$ and $g$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Arrow\_\_homMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $Q$ applied to the left subobject of $\operatorname{toComma}$ applied to $A$, the left subobject of $\operatorname{toComma}$ applied to $B$ and $f$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Arrow\_\_homMk\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for $W$ applied to the right subobject of $\operatorname{toComma}$ applied to $A$, the right subobject of $\operatorname{toComma}$ applied to $B$ and $g$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Arrow\_\_homMk\_\_\_auto\_5}$. Then the homomorphism of $f$ and $g$ is a homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to the homomorphism of $f$ and $g$, $\mathrm{hf}$ and $\mathrm{hg}$.

CategoryTheory.MorphismProperty.Arrow.isoMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the isomorphism of f and g (from the name)

English

Let $f$ be an isomorphism of the left subobject of $\operatorname{toComma}$ applied to $A$ and the left subobject of $\operatorname{toComma}$ applied to $B$. Let $g$ be an isomorphism of the right subobject of $\operatorname{toComma}$ applied to $A$ and the right subobject of $\operatorname{toComma}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $f$ and the homomorphism of $\operatorname{toComma}$ applied to $B$ is equal to the composition of the homomorphism of $\operatorname{toComma}$ applied to $A$ and the homomorphism of $g$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Arrow\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $f$ and $g$ is an isomorphism of $A$ and $B$.

CategoryTheory.MorphismProperty.Arrow.mkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $A$ and $B$ such that $P$ holds for $A$, $B$ and $f$. Then $\operatorname{mk}$ applied to $f$ and $\mathrm{hf}$ is an arrow of $Q$ and $W$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $A$, $B$ and $f$ and $\mathrm{hf}$.

CategoryTheory.MorphismProperty.CommastructureMathlib.CategoryTheory.MorphismProperty.Comma, type

Wording

comma of Q and W (from the name)

English

CategoryTheory.MorphismProperty.Comma.HomstructureMathlib.CategoryTheory.MorphismProperty.Comma, type

Wording

homomorphism of X and Y (from the name)

English

Let $X$ and $Y$ be commas of $Q$ and $W$. Then the homomorphisms of $X$ and $Y$ are a basic type.

CategoryTheory.MorphismProperty.Comma.Hom.compdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the composition of f and g (from the name)

English

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

CategoryTheory.MorphismProperty.Comma.Hom.homdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a homomorphism of $\operatorname{toComma}$ applied to $X$ and $\operatorname{toComma}$ applied to $Y$ defined as $\operatorname{toCommaMorphism}$ applied to $f$.

CategoryTheory.MorphismProperty.Comma.changePropdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Assume that $P \leq \mathrm{P'}$. Assume that $Q \leq \mathrm{Q'}$. Assume that $W \leq \mathrm{W'}$. Then $\operatorname{changeProp}$ applied to $L$, $R$, $\mathrm{hP}$, $\mathrm{hQ}$ and $\mathrm{hW}$ is a functor of the set of commas of $Q$ and $W$ and the set of commas of $\mathrm{Q'}$ and $\mathrm{W'}$.

CategoryTheory.MorphismProperty.Comma.forgetdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Let $P$ be a morphism property of $T$. Let $Q$ be a morphism property of $A$. Let $W$ be a morphism property of $B$. Then $\operatorname{forget}$ applied to $L$, $R$, $P$, $Q$ and $W$ is a functor of the set of commas of $Q$ and $W$ and the set of commas of $L$ and $R$.

CategoryTheory.MorphismProperty.Comma.forgetFullyFaithfuldefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the forgetful functor from the full subcategory of L (from the docstring)

English

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Let $P$ be a morphism property of $T$. Then the forgetful functor from the full subcategory of $L$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forget}$ applied to $L$, $R$, $P$, the top and the top.

CategoryTheory.MorphismProperty.Comma.fullyFaithfulChangePropdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Assume that $P \leq \mathrm{P'}$. Then $\operatorname{fullyFaithfulChangeProp}$ applied to $L$, $R$ and $\mathrm{hP}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{changeProp}$ applied to $L$, $R$, $\mathrm{hP}$, $\mathrm{le\_rfl}$ and $\mathrm{le\_rfl}$.

CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIsodefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the homomorphism from comma of i (from the name)

English

Let $i$ be a homomorphism of $\operatorname{toComma}$ applied to $X$ and $\operatorname{toComma}$ applied to $Y$. Then the homomorphism from comma of $i$ is a homomorphism of $X$ and $Y$.

CategoryTheory.MorphismProperty.Comma.iddefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the identity morphism in X (from the docstring)

English

Let $X$ be a comma of $Q$ and $W$. Then the identity morphism in $X$ is a homomorphism of $X$ and $X$.

CategoryTheory.MorphismProperty.Comma.isoFromCommadefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the isomorphism from comma of i (from the name)

English

Let $i$ be an isomorphism of $\operatorname{toComma}$ applied to $X$ and $\operatorname{toComma}$ applied to $Y$. Then the isomorphism from comma of $i$ is an isomorphism of $X$ and $Y$.

CategoryTheory.MorphismProperty.Comma.isoMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the isomorphism of l and r (from the name)

English

Let $l$ be an isomorphism of the left subobject of $\operatorname{toComma}$ applied to $X$ and the left subobject of $\operatorname{toComma}$ applied to $Y$. Let $r$ be an isomorphism of the right subobject of $\operatorname{toComma}$ applied to $X$ and the right subobject of $\operatorname{toComma}$ applied to $Y$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $L$ and the homomorphism of $l$ and the homomorphism of $\operatorname{toComma}$ applied to $Y$ is equal to the composition of the homomorphism of $\operatorname{toComma}$ applied to $X$ and the map of $R$ and the homomorphism of $r$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Comma\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $l$ and $r$ is an isomorphism of $X$ and $Y$ defined as the isomorphism from comma of the isomorphism of $l$ and $r$.

CategoryTheory.MorphismProperty.Comma.liftdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the lift of F (from the name)

English

Let $F$ be a functor of $C$ and the set of commas of $L$ and $R$ such that for all elements $X_{2}$ of $C$, $P$ holds for the action of $L$ and the left subobject of the action of $F$ and $X_{2}$, the action of $R$ and the right subobject of the action of $F$ and $X_{2}$ and the homomorphism of the action of $F$ and $X_{2}$, for all elements $X_{1}$ of $C$, for all elements $Y_{1}$ of $C$, for all homomorphisms $f_{1}$ of $X_{1}$ and $Y_{1}$, $Q$ holds for the left subobject of the action of $F$ and $X_{1}$, the left subobject of the action of $F$ and $Y_{1}$ and the left of the map of $F$ and $f_{1}$ and for all elements $X$ of $C$, for all elements $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, $W$ holds for the right subobject of the action of $F$ and $X$, the right subobject of the action of $F$ and $Y$ and the right of the map of $F$ and $f$. Then the lift of $F$ is a functor of $C$ and the set of commas of $Q$ and $W$.

CategoryTheory.MorphismProperty.Comma.mapLeftdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the left map of R and l (from the name)

English

Let $R$ be a functor of $B$ and $T$. Let $l$ be a homomorphism of $x_{3}$ and $x_{4}$ such that for all commas $X$ of $Q$ and $W$, $P$ holds for the action of $x_{3}$ and the left subobject of $\operatorname{toComma}$ applied to $X$, the action of $R$ and the right subobject of $\operatorname{toComma}$ applied to $X$ and the composition of the component of $l$ and the left subobject of $\operatorname{toComma}$ applied to $X$ and the homomorphism of $\operatorname{toComma}$ applied to $X$. Then the left map of $R$ and $l$ is a functor of the set of commas of $Q$ and $W$ and the set of commas of $Q$ and $W$ defined as the lift of the composition of $\operatorname{forget}$ applied to $x_{4}$, $R$, $P$, $Q$ and $W$ and the left map of $R$ and $l$.

CategoryTheory.MorphismProperty.Comma.mapLeftCompdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the map left composition of l and hl (from the name)

English

Let $R$ be a functor of $B$ and $T$. Let $l$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{l'}$ be a homomorphism of $x_{4}$ and $x_{5}$. Assume that for all commas $X_{2}$ of $Q$ and $W$, $P$ holds for the action of $x_{3}$ and the left subobject of $\operatorname{toComma}$ applied to $X_{2}$, the action of $R$ and the right subobject of $\operatorname{toComma}$ applied to $X_{2}$ and the composition of the component of $l$ and the left subobject of $\operatorname{toComma}$ applied to $X_{2}$ and the homomorphism of $\operatorname{toComma}$ applied to $X_{2}$. Assume that for all commas $X_{1}$ of $Q$ and $W$, $P$ holds for the action of $x_{4}$ and the left subobject of $\operatorname{toComma}$ applied to $X_{1}$, the action of $R$ and the right subobject of $\operatorname{toComma}$ applied to $X_{1}$ and the composition of the component of $\mathrm{l'}$ and the left subobject of $\operatorname{toComma}$ applied to $X_{1}$ and the homomorphism of $\operatorname{toComma}$ applied to $X_{1}$. Assume that for all commas $X$ of $Q$ and $W$, $P$ holds for the action of $x_{3}$ and the left subobject of $\operatorname{toComma}$ applied to $X$, the action of $R$ and the right subobject of $\operatorname{toComma}$ applied to $X$ and the composition of the component of the composition of $l$ and $\mathrm{l'}$ and the left subobject of $\operatorname{toComma}$ applied to $X$ and the homomorphism of $\operatorname{toComma}$ applied to $X$. Then the map left composition of $l$ and $\mathrm{l'}$ is an isomorphism of the left map of $R$ and the composition of $l$ and $\mathrm{l'}$ and the composition of the left map of $R$ and $\mathrm{l'}$ and the left map of $R$ and $l$.

CategoryTheory.MorphismProperty.Comma.mapLeftEqdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $R$ be a functor of $B$ and $T$. Let $l$ and $\mathrm{l'}$ be homomorphisms of $x_{3}$ and $x_{4}$ such that $\EqtMACRoH {l}{\mathrm{l'}}$ and for all commas $X$ of $Q$ and $W$, $P$ holds for the action of $x_{3}$ and the left subobject of $\operatorname{toComma}$ applied to $X$, the action of $R$ and the right subobject of $\operatorname{toComma}$ applied to $X$ and the composition of the component of $l$ and the left subobject of $\operatorname{toComma}$ applied to $X$ and the homomorphism of $\operatorname{toComma}$ applied to $X$. Then $\operatorname{mapLeftEq}$ applied to $R$, $l$, $\mathrm{l'}$, $h_{4}$ and $\mathrm{hl}$ is an isomorphism of the left map of $R$ and $l$ and the left map of $R$ and $\mathrm{l'}$.

CategoryTheory.MorphismProperty.Comma.mapLeftIddefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the map left identity of L and R (from the name)

English

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the map left identity of $L$ and $R$ is an isomorphism of the left map of $R$ and the identity morphism of $L$ and the identity of the set of commas of $Q$ and $W$.

CategoryTheory.MorphismProperty.Comma.mapLeftIsodefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the map left isomorphism of R and e (from the name)

English

Let $R$ be a functor of $B$ and $T$. Let $e$ be an isomorphism of $x_{3}$ and $x_{4}$. Then the map left isomorphism of $R$ and $e$ is an equivalence of the set of commas of $Q$ and $W$ and the set of commas of $Q$ and $W$.

CategoryTheory.MorphismProperty.Comma.mapRightdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the right map of L and r (from the name)

English

Let $L$ be a functor of $A$ and $T$. Let $r$ be a homomorphism of $x_{3}$ and $x_{4}$ such that for all commas $X$ of $Q$ and $W$, $P$ holds for the action of $L$ and the left subobject of $\operatorname{toComma}$ applied to $X$, the action of $x_{4}$ and the right subobject of $\operatorname{toComma}$ applied to $X$ and the composition of the homomorphism of $\operatorname{toComma}$ applied to $X$ and the component of $r$ and the right subobject of $\operatorname{toComma}$ applied to $X$. Then the right map of $L$ and $r$ is a functor of the set of commas of $Q$ and $W$ and the set of commas of $Q$ and $W$ defined as the lift of the composition of $\operatorname{forget}$ applied to $L$, $x_{3}$, $P$, $Q$ and $W$ and the right map of $L$ and $r$.

CategoryTheory.MorphismProperty.Comma.mapRightCompdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the map right composition of r and hr (from the name)

English

Let $L$ be a functor of $A$ and $T$. Let $r$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{r'}$ be a homomorphism of $x_{4}$ and $x_{5}$. Assume that for all commas $X_{2}$ of $Q$ and $W$, $P$ holds for the action of $L$ and the left subobject of $\operatorname{toComma}$ applied to $X_{2}$, the action of $x_{4}$ and the right subobject of $\operatorname{toComma}$ applied to $X_{2}$ and the composition of the homomorphism of $\operatorname{toComma}$ applied to $X_{2}$ and the component of $r$ and the right subobject of $\operatorname{toComma}$ applied to $X_{2}$. Assume that for all commas $X_{1}$ of $Q$ and $W$, $P$ holds for the action of $L$ and the left subobject of $\operatorname{toComma}$ applied to $X_{1}$, the action of $x_{5}$ and the right subobject of $\operatorname{toComma}$ applied to $X_{1}$ and the composition of the homomorphism of $\operatorname{toComma}$ applied to $X_{1}$ and the component of $\mathrm{r'}$ and the right subobject of $\operatorname{toComma}$ applied to $X_{1}$. Assume that for all commas $X$ of $Q$ and $W$, $P$ holds for the action of $L$ and the left subobject of $\operatorname{toComma}$ applied to $X$, the action of $x_{5}$ and the right subobject of $\operatorname{toComma}$ applied to $X$ and the composition of the homomorphism of $\operatorname{toComma}$ applied to $X$ and the component of the composition of $r$ and $\mathrm{r'}$ and the right subobject of $\operatorname{toComma}$ applied to $X$. Then the map right composition of $r$ and $\mathrm{r'}$ is an isomorphism of the right map of $L$ and the composition of $r$ and $\mathrm{r'}$ and the composition of the right map of $L$ and $r$ and the right map of $L$ and $\mathrm{r'}$.

CategoryTheory.MorphismProperty.Comma.mapRightEqdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $L$ be a functor of $A$ and $T$. Let $r$ and $\mathrm{r'}$ be homomorphisms of $x_{3}$ and $x_{4}$ such that $\EqtMACRoH {r}{\mathrm{r'}}$ and for all commas $X$ of $Q$ and $W$, $P$ holds for the action of $L$ and the left subobject of $\operatorname{toComma}$ applied to $X$, the action of $x_{4}$ and the right subobject of $\operatorname{toComma}$ applied to $X$ and the composition of the homomorphism of $\operatorname{toComma}$ applied to $X$ and the component of $r$ and the right subobject of $\operatorname{toComma}$ applied to $X$. Then $\operatorname{mapRightEq}$ applied to $L$, $r$, $\mathrm{r'}$, $h_{4}$ and $\mathrm{hr}$ is an isomorphism of the right map of $L$ and $r$ and the right map of $L$ and $\mathrm{r'}$.

CategoryTheory.MorphismProperty.Comma.mapRightIddefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the map right identity of L and R (from the name)

English

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the map right identity of $L$ and $R$ is an isomorphism of the right map of $L$ and the identity morphism of $R$ and the identity of the set of commas of $Q$ and $W$.

CategoryTheory.MorphismProperty.Comma.mapRightIsodefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the map right isomorphism of L and e (from the name)

English

Let $L$ be a functor of $A$ and $T$. Let $e$ be an isomorphism of $x_{3}$ and $x_{4}$. Then the map right isomorphism of $L$ and $e$ is an equivalence of the set of commas of $Q$ and $W$ and the set of commas of $Q$ and $W$.

CategoryTheory.MorphismProperty.CostructuredArrowdefMathlib.CategoryTheory.MorphismProperty.Comma, type

Wording

costructured arrow of F and X (from the name)

English

Let $P$ be a morphism property of $D$. Let $Q$ be a morphism property of $C$. Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Then a costructured arrow of $F$ and $X$ is an element of the function that maps $P$, $Q$, $F$ and $X$ to the set of commas of $Q$ and the top.

CategoryTheory.MorphismProperty.CostructuredArrow.forgetdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $P$ be a morphism property of $D$. Let $Q$ be a morphism property of $C$. Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Then $\operatorname{forget}$ applied to $P$, $Q$, $F$ and $X$ is a functor of the set of costructured arrows of $F$ and $X$ and the set of costructured arrows of $F$ and $X$ defined as $\operatorname{forget}$ applied to $F$, $\operatorname{fromPUnit}$ applied to $X$, $P$, $Q$ and the top.

CategoryTheory.MorphismProperty.CostructuredArrow.homMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of the left subobject of $\operatorname{toComma}$ applied to $A$ and the left subobject of $\operatorname{toComma}$ applied to $B$ such that $Q$ holds for the left subobject of $\operatorname{toComma}$ applied to $A$, the left subobject of $\operatorname{toComma}$ applied to $B$ and $f$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and $f$ and the homomorphism of $\operatorname{toComma}$ applied to $B$ is equal to the homomorphism of $\operatorname{toComma}$ applied to $A$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_CostructuredArrow\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $f$ is a homomorphism of $A$ and $B$.

CategoryTheory.MorphismProperty.CostructuredArrow.isoMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the isomorphism of f (from the name)

English

Let $f$ be an isomorphism of the left subobject of $\operatorname{toComma}$ applied to $A$ and the left subobject of $\operatorname{toComma}$ applied to $B$ such that $Q$ holds for the left subobject of $\operatorname{toComma}$ applied to $A$, the left subobject of $\operatorname{toComma}$ applied to $B$ and the homomorphism of $f$, $Q$ holds for the left subobject of $\operatorname{toComma}$ applied to $B$, the left subobject of $\operatorname{toComma}$ applied to $A$ and the inverse of $f$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the homomorphism of $f$ and the homomorphism of $\operatorname{toComma}$ applied to $B$ is equal to the homomorphism of $\operatorname{toComma}$ applied to $A$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_CostructuredArrow\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $f$ is an isomorphism of $A$ and $B$.

CategoryTheory.MorphismProperty.CostructuredArrow.mkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $Q$ be a morphism property of $C$. Let $f$ be a homomorphism of the action of $F$ and $A$ and $X$ such that $P$ holds for the action of $F$ and $A$, $X$ and $f$. Then $\operatorname{mk}$ applied to $Q$, $f$ and $\mathrm{hf}$ is a costructured arrow of $F$ and $X$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $A$, $\operatorname{mk}$ applied to $\operatorname{unit}$ and $f$ and $\mathrm{hf}$.

CategoryTheory.MorphismProperty.CostructuredArrow.toOverdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $P$ be a morphism property of $D$. Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Then $\operatorname{toOver}$ applied to $P$, $F$ and $X$ is a functor of the set of costructured arrows of $F$ and $X$ and $\operatorname{Over}$ applied to $P$, the top and $X$.

CategoryTheory.MorphismProperty.OverdefMathlib.CategoryTheory.MorphismProperty.Comma, type

Wording

no wording

English

Let $P$ and $Q$ be morphism properties of $T$. Let $X$ be an element of $T$. Then an element of $\operatorname{Over}$ applied to $P$, $Q$ and $X$ is an element of the function that maps $P$, $Q$ and $X$ to the set of commas of $Q$ and the top.

CategoryTheory.MorphismProperty.Over.Hom.mkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

CategoryTheory.MorphismProperty.Over.changePropdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $X$ be an element of $T$. Assume that $P \leq \mathrm{P'}$. Assume that $Q \leq \mathrm{Q'}$. Then $\operatorname{changeProp}$ applied to $X$, $\mathrm{hPP'}$ and $\mathrm{hQQ'}$ is a functor of $\operatorname{Over}$ applied to $P$, $Q$ and $X$ and $\operatorname{Over}$ applied to $\mathrm{P'}$, $\mathrm{Q'}$ and $X$.

CategoryTheory.MorphismProperty.Over.forgetdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the forgetful functor from the full subcategory of P (from the docstring)

English

Let $P$ and $Q$ be morphism properties of $T$. Let $X$ be an element of $T$. Then the forgetful functor from the full subcategory of $P$ is a functor of $\operatorname{Over}$ applied to $P$, $Q$ and $X$ and $\operatorname{Over}$ applied to $X$ defined as $\operatorname{forget}$ applied to the identity of $T$, $\operatorname{fromPUnit}$ applied to $X$, $P$, $Q$ and the top.

CategoryTheory.MorphismProperty.Over.homMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of the left subobject of $\operatorname{toComma}$ applied to $A$ and the left subobject of $\operatorname{toComma}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and the homomorphism of $\operatorname{toComma}$ applied to $B$ is equal to the homomorphism of $\operatorname{toComma}$ applied to $A$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_homMk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $Q$ applied to the left subobject of $\operatorname{toComma}$ applied to $A$, the left subobject of $\operatorname{toComma}$ applied to $B$ and $f$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_homMk\_\_\_auto\_3}$. Then the homomorphism of $f$ is a homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to the homomorphism of $f$ and $w$, $\mathrm{hf}$ and $\mathrm{trivial}$.

CategoryTheory.MorphismProperty.Over.isoMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the isomorphism of f and w (from the name)

English

Let $f$ be an isomorphism of the left subobject of $\operatorname{toComma}$ applied to $A$ and the left subobject of $\operatorname{toComma}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $f$ and the homomorphism of $\operatorname{toComma}$ applied to $B$ is equal to the homomorphism of $\operatorname{toComma}$ applied to $A$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $f$ and $w$ is an isomorphism of $A$ and $B$.

CategoryTheory.MorphismProperty.Over.mkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $Q$ be a morphism property of $T$. Let $f$ be a homomorphism of $A$ and $X$ such that $P$ holds for $A$, $X$ and $f$. Then $\operatorname{mk}$ applied to $Q$, $f$ and $\mathrm{hf}$ is an element of $\operatorname{Over}$ applied to $P$, $Q$ and $X$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $A$, $\operatorname{mk}$ applied to $\operatorname{unit}$ and $f$ and $\mathrm{hf}$.

CategoryTheory.MorphismProperty.UnderdefMathlib.CategoryTheory.MorphismProperty.Comma, type

Wording

no wording

English

Let $P$ and $Q$ be morphism properties of $T$. Let $X$ be an element of $T$. Then an element of $\operatorname{Under}$ applied to $P$, $Q$ and $X$ is an element of the function that maps $P$, $Q$ and $X$ to the set of commas of the top and $Q$.

CategoryTheory.MorphismProperty.Under.Hom.mkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

CategoryTheory.MorphismProperty.Under.forgetdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the forgetful functor from the full subcategory of P (from the docstring)

English

Let $P$ and $Q$ be morphism properties of $T$. Let $X$ be an element of $T$. Then the forgetful functor from the full subcategory of $P$ is a functor of $\operatorname{Under}$ applied to $P$, $Q$ and $X$ and $\operatorname{Under}$ applied to $X$ defined as $\operatorname{forget}$ applied to $\operatorname{fromPUnit}$ applied to $X$, the identity of $T$, $P$, the top and $Q$.

CategoryTheory.MorphismProperty.Under.homMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of the right subobject of $\operatorname{toComma}$ applied to $A$ and the right subobject of $\operatorname{toComma}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $\operatorname{toComma}$ applied to $A$ and $f$ is equal to the homomorphism of $\operatorname{toComma}$ applied to $B$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Under\_\_homMk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $Q$ applied to the right subobject of $\operatorname{toComma}$ applied to $A$, the right subobject of $\operatorname{toComma}$ applied to $B$ and $f$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Under\_\_homMk\_\_\_auto\_3}$. Then the homomorphism of $f$ is a homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to the homomorphism of $f$ and $w$, $\mathrm{trivial}$ and $\mathrm{hf}$.

CategoryTheory.MorphismProperty.Under.isoMkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the isomorphism of f and w (from the name)

English

Let $f$ be an isomorphism of the right subobject of $\operatorname{toComma}$ applied to $A$ and the right subobject of $\operatorname{toComma}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $\operatorname{toComma}$ applied to $A$ and the homomorphism of $f$ is equal to the homomorphism of $\operatorname{toComma}$ applied to $B$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Under\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $f$ and $w$ is an isomorphism of $A$ and $B$.

CategoryTheory.MorphismProperty.Under.mkdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $Q$ be a morphism property of $T$. Let $f$ be a homomorphism of $X$ and $A$ such that $P$ holds for $X$, $A$ and $f$. Then $\operatorname{mk}$ applied to $Q$, $f$ and $\mathrm{hf}$ is an element of $\operatorname{Under}$ applied to $P$, $Q$ and $X$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{unit}$, $A$ and $f$ and $\mathrm{hf}$.

CategoryTheory.MorphismProperty.commaObjdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the comma object of R and W (from the name)

English

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Let $W$ be a morphism property of $T$. Then the comma object of $R$ and $W$ is an object property of the set of commas of $L$ and $R$ defined as the function that maps $f$ to $W$ applied to the action of $L$ and the left subobject of $f$, the action of $R$ and the right subobject of $f$ and the homomorphism of $f$.

CategoryTheory.MorphismProperty.costructuredArrowObjdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the costructured arrow object of L and W (from the name)

English

Let $L$ be a functor of $A$ and $T$. Let $W$ be a morphism property of $T$. Then the costructured arrow object of $L$ and $W$ is an object property of the set of costructured arrows of $L$ and $X$ defined as the function that maps $f$ to $W$ applied to the action of $L$ and the left object of $f$, $X$ and the homomorphism of $f$.

CategoryTheory.MorphismProperty.overdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $T$. Then there is a morphism property of $\operatorname{Over}$ applied to $X$. Proof. Let $W$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $f$ be arbitrary. By x1. By CategoryTheory__Over__left. By x2. By CategoryTheory__Over__left. By f. By CategoryTheory__Over__Hom__left. By W.

CategoryTheory.MorphismProperty.overObjdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $T$. Then there is an object property of $\operatorname{Over}$ applied to $X$. Proof. Let $W$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__Over__left. By X. By f. By CategoryTheory__Over__hom. By W.

CategoryTheory.MorphismProperty.structuredArrowObjdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

the structured arrow object of R and W (from the name)

English

Let $R$ be a functor of $B$ and $T$. Let $W$ be a morphism property of $T$. Then the structured arrow object of $R$ and $W$ is an object property of the set of structured arrows of $X$ and $R$ defined as the function that maps $f$ to $W$ applied to $X$, the action of $R$ and the right object of $f$ and the homomorphism of $f$.

CategoryTheory.MorphismProperty.underdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $T$. Then there is a morphism property of $\operatorname{Under}$ applied to $X$. Proof. Let $W$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $f$ be arbitrary. By x1. By CategoryTheory__Under__right. By x2. By CategoryTheory__Under__right. By f. By CategoryTheory__Under__Hom__right. By W.

CategoryTheory.MorphismProperty.underObjdefMathlib.CategoryTheory.MorphismProperty.Comma, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $T$. Then there is an object property of $\operatorname{Under}$ applied to $X$. Proof. Let $W$ be arbitrary. Let $f$ be arbitrary. By X. By f. By CategoryTheory__Under__right. By f. By CategoryTheory__Under__hom. By W.

Mathlib.CategoryTheory.MorphismProperty.Composition

CategoryTheory.MorphismProperty.ContainsIdentitiesclassMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{ContainsIdentities}$ holds for $W$.

CategoryTheory.MorphismProperty.HasOfPostcompPropertyclassMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

no wording

English

Let $W$ and $\mathrm{W'}$ be morphism properties of $C$. Then we can say that $\operatorname{HasOfPostcompProperty}$ holds for $W$ and $\mathrm{W'}$.

CategoryTheory.MorphismProperty.HasOfPrecompPropertyclassMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

no wording

English

Let $W$ and $\mathrm{W'}$ be morphism properties of $C$. Then we can say that $\operatorname{HasOfPrecompProperty}$ holds for $W$ and $\mathrm{W'}$.

CategoryTheory.MorphismProperty.HasTwoOutOfThreePropertyclassMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{HasTwoOutOfThreeProperty}$ holds for $W$.

CategoryTheory.MorphismProperty.IsMultiplicativeclassMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

W is multiplicative (from the docstring)

English

Let $W$ be a morphism property of $C$. Then we can say that $W$ is multiplicative.

CategoryTheory.MorphismProperty.IsStableUnderCompositionclassMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

P is a stable under composition (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ is a stable under composition.

CategoryTheory.MorphismProperty.StableUnderInversedefMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

P is stable under inverse (from the name)

English

Let $P$ be a morphism property of $C$. Then $P$ is stable under inverse, if for all elements $X$ and $Y$ of $C$, for all isomorphisms $e$ of $X$ and $Y$, if $P$ holds for $X$, $Y$ and the homomorphism of $e$, then $P$ holds for $Y$, $X$ and the inverse of $e$.

CategoryTheory.MorphismProperty.identitiesdefMathlib.CategoryTheory.MorphismProperty.Composition, function or constant

Wording

the identity of C (from the name)

English

Let $C$ be a set. Then the identity of $C$ is a morphism property of $C$ defined as the morphism property of the function that maps $X$ to the identity morphism of $X$.

CategoryTheory.MorphismProperty.multiplicativeClosureinductiveMathlib.CategoryTheory.MorphismProperty.Composition, function or constant

Wording

the multiplicative closure of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the multiplicative closure of $W$ is a morphism property of $C$.

CategoryTheory.MorphismProperty.multiplicativeClosure'inductiveMathlib.CategoryTheory.MorphismProperty.Composition, function or constant

Wording

the multiplicative closure of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the multiplicative closure of $W$ is a morphism property of $C$.

CategoryTheory.MorphismProperty.multiplicativeClosure'.belowinductiveMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

no wording

English

Assume that $\operatorname{multiplicativeClosure'}$ holds for $W$. Then we can say that $\operatorname{below}$ holds for $t$.

CategoryTheory.MorphismProperty.multiplicativeClosure.belowinductiveMathlib.CategoryTheory.MorphismProperty.Composition, predicate

Wording

no wording

English

Assume that $\operatorname{multiplicativeClosure}$ holds for $W$. Then we can say that $\operatorname{below}$ holds for $t$.

CategoryTheory.MorphismProperty.naturalityPropertydefMathlib.CategoryTheory.MorphismProperty.Composition, function or constant

Wording

the naturality property of app (from the name)

English

Let $\mathrm{app}$ be a function from elements $X$ of $C$ to homomorphisms of the action of $x_{2}$ and $X$ and the action of $x_{3}$ and $X$. Then the naturality property of $X$ is a morphism property of $C$ defined as the function that maps $X$, $Y$ and $f$ to the proposition that the composition of the map of $x_{2}$ and $f$ and $X$ applied to $Y$ is equal to the composition of $X$ applied to $\mathrm{app}$ and the map of $x_{3}$ and $f$.

Mathlib.CategoryTheory.MorphismProperty.Concrete

CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationDatadefMathlib.CategoryTheory.MorphismProperty.Concrete, type

Wording

functorial surjective injective factorization data of C (from the name)

English

Let $C$ be a set. Then a functorial surjective injective factorization data of $C$ is an element of the function that maps $C$ to the set of functorial factorization data of $\operatorname{surjective}$ applied to $C$ and the injective of $C$.

CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorizationdefMathlib.CategoryTheory.MorphismProperty.Concrete, predicate

Wording

C has functorial surjective injective factorizations (from the name)

English

Let $C$ be a set. Then $C$ has functorial surjective injective factorizations, if $\operatorname{HasFunctorialFactorization}$ holds for $\operatorname{surjective}$ applied to $C$ and the injective of $C$.

CategoryTheory.ConcreteCategory.HasSurjectiveInjectiveFactorizationdefMathlib.CategoryTheory.MorphismProperty.Concrete, predicate

Wording

C has surjective injective factorizations (from the name)

English

Let $C$ be a set. Then $C$ has surjective injective factorizations, if $\operatorname{HasFactorization}$ holds for $\operatorname{surjective}$ applied to $C$ and the injective of $C$.

CategoryTheory.MorphismProperty.bijectivedefMathlib.CategoryTheory.MorphismProperty.Concrete, function or constant

Wording

no wording

English

Let $C$ be a set. Then there is a morphism property of $C$. Proof. Let $C$ be arbitrary. Let $x_{3}$ be arbitrary. Let $x_{4}$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__ConcreteCategory__hom. By DFunLike__coe. By Function__Bijective.

CategoryTheory.MorphismProperty.injectivedefMathlib.CategoryTheory.MorphismProperty.Concrete, function or constant

Wording

the injective of C (from the name)

English

Let $C$ be a set. Then the injective of $C$ is a morphism property of $C$ defined as the function that maps $x_{3}$, $x_{4}$ and $f$ to the proposition that $\operatorname{coe}$ applied to the homomorphism of $f$ is injective.

CategoryTheory.MorphismProperty.surjectivedefMathlib.CategoryTheory.MorphismProperty.Concrete, function or constant

Wording

no wording

English

CategoryTheory.functorialSurjectiveInjectiveFactorizationDatadefMathlib.CategoryTheory.MorphismProperty.Concrete, function or constant

Wording

the functorial surjective injective factorization data (from the name)

English

The functorial surjective injective factorization data is a functorial surjective injective factorization data of the set of sets.

Mathlib.CategoryTheory.MorphismProperty.Descent

CategoryTheory.MorphismProperty.CodescendsAlongclassMathlib.CategoryTheory.MorphismProperty.Descent, predicate

Wording

no wording

English

Let $P$ and $Q$ be morphism properties of $C$. Then we can say that $\operatorname{CodescendsAlong}$ holds for $P$ and $Q$.

CategoryTheory.MorphismProperty.DescendsAlongclassMathlib.CategoryTheory.MorphismProperty.Descent, predicate

Wording

no wording

English

Let $P$ and $Q$ be morphism properties of $C$. Then we can say that $\operatorname{DescendsAlong}$ holds for $P$ and $Q$.

Mathlib.CategoryTheory.MorphismProperty.Factorization

CategoryTheory.MorphismProperty.FactorizationDatadefMathlib.CategoryTheory.MorphismProperty.Factorization, type

Wording

factorization data of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then a factorization data of $x_{1}$ and $x_{2}$ is an element of the function that maps $x_{1}$ and $x_{2}$ to the set of functions from elements $X$ of $C$ and elements $Y$ of $C$ and homomorphisms $f$ of $X$ and $Y$ to map factorization data of $x_{2}$ and $f$.

CategoryTheory.MorphismProperty.FunctorialFactorizationDatastructureMathlib.CategoryTheory.MorphismProperty.Factorization, type

Wording

functorial factorization data of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then the functorial factorization data of $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.ZdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a functorial factorization data of $x_{1}$ and $x_{2}$. Then $\operatorname{Z}$ applied to $\mathrm{self}$ is a functor of the set of arrows of $C$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.factorizationDatadefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the factorization data of data (from the name)

English

Let $\mathrm{data}$ be a functorial factorization data of $x_{1}$ and $x_{2}$. Then the factorization data of $\mathrm{data}$ is a factorization data of $x_{1}$ and $x_{2}$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategorydefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the functor category of data and J (from the name)

English

Let $\mathrm{data}$ be a functorial factorization data of $x_{1}$ and $x_{2}$. Let $J$ be a set. Then the functor category of $\mathrm{data}$ and $J$ is a functorial factorization data of the functor category of $x_{1}$ and $J$ and the functor category of $x_{2}$ and $J$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.idefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a functorial factorization data of $x_{1}$ and $x_{2}$. Then $\operatorname{i}$ applied to $\mathrm{self}$ is a homomorphism of the left function and $\operatorname{Z}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the map of data and x3 (from the name)

English

Let $\mathrm{data}$ be a functorial factorization data of $x_{1}$ and $x_{2}$. Let $x_{3}$ be a homomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$. Then the map of $\mathrm{data}$ and $x_{3}$ is a homomorphism of $\operatorname{Z}$ applied to the factorization data of $\mathrm{data}$ and $\operatorname{Z}$ applied to the factorization data of $\mathrm{data}$ defined as the map of $\operatorname{Z}$ applied to $\mathrm{data}$ and $x_{3}$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.ofLEdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the functorial factorization data of data (from the name)

English

Let $\mathrm{data}$ be a functorial factorization data of $x_{1}$ and $x_{2}$. Assume that $x_{1} \leq x_{3}$. Assume that $x_{2} \leq x_{4}$. Then the functorial factorization data of $\mathrm{data}$ is a functorial factorization data of $x_{3}$ and $x_{4}$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.pdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a functorial factorization data of $x_{1}$ and $x_{2}$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{Z}$ applied to $\mathrm{self}$ and the right function defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.HasFactorizationclassMathlib.CategoryTheory.MorphismProperty.Factorization, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then we can say that $\operatorname{HasFactorization}$ holds for $x_{1}$ and $x_{2}$.

CategoryTheory.MorphismProperty.HasFunctorialFactorizationclassMathlib.CategoryTheory.MorphismProperty.Factorization, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then we can say that $\operatorname{HasFunctorialFactorization}$ holds for $x_{1}$ and $x_{2}$.

CategoryTheory.MorphismProperty.MapFactorizationDatastructureMathlib.CategoryTheory.MorphismProperty.Factorization, type

Wording

map factorization data of x2 and f (from the name)

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map factorization data of $x_{2}$ and $f$ are a basic type.

CategoryTheory.MorphismProperty.MapFactorizationData.ZdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a map factorization data of $x_{2}$ and $f$. Then $\operatorname{Z}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.MapFactorizationData.idefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a map factorization data of $x_{2}$ and $f$. Then $\operatorname{i}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\operatorname{Z}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.MapFactorizationData.ofIsEquivalencedefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the map factorization data of h3 (from the name)

English

Let $h_{3}$ be a map factorization data of $x_{3}$ and the map of $F$ and $f$. Then the map factorization data of $h_{3}$ is a map factorization data of the inverse image of $x_{3}$ and $F$ and $f$.

CategoryTheory.MorphismProperty.MapFactorizationData.opdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the opposite of x2 and hf (from the name)

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Let $\mathrm{hf}$ be a map factorization data of $x_{2}$ and $f$. Then the opposite of $x_{2}$ and $\mathrm{hf}$ is a map factorization data of the opposite of $x_{1}$ and the opposite in $f$.

CategoryTheory.MorphismProperty.MapFactorizationData.opEquivdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the opposite equivalence (from the name)

English

The opposite equivalence is an equivalence from the set of map factorization data of $x_{2}$ and $f$ to the set of map factorization data of the opposite of $x_{1}$ and the opposite in $f$.

CategoryTheory.MorphismProperty.MapFactorizationData.pdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a map factorization data of $x_{2}$ and $f$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{Z}$ applied to $\mathrm{self}$ and $Y$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.MorphismProperty.MapFactorizationData.unopdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the opposite of x3 (from the name)

English

Let $x_{3}$ be a map factorization data of $x_{2}$ and $f$. Then the opposite of $x_{3}$ is a map factorization data of the opposite of $x_{1}$ and the opposite of $f$.

CategoryTheory.MorphismProperty.compdefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the composition of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then the composition of $x_{1}$ and $x_{2}$ is a morphism property of $C$ defined as the function that maps $x_{3}$, $x_{4}$ and $f$ to $\mathrm{Nonempty}$ applied to the set of map factorization data of $x_{2}$ and $f$.

CategoryTheory.MorphismProperty.factorizationDatadefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the factorization data of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then the factorization data of $x_{1}$ and $x_{2}$ is a factorization data of $x_{1}$ and $x_{2}$ defined as the function that maps $x_{3}$, $x_{4}$ and $x_{5}$ to $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_HasFactorization\_\_nonempty\_mapFactorizationData}$ applied to $x_{5}$.

CategoryTheory.MorphismProperty.functorialFactorizationDatadefMathlib.CategoryTheory.MorphismProperty.Factorization, function or constant

Wording

the functorial factorization data of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then the functorial factorization data of $x_{1}$ and $x_{2}$ is a functorial factorization data of $x_{1}$ and $x_{2}$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_MorphismProperty\_\_HasFunctorialFactorization\_\_nonempty\_functorialFactorizationData}$.

Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

CategoryTheory.MorphismProperty.HasCardinalLTdefMathlib.CategoryTheory.MorphismProperty.HasCardinalLT, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Let $x_{1}$ be a cardinal. Then $\operatorname{HasCardinalLT}$ holds for $P$ and $x_{1}$, if $\mathrm{HasCardinalLT}$ holds for the set of elements of the set in $P$ and $x_{1}$.

Mathlib.CategoryTheory.MorphismProperty.Ind

CategoryTheory.MorphismProperty.PreIndSpreadsclassMathlib.CategoryTheory.MorphismProperty.Ind, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Then we can say that $\operatorname{PreIndSpreads}$ holds for $P$.

CategoryTheory.MorphismProperty.inddefMathlib.CategoryTheory.MorphismProperty.Ind, function or constant

Wording

the ind of P (from the name)

English

Let $P$ be a morphism property of $C$. Then the ind of $P$ is a morphism property of $C$ defined as the function that maps $X$, $Y$ and $f$ to the proposition that there exists a set $J$, such that there exists a small category $x_{1}$ of $J$, such that there exists an element $h$ of $\operatorname{IsFiltered}$ applied to $J$, such that there exists a functor $D$ of $J$ and $C$, such that there exists a homomorphism $t$ of the action of the constant of $J$ and $X$ and $D$, such that there exists a homomorphism $s$ of $D$ and the action of the constant of $J$ and $Y$, such that there exists an element $x_{2}$ of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $Y$ and $s$, such that for all elements $j$ of $J$, $P$ holds for the action of the action of the constant of $J$ and $X$ and $j$, the action of $D$ and $j$ and the component of $t$ and $j$ and the composition of the component of $t$ and $j$ and the component of $s$ and $j$ is equal to $f$.

Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

CategoryTheory.MorphismProperty.FunctorsInvertingdefMathlib.CategoryTheory.MorphismProperty.IsInvertedBy, type

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $D$ be a set. Then an element of $\operatorname{FunctorsInverting}$ applied to $W$ and $D$ is an element of the function that maps $W$ and $D$ to the set of full subcategories of the function that maps $F$ to $\operatorname{IsInvertedBy}$ applied to $W$ and $F$.

CategoryTheory.MorphismProperty.FunctorsInverting.mkdefMathlib.CategoryTheory.MorphismProperty.IsInvertedBy, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$ such that $\operatorname{IsInvertedBy}$ holds for $W$ and $F$. Then $\operatorname{mk}$ applied to $F$ and $\mathrm{hF}$ is an element of $\operatorname{FunctorsInverting}$ applied to $W$ and $D$ defined as $\operatorname{mk}$ applied to $F$ and $\mathrm{hF}$.

CategoryTheory.MorphismProperty.IsInvertedBydefMathlib.CategoryTheory.MorphismProperty.IsInvertedBy, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Let $F$ be a functor of $C$ and $D$. Then $\operatorname{IsInvertedBy}$ holds for $P$ and $F$, if for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, if $P$ holds for $X$, $Y$ and $f$, then the map of $F$ and $f$ is an isomorphism.

Mathlib.CategoryTheory.MorphismProperty.IsSmall

CategoryTheory.MorphismProperty.IsSmallclassMathlib.CategoryTheory.MorphismProperty.IsSmall, predicate

Wording

W is a small (from the name)

English

Let $W$ be a morphism property of $C$. Then we can say that $W$ is a small.

Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

CategoryTheory.MorphismProperty.llpdefMathlib.CategoryTheory.MorphismProperty.LiftingProperty, function or constant

Wording

no wording

English

Let $T$ be a morphism property of $C$. Then there is a morphism property of $C$. Proof. Let $T$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $f$ be arbitrary. By C. Let $X$ be arbitrary. By C. Let $Y$ be arbitrary. By X. By Y. By Quiver__Hom. Let $g$ be arbitrary. By X. By Y. By g. By T. By f. By g. By CategoryTheory__HasLiftingProperty. By if. By forall. By forall. By forall.

CategoryTheory.MorphismProperty.rlpdefMathlib.CategoryTheory.MorphismProperty.LiftingProperty, function or constant

Wording

no wording

English

Let $T$ be a morphism property of $C$. Then there is a morphism property of $C$. Proof. Let $T$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. Let $f$ be arbitrary. By C. Let $X$ be arbitrary. By C. Let $Y$ be arbitrary. By X. By Y. By Quiver__Hom. Let $g$ be arbitrary. By X. By Y. By g. By T. By g. By f. By CategoryTheory__HasLiftingProperty. By if. By forall. By forall. By forall.

Mathlib.CategoryTheory.MorphismProperty.Limits

CategoryTheory.MorphismProperty.HasPullbacksclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

P has pullbacks (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ has pullbacks.

CategoryTheory.MorphismProperty.HasPullbacksAgainstclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $P$ and $\mathrm{P'}$ be morphism properties of $C$. Then we can say that $\operatorname{HasPullbacksAgainst}$ holds for $P$ and $\mathrm{P'}$.

CategoryTheory.MorphismProperty.HasPullbacksAlongclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $\operatorname{HasPullbacksAlong}$ holds for $P$ and $f$.

CategoryTheory.MorphismProperty.HasPushoutsclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

P has pushouts (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ has pushouts.

CategoryTheory.MorphismProperty.HasPushoutsAgainstclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $P$ and $\mathrm{P'}$ be morphism properties of $C$. Then we can say that $\operatorname{HasPushoutsAgainst}$ holds for $P$ and $\mathrm{P'}$.

CategoryTheory.MorphismProperty.HasPushoutsAlongclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $\operatorname{HasPushoutsAlong}$ holds for $P$ and $f$.

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

P is a stable under base change (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ is a stable under base change.

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAgainstclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $P$ and $\mathrm{P'}$ be morphism properties of $C$. Then we can say that $\operatorname{IsStableUnderBaseChangeAgainst}$ holds for $P$ and $\mathrm{P'}$.

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlongclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $\operatorname{IsStableUnderBaseChangeAlong}$ holds for $P$ and $f$.

CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

P is a stable under cobase change (from the name)

English

Let $P$ be a morphism property of $C$. Then we can say that $P$ is a stable under cobase change.

CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAgainstclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $P$ and $\mathrm{P'}$ be morphism properties of $C$. Then we can say that $\operatorname{IsStableUnderCobaseChangeAgainst}$ holds for $P$ and $\mathrm{P'}$.

CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlongclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $\operatorname{IsStableUnderCobaseChangeAlong}$ holds for $P$ and $f$.

CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShapeclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then we can say that $\operatorname{IsStableUnderColimitsOfShape}$ holds for $W$ and $J$.

CategoryTheory.MorphismProperty.IsStableUnderCoproductsclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{IsStableUnderCoproducts}$ holds for $W$.

CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShapedefMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then $\operatorname{IsStableUnderCoproductsOfShape}$ holds for $W$ and $J$, if $\operatorname{IsStableUnderColimitsOfShape}$ holds for $W$ and $\operatorname{Discrete}$ applied to $J$.

CategoryTheory.MorphismProperty.IsStableUnderFilteredColimitsclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{IsStableUnderFilteredColimits}$ holds for $W$.

CategoryTheory.MorphismProperty.IsStableUnderFiniteCoproductsclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{IsStableUnderFiniteCoproducts}$ holds for $W$.

CategoryTheory.MorphismProperty.IsStableUnderFiniteProductsclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{IsStableUnderFiniteProducts}$ holds for $W$.

CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShapeclassMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then we can say that $\operatorname{IsStableUnderLimitsOfShape}$ holds for $W$ and $J$.

CategoryTheory.MorphismProperty.IsStableUnderProductsOfShapedefMathlib.CategoryTheory.MorphismProperty.Limits, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then $\operatorname{IsStableUnderProductsOfShape}$ holds for $W$ and $J$, if $\operatorname{IsStableUnderLimitsOfShape}$ holds for $W$ and $\operatorname{Discrete}$ applied to $J$.

CategoryTheory.MorphismProperty.colimitsOfShapeinductiveMathlib.CategoryTheory.MorphismProperty.Limits, function or constant

Wording

the colimit of W and J (from the name)

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then the colimit of $W$ and $J$ is a morphism property of $C$.

CategoryTheory.MorphismProperty.coproductsdefMathlib.CategoryTheory.MorphismProperty.Limits, function or constant

Wording

the coproduct of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the coproduct of $W$ is a morphism property of $C$ defined as the supremum of the function that maps $J$ to the colimit of $W$ and $\operatorname{Discrete}$ applied to $J$.

CategoryTheory.MorphismProperty.diagonaldefMathlib.CategoryTheory.MorphismProperty.Limits, function or constant

Wording

the diagonal of P (from the name)

English

Let $P$ be a morphism property of $C$. Then the diagonal of $P$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to $P$ applied to $x_{1}$, the diagonal object of $f$ and the diagonal morphism of $f$.

CategoryTheory.MorphismProperty.limitsOfShapeinductiveMathlib.CategoryTheory.MorphismProperty.Limits, function or constant

Wording

the limit of W and J (from the name)

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then the limit of $W$ and $J$ is a morphism property of $C$.

CategoryTheory.MorphismProperty.pullbacksdefMathlib.CategoryTheory.MorphismProperty.Limits, function or constant

Wording

the pullback of P (from the name)

English

Let $P$ be a morphism property of $C$. Then the pullback of $P$ is a morphism property of $C$ defined as the function that maps $A$, $B$ and $q$ to the proposition that there exist elements $X$ and $Y$ of $C$, such that there exists a homomorphism $p$ of $X$ and $Y$, such that there exists a homomorphism $f$ of $A$ and $X$, such that there exists a homomorphism $g$ of $B$ and $Y$, such that there exists an element $h$ of $P$ applied to $X$, $Y$ and $p$, such that $\operatorname{IsPullback}$ holds for $f$, $q$, $p$ and $g$.

CategoryTheory.MorphismProperty.pushoutsdefMathlib.CategoryTheory.MorphismProperty.Limits, function or constant

Wording

the pushout of P (from the name)

English

Let $P$ be a morphism property of $C$. Then the pushout of $P$ is a morphism property of $C$ defined as the function that maps $X$, $Y$ and $q$ to the proposition that there exist elements $A$ and $B$ of $C$, such that there exists a homomorphism $p$ of $A$ and $B$, such that there exists a homomorphism $f$ of $A$ and $X$, such that there exists a homomorphism $g$ of $B$ and $Y$, such that there exists an element $h$ of $P$ applied to $A$, $B$ and $p$, such that $\operatorname{IsPushout}$ holds for $f$, $p$, $q$ and $g$.

CategoryTheory.MorphismProperty.universallydefMathlib.CategoryTheory.MorphismProperty.Limits, function or constant

Wording

no wording

English

Let $P$ be a morphism property of $C$. Then there is a morphism property of $C$. Proof. Let $P$ be arbitrary. Let $X$ be arbitrary. Let $Y$ be arbitrary. Let $f$ be arbitrary. By C. Let $\mathrm{X'}$ be arbitrary. By C. Let $\mathrm{Y'}$ be arbitrary. By X'. By X. By Quiver__Hom. Let $x_{1}$ be arbitrary. By Y'. By Y. By Quiver__Hom. Let $x_{2}$ be arbitrary. By X'. By Y'. By Quiver__Hom. Let $\mathrm{f'}$ be arbitrary. By f'. By x1. By x2. By f. By CategoryTheory__IsPullback. By X'. By Y'. By f'. By P. By if. By forall. By forall. By forall. By forall. By forall.

Mathlib.CategoryTheory.MorphismProperty.Local

CategoryTheory.MorphismProperty.IsLocalAtSourceclassMathlib.CategoryTheory.MorphismProperty.Local, predicate

Wording

P is local at source to K (from the name)

English

Let $P$ be a morphism property of $C$. Let $K$ be a precoverage of $C$. Then we can say that $P$ is local at source to $K$.

CategoryTheory.MorphismProperty.IsLocalAtTargetclassMathlib.CategoryTheory.MorphismProperty.Local, predicate

Wording

P is local at target to K (from the name)

English

Let $P$ be a morphism property of $C$. Let $K$ be a precoverage of $C$. Then we can say that $P$ is local at target to $K$.

Mathlib.CategoryTheory.MorphismProperty.LocalClosure

CategoryTheory.MorphismProperty.sourceLocalClosureinductiveMathlib.CategoryTheory.MorphismProperty.LocalClosure, function or constant

Wording

the source local closure of K and P (from the name)

English

Let $K$ be a precoverage of $C$. Let $P$ be a morphism property of $C$. Then the source local closure of $K$ and $P$ is a morphism property of $C$.

CategoryTheory.MorphismProperty.sourceLocalClosure.belowinductiveMathlib.CategoryTheory.MorphismProperty.LocalClosure, predicate

Wording

no wording

English

Assume that $\operatorname{sourceLocalClosure}$ holds for $K$ and $P$. Then we can say that $\operatorname{below}$ holds for $t$.

Mathlib.CategoryTheory.MorphismProperty.LocalEpi

CategoryTheory.ObjectProperty.localEpidefMathlib.CategoryTheory.MorphismProperty.LocalEpi, function or constant

Wording

the local epimorphism of P (from the name)

English

Let $P$ be an object property of $C$. Then the local epimorphism of $P$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that for all elements $Z$ of $C$, if $P$ holds for $Z$, then the function that maps $g$ to the composition of $f$ and $g$ is injective.

Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

CategoryTheory.MorphismProperty.ofObjectPropertydefMathlib.CategoryTheory.MorphismProperty.OfObjectProperty, function or constant

Wording

the morphism property of P and Q (from the name)

English

Let $P$ and $Q$ be object properties of $C$. Then the morphism property of $P$ and $Q$ is a morphism property of $C$ defined as the function that maps $X$, $Y$ and $x_{1}$ to the proposition that $P$ holds for $X$ and $Q$ holds for $Y$.

Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

CategoryTheory.MorphismProperty.Over.mapdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map of Q and hPf (from the name)

English

Let $Q$ be a morphism property of $T$. Assume that $P$ holds for $X$, $Y$ and $f$. Then the map of $Q$ and $\mathrm{hPf}$ is a functor of $\operatorname{Over}$ applied to $P$, $Q$ and $X$ and $\operatorname{Over}$ applied to $P$, $Q$ and $Y$.

CategoryTheory.MorphismProperty.Over.mapCompdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map composition of Q and fg (from the name)

English

Let $Q$ be a morphism property of $T$. Assume that $P$ holds for $X$, $Y$ and $f$. Assume that $P$ holds for $Y$, $Z$ and $g$. Let $\mathrm{fg}$ be an element of $\mathrm{optParam}$ applied to the set of homomorphisms of $X$ and $Z$ and the composition of $f$ and $g$ such that $\mathrm{autoParam}$ holds for the proposition that $\mathrm{fg}$ is equal to the composition of $f$ and $g$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_mapComp\_\_\_auto\_1}$. Then the map composition of $Q$ and $\mathrm{fg}$ is an isomorphism of the map of $Q$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_mapComp\_\_\_proof\_3}$ applied to $\mathrm{hf}$, $\mathrm{hg}$, $\mathrm{fg}$ and $\mathrm{hfg}$ and the composition of the map of $Q$ and $\mathrm{hf}$ and the map of $Q$ and $\mathrm{hg}$.

CategoryTheory.MorphismProperty.Over.mapCongrdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map congruence of Q (from the name)

English

Let $Q$ be a morphism property of $T$. Assume that $\EqtMACRoH {f}{g}$. Assume that $P$ holds for $X$, $Y$ and $f$. Then the map congruence of $Q$ is an isomorphism of the map of $Q$ and $\mathrm{hf}$ and the map of $Q$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_mapCongr\_\_\_proof\_2}$ applied to $\mathrm{hfg}$ and $\mathrm{hf}$.

CategoryTheory.MorphismProperty.Over.mapIddefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map identity of X and f (from the name)

English

Let $Q$ be a morphism property of $T$. Let $X$ be an element of $T$. Let $f$ be an element of $\mathrm{optParam}$ applied to the set of homomorphisms of $X$ and $X$ and the identity morphism of $X$ such that $\mathrm{autoParam}$ holds for the proposition that $f$ is equal to the identity morphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_mapId\_\_\_auto\_1}$. Then the map identity of $X$ and $f$ is an isomorphism of the map of $Q$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_mapId\_\_\_proof\_3}$ applied to $X$, $f$ and $\mathrm{hf}$ and the identity of $\operatorname{Over}$ applied to $P$, $Q$ and $X$.

CategoryTheory.MorphismProperty.Over.mapPullbackAdjdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map pullback adjoint of Q and f (from the name)

English

Let $P$ and $Q$ be morphism properties of $T$. Let $f$ be a homomorphism of $X$ and $Y$ such that $P$ holds for $X$, $Y$ and $f$ and $Q$ holds for $X$, $Y$ and $f$. Then the map pullback adjoint of $Q$ and $f$ is an adjunction of the map of $Q$ and $\mathrm{hPf}$ and the pullback of $Q$ and $f$.

CategoryTheory.MorphismProperty.Over.pullbackdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the pullback of Q and f (from the name)

English

Let $P$ and $Q$ be morphism properties of $T$. Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback of $Q$ and $f$ is a functor of $\operatorname{Over}$ applied to $P$, $Q$ and $Y$ and $\operatorname{Over}$ applied to $P$, $Q$ and $X$.

CategoryTheory.MorphismProperty.Over.pullbackCompdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the pullback composition of g and fg (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{fg}$ be an element of $\mathrm{optParam}$ applied to the set of homomorphisms of $X$ and $Z$ and the composition of $f$ and $g$ such that $\mathrm{autoParam}$ holds for the proposition that $\mathrm{fg}$ is equal to the composition of $f$ and $g$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_pullbackComp\_\_\_auto\_1}$. Then the pullback composition of $g$ and $\mathrm{fg}$ is an isomorphism of the pullback of $Q$ and $\mathrm{fg}$ and the composition of the pullback of $Q$ and $g$ and the pullback of $Q$ and $f$.

CategoryTheory.MorphismProperty.Over.pullbackCompForgetIsodefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{pullbackCompForgetIso}$ applied to $f$ is an isomorphism of the composition of the pullback of $Q$ and $f$ and the forgetful functor from the full subcategory of $P$ and the composition of the forgetful functor from the full subcategory of $P$ and the pullback of $f$ defined as the identity of the composition of the pullback of $Q$ and $f$ and the forgetful functor from the full subcategory of $P$.

CategoryTheory.MorphismProperty.Over.pullbackCongrdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the pullback congruence of h4 (from the name)

English

Assume that $\EqtMACRoH {f}{g}$. Then the pullback congruence of $h_{4}$ is an isomorphism of the pullback of $Q$ and $f$ and the pullback of $Q$ and $g$.

CategoryTheory.MorphismProperty.Over.pullbackMapHomPullbackdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the pullback map homomorphism pullback of g and fg (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$ such that $P$ holds for $X$, $Y$ and $f$ and $Q$ holds for $X$, $Y$ and $f$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{fg}$ be an element of $\mathrm{optParam}$ applied to the set of homomorphisms of $X$ and $Z$ and the composition of $f$ and $g$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and $g$ is equal to $\mathrm{fg}$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Over\_\_pullbackMapHomPullback\_\_\_auto\_1}$. Then the pullback map homomorphism pullback of $g$ and $\mathrm{fg}$ is a homomorphism of the composition of the pullback of $Q$ and $\mathrm{fg}$ and the map of $Q$ and $\mathrm{hPf}$ and the pullback of $Q$ and $g$.

CategoryTheory.MorphismProperty.Under.mapdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map of Q and hPf (from the name)

English

Let $Q$ be a morphism property of $T$. Assume that $P$ holds for $X$, $Y$ and $f$. Then the map of $Q$ and $\mathrm{hPf}$ is a functor of $\operatorname{Under}$ applied to $P$, $Q$ and $Y$ and $\operatorname{Under}$ applied to $P$, $Q$ and $X$.

CategoryTheory.MorphismProperty.Under.mapCompdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map composition of Q and fg (from the name)

English

Let $Q$ be a morphism property of $T$. Assume that $P$ holds for $X$, $Y$ and $f$. Assume that $P$ holds for $Y$, $Z$ and $g$. Let $\mathrm{fg}$ be an element of $\mathrm{optParam}$ applied to the set of homomorphisms of $X$ and $Z$ and the composition of $f$ and $g$ such that $\mathrm{autoParam}$ holds for the proposition that $\mathrm{fg}$ is equal to the composition of $f$ and $g$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Under\_\_mapComp\_\_\_auto\_1}$. Then the map composition of $Q$ and $\mathrm{fg}$ is an isomorphism of the map of $Q$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Under\_\_mapComp\_\_\_proof\_3}$ applied to $\mathrm{hf}$, $\mathrm{hg}$, $\mathrm{fg}$ and $\mathrm{hfg}$ and the composition of the map of $Q$ and $\mathrm{hg}$ and the map of $Q$ and $\mathrm{hf}$.

CategoryTheory.MorphismProperty.Under.mapCongrdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map congruence of Q (from the name)

English

CategoryTheory.MorphismProperty.Under.mapIddefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map identity of X and f (from the name)

English

Let $Q$ be a morphism property of $T$. Let $X$ be an element of $T$. Let $f$ be an element of $\mathrm{optParam}$ applied to the set of homomorphisms of $X$ and $X$ and the identity morphism of $X$ such that $\mathrm{autoParam}$ holds for the proposition that $f$ is equal to the identity morphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Under\_\_mapId\_\_\_auto\_1}$. Then the map identity of $X$ and $f$ is an isomorphism of the map of $Q$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Under\_\_mapId\_\_\_proof\_3}$ applied to $X$, $f$ and $\mathrm{hf}$ and the identity of $\operatorname{Under}$ applied to $P$, $Q$ and $X$.

CategoryTheory.MorphismProperty.Under.mapPushoutAdjdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the map pushout adjoint of Q and f (from the name)

English

Let $P$ and $Q$ be morphism properties of $T$. Let $f$ be a homomorphism of $X$ and $Y$ such that $P$ holds for $X$, $Y$ and $f$ and $Q$ holds for $X$, $Y$ and $f$. Then the map pushout adjoint of $Q$ and $f$ is an adjunction of the pushout of $Q$ and $f$ and the map of $Q$ and $\mathrm{hPf}$.

CategoryTheory.MorphismProperty.Under.pushoutdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the pushout of Q and f (from the name)

English

Let $P$ and $Q$ be morphism properties of $T$. Let $f$ be a homomorphism of $X$ and $Y$. Then the pushout of $Q$ and $f$ is a functor of $\operatorname{Under}$ applied to $P$, $Q$ and $X$ and $\operatorname{Under}$ applied to $P$, $Q$ and $Y$.

CategoryTheory.MorphismProperty.Under.pushoutCompdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the pushout composition of g and fg (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{fg}$ be an element of $\mathrm{optParam}$ applied to the set of homomorphisms of $X$ and $Z$ and the composition of $f$ and $g$ such that $\mathrm{autoParam}$ holds for the proposition that $\mathrm{fg}$ is equal to the composition of $f$ and $g$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_Under\_\_pushoutComp\_\_\_auto\_1}$. Then the pushout composition of $g$ and $\mathrm{fg}$ is an isomorphism of the pushout of $Q$ and $\mathrm{fg}$ and the composition of the pushout of $Q$ and $f$ and the pushout of $Q$ and $g$.

CategoryTheory.MorphismProperty.Under.pushoutCompForgetIsodefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{pushoutCompForgetIso}$ applied to $f$ is an isomorphism of the composition of the pushout of $Q$ and $f$ and the forgetful functor from the full subcategory of $P$ and the composition of the forgetful functor from the full subcategory of $P$ and the pushout of $f$ defined as the identity of the composition of the pushout of $Q$ and $f$ and the forgetful functor from the full subcategory of $P$.

CategoryTheory.MorphismProperty.Under.pushoutCongrdefMathlib.CategoryTheory.MorphismProperty.OverAdjunction, function or constant

Wording

the pushout congruence of h4 (from the name)

English

Assume that $\EqtMACRoH {f}{g}$. Then the pushout congruence of $h_{4}$ is an isomorphism of the pushout of $Q$ and $f$ and the pushout of $Q$ and $g$.

Mathlib.CategoryTheory.MorphismProperty.Quotient

CategoryTheory.MorphismProperty.HasQuotientclassMathlib.CategoryTheory.MorphismProperty.Quotient, predicate

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $\mathrm{homRel}$ be a homomorphism relation of $C$. Then we can say that $\operatorname{HasQuotient}$ holds for $W$ and $\mathrm{homRel}$.

CategoryTheory.MorphismProperty.quotientdefMathlib.CategoryTheory.MorphismProperty.Quotient, function or constant

Wording

the quotient of W and homRel (from the name)

English

Let $W$ be a morphism property of $C$. Let $\mathrm{homRel}$ be a homomorphism relation of $C$. Then the quotient of $W$ and $\mathrm{homRel}$ is a morphism property of the set of quotients of $\mathrm{homRel}$.

Mathlib.CategoryTheory.MorphismProperty.Representable

CategoryTheory.Functor.relativelyRepresentabledefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then there is a morphism property of $D$. Proof. Let $F$ be arbitrary. Let $X$ be arbitrary. Let $Y$ be arbitrary. Let $f$ be arbitrary. By C. Let $a$ be arbitrary. By F. By a. By CategoryTheory__Functor__obj. By Y. By Quiver__Hom. Let $g$ be arbitrary. By C. Let $b$ be arbitrary. By b. By a. By Quiver__Hom. Let $\mathrm{snd}$ be arbitrary. By F. By b. By CategoryTheory__Functor__obj. By X. By Quiver__Hom. Let $\mathrm{fst}$ be arbitrary. By fst. By F. By snd. By CategoryTheory__Functor__map. By f. By g. By CategoryTheory__IsPullback. By exists. By exists. By exists. By forall. By forall.

CategoryTheory.Functor.relativelyRepresentable.fstdefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the first component of hf and g (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, $X$, $Y$ and $f$. Let $g$ be a homomorphism of the action of $F$ and $a$ and $Y$. Then the first component of $\mathrm{hf}$ and $g$ is a homomorphism of the action of $F$ and the pullback of $\mathrm{hf}$ and $g$ and $X$.

CategoryTheory.Functor.relativelyRepresentable.fst'defMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the first component of g and #2 (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $b$, $Y$ and $\mathrm{f'}$. Let $g$ be a homomorphism of the action of $F$ and $a$ and $Y$. Then the first component of $\mathrm{hf'}$ and $g$ is a homomorphism of the pullback of $\mathrm{hf'}$ and $g$ and $b$ defined as the choice of $F$ and the first component of $\mathrm{hf'}$ and $g$.

CategoryTheory.Functor.relativelyRepresentable.liftdefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the lift of i and h (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, $X$, $Y$ and $f$. Let $i$ be a homomorphism of the action of $F$ and $c$ and $X$. Let $h$ be a homomorphism of $c$ and $a$ such that the composition of $i$ and $f$ is equal to the composition of the map of $F$ and $h$ and $g$. Then the lift of $i$ and $h$ is a homomorphism of $c$ and the pullback of $\mathrm{hf}$ and $g$ defined as the choice of $F$ and the lift of $i$ and the map of $F$ and $h$.

CategoryTheory.Functor.relativelyRepresentable.lift'defMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the lift of h and hi (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $b$, $Y$ and $\mathrm{f'}$. Let $i$ be a homomorphism of $c$ and $b$. Let $h$ be a homomorphism of $c$ and $a$ such that the composition of the map of $F$ and $i$ and $\mathrm{f'}$ is equal to the composition of the map of $F$ and $h$ and $g$. Then the lift of $i$ and $h$ is a homomorphism of $c$ and the pullback of $\mathrm{hf'}$ and $g$ defined as the lift of the map of $F$ and $i$ and $h$.

CategoryTheory.Functor.relativelyRepresentable.lift₃defMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the lift of x9 and x10 (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $x_{2}$, $X$ and $x_{5}$. Let $x_{6}$ be a homomorphism of the action of $F$ and $x_{3}$ and $X$. Let $x_{7}$ be a homomorphism of the action of $F$ and $x_{4}$ and $X$. Let $x_{8}$ be a homomorphism of $Z$ and $x_{2}$. Let $x_{9}$ be a homomorphism of $Z$ and $x_{3}$. Let $x_{10}$ be a homomorphism of $Z$ and $x_{4}$. Assume that the composition of the map of $F$ and $x_{8}$ and $x_{5}$ is equal to the composition of the map of $F$ and $x_{9}$ and $x_{6}$. Assume that the composition of the map of $F$ and $x_{8}$ and $x_{5}$ is equal to the composition of the map of $F$ and $x_{10}$ and $x_{7}$. Then the lift of $x_{9}$ and $x_{10}$ is a homomorphism of $Z$ and the pullback of $x_{6}$ and $x_{7}$.

CategoryTheory.Functor.relativelyRepresentable.pullbackdefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the pullback of hf and g (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, $X$, $Y$ and $f$. Let $g$ be a homomorphism of the action of $F$ and $a$ and $Y$. Then the pullback of $\mathrm{hf}$ and $g$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{hf}$ applied to $a$ and $g$.

CategoryTheory.Functor.relativelyRepresentable.pullback₃defMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the pullback of x6 and x7 (from the name)

English

CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁defMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

no wording

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $x_{2}$, $X$ and $x_{5}$. Let $x_{6}$ be a homomorphism of the action of $F$ and $x_{3}$ and $X$. Let $x_{7}$ be a homomorphism of the action of $F$ and $x_{4}$ and $X$. Then $\mathrm{CategoryTheory\_\_Functor\_\_relativelyRepresentable\_\_pullback\_u2083\_\_\_p\_u2081\_}$ applied to $h_{1}$, $x_{6}$ and $x_{7}$ is a homomorphism of the pullback of $x_{6}$ and $x_{7}$ and $x_{2}$ defined as the composition of the first projection of the pullback of the first component of $h_{1}$ and $x_{6}$ and the first component of $h_{1}$ and $x_{7}$ and the first component of $h_{1}$ and $x_{6}$.

CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂defMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

no wording

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $x_{2}$, $X$ and $x_{5}$. Let $x_{6}$ be a homomorphism of the action of $F$ and $x_{3}$ and $X$. Let $x_{7}$ be a homomorphism of the action of $F$ and $x_{4}$ and $X$. Then $\mathrm{CategoryTheory\_\_Functor\_\_relativelyRepresentable\_\_pullback\_u2083\_\_\_p\_u2082\_}$ applied to $h_{1}$, $x_{6}$ and $x_{7}$ is a homomorphism of the pullback of $x_{6}$ and $x_{7}$ and $x_{3}$ defined as the composition of the first projection of the pullback of the first component of $h_{1}$ and $x_{6}$ and the first component of $h_{1}$ and $x_{7}$ and the second component of $h_{1}$ and $x_{6}$.

CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃defMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

no wording

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $x_{2}$, $X$ and $x_{5}$. Let $x_{6}$ be a homomorphism of the action of $F$ and $x_{3}$ and $X$. Let $x_{7}$ be a homomorphism of the action of $F$ and $x_{4}$ and $X$. Then $\mathrm{CategoryTheory\_\_Functor\_\_relativelyRepresentable\_\_pullback\_u2083\_\_\_p\_u2083\_}$ applied to $h_{1}$, $x_{6}$ and $x_{7}$ is a homomorphism of the pullback of $x_{6}$ and $x_{7}$ and $x_{4}$ defined as the composition of the second projection of the pullback of the first component of $h_{1}$ and $x_{6}$ and the first component of $h_{1}$ and $x_{7}$ and the second component of $h_{1}$ and $x_{7}$.

CategoryTheory.Functor.relativelyRepresentable.pullback₃.πdefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the projection of x6 and x7 (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $x_{2}$, $X$ and $x_{5}$. Let $x_{6}$ be a homomorphism of the action of $F$ and $x_{3}$ and $X$. Let $x_{7}$ be a homomorphism of the action of $F$ and $x_{4}$ and $X$. Then the projection of $x_{6}$ and $x_{7}$ is a homomorphism of the action of $F$ and the pullback of $x_{6}$ and $x_{7}$ and $X$ defined as the composition of the map of $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_relativelyRepresentable\_\_pullback\_u2083\_\_\_p\_u2081\_}$ applied to $h_{1}$, $x_{6}$ and $x_{7}$ and $x_{5}$.

CategoryTheory.Functor.relativelyRepresentable.snddefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the second component of hf and g (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, $X$, $Y$ and $f$. Let $g$ be a homomorphism of the action of $F$ and $a$ and $Y$. Then the second component of $\mathrm{hf}$ and $g$ is a homomorphism of the pullback of $\mathrm{hf}$ and $g$ and $a$.

CategoryTheory.Functor.relativelyRepresentable.symmetrydefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the symmetry of hg and #2 (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $b$, $Y$ and $\mathrm{f'}$. Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $a$, $Y$ and $g$. Then the symmetry of $\mathrm{hf'}$ and $\mathrm{hg}$ is a homomorphism of the pullback of $\mathrm{hf'}$ and $g$ and the pullback of $\mathrm{hg}$ and $\mathrm{f'}$.

CategoryTheory.Functor.relativelyRepresentable.symmetryIsodefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the symmetry isomorphism of hg and #2 (from the name)

English

Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $b$, $Y$ and $\mathrm{f'}$. Assume that $\operatorname{relativelyRepresentable}$ holds for $F$, the action of $F$ and $a$, $Y$ and $g$. Then the symmetry isomorphism of $\mathrm{hf'}$ and $\mathrm{hg}$ is an isomorphism of the pullback of $\mathrm{hf'}$ and $g$ and the pullback of $\mathrm{hg}$ and $\mathrm{f'}$.

CategoryTheory.MorphismProperty.presheafdefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

the presheaf of P (from the name)

English

Let $P$ be a morphism property of $C$. Then the presheaf of $P$ is a morphism property of the set of functors of the set of opposites of $C$ and the set of sets defined as $\operatorname{relative}$ applied to the Yoneda and $P$.

CategoryTheory.MorphismProperty.relativedefMathlib.CategoryTheory.MorphismProperty.Representable, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Let $P$ be a morphism property of $C$. Then there is a morphism property of $D$. Proof. Let $F$ be arbitrary. Let $P$ be arbitrary. Let $X$ be arbitrary. Let $Y$ be arbitrary. Let $f$ be arbitrary. By F. By X. By Y. By f. By CategoryTheory__Functor__relativelyRepresentable. By C. Let $a$ be arbitrary. By C. Let $b$ be arbitrary. By F. By a. By CategoryTheory__Functor__obj. By Y. By Quiver__Hom. Let $g$ be arbitrary. By F. By b. By CategoryTheory__Functor__obj. By X. By Quiver__Hom. Let $\mathrm{fst}$ be arbitrary. By b. By a. By Quiver__Hom. Let $\mathrm{snd}$ be arbitrary. By fst. By F. By snd. By CategoryTheory__Functor__map. By f. By g. By CategoryTheory__IsPullback. By b. By a. By snd. By P. By if. By forall. By forall. By forall. By forall. By forall. By and.

Mathlib.CategoryTheory.MorphismProperty.Retract

CategoryTheory.MorphismProperty.IsStableUnderRetractsclassMathlib.CategoryTheory.MorphismProperty.Retract, predicate

Wording

no wording

English

Let $P$ be a morphism property of $C$. Then we can say that $\operatorname{IsStableUnderRetracts}$ holds for $P$.

CategoryTheory.MorphismProperty.retractsdefMathlib.CategoryTheory.MorphismProperty.Retract, function or constant

Wording

the retract of P (from the name)

English

Let $P$ be a morphism property of $C$. Then the retract of $P$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that there exist elements $Z$ and $W$ of $C$, such that there exists a homomorphism $g$ of $Z$ and $W$, such that there exists a retract arrow $x_{3}$ of $f$ and $g$, such that $P$ holds for $Z$, $W$ and $g$.

Mathlib.CategoryTheory.MorphismProperty.RetractArgument

CategoryTheory.RetractArrow.ofLeftLiftingPropertydefMathlib.CategoryTheory.MorphismProperty.RetractArgument, function or constant

Wording

the retract arrow of h (from the name)

English

Assume that the composition of $i$ and $p$ is equal to $f$. Then the retract arrow of $h$ is a retract arrow of $f$ and $i$.

CategoryTheory.RetractArrow.ofRightLiftingPropertydefMathlib.CategoryTheory.MorphismProperty.RetractArgument, function or constant

Wording

the retract arrow of h (from the name)

English

Assume that the composition of $i$ and $p$ is equal to $f$. Then the retract arrow of $h$ is a retract arrow of $f$ and $p$.

Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

CategoryTheory.MorphismProperty.IsStableUnderInfiniteCompositiondefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, predicate

Wording

W is stable under infinite composition (from the name)

English

Let $W$ be a morphism property of $C$. Then $W$ is stable under infinite composition, if $W$ is a stable under transfinite composition of shape.

CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionclassMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, predicate

Wording

W is stable under transfinite composition (from the name)

English

Let $W$ be a morphism property of $C$. Then we can say that $W$ is stable under transfinite composition.

CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShapeclassMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, predicate

Wording

W is a stable under transfinite composition of shape (from the name)

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then we can say that $W$ is a stable under transfinite composition of shape.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShapestructureMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, type

Wording

transfinite composition of shape of J and f (from the name)

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the transfinite compositions of shape of $J$ and $f$ are a basic type.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.icidefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

no wording

English

Let $h_{1}$ be a transfinite composition of shape of $J$ and $f$. Let $j$ be an element of $J$. Then $\operatorname{ici}$ applied to $h_{1}$ and $j$ is a transfinite composition of shape of the set of elements of $\operatorname{Ici}$ applied to $j$ and the component of the inclusion of $\operatorname{toTransfiniteCompositionOfShape}$ applied to $h_{1}$ and $j$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.iddefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the identity of W and X (from the docstring)

English

Let $W$ be a morphism property of $C$. Let $X$ be an element of $C$. Then the identity of $W$ and $X$ is a transfinite composition of shape of $\mathrm{Fin}$ applied to $1$ and the identity morphism of $X$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.iicdefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

no wording

English

Let $h_{1}$ be a transfinite composition of shape of $J$ and $f$. Let $j$ be an element of $J$. Then $\operatorname{iic}$ applied to $h_{1}$ and $j$ is a transfinite composition of shape of the set of elements of $\operatorname{Iic}$ applied to $j$ and the map of $\operatorname{F}$ applied to $\operatorname{toTransfiniteCompositionOfShape}$ applied to $h_{1}$ and the homomorphism of $\mathrm{bot\_le}$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mapdefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the map of h3 (from the name)

English

Let $h_{3}$ be a transfinite composition of shape of $J$ and $f$. Then the map of $h_{3}$ is a transfinite composition of shape of $J$ and the map of $F$ and $f$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofArrowIsodefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the transfinite composition of shape of h1 and e (from the name)

English

Let $h_{1}$ be a transfinite composition of shape of $J$ and $f$. Let $e$ be an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $\mathrm{f'}$. Then the transfinite composition of shape of $h_{1}$ and $e$ is a transfinite composition of shape of $J$ and $\mathrm{f'}$ defined as $\operatorname{mk}$ applied to the transfinite composition of shape of $\operatorname{toTransfiniteCompositionOfShape}$ applied to $h_{1}$ and $e$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_TransfiniteCompositionOfShape\_\_map\_mem}$ applied to $h_{1}$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofCompdefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the transfinite composition of shape of f and g (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Assume that $W$ holds for $X$, $Y$ and $f$. Assume that $W$ holds for $Y$, $Z$ and $g$. Then the transfinite composition of shape of $f$ and $g$ is a transfinite composition of shape of $\mathrm{Fin}$ applied to $3$ and the composition of $f$ and $g$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrowsdefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the transfinite composition of shape of W and F (from the name)

English

Let $W$ be a morphism property of $C$. Let $F$ be a composable arrow of $C$ and $n$ such that for all elements $i$ of $\mathrm{Fin}$ applied to $n$, $W$ holds for the action of $F$ and $\operatorname{castSucc}$ applied to $i$, the action of $F$ and $\operatorname{succ}$ applied to $i$ and the map of $F$ and the homomorphism of $\mathrm{Fin\_\_castSucc\_le\_succ}$ applied to $i$. Then the transfinite composition of shape of $W$ and $F$ is a transfinite composition of shape of $\mathrm{Fin}$ applied to $n + 1$ and the homomorphism of $F$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofLEdefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the transfinite composition of shape of h1 and hW (from the name)

English

Let $h_{1}$ be a transfinite composition of shape of $J$ and $f$. Assume that $W \leq \mathrm{W'}$. Then the transfinite composition of shape of $h_{1}$ and $\mathrm{hW}$ is a transfinite composition of shape of $J$ and $f$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofMemdefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the transfinite composition of shape of f and hf (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$ such that $W$ holds for $X$, $Y$ and $f$. Then the transfinite composition of shape of $f$ and $\mathrm{hf}$ is a transfinite composition of shape of $\mathrm{Fin}$ applied to $2$ and $f$.

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofOrderIsodefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the transfinite composition of shape of h1 and e (from the name)

English

Let $h_{1}$ be a transfinite composition of shape of $J$ and $f$. Let $e$ be an order isomorphism of $\mathrm{J'}$ and $J$. Then the transfinite composition of shape of $h_{1}$ and $e$ is a transfinite composition of shape of $\mathrm{J'}$ and $f$.

CategoryTheory.MorphismProperty.transfiniteCompositionsdefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the transfinite composition of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the transfinite composition of $W$ is a morphism property of $C$ defined as the supremum of the function that maps $J$ to the supremum of the function that maps $x_{1}$ to the supremum of the function that maps $x_{2}$ to the supremum of the function that maps $x_{3}$ to the supremum of the function that maps $h$ to the transfinite composition of $W$ and $J$.

CategoryTheory.MorphismProperty.transfiniteCompositionsOfShapedefMathlib.CategoryTheory.MorphismProperty.TransfiniteComposition, function or constant

Wording

the transfinite composition of W and J (from the name)

English

Let $W$ be a morphism property of $C$. Let $J$ be a set. Then the transfinite composition of $W$ and $J$ is a morphism property of $C$ defined as the function that maps $x_{4}$, $x_{5}$ and $f$ to $\mathrm{Nonempty}$ applied to the set of transfinite compositions of shape of $J$ and $f$.

Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem

CategoryTheory.MorphismProperty.IsWeakFactorizationSystemclassMathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then we can say that $\operatorname{IsWeakFactorizationSystem}$ holds for $x_{1}$ and $x_{2}$.

Mathlib.CategoryTheory.NatIso

CategoryTheory.Functor.copyObjdefMathlib.CategoryTheory.NatIso, function or constant

Wording

the copy object of obj and e (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{obj}$ be a function from elements of $C$ to elements of $D$. Let $e$ be a function from elements $X$ of $C$ to isomorphisms of the action of $F$ and $X$ and $\mathrm{obj}$ applied to $X$. Then the copy object of $\mathrm{obj}$ and $X$ is a functor of $C$ and $D$.

CategoryTheory.Functor.isoCopyObjdefMathlib.CategoryTheory.NatIso, function or constant

Wording

the isomorphism copy object of obj and e (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{obj}$ be a function from elements of $C$ to elements of $D$. Let $e$ be a function from elements $X$ of $C$ to isomorphisms of the action of $F$ and $X$ and $\mathrm{obj}$ applied to $X$. Then the isomorphism copy object of $\mathrm{obj}$ and $X$ is an isomorphism of $F$ and the copy object of $\mathrm{obj}$ and $e$.

CategoryTheory.Iso.appdefMathlib.CategoryTheory.NatIso, function or constant

Wording

the application of x2 and X (from the docstring)

English

Let $x_{2}$ be an isomorphism of $F$ and $G$. Let $X$ be an element of $C$. Then the application of $x_{2}$ and $X$ is an isomorphism of the action of $F$ and $X$ and the action of $G$ and $X$.

CategoryTheory.NatIso.hcompdefMathlib.CategoryTheory.NatIso, function or constant

Wording

no wording

English

Let $x_{3}$ be an isomorphism of $F$ and $G$. Let $x_{4}$ be an isomorphism of $H$ and $I$. Then $\operatorname{hcomp}$ applied to $x_{3}$ and $x_{4}$ is an isomorphism of the composition of $F$ and $H$ and the composition of $G$ and $I$.

CategoryTheory.NatIso.ofComponentsdefMathlib.CategoryTheory.NatIso, function or constant

Wording

the natural isomorphism of app and X1 (from the name)

English

Let $\mathrm{app}$ be a function from elements $X_{1}$ of $C$ to isomorphisms of the action of $F$ and $X_{1}$ and the action of $G$ and $X_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, the composition of the map of $F$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $Y$ is equal to the composition of the homomorphism of $\mathrm{app}$ applied to $X$ and the map of $G$ and $f$ and $\mathrm{CategoryTheory\_\_NatIso\_\_ofComponents\_\_\_auto\_1}$. Then the natural isomorphism of $X_{1}$ and $\mathrm{app}$ is an isomorphism of $F$ and $G$.

CategoryTheory.NatIso.ofComponents'defMathlib.CategoryTheory.NatIso, function or constant

Wording

the natural isomorphism of app and X1 (from the name)

English

Let $\mathrm{app}$ be a function from elements $X_{1}$ of $C$ to isomorphisms of the action of $F$ and $X_{1}$ and the action of $G$ and $X_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $Y$ and $X$, the composition of the inverse of $\mathrm{app}$ applied to $Y$ and the map of $F$ and $f$ is equal to the composition of the map of $G$ and $f$ and the inverse of $\mathrm{app}$ applied to $X$ and $\mathrm{CategoryTheory\_\_NatIso\_\_ofComponents'\_\_\_auto\_1}$. Then the natural isomorphism of $X_{1}$ and $\mathrm{app}$ is an isomorphism of $F$ and $G$.

Mathlib.CategoryTheory.NatTrans

CategoryTheory.NatTransstructureMathlib.CategoryTheory.NatTrans, type

Wording

natural transformation of F and G (from the name)

English

Let $F$ and $G$ be functors of $C$ and $D$. Then the natural transformations of $F$ and $G$ are a basic type.

CategoryTheory.NatTrans.appdefMathlib.CategoryTheory.NatTrans, function or constant

Wording

the component of self and X (from the docstring)

English

Let $\mathrm{self}$ be a natural transformation of $F$ and $G$. Let $X$ be an element of $C$. Then the component of $\mathrm{self}$ and $X$ is a homomorphism of the action of $F$ and $X$ and the action of $G$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $X$.

CategoryTheory.NatTrans.iddefMathlib.CategoryTheory.NatTrans, function or constant

Wording

the identity of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the identity of $F$ is a natural transformation of $F$ and $F$.

CategoryTheory.NatTrans.vcompdefMathlib.CategoryTheory.NatTrans, function or constant

Wording

the vertical composition of x2 and x3 (from the name)

English

Let $x_{2}$ be a natural transformation of $F$ and $G$. Let $x_{3}$ be a natural transformation of $G$ and $H$. Then the vertical composition of $x_{2}$ and $x_{3}$ is a natural transformation of $F$ and $H$.

Mathlib.CategoryTheory.Noetherian

CategoryTheory.ArtinianclassMathlib.CategoryTheory.Noetherian, predicate

Wording

C is a Artinian (from the name)

English

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

CategoryTheory.NoetherianclassMathlib.CategoryTheory.Noetherian, predicate

Wording

C is Noetherian (from the name)

English

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

Mathlib.CategoryTheory.ObjectProperty.Basic

CategoryTheory.ObjectPropertydefMathlib.CategoryTheory.ObjectProperty.Basic, type

Wording

object property of C (from the name)

English

Let $C$ be a set. Then an object property of $C$ is an element of the function that maps $C$ to the set of functions from elements of $C$ to propositions.

CategoryTheory.ObjectProperty.IsclassMathlib.CategoryTheory.ObjectProperty.Basic, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Let $X$ be an element of $C$. Then we can say that $\operatorname{Is}$ holds for $P$ and $X$.

CategoryTheory.ObjectProperty.NonemptyclassMathlib.CategoryTheory.ObjectProperty.Basic, predicate

Wording

P is nonempty (from the name)

English

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

CategoryTheory.ObjectProperty.arbitrarydefMathlib.CategoryTheory.ObjectProperty.Basic, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Then $\operatorname{arbitrary}$ applied to $P$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_ObjectProperty\_\_exists\_prop\_of\_nonempty}$ applied to $P$.

CategoryTheory.ObjectProperty.inverseImagedefMathlib.CategoryTheory.ObjectProperty.Basic, function or constant

Wording

the inverse image of P and F (from the docstring)

English

Let $P$ be an object property of $D$. Let $F$ be a functor of $C$ and $D$. Then the inverse image of $P$ and $F$ is an object property of $C$ defined as the function that maps $X$ to $P$ applied to the action of $F$ and $X$.

CategoryTheory.ObjectProperty.mapdefMathlib.CategoryTheory.ObjectProperty.Basic, function or constant

Wording

the map of P and F (from the name)

English

Let $P$ be an object property of $C$. Let $F$ be a functor of $C$ and $D$. Then the map of $P$ and $F$ is an object property of $D$ defined as the function that maps $Y$ to the proposition that there exists an element $X$ of $C$, such that $P$ holds for $X$ and $\mathrm{Nonempty}$ holds for the set of isomorphisms of the action of $F$ and $X$ and $Y$.

CategoryTheory.ObjectProperty.ofObjinductiveMathlib.CategoryTheory.ObjectProperty.Basic, function or constant

Wording

the object property of X (from the name)

English

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Then the object property of $X$ is an object property of $C$.

CategoryTheory.ObjectProperty.pairdefMathlib.CategoryTheory.ObjectProperty.Basic, function or constant

Wording

the pair of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $C$. Then the pair of $X$ and $Y$ is an object property of $C$ defined as the object property of $\operatorname{elim}$ applied to the function that maps $x_{1}$ to $X$ and the function that maps $x_{2}$ to $Y$.

CategoryTheory.ObjectProperty.singletondefMathlib.CategoryTheory.ObjectProperty.Basic, function or constant

Wording

the singleton of X (from the name)

English

Let $X$ be an element of $C$. Then the singleton of $X$ is an object property of $C$ defined as the object property of the function that maps $x_{1}$ to $X$.

CategoryTheory.ObjectProperty.strictMapinductiveMathlib.CategoryTheory.ObjectProperty.Basic, function or constant

Wording

the strict image of P and F (from the docstring)

English

Let $P$ be an object property of $C$. Let $F$ be a functor of $C$ and $D$. Then the strict image of $P$ and $F$ is an object property of $D$.

Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

CategoryTheory.ObjectProperty.IsClosedUnderIsomorphismsclassMathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderIsomorphisms}$ holds for $P$.

CategoryTheory.ObjectProperty.isoClosuredefMathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms, function or constant

Wording

the isomorphism closure of P (from the name)

English

Let $P$ be an object property of $C$. Then the isomorphism closure of $P$ is an object property of $C$ defined as the function that maps $X$ to the proposition that there exists an element $Y$ of $C$, such that there exists an element $h$ of $P$ applied to $Y$, such that $\mathrm{Nonempty}$ holds for the set of isomorphisms of $X$ and $Y$.

Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

CategoryTheory.ObjectProperty.colimitsCardinalClosuredefMathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure, function or constant

Wording

the colimit cardinal closure of P and x1 (from the name)

English

Let $P$ be an object property of $C$. Let $x_{1}$ be a cardinal. Then the colimit cardinal closure of $P$ and $x_{1}$ is an object property of $C$ defined as the closure of $P$ and the set of elements of $\operatorname{categoryFamily}$ applied to $x_{1}$.

Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure

CategoryTheory.ObjectProperty.colimitClosuredefMathlib.CategoryTheory.ObjectProperty.ColimitsClosure, function or constant

Wording

the closure of P and J (from the docstring)

English

Let $P$ be an object property of $C$. Let $J$ be a set. Then the closure of $P$ and $J$ is an object property of $C$ defined as the closure of $P$ and the function that maps $x_{2}$ to $J$.

CategoryTheory.ObjectProperty.colimitsClosureinductiveMathlib.CategoryTheory.ObjectProperty.ColimitsClosure, function or constant

Wording

the closure of P and J (from the docstring)

English

Let $P$ be an object property of $C$. Let $J$ be a function from elements of $x_{1}$ to sets. Then the closure of $P$ and $J$ is an object property of $C$.

CategoryTheory.ObjectProperty.colimitsClosure.belowinductiveMathlib.CategoryTheory.ObjectProperty.ColimitsClosure, predicate

Wording

no wording

English

Assume that $\operatorname{colimitsClosure}$ holds for $P$ and $J$. Then we can say that $\operatorname{below}$ holds for $t$.

Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

CategoryTheory.ObjectProperty.ColimitOfShapestructureMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, type

Wording

colimit of shape of J and X (from the name)

English

Let $P$ be an object property of $C$. Let $J$ be a set. Let $X$ be an element of $C$. Then the colimits of shape of $J$ and $X$ are a basic type.

CategoryTheory.ObjectProperty.ColimitOfShape.colimitdefMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, function or constant

Wording

the colimit of F and hF (from the name)

English

Let $F$ be a functor of $J$ and $C$ such that for all elements $j$ of $J$, $P$ holds for the action of $F$ and $j$. Then the colimit of $F$ and $\mathrm{hF}$ is a colimit of shape of $J$ and the colimit of $F$ defined as $\operatorname{mk}$ applied to the colimit of $F$ and $\mathrm{hF}$.

CategoryTheory.ObjectProperty.ColimitOfShape.ofIsodefMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, function or constant

Wording

the colimit of shape of h and e (from the name)

English

Let $h$ be a colimit of shape of $J$ and $X$. Let $e$ be an isomorphism of $X$ and $Y$. Then the colimit of shape of $h$ and $e$ is a colimit of shape of $J$ and $Y$ defined as $\operatorname{mk}$ applied to the colimit presentation of $\operatorname{toColimitPresentation}$ applied to $h$ and $e$ and $\mathrm{CategoryTheory\_\_ObjectProperty\_\_ColimitOfShape\_\_prop\_diag\_obj}$ applied to $h$.

CategoryTheory.ObjectProperty.ColimitOfShape.ofLEdefMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, function or constant

Wording

the colimit of shape of h and hPQ (from the name)

English

Let $h$ be a colimit of shape of $J$ and $X$. Assume that $P \leq Q$. Then the colimit of shape of $h$ and $\mathrm{hPQ}$ is a colimit of shape of $J$ and $X$.

CategoryTheory.ObjectProperty.ColimitOfShape.reindexdefMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, function or constant

Wording

the reindexing of h and G (from the name)

English

Let $h$ be a colimit of shape of $J$ and $X$. Let $G$ be a functor of $\mathrm{J'}$ and $J$. Then the reindexing of $h$ and $G$ is a colimit of shape of $\mathrm{J'}$ and $X$.

CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrowdefMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, function or constant

Wording

the costructured arrow of p (from the name)

English

Let $p$ be a colimit of shape of $J$ and $X$. Then the costructured arrow of $p$ is a functor of $J$ and the set of costructured arrows of the inclusion of $P$ and $X$.

CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShapeclassMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Let $J$ be a set. Then we can say that $\operatorname{IsClosedUnderColimitsOfShape}$ holds for $P$ and $J$.

CategoryTheory.ObjectProperty.colimitsOfShapedefMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, function or constant

Wording

the colimit of P and J (from the name)

English

Let $P$ be an object property of $C$. Let $J$ be a set. Then the colimit of $P$ and $J$ is an object property of $C$ defined as the function that maps $X$ to $\mathrm{Nonempty}$ applied to the set of colimits of shape of $J$ and $X$.

CategoryTheory.ObjectProperty.strictColimitsOfShapeinductiveMathlib.CategoryTheory.ObjectProperty.ColimitsOfShape, function or constant

Wording

the strict colimit of P and J (from the name)

English

Let $P$ be an object property of $C$. Let $J$ be a set. Then the strict colimit of $P$ and $J$ is an object property of $C$.

Mathlib.CategoryTheory.ObjectProperty.Comma

CategoryTheory.ObjectProperty.commadefMathlib.CategoryTheory.ObjectProperty.Comma, function or constant

Wording

the comma of x7 and x8 (from the name)

English

Let $x_{5}$ be a functor of $x$ and $D$. Let $x_{6}$ be a functor of $x_{1}$ and $D$. Let $x_{7}$ be an object property of $x$. Let $x_{8}$ be an object property of $x_{1}$. Then the comma of $x_{7}$ and $x_{8}$ is an object property of the set of commas of $x_{5}$ and $x_{6}$ defined as the minimum of the inverse image of $x_{7}$ and the first component of $x_{5}$ and $x_{6}$ and the inverse image of $x_{8}$ and the second component of $x_{5}$ and $x_{6}$.

Mathlib.CategoryTheory.ObjectProperty.ContainsZero

CategoryTheory.Functor.kerneldefMathlib.CategoryTheory.ObjectProperty.ContainsZero, function or constant

Wording

the kernel of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the kernel of $F$ is an object property of $C$ defined as the inverse image of the proposition that $\operatorname{IsZero}$ and $F$.

CategoryTheory.ObjectProperty.ContainsZeroclassMathlib.CategoryTheory.ObjectProperty.ContainsZero, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{ContainsZero}$ holds for $P$.

Mathlib.CategoryTheory.ObjectProperty.EpiMono

CategoryTheory.ObjectProperty.IsClosedUnderQuotientsclassMathlib.CategoryTheory.ObjectProperty.EpiMono, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderQuotients}$ holds for $P$.

CategoryTheory.ObjectProperty.IsClosedUnderSubobjectsclassMathlib.CategoryTheory.ObjectProperty.EpiMono, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderSubobjects}$ holds for $P$.

Mathlib.CategoryTheory.ObjectProperty.Equivalence

CategoryTheory.Equivalence.congrFullSubcategorydefMathlib.CategoryTheory.ObjectProperty.Equivalence, function or constant

Wording

the congruence full subcategory of e and h1 (from the name)

English

Let $e$ be an equivalence of $C$ and $D$ such that the inverse image of $Q$ and the functor of $e$ is equal to $P$. Then the congruence full subcategory of $e$ and $h_{1}$ is an equivalence of the set of full subcategories of $P$ and the set of full subcategories of $Q$.

CategoryTheory.ObjectProperty.topEquivalencedefMathlib.CategoryTheory.ObjectProperty.Equivalence, function or constant

Wording

the equivalence between the full subcategory of C (from the docstring)

English

Let $C$ be a set. Then the equivalence between the full subcategory of $C$ is an equivalence of the set of full subcategories of the top and $C$.

Mathlib.CategoryTheory.ObjectProperty.Extensions

CategoryTheory.ObjectProperty.IsClosedUnderExtensionsclassMathlib.CategoryTheory.ObjectProperty.Extensions, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderExtensions}$ holds for $P$.

Mathlib.CategoryTheory.ObjectProperty.FiniteLimits

CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimitsclassMathlib.CategoryTheory.ObjectProperty.FiniteLimits, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderFiniteColimits}$ holds for $P$.

CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimitsclassMathlib.CategoryTheory.ObjectProperty.FiniteLimits, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderFiniteLimits}$ holds for $P$.

Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

CategoryTheory.ObjectProperty.IsClosedUnderBinaryCoproductsdefMathlib.CategoryTheory.ObjectProperty.FiniteProducts, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then $\operatorname{IsClosedUnderBinaryCoproducts}$ holds for $P$, if $\operatorname{IsClosedUnderColimitsOfShape}$ holds for $P$ and $\operatorname{Discrete}$ applied to the set of walking pairs.

CategoryTheory.ObjectProperty.IsClosedUnderBinaryProductsdefMathlib.CategoryTheory.ObjectProperty.FiniteProducts, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then $\operatorname{IsClosedUnderBinaryProducts}$ holds for $P$, if $\operatorname{IsClosedUnderLimitsOfShape}$ holds for $P$ and $\operatorname{Discrete}$ applied to the set of walking pairs.

CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproductsclassMathlib.CategoryTheory.ObjectProperty.FiniteProducts, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderFiniteCoproducts}$ holds for $P$.

CategoryTheory.ObjectProperty.IsClosedUnderFiniteProductsclassMathlib.CategoryTheory.ObjectProperty.FiniteProducts, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderFiniteProducts}$ holds for $P$.

CategoryTheory.ObjectProperty.binaryCoproductsClosuredefMathlib.CategoryTheory.ObjectProperty.FiniteProducts, function or constant

Wording

the binary coproduct closure of P (from the name)

English

Let $P$ be an object property of $C$. Then the binary coproduct closure of $P$ is an object property of $C$ defined as the closure of $P$ and $\operatorname{Discrete}$ applied to the set of walking pairs.

CategoryTheory.ObjectProperty.binaryProductsClosuredefMathlib.CategoryTheory.ObjectProperty.FiniteProducts, function or constant

Wording

the binary product closure of P (from the name)

English

Let $P$ be an object property of $C$. Then the binary product closure of $P$ is an object property of $C$ defined as the closure of $P$ and $\operatorname{Discrete}$ applied to the set of walking pairs.

Mathlib.CategoryTheory.ObjectProperty.FullSubcategory

CategoryTheory.ObjectProperty.FullSubcategorystructureMathlib.CategoryTheory.ObjectProperty.FullSubcategory, type

Wording

full subcategory of P (from the name)

English

Let $P$ be an object property of $C$. Then the full subcategories of $P$ are a basic type.

CategoryTheory.ObjectProperty.FullSubcategory.objdefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the object of self (from the name)

English

Let $\mathrm{self}$ be a full subcategory of $P$. Then the object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.ObjectProperty.fullyFaithfulιdefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the inclusion of P (from the docstring)

English

Let $P$ be an object property of $C$. Then the inclusion of $P$ is an element of $\operatorname{FullyFaithful}$ applied to the inclusion of $P$.

CategoryTheory.ObjectProperty.fullyFaithfulιOfLEdefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the fully faithful inclusion of h (from the name)

English

generation took over the time limit

CategoryTheory.ObjectProperty.homMkdefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of the object of $X$ and the object of $Y$. Then the homomorphism of $f$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $f$.

CategoryTheory.ObjectProperty.isoMkdefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the isomorphism of P and e (from the name)

English

Let $P$ be an object property of $C$. Let $e$ be an isomorphism of the object of $X$ and the object of $Y$. Then the isomorphism of $P$ and $e$ is an isomorphism of $X$ and $Y$.

CategoryTheory.ObjectProperty.liftdefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the lift of P and F (from the name)

English

Let $P$ be an object property of $D$. Let $F$ be a functor of $C$ and $D$ such that for all elements $X$ of $C$, $P$ holds for the action of $F$ and $X$. Then the lift of $P$ and $F$ is a functor of $C$ and the set of full subcategories of $P$.

CategoryTheory.ObjectProperty.liftCompιIsodefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the lift composition inclusion isomorphism of P and F (from the name)

English

Let $P$ be an object property of $D$. Let $F$ be a functor of $C$ and $D$ such that for all elements $X$ of $C$, $P$ holds for the action of $F$ and $X$. Then the lift composition inclusion isomorphism of $P$ and $F$ is an isomorphism of the composition of the lift of $P$ and $F$ and the inclusion of $P$ and $F$ defined as the identity of the composition of the lift of $P$ and $F$ and the inclusion of $P$.

CategoryTheory.ObjectProperty.liftCompιOfLEIsodefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the lift composition inclusion of P and F (from the name)

English

Let $P$ be an object property of $D$. Let $F$ be a functor of $C$ and $D$ such that for all elements $X_{1}$ of $C$, $P$ holds for the action of $F$ and $X_{1}$. Assume that $P \leq Q$. Then the lift composition inclusion of $P$ and $F$ is an isomorphism of the composition of the lift of $P$ and $F$ and the inclusion of $h$ and the lift of $Q$ and $F$ defined as the identity of the composition of the lift of $P$ and $F$ and the inclusion of $h$.

CategoryTheory.ObjectProperty.ιdefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the inclusion of P (from the name)

English

Let $P$ be an object property of $C$. Then the inclusion of $P$ is a functor of the set of full subcategories of $P$ and $C$ defined as the induced functor of $\operatorname{obj}$.

CategoryTheory.ObjectProperty.ιOfLEdefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $P \leq \mathrm{P'}$. Then the inclusion of $h$ is a functor of the set of full subcategories of $P$ and the set of full subcategories of $\mathrm{P'}$.

CategoryTheory.ObjectProperty.ιOfLECompιIsodefMathlib.CategoryTheory.ObjectProperty.FullSubcategory, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $P \leq \mathrm{P'}$. Then the inclusion of $h$ is an isomorphism of the composition of the inclusion of $h$ and the inclusion of $\mathrm{P'}$ and the inclusion of $P$ defined as the identity of the composition of the inclusion of $h$ and the inclusion of $\mathrm{P'}$.

Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

CategoryTheory.ObjectProperty.preservesColimitdefMathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits, function or constant

Wording

no wording

English

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

CategoryTheory.ObjectProperty.preservesColimitsOfShapedefMathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits, function or constant

Wording

no wording

English

Let $K$ be a set. Then there is an object property of the set of functors of $J$ and $C$. Proof. Let $K$ be arbitrary. By CategoryTheory__Limits__PreservesColimitsOfShape.

CategoryTheory.ObjectProperty.preservesFiniteColimitsdefMathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits, function or constant

Wording

no wording

English

There is an object property of the set of functors of $J$ and $C$. Proof. By CategoryTheory__Limits__PreservesFiniteColimits.

CategoryTheory.ObjectProperty.preservesFiniteLimitsdefMathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits, function or constant

Wording

no wording

English

There is an object property of the set of functors of $J$ and $C$. Proof. By CategoryTheory__Limits__PreservesFiniteLimits.

CategoryTheory.ObjectProperty.preservesLimitdefMathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits, function or constant

Wording

no wording

English

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

CategoryTheory.ObjectProperty.preservesLimitsOfShapedefMathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits, function or constant

Wording

no wording

English

Let $K$ be a set. Then there is an object property of the set of functors of $J$ and $C$. Proof. Let $K$ be arbitrary. By CategoryTheory__Limits__PreservesLimitsOfShape.

Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT

CategoryTheory.ObjectProperty.HasCardinalLTdefMathlib.CategoryTheory.ObjectProperty.HasCardinalLT, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Let $x_{1}$ be a cardinal. Then $\operatorname{HasCardinalLT}$ holds for $P$ and $x_{1}$, if $\mathrm{HasCardinalLT}$ holds for $\SubtypeSet {x_{2}}{P (x_{2})}$ and $x_{1}$.

Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic

CategoryTheory.ObjectProperty.hasFiniteResolutiondefMathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Then there is an object property of $C$. Proof. Let $P$ be arbitrary. Let $n$ be arbitrary. By P. By n. By CategoryTheory__ObjectProperty__hasFiniteResolutionOfLength. By iSup.

CategoryTheory.ObjectProperty.hasFiniteResolutionOfLengthinductiveMathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Let $x_{2}$ be a natural number. Then there is an object property of $C$.

CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.belowinductiveMathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic, predicate

Wording

no wording

English

Assume that $\operatorname{hasFiniteResolutionOfLength}$ holds for $P$, $x_{2}$ and $x_{3}$. Then we can say that $\operatorname{below}$ holds for $t$.

Mathlib.CategoryTheory.ObjectProperty.Ind

CategoryTheory.ObjectProperty.inddefMathlib.CategoryTheory.ObjectProperty.Ind, function or constant

Wording

the ind of P (from the name)

English

Let $P$ be an object property of $C$. Then the ind of $P$ is an object property of $C$ defined as the function that maps $X$ to the proposition that there exists a set $J$, such that there exists a small category $x_{1}$ of $J$, such that there exists an element $h$ of $\operatorname{IsFiltered}$ applied to $J$, such that there exists a colimit presentation $\mathrm{pres}$ of $J$ and $X$, such that for all elements $i$ of $J$, $P$ holds for the action of the diagram of $\mathrm{pres}$ and $i$.

Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom

CategoryTheory.ObjectProperty.InheritedFromSourceclassMathlib.CategoryTheory.ObjectProperty.InheritedFromHom, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Let $Q$ be a morphism property of $C$. Then we can say that $\operatorname{InheritedFromSource}$ holds for $P$ and $Q$.

CategoryTheory.ObjectProperty.InheritedFromTargetclassMathlib.CategoryTheory.ObjectProperty.InheritedFromHom, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Let $Q$ be a morphism property of $C$. Then we can say that $\operatorname{InheritedFromTarget}$ holds for $P$ and $Q$.

Mathlib.CategoryTheory.ObjectProperty.IsClosedUnderCardinalFilteredColimits

CategoryTheory.ObjectProperty.IsClosedUnderCardinalFilteredColimitsclassMathlib.CategoryTheory.ObjectProperty.IsClosedUnderCardinalFilteredColimits, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Let $x_{1}$ be a cardinal. Then we can say that $\operatorname{IsClosedUnderCardinalFilteredColimits}$ holds for $P$ and $x_{1}$.

Mathlib.CategoryTheory.ObjectProperty.Kernels

CategoryTheory.MorphismProperty.cokernelsinductiveMathlib.CategoryTheory.ObjectProperty.Kernels, function or constant

Wording

the cokernel of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the cokernel of $W$ is an object property of $C$.

CategoryTheory.MorphismProperty.kernelsinductiveMathlib.CategoryTheory.ObjectProperty.Kernels, function or constant

Wording

the kernel of W (from the name)

English

Let $W$ be a morphism property of $C$. Then the kernel of $W$ is an object property of $C$.

CategoryTheory.ObjectProperty.IsClosedUnderCokernelsclassMathlib.CategoryTheory.ObjectProperty.Kernels, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderCokernels}$ holds for $P$.

CategoryTheory.ObjectProperty.IsClosedUnderKernelsclassMathlib.CategoryTheory.ObjectProperty.Kernels, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsClosedUnderKernels}$ holds for $P$.

Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

CategoryTheory.ObjectProperty.limitClosuredefMathlib.CategoryTheory.ObjectProperty.LimitsClosure, function or constant

Wording

the closure of P and J (from the docstring)

English

Let $P$ be an object property of $C$. Let $J$ be a set. Then the closure of $P$ and $J$ is an object property of $C$ defined as the closure of $P$ and the function that maps $x_{2}$ to $J$.

CategoryTheory.ObjectProperty.limitsClosureinductiveMathlib.CategoryTheory.ObjectProperty.LimitsClosure, function or constant

Wording

the closure of P and J (from the docstring)

English

Let $P$ be an object property of $C$. Let $J$ be a function from elements of $x_{1}$ to sets. Then the closure of $P$ and $J$ is an object property of $C$.

CategoryTheory.ObjectProperty.limitsClosure.belowinductiveMathlib.CategoryTheory.ObjectProperty.LimitsClosure, predicate

Wording

no wording

English

Assume that $\operatorname{limitsClosure}$ holds for $P$ and $J$. Then we can say that $\operatorname{below}$ holds for $t$.

CategoryTheory.ObjectProperty.strictLimitsClosureIterdefMathlib.CategoryTheory.ObjectProperty.LimitsClosure, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Let $J$ be a function from elements of $x_{1}$ to sets. Let $b$ be an element of $x_{3}$. Then there is an object property of $C$. Proof. Let $P$ be arbitrary. Let $J$ be arbitrary. Let $b$ be arbitrary. Let $Q$ be arbitrary. By Q. By J. By CategoryTheory__ObjectProperty__strictLimitsClosureStep. By b. By P. By transfiniteIterate.

CategoryTheory.ObjectProperty.strictLimitsClosureStepdefMathlib.CategoryTheory.ObjectProperty.LimitsClosure, function or constant

Wording

the strict limit closure step of P and J (from the name)

English

Let $P$ be an object property of $C$. Let $J$ be a function from elements of $x_{1}$ to sets. Then the strict limit closure step of $P$ and $J$ is an object property of $C$ defined as the maximum of $P$ and the supremum of the function that maps $a$ to the strict limit of $P$ and $J$ applied to $a$.

Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShapeclassMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Let $J$ be a set. Then we can say that $\operatorname{IsClosedUnderLimitsOfShape}$ holds for $P$ and $J$.

CategoryTheory.ObjectProperty.LimitOfShapestructureMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, type

Wording

limit of shape of J and X (from the name)

English

Let $P$ be an object property of $C$. Let $J$ be a set. Let $X$ be an element of $C$. Then the limits of shape of $J$ and $X$ are a basic type.

CategoryTheory.ObjectProperty.LimitOfShape.limitdefMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, function or constant

Wording

the limit of F and hF (from the name)

English

Let $F$ be a functor of $J$ and $C$ such that for all elements $j$ of $J$, $P$ holds for the action of $F$ and $j$. Then the limit of $F$ and $\mathrm{hF}$ is a limit of shape of $J$ and the limit of $F$ defined as $\operatorname{mk}$ applied to the limit of $F$ and $\mathrm{hF}$.

CategoryTheory.ObjectProperty.LimitOfShape.ofIsodefMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, function or constant

Wording

the limit of shape of h and e (from the name)

English

Let $h$ be a limit of shape of $J$ and $X$. Let $e$ be an isomorphism of $X$ and $Y$. Then the limit of shape of $h$ and $e$ is a limit of shape of $J$ and $Y$ defined as $\operatorname{mk}$ applied to the limit presentation of $\operatorname{toLimitPresentation}$ applied to $h$ and $e$ and $\mathrm{CategoryTheory\_\_ObjectProperty\_\_LimitOfShape\_\_prop\_diag\_obj}$ applied to $h$.

CategoryTheory.ObjectProperty.LimitOfShape.ofLEdefMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, function or constant

Wording

the limit of shape of h and hPQ (from the name)

English

Let $h$ be a limit of shape of $J$ and $X$. Assume that $P \leq Q$. Then the limit of shape of $h$ and $\mathrm{hPQ}$ is a limit of shape of $J$ and $X$.

CategoryTheory.ObjectProperty.LimitOfShape.reindexdefMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, function or constant

Wording

the reindexing of h and G (from the name)

English

Let $h$ be a limit of shape of $J$ and $X$. Let $G$ be a functor of $\mathrm{J'}$ and $J$. Then the reindexing of $h$ and $G$ is a limit of shape of $\mathrm{J'}$ and $X$.

CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrowdefMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, function or constant

Wording

the structured arrow of p (from the name)

English

Let $p$ be a limit of shape of $J$ and $X$. Then the structured arrow of $p$ is a functor of $J$ and the set of structured arrows of $X$ and the inclusion of $P$.

CategoryTheory.ObjectProperty.limitsOfShapedefMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, function or constant

Wording

the limit of P and J (from the name)

English

Let $P$ be an object property of $C$. Let $J$ be a set. Then the limit of $P$ and $J$ is an object property of $C$ defined as the function that maps $X$ to $\mathrm{Nonempty}$ applied to the set of limits of shape of $J$ and $X$.

CategoryTheory.ObjectProperty.strictLimitsOfShapeinductiveMathlib.CategoryTheory.ObjectProperty.LimitsOfShape, function or constant

Wording

the strict limit of P and J (from the name)

English

Let $P$ be an object property of $C$. Let $J$ be a set. Then the strict limit of $P$ and $J$ is an object property of $C$.

Mathlib.CategoryTheory.ObjectProperty.Local

CategoryTheory.MorphismProperty.isColocaldefMathlib.CategoryTheory.ObjectProperty.Local, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then there is an object property of $C$. Proof. Let $W$ be arbitrary. Let $X$ be arbitrary. By C. Let $Y$ be arbitrary. By C. Let $Z$ be arbitrary. By Y. By Z. By Quiver__Hom. Let $g$ be arbitrary. By Y. By Z. By g. By W. Let $f$ be arbitrary. By f. By g. By CategoryTheory__CategoryStruct__comp. By Function__Bijective. By if. By forall. By forall. By forall.

CategoryTheory.MorphismProperty.isLocaldefMathlib.CategoryTheory.ObjectProperty.Local, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Then there is an object property of $C$. Proof. Let $W$ be arbitrary. Let $Z$ be arbitrary. By C. Let $X$ be arbitrary. By C. Let $Y$ be arbitrary. By X. By Y. By Quiver__Hom. Let $f$ be arbitrary. By X. By Y. By f. By W. Let $g$ be arbitrary. By f. By g. By CategoryTheory__CategoryStruct__comp. By Function__Bijective. By if. By forall. By forall. By forall.

Mathlib.CategoryTheory.ObjectProperty.Opposite

CategoryTheory.ObjectProperty.opdefMathlib.CategoryTheory.ObjectProperty.Opposite, function or constant

Wording

the opposite of P (from the name)

English

Let $P$ be an object property of $C$. Then the opposite of $P$ is an object property of the set of opposites of $C$ defined as the function that maps $X$ to $P$ applied to the opposite of $X$.

CategoryTheory.ObjectProperty.opEquivalencedefMathlib.CategoryTheory.ObjectProperty.Opposite, function or constant

Wording

the opposite equivalence of P (from the name)

English

Let $P$ be an object property of $C$. Then the opposite equivalence of $P$ is an equivalence of the set of full subcategories of the opposite of $P$ and the set of opposites of the set of full subcategories of $P$.

CategoryTheory.ObjectProperty.subtypeOpEquivdefMathlib.CategoryTheory.ObjectProperty.Opposite, function or constant

Wording

the subtype opposite equivalence of P (from the name)

English

Let $P$ be an object property of $C$. Then the subtype opposite equivalence of $P$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{\operatorname{op} (P)})}{(\SubtypeSet {x_{2}}{P (x_{2})})}$.

CategoryTheory.ObjectProperty.unopdefMathlib.CategoryTheory.ObjectProperty.Opposite, function or constant

Wording

the opposite of P (from the name)

English

Let $P$ be an object property of the set of opposites of $C$. Then the opposite of $P$ is an object property of $C$ defined as the function that maps $X$ to $P$ applied to $\operatorname{op}$ applied to $X$.

Mathlib.CategoryTheory.ObjectProperty.Orthogonal

CategoryTheory.ObjectProperty.leftOrthogonaldefMathlib.CategoryTheory.ObjectProperty.Orthogonal, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Then there is an object property of $C$. Proof. Let $P$ be arbitrary. Let $X$ be arbitrary. By C. Let $Y$ be arbitrary. By X. By Y. By Quiver__Hom. Let $f$ be arbitrary. By Y. By P. By f. By 0. By Eqt. By if. By forall. By forall.

CategoryTheory.ObjectProperty.rightOrthogonaldefMathlib.CategoryTheory.ObjectProperty.Orthogonal, function or constant

Wording

no wording

English

Let $P$ be an object property of $C$. Then there is an object property of $C$. Proof. Let $P$ be arbitrary. Let $Y$ be arbitrary. By C. Let $X$ be arbitrary. By X. By Y. By Quiver__Hom. Let $f$ be arbitrary. By X. By P. By f. By 0. By Eqt. By if. By forall. By forall.

Mathlib.CategoryTheory.ObjectProperty.Retract

CategoryTheory.ObjectProperty.IsStableUnderRetractsclassMathlib.CategoryTheory.ObjectProperty.Retract, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsStableUnderRetracts}$ holds for $P$.

CategoryTheory.ObjectProperty.retractClosuredefMathlib.CategoryTheory.ObjectProperty.Retract, function or constant

Wording

the retract closure of P (from the name)

English

Let $P$ be an object property of $C$. Then the retract closure of $P$ is an object property of $C$ defined as the function that maps $X$ to the proposition that there exists an element $Y$ of $C$, such that there exists an element $h$ of $P$ applied to $Y$, such that $\mathrm{Nonempty}$ holds for the set of retracts of $X$ and $Y$.

Mathlib.CategoryTheory.ObjectProperty.Shift

CategoryTheory.ObjectProperty.IsStableUnderShiftclassMathlib.CategoryTheory.ObjectProperty.Shift, predicate

Wording

P is a stable under shift (from the name)

English

Let $P$ be an object property of $C$. Let $A$ be a set. Then we can say that $P$ is a stable under shift.

CategoryTheory.ObjectProperty.IsStableUnderShiftByclassMathlib.CategoryTheory.ObjectProperty.Shift, predicate

Wording

no wording

English

Let $P$ be an object property of $C$. Let $a$ be an element of $A$. Then we can say that $\operatorname{IsStableUnderShiftBy}$ holds for $P$ and $a$.

CategoryTheory.ObjectProperty.shiftdefMathlib.CategoryTheory.ObjectProperty.Shift, function or constant

Wording

the shift of P and a (from the name)

English

Let $P$ be an object property of $C$. Let $a$ be an element of $A$. Then the shift of $P$ and $a$ is an object property of $C$ defined as the function that maps $X$ to $P$ applied to the action of the shift functor of $C$ and $a$ and $X$.

CategoryTheory.ObjectProperty.shiftClosuredefMathlib.CategoryTheory.ObjectProperty.Shift, function or constant

Wording

the shift closure of P and A (from the name)

English

Let $P$ be an object property of $C$. Let $A$ be a set. Then the shift closure of $P$ and $A$ is an object property of $C$ defined as the function that maps $X$ to the proposition that there exists an element $Y$ of $C$, such that there exists an element $a$ of $A$, such that there exists an isomorphism $x_{3}$ of $X$ and the action of the shift functor of $C$ and $a$ and $Y$, such that $P$ holds for $Y$.

Mathlib.CategoryTheory.ObjectProperty.SiteLocal

CategoryTheory.ObjectProperty.IsLocalclassMathlib.CategoryTheory.ObjectProperty.SiteLocal, predicate

Wording

P is local (from the docstring)

English

Let $P$ be an object property of $C$. Let $K$ be a precoverage of $C$. Then we can say that $P$ is local.

Mathlib.CategoryTheory.ObjectProperty.Small

CategoryTheory.ObjectProperty.EssentiallySmallclassMathlib.CategoryTheory.ObjectProperty.Small, predicate

Wording

P is essentially small (from the name)

English

generation took over the time limit

CategoryTheory.ObjectProperty.SmalldefMathlib.CategoryTheory.ObjectProperty.Small, predicate

Wording

P is small (from the name)

English

Let $P$ be an object property of $C$. Then $P$ is small, if $\SubtypeSet {x_{1}}{P (x_{1})}$ is small.

Mathlib.CategoryTheory.Opposites

CategoryTheory.Equivalence.leftOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the left opposite of e (from the name)

English

Let $e$ be an equivalence of $C$ and the set of opposites of $D$. Then the left opposite of $e$ is an equivalence of the set of opposites of $C$ and $D$ defined as the composition of the opposite of $e$ and the double opposite category of $D$.

CategoryTheory.Equivalence.opdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of e (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Then the opposite of $e$ is an equivalence of the set of opposites of $C$ and the set of opposites of $D$.

CategoryTheory.Equivalence.rightOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the right opposite of e (from the name)

English

Let $e$ be an equivalence of the set of opposites of $C$ and $D$. Then the right opposite of $e$ is an equivalence of $C$ and the set of opposites of $D$ defined as the composition of the inverse of the double opposite category of $C$ and the opposite of $e$.

CategoryTheory.Equivalence.unopdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of e (from the name)

English

Let $e$ be an equivalence of the set of opposites of $C$ and the set of opposites of $D$. Then the opposite of $e$ is an equivalence of $C$ and $D$.

CategoryTheory.Functor.FullyFaithful.leftOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of hF (from the docstring)

English

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the opposite of $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to the left opposite of $F$.

CategoryTheory.Functor.FullyFaithful.opdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of hF (from the docstring)

English

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the opposite of $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to the opposite of $F$.

CategoryTheory.Functor.FullyFaithful.rightOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of hF (from the docstring)

English

CategoryTheory.Functor.FullyFaithful.unopdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of hF (from the name)

English

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the opposite of $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to the opposite of $F$.

CategoryTheory.Functor.leftOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the left opposite of F (from the name)

English

Let $F$ be a functor of $C$ and the set of opposites of $D$. Then the left opposite of $F$ is a functor of the set of opposites of $C$ and $D$.

CategoryTheory.Functor.leftOpCompdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the left opposite composition of F and G (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and the set of opposites of $E$. Then the left opposite composition of $F$ and $G$ is an isomorphism of the left opposite of the composition of $F$ and $G$ and the composition of the opposite of $F$ and the left opposite of $G$ defined as the identity of the left opposite of the composition of $F$ and $G$.

CategoryTheory.Functor.leftOpCompOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the left opposite composition opposite of F and G (from the name)

English

Let $F$ be a functor of $C$ and the set of opposites of $D$. Let $G$ be a functor of $D$ and $E$. Then the left opposite composition opposite of $F$ and $G$ is an isomorphism of the left opposite of the composition of $F$ and the opposite of $G$ and the composition of the left opposite of $F$ and $G$ defined as the identity of the left opposite of the composition of $F$ and the opposite of $G$.

CategoryTheory.Functor.leftOpIddefMathlib.CategoryTheory.Opposites, function or constant

Wording

the left opposite identity of C (from the name)

English

Let $C$ be a set. Then the left opposite identity of $C$ is an isomorphism of the left opposite of the identity of the set of opposites of $C$ and the opposite opposite of $C$ defined as the identity of the left opposite of the identity of the set of opposites of $C$.

CategoryTheory.Functor.leftOpRightOpEquivdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the left opposite right opposite equivalence of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the left opposite right opposite equivalence of $C$ and $D$ is an equivalence of the set of opposites of the set of functors of the set of opposites of $C$ and $D$ and the set of functors of $C$ and the set of opposites of $D$.

CategoryTheory.Functor.leftOpRightOpIsodefMathlib.CategoryTheory.Opposites, function or constant

Wording

the left opposite right opposite isomorphism of F (from the name)

English

Let $F$ be a functor of $C$ and the set of opposites of $D$. Then the left opposite right opposite isomorphism of $F$ is an isomorphism of the right opposite of the left opposite of $F$ and $F$.

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

Wording

the opposite of F (from the docstring)

English

Let $F$ be a functor of $C$ and $D$. Then the opposite of $F$ is a functor of the set of opposites of $C$ and the set of opposites of $D$.

CategoryTheory.Functor.opCompdefMathlib.CategoryTheory.Opposites, function or constant

Wording

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

English

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the opposite composition of $F$ and $G$ is an isomorphism of the opposite of the composition of $F$ and $G$ and the composition of the opposite of $F$ and the opposite of $G$ defined as the identity of the opposite of the composition of $F$ and $G$.

CategoryTheory.Functor.opHomdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite homomorphism of C and D (from the name)

English

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

CategoryTheory.Functor.opIddefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite identity of C (from the name)

English

Let $C$ be a set. Then the opposite identity of $C$ is an isomorphism of the opposite of the identity of $C$ and the identity of the set of opposites of $C$ defined as the identity of the opposite of the identity of $C$.

CategoryTheory.Functor.opInvdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite inverse of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the opposite inverse of $C$ and $D$ is a functor of the set of functors of the set of opposites of $C$ and the set of opposites of $D$ and the set of opposites of the set of functors of $C$ and $D$.

CategoryTheory.Functor.opUnopEquivdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite opposite equivalence of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the opposite opposite equivalence of $C$ and $D$ is an equivalence of the set of opposites of the set of functors of $C$ and $D$ and the set of functors of the set of opposites of $C$ and the set of opposites of $D$.

CategoryTheory.Functor.opUnopIsodefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite opposite isomorphism of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the opposite opposite isomorphism of $F$ is an isomorphism of the opposite of the opposite of $F$ and $F$.

CategoryTheory.Functor.rightOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the right opposite of F (from the name)

English

Let $F$ be a functor of the set of opposites of $C$ and $D$. Then the right opposite of $F$ is a functor of $C$ and the set of opposites of $D$.

CategoryTheory.Functor.rightOpCompdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the right opposite composition of F and G (from the name)

English

Let $F$ be a functor of the set of opposites of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the right opposite composition of $F$ and $G$ is an isomorphism of the right opposite of the composition of $F$ and $G$ and the composition of the right opposite of $F$ and the opposite of $G$ defined as the identity of the right opposite of the composition of $F$ and $G$.

CategoryTheory.Functor.rightOpCompOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the right opposite composition opposite of F and G (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of the set of opposites of $D$ and $E$. Then the right opposite composition opposite of $F$ and $G$ is an isomorphism of the right opposite of the composition of the opposite of $F$ and $G$ and the composition of $F$ and the right opposite of $G$ defined as the identity of the right opposite of the composition of the opposite of $F$ and $G$.

CategoryTheory.Functor.rightOpIddefMathlib.CategoryTheory.Opposites, function or constant

Wording

the right opposite identity of C (from the name)

English

Let $C$ be a set. Then the right opposite identity of $C$ is an isomorphism of the right opposite of the identity of the set of opposites of $C$ and the functor of $C$ defined as the identity of the right opposite of the identity of the set of opposites of $C$.

CategoryTheory.Functor.rightOpLeftOpIsodefMathlib.CategoryTheory.Opposites, function or constant

Wording

the right opposite left opposite isomorphism of F (from the name)

English

Let $F$ be a functor of the set of opposites of $C$ and $D$. Then the right opposite left opposite isomorphism of $F$ is an isomorphism of the left opposite of the right opposite of $F$ and $F$.

CategoryTheory.Functor.unopdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of F (from the name)

English

Let $F$ be a functor of the set of opposites of $C$ and the set of opposites of $D$. Then the opposite of $F$ is a functor of $C$ and $D$.

CategoryTheory.Functor.unopCompdefMathlib.CategoryTheory.Opposites, function or constant

Wording

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

English

Let $F$ be a functor of the set of opposites of $C$ and the set of opposites of $D$. Let $G$ be a functor of the set of opposites of $D$ and the set of opposites of $E$. Then the opposite composition of $F$ and $G$ is an isomorphism of the opposite of the composition of $F$ and $G$ and the composition of the opposite of $F$ and the opposite of $G$ defined as the identity of the opposite of the composition of $F$ and $G$.

CategoryTheory.Functor.unopIddefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite identity of C (from the name)

English

Let $C$ be a set. Then the opposite identity of $C$ is an isomorphism of the opposite of the identity of the set of opposites of $C$ and the identity of $C$ defined as the identity of the opposite of the identity of the set of opposites of $C$.

CategoryTheory.Functor.unopOpIsodefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite opposite isomorphism of F (from the name)

English

Let $F$ be a functor of the set of opposites of $C$ and the set of opposites of $D$. Then the opposite opposite isomorphism of $F$ is an isomorphism of the opposite of the opposite of $F$ and $F$.

CategoryTheory.Iso.opdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite isomorphism of x1 (from the docstring)

English

Let $x_{1}$ be an isomorphism of $X$ and $Y$. Then the opposite isomorphism of $x_{1}$ is an isomorphism of $\operatorname{op}$ applied to $Y$ and $\operatorname{op}$ applied to $X$.

CategoryTheory.Iso.unopdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of f (from the name)

English

Let $f$ be an isomorphism of $X$ and $Y$. Then the opposite of $f$ is an isomorphism of the opposite of $Y$ and the opposite of $X$.

CategoryTheory.NatIso.opdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of x2 (from the name)

English

Let $x_{2}$ be an isomorphism of $F$ and $G$. Then the opposite of $x_{2}$ is an isomorphism of the opposite of $G$ and the opposite of $F$.

CategoryTheory.NatIso.removeOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

no wording

English

Let $x_{2}$ be an isomorphism of the opposite of $F$ and the opposite of $G$. Then $\operatorname{removeOp}$ applied to $x_{2}$ is an isomorphism of $G$ and $F$.

CategoryTheory.NatIso.unopdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of x2 (from the name)

English

Let $x_{2}$ be an isomorphism of $F$ and $G$. Then the opposite of $x_{2}$ is an isomorphism of the opposite of $G$ and the opposite of $F$.

CategoryTheory.NatTrans.leftOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the left opposite of x2 (from the name)

English

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

CategoryTheory.NatTrans.opdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of x2 (from the docstring)

English

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

CategoryTheory.NatTrans.removeLeftOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of the left opposite of $F$ and the left opposite of $G$. Then $\operatorname{removeLeftOp}$ applied to $x_{2}$ is a homomorphism of $G$ and $F$.

CategoryTheory.NatTrans.removeOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of the opposite of $F$ and the opposite of $G$. Then $\operatorname{removeOp}$ applied to $x_{2}$ is a homomorphism of $G$ and $F$.

CategoryTheory.NatTrans.removeRightOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of the right opposite of $F$ and the right opposite of $G$. Then $\operatorname{removeRightOp}$ applied to $x_{2}$ is a homomorphism of $G$ and $F$.

CategoryTheory.NatTrans.removeUnopdefMathlib.CategoryTheory.Opposites, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of the opposite of $F$ and the opposite of $G$. Then $\operatorname{removeUnop}$ applied to $x_{2}$ is a homomorphism of $G$ and $F$.

CategoryTheory.NatTrans.rightOpdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the right opposite of x2 (from the name)

English

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

CategoryTheory.NatTrans.unopdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the opposite of x2 (from the name)

English

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

CategoryTheory.isoOpEquivdefMathlib.CategoryTheory.Opposites, function or constant

Wording

the isomorphism opposite equivalence of A and B (from the name)

English

Let $A$ and $B$ be opposites of $C$. Then the isomorphism opposite equivalence of $A$ and $B$ is an equivalence from the set of isomorphisms of $A$ and $B$ to the set of isomorphisms of the opposite of $B$ and the opposite of $A$.