Definitions: Mathlib.CategoryTheory, part 6 of 25

CategoryTheory.EnrichedOrdinaryCategory.homEquivdefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the homomorphism equivalence (from the name)

English

The homomorphism equivalence is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of the tensor unity in the monoidal structure of $V$ and the homomorphism of $X$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.ForgetEnrichment.equivdefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the equivalence of V (from the name)

English

Let $V$ be a set. Then the equivalence of $V$ is an equivalence of $\operatorname{ForgetEnrichment}$ applied to $V$ and $D$ and $D$.

CategoryTheory.ForgetEnrichment.equivFunctordefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the equivalence functor of V and D (from the name)

English

Let $V$ and $D$ be sets. Then the equivalence functor of $V$ and $D$ is a functor of $\operatorname{ForgetEnrichment}$ applied to $V$ and $D$ and $D$.

CategoryTheory.ForgetEnrichment.equivInversedefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the equivalence inverse of V and D (from the name)

English

Let $V$ and $D$ be sets. Then the equivalence inverse of $V$ and $D$ is a functor of $D$ and $\operatorname{ForgetEnrichment}$ applied to $V$ and $D$.

CategoryTheory.TransportEnrichment.forgetEnrichmentEquivdefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

no wording

English

Let $F$ be a functor of $V$ and $W$. Let $D$ be a set. Let $e$ be a function from elements $v_{1}$ of $V$ to equivalences from the set of homomorphisms of the tensor unity in the monoidal structure of $V$ and $v_{1}$ to the set of homomorphisms of the tensor unity in the monoidal structure of $W$ and the action of $F$ and $v_{1}$ such that for all elements $v$ of $V$, for all homomorphisms $f$ of the tensor unity in the monoidal structure of $V$ and $v$, $e$ applied to $v$ and $f$ is equal to the composition of $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3b5\_}$ applied to $F$ and the map of $F$ and $f$. Then $\operatorname{forgetEnrichmentEquiv}$ applied to $F$, $D$, $v_{1}$, $e$ and $h$ is an equivalence of $\operatorname{TransportEnrichment}$ applied to $F$ and $\operatorname{ForgetEnrichment}$ applied to $V$ and $D$ and $\operatorname{ForgetEnrichment}$ applied to $W$ and $\operatorname{TransportEnrichment}$ applied to $F$ and $D$.

CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctordefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

no wording

English

Let $F$ be a functor of $V$ and $W$. Let $D$ be a set. Let $e$ be a function from elements $v_{1}$ of $V$ to equivalences from the set of homomorphisms of the tensor unity in the monoidal structure of $V$ and $v_{1}$ to the set of homomorphisms of the tensor unity in the monoidal structure of $W$ and the action of $F$ and $v_{1}$ such that for all elements $v$ of $V$, for all homomorphisms $f$ of the tensor unity in the monoidal structure of $V$ and $v$, $e$ applied to $v$ and $f$ is equal to the composition of $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3b5\_}$ applied to $F$ and the map of $F$ and $f$. Then $\operatorname{forgetEnrichmentEquivFunctor}$ applied to $F$, $D$, $v_{1}$, $e$ and $h$ is a functor of $\operatorname{TransportEnrichment}$ applied to $F$ and $\operatorname{ForgetEnrichment}$ applied to $V$ and $D$ and $\operatorname{ForgetEnrichment}$ applied to $W$ and $\operatorname{TransportEnrichment}$ applied to $F$ and $D$.

CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInversedefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

no wording

English

Let $F$ be a functor of $V$ and $W$. Let $D$ be a set. Let $e$ be a function from elements $v_{1}$ of $V$ to equivalences from the set of homomorphisms of the tensor unity in the monoidal structure of $V$ and $v_{1}$ to the set of homomorphisms of the tensor unity in the monoidal structure of $W$ and the action of $F$ and $v_{1}$ such that for all elements $v$ of $V$, for all homomorphisms $f$ of the tensor unity in the monoidal structure of $V$ and $v$, $e$ applied to $v$ and $f$ is equal to the composition of $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3b5\_}$ applied to $F$ and the map of $F$ and $f$. Then $\operatorname{forgetEnrichmentEquivInverse}$ applied to $F$, $D$, $v_{1}$, $e$ and $h$ is a functor of $\operatorname{ForgetEnrichment}$ applied to $W$ and $\operatorname{TransportEnrichment}$ applied to $F$ and $D$ and $\operatorname{TransportEnrichment}$ applied to $F$ and $\operatorname{ForgetEnrichment}$ applied to $V$ and $D$.

CategoryTheory.TransportEnrichment.ofOrdinaryEnrichedCategoryEquivdefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

no wording

English

Let $C$ be a set. Let $F$ be a functor of $V$ and $W$. Then $\operatorname{ofOrdinaryEnrichedCategoryEquiv}$ applied to $C$ and $F$ is an equivalence of $\operatorname{TransportEnrichment}$ applied to $F$ and $C$ and $C$ defined as the identity.

CategoryTheory.eCoyonedadefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the Coyoneda of V and X (from the name)

English

Let $V$ be a set. Let $X$ be an element of $C$. Then the Coyoneda of $V$ and $X$ is a functor of $C$ and $V$ defined as the action of the homomorphism functor of $V$ and $C$ and $\operatorname{op}$ applied to $X$.

CategoryTheory.eHomEquivdefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the homomorphism equivalence of V (from the name)

English

Let $V$ be a set. Then the homomorphism equivalence of $V$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of the tensor unity in the monoidal structure of $V$ and the homomorphism of $X$ and $Y$ defined as the homomorphism equivalence.

CategoryTheory.eHomFunctordefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the homomorphism functor of V and C (from the name)

English

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

CategoryTheory.eHomWhiskerLeftdefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the left homomorphism whisker of X and g (from the name)

English

Let $V$ be a set. Let $X$ be an element of $C$. Let $g$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Then the left homomorphism whisker of $X$ and $g$ is a homomorphism of the homomorphism of $X$ and $Y$ and the homomorphism of $X$ and $\mathrm{Y'}$ defined as the composition of the inverse of the right unitor of the homomorphism of $X$ and $Y$ and the composition of the left whisker of the homomorphism of $X$ and $Y$ and $\operatorname{eHomEquiv}$ applied to $V$ and $g$ and the composition of $Y$ and $\mathrm{Y'}$.

CategoryTheory.eHomWhiskerRightdefMathlib.CategoryTheory.Enriched.Ordinary.Basic, function or constant

Wording

the right homomorphism whisker of f and Y (from the name)

English

Let $V$ be a set. Let $f$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $Y$ be an element of $C$. Then the right homomorphism whisker of $f$ and $Y$ is a homomorphism of the homomorphism of $\mathrm{X'}$ and $Y$ and the homomorphism of $X$ and $Y$ defined as the composition of the inverse of the left unitor of the homomorphism of $\mathrm{X'}$ and $Y$ and the composition of the right whisker of $\operatorname{eHomEquiv}$ applied to $V$ and $f$ and the homomorphism of $\mathrm{X'}$ and $Y$ and the composition of $\mathrm{X'}$ and $Y$.

Mathlib.CategoryTheory.EpiMono

CategoryTheory.IsSplitEpiclassMathlib.CategoryTheory.EpiMono, predicate

Wording

f is a split epimorphism (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is a split epimorphism.

CategoryTheory.IsSplitMonoclassMathlib.CategoryTheory.EpiMono, predicate

Wording

f is a split monomorphism (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is a split monomorphism.

CategoryTheory.MorphismProperty.splitEpimorphismsdefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the split epimorphism of C (from the name)

English

Let $C$ be a set. Then the split 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 a split epimorphism.

CategoryTheory.MorphismProperty.splitMonomorphismsdefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the split monomorphism of C (from the name)

English

Let $C$ be a set. Then the split 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 split monomorphism.

CategoryTheory.SplitEpistructureMathlib.CategoryTheory.EpiMono, type

Wording

split epimorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the split epimorphisms of $f$ are a basic type.

CategoryTheory.SplitEpi.compdefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the composition of sef and seg (from the name)

English

Let $\mathrm{sef}$ be a split epimorphism of $f$. Let $\mathrm{seg}$ be a split epimorphism of $g$. Then the composition of $\mathrm{sef}$ and $\mathrm{seg}$ is a split epimorphism of the composition of $f$ and $g$.

CategoryTheory.SplitEpi.mapdefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the map of se and F (from the name)

English

Let $\mathrm{se}$ be a split epimorphism of $f$. Let $F$ be a functor of $C$ and $D$. Then the map of $\mathrm{se}$ and $F$ is a split epimorphism of the map of $F$ and $f$.

CategoryTheory.SplitEpi.opdefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the opposite of h (from the docstring)

English

Let $h$ be a split epimorphism of $f$. Then the opposite of $h$ is a split monomorphism of the opposite in $f$.

CategoryTheory.SplitEpi.section_defMathlib.CategoryTheory.EpiMono, function or constant

Wording

the section of self (from the name)

English

Let $\mathrm{self}$ be a split epimorphism of $f$. Then the section of $\mathrm{self}$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.SplitEpi.splitMonodefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the section of se (from the docstring)

English

Let $\mathrm{se}$ be a split epimorphism of $f$. Then the section of $\mathrm{se}$ is a split monomorphism of the section of $\mathrm{se}$.

CategoryTheory.SplitEpiCategoryclassMathlib.CategoryTheory.EpiMono, predicate

Wording

C is a split epimorphism category (from the name)

English

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

CategoryTheory.SplitMonostructureMathlib.CategoryTheory.EpiMono, type

Wording

split monomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the split monomorphisms of $f$ are a basic type.

CategoryTheory.SplitMono.compdefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the composition of smf and smg (from the name)

English

Let $\mathrm{smf}$ be a split monomorphism of $f$. Let $\mathrm{smg}$ be a split monomorphism of $g$. Then the composition of $\mathrm{smf}$ and $\mathrm{smg}$ is a split monomorphism of the composition of $f$ and $g$.

CategoryTheory.SplitMono.mapdefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the map of se and F (from the name)

English

Let $\mathrm{se}$ be a split monomorphism of $f$. Let $F$ be a functor of $C$ and $D$. Then the map of $\mathrm{se}$ and $F$ is a split monomorphism of the map of $F$ and $f$.

CategoryTheory.SplitMono.opdefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the opposite of h (from the docstring)

English

Let $h$ be a split monomorphism of $f$. Then the opposite of $h$ is a split epimorphism of the opposite in $f$.

CategoryTheory.SplitMono.retractiondefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the retraction of self (from the name)

English

Let $\mathrm{self}$ be a split monomorphism of $f$. Then the retraction of $\mathrm{self}$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.SplitMono.splitEpidefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the retraction of se (from the docstring)

English

Let $\mathrm{se}$ be a split monomorphism of $f$. Then the retraction of $\mathrm{se}$ is a split epimorphism of the retraction of $\mathrm{se}$.

CategoryTheory.SplitMonoCategoryclassMathlib.CategoryTheory.EpiMono, predicate

Wording

C is a split monomorphism category (from the name)

English

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

CategoryTheory.retractiondefMathlib.CategoryTheory.EpiMono, function or constant

Wording

the chosen retraction of f (from the docstring)

English

Let $f$ be a homomorphism of $Y$ and $X$. Then the chosen retraction of $f$ is a homomorphism of $X$ and $Y$ defined as the retraction of $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_IsSplitMono\_\_exists\_splitMono}$.

CategoryTheory.section_defMathlib.CategoryTheory.EpiMono, function or constant

Wording

the chosen section of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the chosen section of $f$ is a homomorphism of $Y$ and $X$ defined as the section of $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_IsSplitEpi\_\_exists\_splitEpi}$.

Mathlib.CategoryTheory.EqToHom

CategoryTheory.Equivalence.induceddefMathlib.CategoryTheory.EqToHom, function or constant

Wording

no wording

English

Let $e$ be an equivalence from $T$ to $D$. Then $\operatorname{induced}$ applied to $e$ is an equivalence of the set of induced categories of $D$ and $\operatorname{coe}$ applied to $e$ and $D$.

CategoryTheory.eqToHomdefMathlib.CategoryTheory.EqToHom, function or constant

Wording

no wording

English

Assume that $\EqtMACRoH {X}{Y}$. Then $\operatorname{eqToHom}$ applied to $p$ is a homomorphism of $X$ and $Y$.

CategoryTheory.eqToIsodefMathlib.CategoryTheory.EqToHom, function or constant

Wording

no wording

English

Assume that $\EqtMACRoH {X}{Y}$. Then $\operatorname{eqToIso}$ applied to $p$ is an isomorphism of $X$ and $Y$.

Mathlib.CategoryTheory.Equivalence

CategoryTheory.EquivalencestructureMathlib.CategoryTheory.Equivalence, type

Wording

equivalence of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the equivalences of $C$ and $D$ are a basic type.

CategoryTheory.Equivalence.adjointifyηdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

no wording

English

Let $x_{2}$ be an isomorphism of the identity of $C$ and the composition of $F$ and $G$. Let $x_{3}$ be an isomorphism of the composition of $G$ and $F$ and the identity of $D$. Then $\mathrm{CategoryTheory\_\_Equivalence\_\_adjointify\_u3b7\_}$ applied to $x_{2}$ and $x_{3}$ is an isomorphism of the identity of $C$ and the composition of $F$ and $G$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $x_{2}$ and the left isomorphism whisker of $F$ and the inverse of the left unitor of $G$ and the left isomorphism whisker of $F$ and the right isomorphism whisker of the inverse of $x_{3}$ and $G$ and the left isomorphism whisker of $F$ and the associator of $F$ and $G$ and the inverse of the associator of $G$ and the composition of $F$ and $G$ and the right isomorphism whisker of the inverse of $x_{2}$ and the composition of $F$ and $G$ and the left unitor of the composition of $F$ and $G$.

CategoryTheory.Equivalence.asNatTransdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $e$ and $f$. Then $\operatorname{asNatTrans}$ applied to $x_{2}$ is a homomorphism of the functor of $e$ and the functor of $f$ defined as $x_{2}$.

CategoryTheory.Equivalence.changeFunctordefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the change functor of e and iso (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Let $\mathrm{iso}$ be an isomorphism of the functor of $e$ and $G$. Then the change functor of $e$ and $\mathrm{iso}$ is an equivalence of $C$ and $D$.

CategoryTheory.Equivalence.changeInversedefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the change inverse of e and iso (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Let $\mathrm{iso}$ be an isomorphism of the inverse of $e$ and $G$. Then the change inverse of $e$ and $\mathrm{iso}$ is an equivalence of $C$ and $D$.

CategoryTheory.Equivalence.congrLeftdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the left congruence of e (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Then the left congruence of $e$ is an equivalence of the set of functors of $C$ and $E$ and the set of functors of $D$ and $E$.

CategoryTheory.Equivalence.congrRightdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the right congruence of e (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Then the right congruence of $e$ is an equivalence of the set of functors of $E$ and $C$ and the set of functors of $E$ and $D$.

CategoryTheory.Equivalence.congrRightFunctordefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the congruence right functor of E (from the name)

English

Let $E$ be a set. Then the congruence right functor of $E$ is a functor of the set of equivalences of $C$ and $D$ and the set of equivalences of the set of functors of $E$ and $C$ and the set of functors of $E$ and $D$.

CategoryTheory.Equivalence.counitdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the counit of e (from the docstring)

English

Let $e$ be an equivalence of $C$ and $D$. Then the counit of $e$ is a homomorphism of the composition of the inverse of $e$ and the functor of $e$ and the identity of $D$ defined as the homomorphism of the counit isomorphism of $e$.

CategoryTheory.Equivalence.counitInvdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the inverse of the counit of e (from the docstring)

English

Let $e$ be an equivalence of $C$ and $D$. Then the inverse of the counit of $e$ is a homomorphism of the identity of $D$ and the composition of the inverse of $e$ and the functor of $e$ defined as the inverse of the counit isomorphism of $e$.

CategoryTheory.Equivalence.counitIsodefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the counit isomorphism of self (from the name)

English

Let $\mathrm{self}$ be an equivalence of $C$ and $D$. Then the counit isomorphism of $\mathrm{self}$ is an isomorphism of the composition of the inverse of $\mathrm{self}$ and the functor of $\mathrm{self}$ and the identity of $D$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

CategoryTheory.Equivalence.fullyFaithfulFunctordefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the functor of e (from the docstring)

English

Let $e$ be an equivalence of $C$ and $E$. Then the functor of $e$ is an element of $\operatorname{FullyFaithful}$ applied to the functor of $e$.

CategoryTheory.Equivalence.fullyFaithfulInversedefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the inverse of e (from the docstring)

English

Let $e$ be an equivalence of $C$ and $E$. Then the inverse of $e$ is an element of $\operatorname{FullyFaithful}$ applied to the inverse of $e$.

CategoryTheory.Equivalence.funInvIdAssocdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the function inverse identity associator of e and F (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Let $F$ be a functor of $C$ and $E$. Then the function inverse identity associator of $e$ and $F$ is an isomorphism of the composition of the functor of $e$ and the composition of the inverse of $e$ and $F$ and $F$ defined as the composition of the inverse of the associator of the inverse of $e$ and $F$ and the composition of the right isomorphism whisker of the inverse of the unit isomorphism of $e$ and $F$ and the left unitor of $F$.

CategoryTheory.Equivalence.functordefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the functor of self (from the name)

English

Let $\mathrm{self}$ be an equivalence of $C$ and $D$. Then the functor of $\mathrm{self}$ is a functor of $C$ and $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Equivalence.functorFunctordefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the functor functor of C and D (from the name)

English

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

CategoryTheory.Equivalence.invFunIdAssocdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the inverse function identity associator of e and F (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Let $F$ be a functor of $D$ and $E$. Then the inverse function identity associator of $e$ and $F$ is an isomorphism of the composition of the inverse of $e$ and the composition of the functor of $e$ and $F$ and $F$ defined as the composition of the inverse of the associator of the functor of $e$ and $F$ and the composition of the right isomorphism whisker of the counit isomorphism of $e$ and $F$ and the left unitor of $F$.

CategoryTheory.Equivalence.inversedefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the inverse of self (from the name)

English

Let $\mathrm{self}$ be an equivalence of $C$ and $D$. Then the inverse of $\mathrm{self}$ is a functor of $D$ and $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Equivalence.mkdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $C$. Let $x_{2}$ be an isomorphism of the identity of $C$ and the composition of $F$ and $G$. Let $x_{3}$ be an isomorphism of the composition of $G$ and $F$ and the identity of $D$. Then $\operatorname{mk}$ applied to $F$, $G$, $x_{2}$ and $x_{3}$ is an equivalence of $C$ and $D$ defined as $\operatorname{mk'}$ applied to $F$, $G$, $\mathrm{CategoryTheory\_\_Equivalence\_\_adjointify\_u3b7\_}$ applied to $x_{2}$ and $x_{3}$, $x_{3}$ and $\mathrm{CategoryTheory\_\_Equivalence\_\_adjointify\_\_u3b7\_\_\_u3b5\_}$ applied to $x_{2}$ and $x_{3}$.

CategoryTheory.Equivalence.mkHomdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the homomorphism of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of the functor of $e$ and the functor of $f$. Then the homomorphism of $x_{2}$ is a homomorphism of $e$ and $f$ defined as $x_{2}$.

CategoryTheory.Equivalence.mkIsodefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the isomorphism of x2 (from the name)

English

Let $x_{2}$ be an isomorphism of the functor of $e$ and the functor of $f$. Then the isomorphism of $x_{2}$ is an isomorphism of $e$ and $f$.

CategoryTheory.Equivalence.powdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the power of e and x1 (from the name)

English

Let $e$ be an equivalence of $C$ and $C$. Let $x_{1}$ be an integer. Then the power of $e$ and $x_{1}$ is an equivalence of $C$ and $C$.

CategoryTheory.Equivalence.powNatdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the power natural number of e and x1 (from the name)

English

Let $e$ be an equivalence of $C$ and $C$. Let $x_{1}$ be a natural number. Then the power natural number of $e$ and $x_{1}$ is an equivalence of $C$ and $C$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Equivalence\_\_powNat\_\_\_f}$ applied to $e$.

CategoryTheory.Equivalence.refldefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the identity (from the name)

English

The identity is an equivalence of $C$ and $C$.

CategoryTheory.Equivalence.symmdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Then the inverse of $e$ is an equivalence of $D$ and $C$ defined as $\operatorname{mk'}$ applied to the inverse of $e$, the functor of $e$, the inverse of the counit isomorphism of $e$, the inverse of the unit isomorphism of $e$ and $\mathrm{CategoryTheory\_\_Equivalence\_\_inverse\_counitInv\_comp}$ applied to $e$.

CategoryTheory.Equivalence.transdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the composition of e and f (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Let $f$ be an equivalence of $D$ and $E$. Then the composition of $e$ and $f$ is an equivalence of $C$ and $E$.

CategoryTheory.Equivalence.unitdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the unit of e (from the docstring)

English

Let $e$ be an equivalence of $C$ and $D$. Then the unit of $e$ is a homomorphism of the identity of $C$ and the composition of the functor of $e$ and the inverse of $e$ defined as the homomorphism of the unit isomorphism of $e$.

CategoryTheory.Equivalence.unitInvdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the inverse of the unit of e (from the docstring)

English

Let $e$ be an equivalence of $C$ and $D$. Then the inverse of the unit of $e$ is a homomorphism of the composition of the functor of $e$ and the inverse of $e$ and the identity of $C$ defined as the inverse of the unit isomorphism of $e$.

CategoryTheory.Equivalence.unitIsodefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the unit isomorphism of self (from the name)

English

Let $\mathrm{self}$ be an equivalence of $C$ and $D$. Then the unit isomorphism of $\mathrm{self}$ is an isomorphism of the identity of $C$ and the composition of the functor of $\mathrm{self}$ and the inverse of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.Functor.IsEquivalenceclassMathlib.CategoryTheory.Equivalence, predicate

Wording

F is a equivalence (from the name)

English

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

CategoryTheory.Functor.asEquivalencedefMathlib.CategoryTheory.Equivalence, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{asEquivalence}$ applied to $F$ is an equivalence of $C$ and $D$.

CategoryTheory.Functor.invdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the inverse of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the inverse of $F$ is a functor of $D$ and $C$.

CategoryTheory.Iso.compInverseIsodefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the composition inverse isomorphism of i (from the name)

English

Let $i$ be an isomorphism of $F$ and the composition of $G$ and the functor of $H$. Then the composition inverse isomorphism of $i$ is an isomorphism of the composition of $F$ and the inverse of $H$ and $G$ defined as the composition of the right isomorphism whisker of $i$ and the inverse of $H$ and the composition of the associator of the functor of $H$ and the inverse of $H$ and the composition of the left isomorphism whisker of $G$ and the inverse of the unit isomorphism of $H$ and the right unitor of $G$.

CategoryTheory.Iso.inverseCompIsodefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the inverse composition isomorphism of i (from the name)

English

Let $i$ be an isomorphism of $F$ and the composition of the functor of $G$ and $H$. Then the inverse composition isomorphism of $i$ is an isomorphism of the composition of the inverse of $G$ and $F$ and $H$ defined as the composition of the left isomorphism whisker of the inverse of $G$ and $i$ and the composition of the inverse of the associator of the functor of $G$ and $H$ and the composition of the right isomorphism whisker of the counit isomorphism of $G$ and $H$ and the left unitor of $H$.

CategoryTheory.Iso.isoCompInversedefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the isomorphism composition inverse of i (from the name)

English

Let $i$ be an isomorphism of the composition of $G$ and the functor of $H$ and $F$. Then the isomorphism composition inverse of $i$ is an isomorphism of $G$ and the composition of $F$ and the inverse of $H$ defined as the composition of the inverse of the right unitor of $G$ and the composition of the left isomorphism whisker of $G$ and the unit isomorphism of $H$ and the composition of the inverse of the associator of the functor of $H$ and the inverse of $H$ and the right isomorphism whisker of $i$ and the inverse of $H$.

CategoryTheory.Iso.isoFunctorOfIsoInversedefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the isomorphism functor of i (from the name)

English

Let $i$ be an isomorphism of the inverse of $G$ and the inverse of $\mathrm{G'}$. Then the isomorphism functor of $i$ is an isomorphism of the functor of $G$ and the functor of $\mathrm{G'}$ defined as the isomorphism inverse of $i$.

CategoryTheory.Iso.isoInverseCompdefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the isomorphism inverse composition of i (from the name)

English

Let $i$ be an isomorphism of the composition of the functor of $G$ and $H$ and $F$. Then the isomorphism inverse composition of $i$ is an isomorphism of $H$ and the composition of the inverse of $G$ and $F$ defined as the composition of the inverse of the left unitor of $H$ and the composition of the right isomorphism whisker of the inverse of the counit isomorphism of $G$ and $H$ and the composition of the associator of the functor of $G$ and $H$ and the left isomorphism whisker of the inverse of $G$ and $i$.

CategoryTheory.Iso.isoInverseOfIsoFunctordefMathlib.CategoryTheory.Equivalence, function or constant

Wording

the isomorphism inverse of i (from the name)

English

Let $i$ be an isomorphism of the functor of $G$ and the functor of $\mathrm{G'}$. Then the isomorphism inverse of $i$ is an isomorphism of the inverse of $G$ and the inverse of $\mathrm{G'}$ defined as the composition of the isomorphism composition inverse of the composition of the inverse of the left isomorphism whisker of the inverse of $G$ and $i$ and the counit isomorphism of $G$ and the left unitor of the inverse of $\mathrm{G'}$.

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

Wording

the full subcategory congruence of h (from the name)

English

Assume that $\EqtMACRoH {P}{\mathrm{P'}}$. Then the full subcategory congruence of $h$ is an equivalence of the set of full subcategories of $P$ and the set of full subcategories of $\mathrm{P'}$.

Mathlib.CategoryTheory.Equivalence.Symmetry

CategoryTheory.Equivalence.congrLeftFunctordefMathlib.CategoryTheory.Equivalence.Symmetry, function or constant

Wording

the congruence left functor of D and E (from the name)

English

Let $C$, $D$ and $E$ be sets. Then the congruence left functor of $D$ and $E$ is a functor of the set of equivalences of $C$ and $D$ and the set of opposites of the set of equivalences of the set of functors of $C$ and $E$ and the set of functors of $D$ and $E$.

CategoryTheory.Equivalence.inverseFunctordefMathlib.CategoryTheory.Equivalence.Symmetry, function or constant

Wording

the inverse functor of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the inverse functor of $C$ and $D$ is a functor of the set of equivalences of $C$ and $D$ and the set of opposites of the set of functors of $D$ and $C$ defined as the composition of the functor of the inverse equivalence of $C$ and $D$ and the opposite of the functor functor of $D$ and $C$.

CategoryTheory.Equivalence.inverseFunctorObj'defMathlib.CategoryTheory.Equivalence.Symmetry, function or constant

Wording

the inverse functor object of e (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Then the inverse functor object of $e$ is an isomorphism of the opposite of the action of the inverse functor of $C$ and $D$ and $e$ and the inverse of $e$ defined as the identity of the opposite of the action of the inverse functor of $C$ and $D$ and $e$.

CategoryTheory.Equivalence.inverseFunctorObjIsodefMathlib.CategoryTheory.Equivalence.Symmetry, function or constant

Wording

the inverse functor object isomorphism of e (from the name)

English

Let $e$ be an equivalence of $C$ and $D$. Then the inverse functor object isomorphism of $e$ is an isomorphism of the action of the inverse functor of $C$ and $D$ and $e$ and $\operatorname{op}$ applied to the inverse of $e$ defined as the identity of the action of the inverse functor of $C$ and $D$ and $e$.

CategoryTheory.Equivalence.symmEquivdefMathlib.CategoryTheory.Equivalence.Symmetry, function or constant

Wording

the inverse equivalence of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the inverse equivalence of $C$ and $D$ is an equivalence of the set of equivalences of $C$ and $D$ and the set of opposites of the set of equivalences of $D$ and $C$.

CategoryTheory.Equivalence.symmEquivFunctordefMathlib.CategoryTheory.Equivalence.Symmetry, function or constant

Wording

the forward functor of the equivalence of C and D (from the docstring)

English

Let $C$ and $D$ be sets. Then the forward functor of the equivalence of $C$ and $D$ is a functor of the set of equivalences of $C$ and $D$ and the set of opposites of the set of equivalences of $D$ and $C$.

CategoryTheory.Equivalence.symmEquivInversedefMathlib.CategoryTheory.Equivalence.Symmetry, function or constant

Wording

the inverse functor of the equivalence of C and D (from the docstring)

English

Let $C$ and $D$ be sets. Then the inverse functor of the equivalence of $C$ and $D$ is a functor of the set of opposites of the set of equivalences of $D$ and $C$ and the set of equivalences of $C$ and $D$.

Mathlib.CategoryTheory.EquivalenceRelation

CategoryTheory.EffectiveEquivalenceRelationstructureMathlib.CategoryTheory.EquivalenceRelation, type

Wording

effective equivalence relation of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $A$. Then the effective equivalence relations of $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.EffectiveEquivalenceRelation.BdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an effective equivalence relation of $x_{1}$ and $x_{2}$. Then $\operatorname{B}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.EffectiveEquivalenceRelation.isCoequalizerdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $A$. Let $e$ be an effective equivalence relation of $x_{1}$ and $x_{2}$. Then $\operatorname{isCoequalizer}$ applied to $x_{1}$, $x_{2}$ and $e$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $e$ and $\operatorname{w}$ applied to $\operatorname{toCommSq}$ applied to $\operatorname{isPushout}$ applied to $e$ defined as $\operatorname{isLimitFork}$ applied to $\operatorname{isPushout}$ applied to $e$.

CategoryTheory.EffectiveEquivalenceRelation.πdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the projection of self (from the name)

English

Let $\mathrm{self}$ be an effective equivalence relation of $x_{1}$ and $x_{2}$. Then the projection of $\mathrm{self}$ is a homomorphism of $A$ and $\operatorname{B}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.EquivalenceRelationstructureMathlib.CategoryTheory.EquivalenceRelation, type

Wording

equivalence relation of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $X$. Then the equivalence relations of $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.EquivalenceRelation.cdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an equivalence relation of $x_{1}$ and $x_{2}$. Then $\operatorname{c}$ applied to $\mathrm{self}$ is a pullback cone of $x_{2}$ and $x_{1}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

CategoryTheory.EquivalenceRelation.isLimitdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an equivalence relation of $x_{1}$ and $x_{2}$. Then $\operatorname{isLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{c}$ applied to $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

CategoryTheory.EquivalenceRelation.sdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an equivalence relation of $x_{1}$ and $x_{2}$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a homomorphism of $R$ and $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.EquivalenceRelation.tdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an equivalence relation of $x_{1}$ and $x_{2}$. Then $\operatorname{t}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $\operatorname{c}$ applied to $\mathrm{self}$ and $R$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$.

CategoryTheory.EquivalenceRelation.toSymmetricRelationdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the symmetric relation of self (from the name)

English

Let $\mathrm{self}$ be an equivalence relation of $x_{1}$ and $x_{2}$. Then the symmetric relation of $\mathrm{self}$ is a symmetric relation of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_ReflexiveRelation\_\_toJointlyMono\_u2082\_}$ applied to $\operatorname{toReflexiveRelation}$ applied to $\mathrm{self}$, $\operatorname{s}$ applied to $\mathrm{self}$, $\mathrm{CategoryTheory\_\_EquivalenceRelation\_\_symmetry\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_EquivalenceRelation\_\_symmetry\_u2082\_}$ applied to $\mathrm{self}$.

CategoryTheory.EquivalenceRelation.toTransitiveRelationdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the transitive relation of self (from the name)

English

Let $\mathrm{self}$ be an equivalence relation of $x_{1}$ and $x_{2}$. Then the transitive relation of $\mathrm{self}$ is a transitive relation of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_ReflexiveRelation\_\_toJointlyMono\_u2082\_}$ applied to $\operatorname{toReflexiveRelation}$ applied to $\mathrm{self}$, $\operatorname{c}$ applied to $\mathrm{self}$, $\operatorname{isLimit}$ applied to $\mathrm{self}$, $\operatorname{t}$ applied to $\mathrm{self}$, $\mathrm{CategoryTheory\_\_EquivalenceRelation\_\_transitivity\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_EquivalenceRelation\_\_transitivity\_u2082\_}$ applied to $\mathrm{self}$.

CategoryTheory.IsEffectiveEquivalenceRelationclassMathlib.CategoryTheory.EquivalenceRelation, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $A$. Then we can say that $\operatorname{IsEffectiveEquivalenceRelation}$ holds for $x_{1}$ and $x_{2}$.

CategoryTheory.IsEquivalenceRelationclassMathlib.CategoryTheory.EquivalenceRelation, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $X$. Then we can say that $\operatorname{IsEquivalenceRelation}$ holds for $x_{1}$ and $x_{2}$.

CategoryTheory.IsKernelPair.equivalenceRelationdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the equivalence relation of x2 and ht (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $X$. Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Assume that $\operatorname{IsKernelPair}$ holds for $f$, $x_{1}$ and $x_{2}$. Then the equivalence relation of $x_{2}$ and $\mathrm{ht}$ is an equivalence relation of $x_{1}$ and $x_{2}$.

CategoryTheory.IsUniversallyEffectiveEquivalenceRelationclassMathlib.CategoryTheory.EquivalenceRelation, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $A$. Then we can say that $\operatorname{IsUniversallyEffectiveEquivalenceRelation}$ holds for $x_{1}$ and $x_{2}$.

CategoryTheory.IsUniversallyEffectiveEquivalenceRelationCategoryclassMathlib.CategoryTheory.EquivalenceRelation, predicate

Wording

C is a universally effective equivalence relation category (from the name)

English

generation took over the time limit

CategoryTheory.JointlyMono₂classMathlib.CategoryTheory.EquivalenceRelation, predicate

Wording

no wording

English

Let $x_{3}$ be a homomorphism of $R$ and $x_{1}$. Let $x_{4}$ be a homomorphism of $R$ and $x_{2}$. Then we can say that $\mathrm{CategoryTheory\_\_JointlyMono\_u2082\_}$ holds for $x_{3}$ and $x_{4}$.

CategoryTheory.ReflexiveRelationstructureMathlib.CategoryTheory.EquivalenceRelation, type

Wording

reflexive relation of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $X$. Then the reflexive relations of $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.ReflexiveRelation.mapdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the map of e and F (from the name)

English

Let $e$ be a reflexive relation of $x_{2}$ and $x_{3}$. Let $F$ be a functor of $C$ and $D$. Then the map of $e$ and $F$ is a reflexive relation of the map of $F$ and $x_{2}$ and the map of $F$ and $x_{3}$.

CategoryTheory.ReflexiveRelation.rdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a reflexive relation of $x_{1}$ and $x_{2}$. Then $\operatorname{r}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.SymmetricRelationstructureMathlib.CategoryTheory.EquivalenceRelation, type

Wording

symmetric relation of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $X$. Then the symmetric relations of $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.SymmetricRelation.mapdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the map of e and F (from the name)

English

Let $e$ be a symmetric relation of $x_{2}$ and $x_{3}$. Let $F$ be a functor of $C$ and $D$. Then the map of $e$ and $F$ is a symmetric relation of the map of $F$ and $x_{2}$ and the map of $F$ and $x_{3}$.

CategoryTheory.SymmetricRelation.sdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a symmetric relation of $x_{1}$ and $x_{2}$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a homomorphism of $R$ and $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.TransitiveRelationstructureMathlib.CategoryTheory.EquivalenceRelation, type

Wording

transitive relation of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be homomorphisms of $R$ and $X$. Then the transitive relations of $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.TransitiveRelation.cdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a transitive relation of $x_{1}$ and $x_{2}$. Then $\operatorname{c}$ applied to $\mathrm{self}$ is a pullback cone of $x_{2}$ and $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.TransitiveRelation.isLimitdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a transitive relation of $x_{1}$ and $x_{2}$. Then $\operatorname{isLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{c}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.TransitiveRelation.mapdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the map of e and F (from the name)

English

Let $e$ be a transitive relation of $x_{2}$ and $x_{3}$. Let $F$ be a functor of $C$ and $D$. Then the map of $e$ and $F$ is a transitive relation of the map of $F$ and $x_{2}$ and the map of $F$ and $x_{3}$.

CategoryTheory.TransitiveRelation.tdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a transitive relation of $x_{1}$ and $x_{2}$. Then $\operatorname{t}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $\operatorname{c}$ applied to $\mathrm{self}$ and $R$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

CategoryTheory.UniversallyEffectiveEquivalenceRelationstructureMathlib.CategoryTheory.EquivalenceRelation, type

Wording

universally effective equivalence relation of x1 and x2 (from the name)

English

generation took over the time limit

TypeCat.EquivalenceRelation.ofEquivalencedefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the equivalence relation of h (from the name)

English

Assume that $x$ is an equivalence relation. Then the equivalence relation of $h$ is an equivalence relation of $\mathrm{TypeCat\_\_p\_u2081\_OfRel}$ applied to $x$ and $\mathrm{TypeCat\_\_p\_u2082\_OfRel}$ applied to $x$.

TypeCat.ROfReldefMathlib.CategoryTheory.EquivalenceRelation, type

Wording

no wording

English

Let $x$ be a function from elements of $X$ and elements of $X$ to propositions. Then an element of $\operatorname{ROfRel}$ applied to $x$ is an element of the function that maps $x$ to $\SubtypeSet {x_{1}}{\operatorname{uncurry} (x , x_{1})}$.

TypeCat.ReflexiveRelation.ofRefldefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the reflexive relation of h (from the name)

English

Assume that $x$ is reflexive. Then the reflexive relation of $h$ is a reflexive relation of $\mathrm{TypeCat\_\_p\_u2081\_OfRel}$ applied to $x$ and $\mathrm{TypeCat\_\_p\_u2082\_OfRel}$ applied to $x$.

TypeCat.Rel.ofPairdefMathlib.CategoryTheory.EquivalenceRelation, predicate

Wording

no wording

English

Let $x$ and $x_{1}$ be homomorphisms of $R$ and $X$. Let $x_{2}$ and $x_{3}$ be elements of $X$. Then $\operatorname{ofPair}$ holds for $x$, $x_{1}$, $x_{2}$ and $x_{3}$, if there exists an element $r$ of $R$, such that $\EqtMACRoH {\operatorname{hom} (x , r)}{x_{2}}$ and $\EqtMACRoH {\operatorname{hom} (x_{1} , r)}{x_{3}}$.

TypeCat.SymmetricRelation.ofSymmetricdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the symmetric relation (from the name)

English

The symmetric relation is a symmetric relation of $\mathrm{TypeCat\_\_p\_u2081\_OfRel}$ applied to $x$ and $\mathrm{TypeCat\_\_p\_u2082\_OfRel}$ applied to $x$.

TypeCat.TransitiveRelation.ofIsTransdefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

the transitive relation of h (from the name)

English

Assume that $x$ is transitive. Then the transitive relation of $h$ is a transitive relation of $\mathrm{TypeCat\_\_p\_u2081\_OfRel}$ applied to $x$ and $\mathrm{TypeCat\_\_p\_u2082\_OfRel}$ applied to $x$.

TypeCat.p₁OfReldefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $x$ be a function from elements of $X$ and elements of $X$ to propositions. Then $\mathrm{TypeCat\_\_p\_u2081\_OfRel}$ applied to $x$ is a homomorphism of $\operatorname{ROfRel}$ applied to $x$ and $X$ defined as the type category of $\operatorname{comp}$ applied to $\ProdfstMACRoZ$ and $\operatorname{uncurry}$ applied to $x$.

TypeCat.p₂OfReldefMathlib.CategoryTheory.EquivalenceRelation, function or constant

Wording

no wording

English

Let $x$ be a function from elements of $X$ and elements of $X$ to propositions. Then $\mathrm{TypeCat\_\_p\_u2082\_OfRel}$ applied to $x$ is a homomorphism of $\operatorname{ROfRel}$ applied to $x$ and $X$ defined as the type category of $\operatorname{comp}$ applied to $\ProdsndMACRoAA$ and $\operatorname{uncurry}$ applied to $x$.

Mathlib.CategoryTheory.EssentialImage

CategoryTheory.Functor.EssImageSubcategorydefMathlib.CategoryTheory.EssentialImage, type

Wording

essential image subcategory of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then an essential image subcategory of $F$ is an element of the function that maps $F$ to the set of full subcategories of the essential image of $F$.

CategoryTheory.Functor.EssSurjclassMathlib.CategoryTheory.EssentialImage, predicate

Wording

F is a essential surjection (from the name)

English

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

CategoryTheory.Functor.essImagedefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

the essential image of F (from the docstring)

English

Let $F$ be a functor of $C$ and $D$. Then the essential image of $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 $\mathrm{Nonempty}$ holds for the set of isomorphisms of the action of $F$ and $X$ and $Y$.

CategoryTheory.Functor.essImage.getIsodefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

no wording

English

Assume that $\operatorname{essImage}$ holds for $F$. Then $\operatorname{getIso}$ applied to $h$ is an isomorphism of the action of $F$ and the witness of $h$ and $Y$.

CategoryTheory.Functor.essImage.liftFunctordefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

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

English

Let $G$ be a functor of $J$ and $D$. Let $F$ be a functor of $C$ and $D$ such that for all elements $j$ of $J$, $\operatorname{essImage}$ holds for $F$. Then the lift functor of $G$ and $F$ is a functor of $J$ and $C$.

CategoryTheory.Functor.essImage.liftFunctorCompIsodefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

the lift functor composition isomorphism of G and F (from the name)

English

Let $G$ be a functor of $J$ and $D$. Let $F$ be a functor of $C$ and $D$ such that for all elements $j$ of $J$, $\operatorname{essImage}$ holds for $F$. Then the lift functor composition isomorphism of $G$ and $F$ is an isomorphism of the composition of the lift functor of $G$ and $F$ and $F$ and $G$.

CategoryTheory.Functor.essImage.witnessdefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

the witness of h (from the name)

English

Assume that $\operatorname{essImage}$ holds for $F$. Then the witness of $h$ is an element of $C$ defined as $\operatorname{choose}$ applied to $h$.

CategoryTheory.Functor.objObjPreimageIsodefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

the object object preimage isomorphism of F and Y (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $Y$ be an element of $D$. Then the object object preimage isomorphism of $F$ and $Y$ is an isomorphism of the action of $F$ and the object preimage of $F$ and $Y$ and $Y$ defined as $\operatorname{getIso}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_EssSurj\_\_mem\_essImage}$ applied to $F$ and $Y$.

CategoryTheory.Functor.objPreimagedefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

the object preimage of F and Y (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $Y$ be an element of $D$. Then the object preimage of $F$ and $Y$ is an element of $C$ defined as the witness of $\mathrm{CategoryTheory\_\_Functor\_\_EssSurj\_\_mem\_essImage}$ applied to $F$ and $Y$.

CategoryTheory.Functor.toEssImagedefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

the essential image of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the essential image of $F$ is a functor of $C$ and the set of essential image subcategories of $F$ defined as the lift of the essential image of $F$ and $F$.

CategoryTheory.Functor.toEssImageCompιdefMathlib.CategoryTheory.EssentialImage, function or constant

Wording

the essential image composition inclusion of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the essential image composition inclusion of $F$ is an isomorphism of the composition of the essential image of $F$ and the inclusion of the essential image of $F$ and $F$ defined as the lift composition inclusion isomorphism of the essential image of $F$ and $F$.

Mathlib.CategoryTheory.EssentiallySmall

CategoryTheory.EssentiallySmallclassMathlib.CategoryTheory.EssentiallySmall, predicate

Wording

C is essentially small (from the name)

English

generation took over the time limit

CategoryTheory.LocallySmallclassMathlib.CategoryTheory.EssentiallySmall, predicate

Wording

C is locally small (from the name)

English

generation took over the time limit

CategoryTheory.Shrink.equivalencedefMathlib.CategoryTheory.EssentiallySmall, function or constant

Wording

the equivalence of C (from the name)

English

Let $C$ be a set. Then the equivalence of $C$ is an equivalence of $C$ and the set of shrinks of $C$ defined as the inverse of $\operatorname{induced}$ applied to the inverse of the equivalence shrink of $C$.

CategoryTheory.ShrinkHomsdefMathlib.CategoryTheory.EssentiallySmall, type

Wording

shrink hom of C (from the name)

English

Let $C$ be a set. Then a shrink hom of $C$ is an element of the function that maps $C$ to $C$.

CategoryTheory.ShrinkHoms.equivalencedefMathlib.CategoryTheory.EssentiallySmall, function or constant

Wording

the equivalence of C (from the name)

English

Let $C$ be a set. Then the equivalence of $C$ is an equivalence of $C$ and the set of shrink homs of $C$.

CategoryTheory.ShrinkHoms.fromShrinkHomsdefMathlib.CategoryTheory.EssentiallySmall, function or constant

Wording

no wording

English

Let $X$ be a shrink hom of $\mathrm{C'}$. Then $\operatorname{fromShrinkHoms}$ applied to $X$ is an element of $\mathrm{C'}$ defined as $X$.

CategoryTheory.ShrinkHoms.toShrinkHomsdefMathlib.CategoryTheory.EssentiallySmall, function or constant

Wording

the shrink hom of X (from the name)

English

Let $X$ be an element of $\mathrm{C'}$. Then the shrink hom of $X$ is a shrink hom of $\mathrm{C'}$ defined as $X$.

CategoryTheory.SmallModeldefMathlib.CategoryTheory.EssentiallySmall, type

Wording

small model of C (from the name)

English

Let $C$ be a set. Then a small model of $C$ is an element of the function that maps $C$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_EssentiallySmall\_\_equiv\_smallCategory}$.

CategoryTheory.equivSmallModeldefMathlib.CategoryTheory.EssentiallySmall, function or constant

Wording

the equivalence small model of C (from the name)

English

Let $C$ be a set. Then the equivalence small model of $C$ is an equivalence of $C$ and the set of small models of $C$.

Mathlib.CategoryTheory.Extensive

CategoryTheory.FinitaryExtensiveclassMathlib.CategoryTheory.Extensive, predicate

Wording

no wording

English

Let $C$ be a set. Then we can say that $\operatorname{FinitaryExtensive}$ holds for $C$.

CategoryTheory.FinitaryPreExtensiveclassMathlib.CategoryTheory.Extensive, predicate

Wording

no wording

English

Let $C$ be a set. Then we can say that $\operatorname{FinitaryPreExtensive}$ holds for $C$.

CategoryTheory.HasPullbacksOfInclusionsclassMathlib.CategoryTheory.Extensive, predicate

Wording

C has pullbacks of inclusions (from the name)

English

Let $C$ be a set. Then we can say that $C$ has pullbacks of inclusions.

CategoryTheory.PreservesPullbacksOfInclusionsclassMathlib.CategoryTheory.Extensive, predicate

Wording

F preserves pullbacks of inclusions (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ preserves pullbacks of inclusions.

Mathlib.CategoryTheory.ExtremalEpi

CategoryTheory.ExtremalEpiclassMathlib.CategoryTheory.ExtremalEpi, predicate

Wording

f is a extremal epimorphism (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is an extremal epimorphism.

Mathlib.CategoryTheory.FiberedCategory.BasedCategory

CategoryTheory.BasedCategorystructureMathlib.CategoryTheory.FiberedCategory.BasedCategory, type

Wording

no wording

English

Let $x$ be a set. Then the elements of $\operatorname{BasedCategory}$ applied to $x$ are a basic type.

CategoryTheory.BasedCategory.objdefMathlib.CategoryTheory.FiberedCategory.BasedCategory, type

Wording

object of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{BasedCategory}$ applied to $x$. Then an object of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.BasedCategory.ofFunctordefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

no wording

English

Let $p$ be a functor of $x_{2}$ and $x$. Then $\operatorname{ofFunctor}$ applied to $p$ is an element of $\operatorname{BasedCategory}$ applied to $x$ defined as $\operatorname{mk}$ applied to $x_{2}$, $\mathrm{inferInstance}$ and $p$.

CategoryTheory.BasedCategory.pdefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{BasedCategory}$ applied to $x$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is a functor of the set of objects of $\mathrm{self}$ and $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CategoryTheory.BasedCategory.whiskerLeftdefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

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

English

Let $F$ be an element of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{3}$. Let $x_{5}$ be a homomorphism of $G$ and $H$. Then the left whisker of $F$ and $x_{5}$ is a homomorphism of the composition of $F$ and $G$ and the composition of $F$ and $H$.

CategoryTheory.BasedCategory.whiskerRightdefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

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

English

Let $x_{5}$ be a homomorphism of $F$ and $G$. Let $H$ be an element of $\operatorname{BasedFunctor}$ applied to $x_{3}$ and $x_{4}$. Then the right whisker of $x_{5}$ and $H$ is a homomorphism of the composition of $F$ and $H$ and the composition of $G$ and $H$.

CategoryTheory.BasedFunctorstructureMathlib.CategoryTheory.FiberedCategory.BasedCategory, type

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $\operatorname{BasedCategory}$ applied to $x$. Then the elements of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.BasedFunctor.compdefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

the composition of F and G (from the name)

English

Let $F$ be an element of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{3}$. Let $G$ be an element of $\operatorname{BasedFunctor}$ applied to $x_{3}$ and $x_{4}$. Then the composition of $F$ and $G$ is an element of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{4}$.

CategoryTheory.BasedFunctor.iddefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

the identity of x2 (from the name)

English

Let $x_{2}$ be an element of $\operatorname{BasedCategory}$ applied to $x$. Then the identity of $x_{2}$ is an element of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{2}$.

CategoryTheory.BasedNatIso.iddefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

the identity natural transformation of F (from the docstring)

English

Let $F$ be an element of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{3}$. Then the identity natural transformation of $F$ is an isomorphism of $F$ and $F$.

CategoryTheory.BasedNatIso.mkNatIsodefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

the natural isomorphism of x4 and #2 (from the name)

English

Let $x_{4}$ be an isomorphism of $\operatorname{toFunctor}$ applied to $F$ and $\operatorname{toFunctor}$ applied to $G$ such that for all objects $a$ of $x_{2}$, $\operatorname{IsHomLift}$ holds for $\operatorname{p}$ applied to $x_{3}$, the identity morphism of the action of $\operatorname{p}$ applied to $x_{2}$ and $a$ and the component of the homomorphism of $x_{4}$ and $a$. Then the natural isomorphism of $x_{4}$ and $\mathrm{isHomLift'}$ is an isomorphism of $F$ and $G$.

CategoryTheory.BasedNatTransstructureMathlib.CategoryTheory.FiberedCategory.BasedCategory, type

Wording

no wording

English

Let $F$ and $G$ be elements of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{3}$. Then the elements of $\operatorname{BasedNatTrans}$ applied to $F$ and $G$ are a basic type.

CategoryTheory.BasedNatTrans.compdefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

the composition of x4 and x5 (from the name)

English

Let $x_{4}$ be an element of $\operatorname{BasedNatTrans}$ applied to $F$ and $G$. Let $x_{5}$ be an element of $\operatorname{BasedNatTrans}$ applied to $G$ and $H$. Then the composition of $x_{4}$ and $x_{5}$ is an element of $\operatorname{BasedNatTrans}$ applied to $F$ and $H$.

CategoryTheory.BasedNatTrans.forgetfuldefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $\operatorname{BasedCategory}$ applied to $x$. Then $\operatorname{forgetful}$ applied to $x_{2}$ and $x_{3}$ is a functor of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{3}$ and the set of functors of the set of objects of $x_{2}$ and the set of objects of $x_{3}$.

CategoryTheory.BasedNatTrans.iddefMathlib.CategoryTheory.FiberedCategory.BasedCategory, function or constant

Wording

the identity natural transformation of F (from the docstring)

English

Let $F$ be an element of $\operatorname{BasedFunctor}$ applied to $x_{2}$ and $x_{3}$. Then the identity natural transformation of $F$ is an element of $\operatorname{BasedNatTrans}$ applied to $F$ and $F$.

Mathlib.CategoryTheory.FiberedCategory.Cartesian

CategoryTheory.Functor.IsCartesianclassMathlib.CategoryTheory.FiberedCategory.Cartesian, predicate

Wording

x4 is cartesian with respect to f (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Then we can say that $x_{4}$ is cartesian with respect to $f$.

CategoryTheory.Functor.IsCartesian.domainUniqueUpToIsodefMathlib.CategoryTheory.FiberedCategory.Cartesian, function or constant

Wording

no wording

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Let $x_{5}$ be a homomorphism of $\mathrm{a'}$ and $b$. Then $\operatorname{domainUniqueUpToIso}$ applied to $p$, $f$, $x_{4}$ and $x_{5}$ is an isomorphism of $\mathrm{a'}$ and $a$.

CategoryTheory.Functor.IsCartesian.mapdefMathlib.CategoryTheory.FiberedCategory.Cartesian, function or constant

Wording

the map of x4 and x5 (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Let $x_{5}$ be a homomorphism of $\mathrm{a'}$ and $b$. Then the map of $x_{4}$ and $x_{5}$ is a homomorphism of $\mathrm{a'}$ and $a$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsCartesian\_\_universal\_property}$ applied to $f$ and $x_{5}$.

CategoryTheory.Functor.IsStronglyCartesianclassMathlib.CategoryTheory.FiberedCategory.Cartesian, predicate

Wording

no wording

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Then we can say that $\operatorname{IsStronglyCartesian}$ holds for $p$, $f$ and $x_{4}$.

CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIsodefMathlib.CategoryTheory.FiberedCategory.Cartesian, function or constant

Wording

the domain isomorphism of x4 and x5 (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Assume that $\mathrm{f'}$ is equal to the composition of the homomorphism of $g$ and $f$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Let $x_{5}$ be a homomorphism of $\mathrm{a'}$ and $b$. Then the domain isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $\mathrm{a'}$ and $a$.

CategoryTheory.Functor.IsStronglyCartesian.mapdefMathlib.CategoryTheory.FiberedCategory.Cartesian, function or constant

Wording

the map of x4 and #5 (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Assume that $\mathrm{f'}$ is equal to the composition of $g$ and $f$. Let $x_{5}$ be a homomorphism of $\mathrm{a'}$ and $b$. Then the map of $x_{4}$ and $x_{5}$ is a homomorphism of $\mathrm{a'}$ and $a$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsStronglyCartesian\_\_universal\_property}$ applied to $p$, $f$, $x_{4}$, $g$, $\mathrm{f'}$, $\mathrm{hf'}$ and $x_{5}$.

Mathlib.CategoryTheory.FiberedCategory.Cocartesian

CategoryTheory.Functor.IsCocartesianclassMathlib.CategoryTheory.FiberedCategory.Cocartesian, predicate

Wording

no wording

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Then we can say that $\operatorname{IsCocartesian}$ holds for $p$, $f$ and $x_{4}$.

CategoryTheory.Functor.IsCocartesian.codomainUniqueUpToIsodefMathlib.CategoryTheory.FiberedCategory.Cocartesian, function or constant

Wording

no wording

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Let $x_{5}$ be a homomorphism of $a$ and $\mathrm{b'}$. Then $\operatorname{codomainUniqueUpToIso}$ applied to $p$, $f$, $x_{4}$ and $x_{5}$ is an isomorphism of $b$ and $\mathrm{b'}$.

CategoryTheory.Functor.IsCocartesian.mapdefMathlib.CategoryTheory.FiberedCategory.Cocartesian, function or constant

Wording

the map of x4 and x5 (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Let $x_{5}$ be a homomorphism of $a$ and $\mathrm{b'}$. Then the map of $x_{4}$ and $x_{5}$ is a homomorphism of $b$ and $\mathrm{b'}$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsCocartesian\_\_universal\_property}$ applied to $f$ and $x_{5}$.

CategoryTheory.Functor.IsStronglyCocartesianclassMathlib.CategoryTheory.FiberedCategory.Cocartesian, predicate

Wording

no wording

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Then we can say that $\operatorname{IsStronglyCocartesian}$ holds for $p$, $f$ and $x_{4}$.

CategoryTheory.Functor.IsStronglyCocartesian.codomainIsoOfBaseIsodefMathlib.CategoryTheory.FiberedCategory.Cocartesian, function or constant

Wording

the codomain isomorphism of x4 and x5 (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Assume that $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $g$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Let $x_{5}$ be a homomorphism of $a$ and $\mathrm{b'}$. Then the codomain isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $b$ and $\mathrm{b'}$.

CategoryTheory.Functor.IsStronglyCocartesian.mapdefMathlib.CategoryTheory.FiberedCategory.Cocartesian, function or constant

Wording

the map of x4 and #5 (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Assume that $\mathrm{f'}$ is equal to the composition of $f$ and $g$. Let $x_{5}$ be a homomorphism of $a$ and $\mathrm{b'}$. Then the map of $x_{4}$ and $x_{5}$ is a homomorphism of $b$ and $\mathrm{b'}$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsStronglyCocartesian\_\_universal\_property}$ applied to $p$, $f$, $x_{4}$, $g$, $\mathrm{f'}$, $\mathrm{hf'}$ and $x_{5}$.

Mathlib.CategoryTheory.FiberedCategory.Fiber

CategoryTheory.Functor.FiberdefMathlib.CategoryTheory.FiberedCategory.Fiber, type

Wording

fiber of p and S (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $S$ be an element of $x$. Then a fiber of $p$ and $S$ is an element of the function that maps $p$ and $S$ to $\SubtypeSet {a}{(\EqtMACRoH {\operatorname{obj} (p , a)}{S})}$.

CategoryTheory.Functor.Fiber.fiberInclusiondefMathlib.CategoryTheory.FiberedCategory.Fiber, function or constant

Wording

the fiber inclusion (from the name)

English

The fiber inclusion is a functor of the set of fibers of $p$ and $S$ and $x_{1}$.

CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConstdefMathlib.CategoryTheory.FiberedCategory.Fiber, function or constant

Wording

the fiber inclusion composition isomorphism constant (from the name)

English

The fiber inclusion composition isomorphism constant is an isomorphism of the composition of the fiber inclusion and $p$ and the action of the constant of the set of fibers of $p$ and $S$ and $S$.

CategoryTheory.Functor.Fiber.homMkdefMathlib.CategoryTheory.FiberedCategory.Fiber, function or constant

Wording

the homomorphism of S and x4 (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $S$ be an element of $x$. Let $x_{4}$ be a homomorphism of $a$ and $b$. Then the homomorphism of $S$ and $x_{4}$ is a homomorphism of $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_IsHomLift\_\_domain\_eq}$ applied to $p$, the identity morphism of $S$ and $x_{4}$ and $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_IsHomLift\_\_codomain\_eq}$ applied to $p$, the identity morphism of $S$ and $x_{4}$ defined as $x_{4}$.

CategoryTheory.Functor.Fiber.inducedFunctordefMathlib.CategoryTheory.FiberedCategory.Fiber, function or constant

Wording

the induced functor of hF (from the name)

English

Assume that the composition of $F$ and $p$ is equal to the action of the constant of $C$ and $S$. Then the induced functor of $\mathrm{hF}$ is a functor of $C$ and the set of fibers of $p$ and $S$.

CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelfdefMathlib.CategoryTheory.FiberedCategory.Fiber, function or constant

Wording

the induced functor composition isomorphism self of hF (from the name)

English

Assume that the composition of $F$ and $p$ is equal to the action of the constant of $C$ and $S$. Then the induced functor composition isomorphism self of $\mathrm{hF}$ is an isomorphism of the composition of the induced functor of $\mathrm{hF}$ and the fiber inclusion and $F$ defined as the identity of the composition of the induced functor of $\mathrm{hF}$ and the fiber inclusion.

CategoryTheory.Functor.Fiber.mkdefMathlib.CategoryTheory.FiberedCategory.Fiber, function or constant

Wording

no wording

English

Assume that the action of $p$ and $a$ is equal to $S$. Then $\operatorname{mk}$ applied to $\mathrm{ha}$ is a fiber of $p$ and $S$ defined as $a$.

Mathlib.CategoryTheory.FiberedCategory.Fibered

CategoryTheory.Functor.IsFiberedclassMathlib.CategoryTheory.FiberedCategory.Fibered, predicate

Wording

p is fibered (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Then we can say that $p$ is fibered.

CategoryTheory.Functor.IsFibered.pullbackPullbackIsodefMathlib.CategoryTheory.FiberedCategory.Fibered, function or constant

Wording

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

English

Assume that the action of $p$ and $a$ is equal to $S$. Let $f$ be a homomorphism of $R$ and $S$. Let $g$ be a homomorphism of $T$ and $R$. Then the pullback pullback isomorphism of $f$ and $g$ is an isomorphism of the pullback object of $\mathrm{ha}$ and the composition of $g$ and $f$ and the pullback object of $\mathrm{CategoryTheory\_\_Functor\_\_IsPreFibered\_\_pullbackObj\_proj}$ applied to $\mathrm{ha}$ and $f$ and $g$.

CategoryTheory.Functor.IsPreFiberedclassMathlib.CategoryTheory.FiberedCategory.Fibered, predicate

Wording

p is fibered (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Then we can say that $p$ is fibered.

CategoryTheory.Functor.IsPreFibered.pullbackMapdefMathlib.CategoryTheory.FiberedCategory.Fibered, function or constant

Wording

the pullback map of ha and f (from the name)

English

Assume that the action of $p$ and $a$ is equal to $S$. Let $f$ be a homomorphism of $R$ and $S$. Then the pullback map of $\mathrm{ha}$ and $f$ is a homomorphism of the pullback object of $\mathrm{ha}$ and $f$ and $a$.

CategoryTheory.Functor.IsPreFibered.pullbackObjdefMathlib.CategoryTheory.FiberedCategory.Fibered, function or constant

Wording

the pullback object of ha and f (from the name)

English

Assume that the action of $p$ and $a$ is equal to $S$. Let $f$ be a homomorphism of $R$ and $S$. Then the pullback object of $\mathrm{ha}$ and $f$ is an element of $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsPreFibered\_\_exists\_isCartesian}$ applied to $p$, $\mathrm{ha}$ and $f$.

Mathlib.CategoryTheory.FiberedCategory.Grothendieck

CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLiftdefMathlib.CategoryTheory.FiberedCategory.Grothendieck, function or constant

Wording

the cartesian lift of a and f (from the name)

English

Let $a$ be an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$. Let $f$ be a homomorphism of $R$ and $S$. Then the cartesian lift of $a$ and $f$ is a homomorphism of the domain cartesian lift of $a$ and $f$ and $\operatorname{mk}$ applied to $S$ and $a$ defined as $\operatorname{mk}$ applied to $f$ and the identity morphism of the object in the fiber of the base object of the domain cartesian lift of $a$ and $f$.

CategoryTheory.Pseudofunctor.CoGrothendieck.compIsodefMathlib.CategoryTheory.FiberedCategory.Grothendieck, function or constant

Wording

the composition isomorphism of F and S (from the name)

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $x$ and the set of categories. Let $S$ be an element of $x$. Then the composition isomorphism of $F$ and $S$ is an isomorphism of the composition of the inclusion of $F$ and $S$ and $\operatorname{forget}$ applied to $F$ and the action of the constant of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$ and $S$.

CategoryTheory.Pseudofunctor.CoGrothendieck.domainCartesianLiftdefMathlib.CategoryTheory.FiberedCategory.Grothendieck, function or constant

Wording

the domain cartesian lift of a and f (from the name)

English

Let $a$ be an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$. Let $f$ be a homomorphism of $R$ and $S$. Then the domain cartesian lift of $a$ and $f$ is an element of $\operatorname{CoGrothendieck}$ applied to $F$ defined as $\operatorname{mk}$ applied to $R$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $f$ and $a$.

CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLiftdefMathlib.CategoryTheory.FiberedCategory.Grothendieck, function or constant

Wording

the homomorphism cartesian lift of g and x2 (from the name)

English

Let $f$ be a homomorphism of $R$ and $S$. Let $g$ be a homomorphism of the underlying object in the base category of $\mathrm{a'}$ and $R$. Let $x_{2}$ be a homomorphism of $\mathrm{a'}$ and $\operatorname{mk}$ applied to $S$ and $a$. Then the homomorphism cartesian lift of $g$ and $x_{2}$ is a homomorphism of $\mathrm{a'}$ and the domain cartesian lift of $a$ and $f$.

CategoryTheory.Pseudofunctor.CoGrothendieck.ιdefMathlib.CategoryTheory.FiberedCategory.Grothendieck, function or constant

Wording

the inclusion of F and S (from the name)

English

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $x$ and the set of categories. Let $S$ be an element of $x$. Then the inclusion of $F$ and $S$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$ and $\operatorname{CoGrothendieck}$ applied to $F$.

Mathlib.CategoryTheory.FiberedCategory.HasFibers

HasFibersclassMathlib.CategoryTheory.FiberedCategory.HasFibers, predicate

Wording

p has fibers (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Then we can say that $p$ has fibers.

HasFibers.FibdefMathlib.CategoryTheory.FiberedCategory.HasFibers, type

Wording

no wording

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $S$ be an element of $x$. Then an element of $\operatorname{Fib}$ applied to $p$ and $S$ is an element of the function that maps $p$ and $S$ to $\operatorname{proj0}$ applied to $\mathrm{self}$ and $S$.

HasFibers.Fib.homMkdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the homomorphism of x5 (from the name)

English

Let $x_{5}$ be a homomorphism of the action of the inclusion of $S$ and $a$ and the action of the inclusion of $S$ and $b$. Then the homomorphism of $x_{5}$ is a homomorphism of $a$ and $b$ defined as the choice of the induced functor of $p$ and $S$ and the homomorphism of $S$ and $x_{5}$.

HasFibers.Fib.isoMkdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the lift of x5 and h (from the docstring)

English

Let $x_{5}$ be an isomorphism of the action of the inclusion of $S$ and $a$ and the action of the inclusion of $S$ and $b$ such that $\operatorname{IsHomLift}$ holds for $p$, the identity morphism of $S$ and the homomorphism of $x_{5}$. Then the lift of $x_{5}$ and $h$ is an isomorphism of $a$ and $b$.

HasFibers.Fib.mkdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

no wording

English

Assume that the action of $p$ and $a$ is equal to $S$. Then $\operatorname{mk}$ applied to $\mathrm{ha}$ is an element of $\operatorname{Fib}$ applied to $p$ and $S$ defined as the object preimage of the induced functor of $p$ and $S$ and $\operatorname{mk}$ applied to $\mathrm{ha}$.

HasFibers.Fib.mkIsoSelfdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the isomorphism self of ha (from the name)

English

Assume that the action of $p$ and $a$ is equal to $S$. Then the isomorphism self of $\mathrm{ha}$ is an isomorphism of the action of the inclusion of $S$ and $\operatorname{mk}$ applied to $\mathrm{ha}$ and $a$ defined as the map isomorphism of the fiber inclusion and the object object preimage isomorphism of the induced functor of $p$ and $S$ and $\operatorname{mk}$ applied to $\mathrm{ha}$.

HasFibers.inducedFunctordefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the induced functor of p and S (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $S$ be an element of $x$. Then the induced functor of $p$ and $S$ is a functor of $\operatorname{Fib}$ applied to $p$ and $S$ and the set of fibers of $p$ and $S$ defined as the induced functor of $\mathrm{HasFibers\_\_comp\_const}$ applied to $S$.

HasFibers.inducedFunctor.natIsodefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the natural transformation of p and S (from the docstring)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $S$ be an element of $x$. Then the natural transformation of $p$ and $S$ is an isomorphism of the inclusion of $S$ and the composition of the induced functor of $p$ and $S$ and the fiber inclusion defined as the induced functor composition isomorphism self of $\mathrm{HasFibers\_\_comp\_const}$ applied to $S$.

HasFibers.inducedMapdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the induced map of x5 and x6 (from the name)

English

Let $f$ be a homomorphism of $R$ and $S$. Let $x_{5}$ be a homomorphism of the action of the inclusion of $R$ and $\mathrm{b'}$ and $a$. Let $x_{6}$ be a homomorphism of the action of the inclusion of $R$ and $b$ and $a$. Then the induced map of $x_{5}$ and $x_{6}$ is a homomorphism of $b$ and $\mathrm{b'}$ defined as the homomorphism of the map of $x_{5}$ and $x_{6}$.

HasFibers.mkPullbackdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the pullback of f and ha (from the name)

English

Let $f$ be a homomorphism of $R$ and $S$. Assume that the action of $p$ and $a$ is equal to $S$. Then the pullback of $f$ and $\mathrm{ha}$ is an element of $\operatorname{Fib}$ applied to $p$ and $R$.

HasFibers.projMapdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the projection map of x5 (from the name)

English

Let $x_{5}$ be a homomorphism of the action of the inclusion of $R$ and $a$ and the action of the inclusion of $S$ and $b$. Then the projection map of $x_{5}$ is a homomorphism of $R$ and $S$.

HasFibers.pullbackMapdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the pullback map of f and ha (from the name)

English

Let $f$ be a homomorphism of $R$ and $S$. Assume that the action of $p$ and $a$ is equal to $S$. Then the pullback map of $f$ and $\mathrm{ha}$ is a homomorphism of the action of the inclusion of $R$ and the pullback of $f$ and $\mathrm{ha}$ and $a$.

HasFibers.ιdefMathlib.CategoryTheory.FiberedCategory.HasFibers, function or constant

Wording

the inclusion of S (from the name)

English

Let $S$ be an element of $x$. Then the inclusion of $S$ is a functor of $\operatorname{Fib}$ applied to $p$ and $S$ and $x_{1}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $S$.

Mathlib.CategoryTheory.FiberedCategory.HomLift

CategoryTheory.Functor.IsHomLiftclassMathlib.CategoryTheory.FiberedCategory.HomLift, predicate

Wording

no wording

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $x_{4}$ be a homomorphism of $R$ and $S$. Let $x_{5}$ be a homomorphism of $a$ and $b$. Then we can say that $\operatorname{IsHomLift}$ holds for $p$, $x_{4}$ and $x_{5}$.

CategoryTheory.IsHomLift.isoOfIsoLiftdefMathlib.CategoryTheory.FiberedCategory.HomLift, function or constant

Wording

the isomorphism of f and x4 (from the name)

English

Let $p$ be a functor of $x_{1}$ and $x$. Let $f$ be a homomorphism of $R$ and $S$. Let $x_{4}$ be an isomorphism of $a$ and $b$. Then the isomorphism of $f$ and $x_{4}$ is an isomorphism of $R$ and $S$.

CategoryTheory.tacticSubst_hom_lift___defMathlib.CategoryTheory.FiberedCategory.HomLift, function or constant

Wording

no wording

English

generation took over the time limit

Mathlib.CategoryTheory.Filtered.Basic

CategoryTheory.IsCofilteredclassMathlib.CategoryTheory.Filtered.Basic, predicate

Wording

C is cofiltered (from the name)

English

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

CategoryTheory.IsCofiltered.conedefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the cone of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the cone of $F$ is a cone of $F$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_IsCofiltered\_\_cone\_nonempty}$ applied to $F$.

CategoryTheory.IsCofiltered.eqdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $f$ and $\mathrm{f'}$ be homomorphisms of $j$ and $\mathrm{j'}$. Then $\operatorname{eq}$ applied to $f$ and $\mathrm{f'}$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsCofilteredOrEmpty\_\_cone\_maps}$ applied to $f$ and $\mathrm{f'}$.

CategoryTheory.IsCofiltered.eqHomdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $f$ and $\mathrm{f'}$ be homomorphisms of $j$ and $\mathrm{j'}$. Then $\operatorname{eqHom}$ applied to $f$ and $\mathrm{f'}$ is a homomorphism of $\operatorname{eq}$ applied to $f$ and $\mathrm{f'}$ and $j$.

CategoryTheory.IsCofiltered.infdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the infimum of O and H (from the name)

English

Let $O$ be a finite set of $C$. Let $H$ be a finite set of $\mathrm{PSigma}$ applied to the function that maps $X$ to $\mathrm{PSigma}$ applied to the function that maps $Y$ to $\mathrm{PSigma}$ applied to the function that maps $h_{1}$ to $\mathrm{PSigma}$ applied to the function that maps $h_{2}$ to the set of homomorphisms of $X$ and $Y$. Then the infimum of $O$ and $H$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsCofiltered\_\_inf\_exists}$ applied to $O$ and $H$.

CategoryTheory.IsCofiltered.infTodefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $O$ be a finite set of $C$. Let $H$ be a finite set of $\mathrm{PSigma}$ applied to the function that maps $X_{1}$ to $\mathrm{PSigma}$ applied to the function that maps $Y$ to $\mathrm{PSigma}$ applied to the function that maps $h_{1}$ to $\mathrm{PSigma}$ applied to the function that maps $h_{2}$ to the set of homomorphisms of $X_{1}$ and $Y$. Assume that $X$ is an element of $O$. Then $\operatorname{infTo}$ applied to $O$, $H$ and $m$ is a homomorphism of the infimum of $O$ and $H$ and $X$.

CategoryTheory.IsCofiltered.mindefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the minimum of j and #2 (from the name)

English

Let $j$ and $\mathrm{j'}$ be elements of $C$. Then the minimum of $j$ and $\mathrm{j'}$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsCofilteredOrEmpty\_\_cone\_objs}$ applied to $j$ and $\mathrm{j'}$.

CategoryTheory.IsCofiltered.minToLeftdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $j$ and $\mathrm{j'}$ be elements of $C$. Then $\operatorname{minToLeft}$ applied to $j$ and $\mathrm{j'}$ is a homomorphism of the minimum of $j$ and $\mathrm{j'}$ and $j$.

CategoryTheory.IsCofiltered.minToRightdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $j$ and $\mathrm{j'}$ be elements of $C$. Then $\operatorname{minToRight}$ applied to $j$ and $\mathrm{j'}$ is a homomorphism of the minimum of $j$ and $\mathrm{j'}$ and $\mathrm{j'}$.

CategoryTheory.IsCofilteredOrEmptyclassMathlib.CategoryTheory.Filtered.Basic, predicate

Wording

C is cofiltered or empty (from the name)

English

Let $C$ be a set. Then we can say that $C$ is cofiltered or empty.

CategoryTheory.IsFilteredclassMathlib.CategoryTheory.Filtered.Basic, predicate

Wording

C is filtered (from the name)

English

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

CategoryTheory.IsFiltered.coconedefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the cocone of F (from the name)

English

Let $F$ be a functor of $J$ and $C$. Then the cocone of $F$ is a cocone of $F$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_IsFiltered\_\_cocone\_nonempty}$ applied to $F$.

CategoryTheory.IsFiltered.coeqdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $f$ and $\mathrm{f'}$ be homomorphisms of $j$ and $\mathrm{j'}$. Then $\operatorname{coeq}$ applied to $f$ and $\mathrm{f'}$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsFilteredOrEmpty\_\_cocone\_maps}$ applied to $f$ and $\mathrm{f'}$.

CategoryTheory.IsFiltered.coeqHomdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $f$ and $\mathrm{f'}$ be homomorphisms of $j$ and $\mathrm{j'}$. Then $\operatorname{coeqHom}$ applied to $f$ and $\mathrm{f'}$ is a homomorphism of $\mathrm{j'}$ and $\operatorname{coeq}$ applied to $f$ and $\mathrm{f'}$.

CategoryTheory.IsFiltered.coeq₃defMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $f$, $g$ and $h_{1}$ be homomorphisms of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_IsFiltered\_\_coeq\_u2083\_}$ applied to $f$, $g$ and $h_{1}$ is an element of $C$ defined as $\operatorname{coeq}$ applied to the composition of $\operatorname{coeqHom}$ applied to $f$ and $g$ and the left to maximum of $\operatorname{coeq}$ applied to $f$ and $g$ and $\operatorname{coeq}$ applied to $g$ and $h_{1}$ and the composition of $\operatorname{coeqHom}$ applied to $g$ and $h_{1}$ and the right to maximum of $\operatorname{coeq}$ applied to $f$ and $g$ and $\operatorname{coeq}$ applied to $g$ and $h_{1}$.

CategoryTheory.IsFiltered.coeq₃HomdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $f$, $g$ and $h_{1}$ be homomorphisms of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_IsFiltered\_\_coeq\_u2083\_Hom}$ applied to $f$, $g$ and $h_{1}$ is a homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_IsFiltered\_\_coeq\_u2083\_}$ applied to $f$, $g$ and $h_{1}$ defined as the composition of $\operatorname{coeqHom}$ applied to $f$ and $g$ and the composition of the left to maximum of $\operatorname{coeq}$ applied to $f$ and $g$ and $\operatorname{coeq}$ applied to $g$ and $h_{1}$ and $\operatorname{coeqHom}$ applied to the composition of $\operatorname{coeqHom}$ applied to $f$ and $g$ and the left to maximum of $\operatorname{coeq}$ applied to $f$ and $g$ and $\operatorname{coeq}$ applied to $g$ and $h_{1}$ and the composition of $\operatorname{coeqHom}$ applied to $g$ and $h_{1}$ and the right to maximum of $\operatorname{coeq}$ applied to $f$ and $g$ and $\operatorname{coeq}$ applied to $g$ and $h_{1}$.

CategoryTheory.IsFiltered.firstToMax₃defMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_IsFiltered\_\_firstToMax\_u2083\_}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is a homomorphism of $x_{1}$ and the maximum of $x_{2}$ and $x_{3}$ defined as the composition of the left to maximum of $x_{1}$ and $x_{2}$ and the left to maximum of the maximum of $x_{1}$ and $x_{2}$ and $x_{3}$.

CategoryTheory.IsFiltered.leftToMaxdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the left to maximum of j and #2 (from the name)

English

Let $j$ and $\mathrm{j'}$ be elements of $C$. Then the left to maximum of $j$ and $\mathrm{j'}$ is a homomorphism of $j$ and the maximum of $j$ and $\mathrm{j'}$.

CategoryTheory.IsFiltered.maxdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the maximum of j and #2 (from the name)

English

Let $j$ and $\mathrm{j'}$ be elements of $C$. Then the maximum of $j$ and $\mathrm{j'}$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsFilteredOrEmpty\_\_cocone\_objs}$ applied to $j$ and $\mathrm{j'}$.

CategoryTheory.IsFiltered.max₃defMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the maximum of x2 and x3 (from the name)

English

Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $C$. Then the maximum of $x_{2}$ and $x_{3}$ is an element of $C$ defined as the maximum of the maximum of $x_{1}$ and $x_{2}$ and $x_{3}$.

CategoryTheory.IsFiltered.rightToMaxdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the right to maximum of j and #2 (from the name)

English

Let $j$ and $\mathrm{j'}$ be elements of $C$. Then the right to maximum of $j$ and $\mathrm{j'}$ is a homomorphism of $\mathrm{j'}$ and the maximum of $j$ and $\mathrm{j'}$.

CategoryTheory.IsFiltered.secondToMax₃defMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the second to maximum of x2 and x3 (from the name)

English

Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $C$. Then the second to maximum of $x_{2}$ and $x_{3}$ is a homomorphism of $x_{2}$ and the maximum of $x_{2}$ and $x_{3}$ defined as the composition of the right to maximum of $x_{1}$ and $x_{2}$ and the left to maximum of the maximum of $x_{1}$ and $x_{2}$ and $x_{3}$.

CategoryTheory.IsFiltered.supdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the supremum of O and H (from the name)

English

Let $O$ be a finite set of $C$. Let $H$ be a finite set of $\mathrm{PSigma}$ applied to the function that maps $X$ to $\mathrm{PSigma}$ applied to the function that maps $Y$ to $\mathrm{PSigma}$ applied to the function that maps $h_{1}$ to $\mathrm{PSigma}$ applied to the function that maps $h_{2}$ to the set of homomorphisms of $X$ and $Y$. Then the supremum of $O$ and $H$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsFiltered\_\_sup\_exists}$ applied to $O$ and $H$.

CategoryTheory.IsFiltered.thirdToMax₃defMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

no wording

English

Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_IsFiltered\_\_thirdToMax\_u2083\_}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is a homomorphism of $x_{3}$ and the maximum of $x_{2}$ and $x_{3}$ defined as the right to maximum of the maximum of $x_{1}$ and $x_{2}$ and $x_{3}$.

CategoryTheory.IsFiltered.toSupdefMathlib.CategoryTheory.Filtered.Basic, function or constant

Wording

the supremum of O and H (from the name)

English

Let $O$ be a finite set of $C$. Let $H$ be a finite set of $\mathrm{PSigma}$ applied to the function that maps $X_{1}$ to $\mathrm{PSigma}$ applied to the function that maps $Y$ to $\mathrm{PSigma}$ applied to the function that maps $h_{1}$ to $\mathrm{PSigma}$ applied to the function that maps $h_{2}$ to the set of homomorphisms of $X_{1}$ and $Y$. Assume that $X$ is an element of $O$. Then the supremum of $O$ and $H$ is a homomorphism of $X$ and the supremum of $O$ and $H$.

CategoryTheory.IsFilteredOrEmptyclassMathlib.CategoryTheory.Filtered.Basic, predicate

Wording

C is filtered or empty (from the name)

English

Let $C$ be a set. Then we can say that $C$ is filtered or empty.

Mathlib.CategoryTheory.Filtered.FinallySmall

CategoryTheory.FinallySmall.FilteredFinalModeldefMathlib.CategoryTheory.Filtered.FinallySmall, type

Wording

filtered final model of C (from the name)

English

Let $C$ be a set. Then a filtered final model of $C$ is an element of the function that maps $C$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_FinallySmall\_\_exists\_of\_isFiltered}$ applied to $C$.

CategoryTheory.FinallySmall.fromFilteredFinalModeldefMathlib.CategoryTheory.Filtered.FinallySmall, function or constant

Wording

no wording

English

Let $C$ be a set. Then $\operatorname{fromFilteredFinalModel}$ applied to $C$ is a functor of the set of filtered final models of $C$ and $C$.

CategoryTheory.InitiallySmall.CofilteredInitialModeldefMathlib.CategoryTheory.Filtered.FinallySmall, type

Wording

cofiltered initial model of C (from the name)

English

Let $C$ be a set. Then a cofiltered initial model of $C$ is an element of the function that maps $C$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_InitiallySmall\_\_exists\_of\_isCofiltered}$ applied to $C$.

CategoryTheory.InitiallySmall.fromCofilteredInitialModeldefMathlib.CategoryTheory.Filtered.FinallySmall, function or constant

Wording

no wording

English

Let $C$ be a set. Then $\operatorname{fromCofilteredInitialModel}$ applied to $C$ is a functor of the set of cofiltered initial models of $C$ and $C$.

Mathlib.CategoryTheory.Filtered.Small

CategoryTheory.IsCofiltered.SmallCofilteredIntermediatedefMathlib.CategoryTheory.Filtered.Small, type

Wording

no wording

English

Let $F$ be a functor of $D$ and $C$. Then an element of $\operatorname{SmallCofilteredIntermediate}$ applied to $F$ is an element of the function that maps $F$ to the set of small models of the set of full subcategories of the cofiltered closure of $\operatorname{obj}$ applied to $F$.

CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoringdefMathlib.CategoryTheory.Filtered.Small, function or constant

Wording

no wording

English

Let $F$ be a functor of $D$ and $C$. Then $\operatorname{factoring}$ applied to $F$ is a functor of $D$ and $\operatorname{SmallCofilteredIntermediate}$ applied to $F$.

CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoringCompInclusiondefMathlib.CategoryTheory.Filtered.Small, function or constant

Wording

no wording

English

Let $F$ be a functor of $D$ and $C$. Then $\operatorname{factoringCompInclusion}$ applied to $F$ is an isomorphism of the composition of $\operatorname{factoring}$ applied to $F$ and the inclusion of $F$ and $F$.

CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusiondefMathlib.CategoryTheory.Filtered.Small, function or constant

Wording

the inclusion of F (from the name)

English

Let $F$ be a functor of $D$ and $C$. Then the inclusion of $F$ is a functor of $\operatorname{SmallCofilteredIntermediate}$ applied to $F$ and $C$ defined as the composition of the inverse of the equivalence small model of the set of full subcategories of the cofiltered closure of $\operatorname{obj}$ applied to $F$ and the inclusion of the cofiltered closure of $\operatorname{obj}$ applied to $F$.

CategoryTheory.IsCofiltered.cofilteredClosureinductiveMathlib.CategoryTheory.Filtered.Small, function or constant

Wording

the cofiltered closure of f (from the name)

English

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

CategoryTheory.IsCofiltered.cofilteredClosure.belowinductiveMathlib.CategoryTheory.Filtered.Small, predicate

Wording

no wording

English

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

CategoryTheory.IsFiltered.SmallFilteredIntermediatedefMathlib.CategoryTheory.Filtered.Small, type

Wording

no wording

English

Let $F$ be a functor of $D$ and $C$. Then an element of $\operatorname{SmallFilteredIntermediate}$ applied to $F$ is an element of the function that maps $F$ to the set of small models of the set of full subcategories of the filtered closure of $\operatorname{obj}$ applied to $F$.

CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoringdefMathlib.CategoryTheory.Filtered.Small, function or constant

Wording

no wording

English

Let $F$ be a functor of $D$ and $C$. Then $\operatorname{factoring}$ applied to $F$ is a functor of $D$ and $\operatorname{SmallFilteredIntermediate}$ applied to $F$.

CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoringCompInclusiondefMathlib.CategoryTheory.Filtered.Small, function or constant

Wording

no wording

English

CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusiondefMathlib.CategoryTheory.Filtered.Small, function or constant

Wording

the inclusion of F (from the name)

English

Let $F$ be a functor of $D$ and $C$. Then the inclusion of $F$ is a functor of $\operatorname{SmallFilteredIntermediate}$ applied to $F$ and $C$ defined as the composition of the inverse of the equivalence small model of the set of full subcategories of the filtered closure of $\operatorname{obj}$ applied to $F$ and the inclusion of the filtered closure of $\operatorname{obj}$ applied to $F$.

CategoryTheory.IsFiltered.filteredClosureinductiveMathlib.CategoryTheory.Filtered.Small, function or constant

Wording

the filtered closure of f (from the name)

English

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

CategoryTheory.IsFiltered.filteredClosure.belowinductiveMathlib.CategoryTheory.Filtered.Small, predicate

Wording

no wording

English

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

Mathlib.CategoryTheory.Filtration.Basic

CategoryTheory.FilteredObjectstructureMathlib.CategoryTheory.Filtration.Basic, type

Wording

filtered object of C and I (from the name)

English

Let $C$ and $I$ be sets. Then the filtered objects of $C$ and $I$ are a basic type.

CategoryTheory.FilteredObject.HomstructureMathlib.CategoryTheory.Filtration.Basic, type

Wording

homomorphism of F and G (from the name)

English

Let $F$ and $G$ be filtered objects of $C$ and $I$. Then the homomorphisms of $F$ and $G$ are a basic type.

CategoryTheory.FilteredObject.Hom.homdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $F$ and $G$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $\operatorname{X}$ applied to $F$ and $\operatorname{X}$ applied to $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.FilteredObject.Hom.natTransdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the natural transformation of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $F$ and $G$. Then the natural transformation of $\mathrm{self}$ is a homomorphism of the underlying diagram in the filtration of $F$ and the underlying diagram in the filtration of $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.FilteredObject.IsStrictHomclassMathlib.CategoryTheory.Filtration.Basic, predicate

Wording

f is a strict homomorphism (from the name)

English

Let $f$ be a homomorphism of $F$ and $G$. Then we can say that $f$ is a strict homomorphism.

CategoryTheory.FilteredObject.XdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a filtered object of $C$ and $I$. Then $\operatorname{X}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.FilteredObject.filtrationdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the filtration of self (from the name)

English

Let $\mathrm{self}$ be a filtered object of $C$ and $I$. Then the filtration of $\mathrm{self}$ is a filtration of $\operatorname{X}$ applied to $\mathrm{self}$ and $I$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.FilteredObject.filtrationDiagramdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the filtration diagram in F (from the docstring)

English

Let $F$ be a filtered object of $C$ and $I$. Then the filtration diagram in $F$ is a functor of $I$ and $C$ defined as the underlying diagram in the filtration of $F$.

CategoryTheory.FilteredObject.forgetdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the forgetful functor (from the docstring)

English

The forgetful functor is a functor of the set of filtered objects of $C$ and $I$ and $C$.

CategoryTheory.FilteredObject.homMkdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the homomorphism of hom and app (from the name)

English

Let $\mathrm{hom}$ be a homomorphism of $\operatorname{X}$ applied to $F$ and $\operatorname{X}$ applied to $G$. Let $\mathrm{app}$ be a function from elements $i_{1}$ of $I$ to homomorphisms of the object of the filtration of $F$ and $i_{1}$ and the object of the filtration of $G$ and $i_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $I$, the composition of $\mathrm{app}$ applied to $i$ and the component of the inclusion of the filtration of $G$ and $i$ is equal to the composition of the component of the inclusion of the filtration of $F$ and $i$ and $\mathrm{hom}$ and $\mathrm{CategoryTheory\_\_FilteredObject\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $\mathrm{hom}$ and $i_{1}$ is a homomorphism of $F$ and $G$.

CategoryTheory.FilteredObject.isStrictHomdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

no wording

English

Let $C$ and $I$ be sets. Then there is a morphism property of the set of filtered objects of $C$ and $I$. Proof. Let $C$ be arbitrary. Let $I$ be arbitrary. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__FilteredObject__IsStrictHom.

CategoryTheory.FilteredObject.isoMkdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the isomorphism of iso and app (from the name)

English

Let $\mathrm{iso}$ be an isomorphism of $\operatorname{X}$ applied to $F$ and $\operatorname{X}$ applied to $G$. Let $\mathrm{app}$ be a function from elements $i_{1}$ of $I$ to isomorphisms of the object of the filtration of $F$ and $i_{1}$ and the object of the filtration of $G$ and $i_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $I$, the composition of the homomorphism of $\mathrm{app}$ applied to $i$ and the component of the inclusion of the filtration of $G$ and $i$ is equal to the composition of the component of the inclusion of the filtration of $F$ and $i$ and the homomorphism of $\mathrm{iso}$ and $\mathrm{CategoryTheory\_\_FilteredObject\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $\mathrm{iso}$ and $i_{1}$ is an isomorphism of $F$ and $G$.

CategoryTheory.FiltrationstructureMathlib.CategoryTheory.Filtration.Basic, type

Wording

filtration of X and I (from the name)

English

Let $X$ be an element of $C$. Let $I$ be a set. Then the filtrations of $X$ and $I$ are a basic type.

CategoryTheory.Filtration.diagramdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the underlying diagram in F (from the docstring)

English

Let $F$ be a filtration of $X$ and $I$. Then the underlying diagram in $F$ is a functor of $I$ and $C$ defined as the composition of $\operatorname{toMonoOver}$ applied to $F$ and the composition of $\operatorname{forget}$ applied to $X$ and $\operatorname{forget}$ applied to $X$.

CategoryTheory.Filtration.objdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the object of F and i (from the name)

English

Let $F$ be a filtration of $X$ and $I$. Let $i$ be an element of $I$. Then the object of $F$ and $i$ is an element of $C$ defined as the action of the underlying diagram in $F$ and $i$.

CategoryTheory.Filtration.toMonoOverdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a filtration of $X$ and $I$. Then $\operatorname{toMonoOver}$ applied to $\mathrm{self}$ is a functor of $I$ and $\operatorname{MonoOver}$ applied to $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Filtration.ιdefMathlib.CategoryTheory.Filtration.Basic, function or constant

Wording

the inclusion of F (from the name)

English

Let $F$ be a filtration of $X$ and $I$. Then the inclusion of $F$ is a homomorphism of the underlying diagram in $F$ and the action of the constant of $I$ and $X$.

Mathlib.CategoryTheory.FinCategory.AsType

CategoryTheory.FinCategory.AsTypedefMathlib.CategoryTheory.FinCategory.AsType, type

Wording

no wording

English

Let $x$ be a set. Then an element of $\operatorname{AsType}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{Fin}$ applied to the cardinality of $x$.

CategoryTheory.FinCategory.ObjAsTypedefMathlib.CategoryTheory.FinCategory.AsType, type

Wording

object as type of x (from the name)

English

Let $x$ be a set. Then an object as type of $x$ is an element of the function that maps $x$ to the set of induced categories of $x$ and $\operatorname{coe}$ applied to the inverse of $\operatorname{equivFin}$ applied to $x$.

CategoryTheory.FinCategory.asTypeEquivObjAsTypedefMathlib.CategoryTheory.FinCategory.AsType, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{asTypeEquivObjAsType}$ applied to $x$ is an equivalence of $\operatorname{AsType}$ applied to $x$ and the set of objects as type of $x$.

CategoryTheory.FinCategory.asTypeToObjAsTypedefMathlib.CategoryTheory.FinCategory.AsType, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{asTypeToObjAsType}$ applied to $x$ is a functor of $\operatorname{AsType}$ applied to $x$ and the set of objects as type of $x$.

CategoryTheory.FinCategory.equivAsTypedefMathlib.CategoryTheory.FinCategory.AsType, function or constant

Wording

the equivalence as type of x (from the name)

English

Let $x$ be a set. Then the equivalence as type of $x$ is an equivalence of $\operatorname{AsType}$ applied to $x$ and $x$ defined as the composition of $\operatorname{asTypeEquivObjAsType}$ applied to $x$ and the object as type equivalence of $x$.

CategoryTheory.FinCategory.objAsTypeEquivdefMathlib.CategoryTheory.FinCategory.AsType, function or constant

Wording

the object as type equivalence of x (from the name)

English

Let $x$ be a set. Then the object as type equivalence of $x$ is an equivalence of the set of objects as type of $x$ and $x$ defined as $\operatorname{asEquivalence}$ applied to the induced functor of $\operatorname{coe}$ applied to the inverse of $\operatorname{equivFin}$ applied to $x$.

CategoryTheory.FinCategory.objAsTypeToAsTypedefMathlib.CategoryTheory.FinCategory.AsType, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{objAsTypeToAsType}$ applied to $x$ is a functor of the set of objects as type of $x$ and $\operatorname{AsType}$ applied to $x$.

Mathlib.CategoryTheory.FinCategory.Basic

CategoryTheory.FinCategoryclassMathlib.CategoryTheory.FinCategory.Basic, predicate

Wording

J is a finite category (from the name)

English

Let $J$ be a set. Then we can say that $J$ is a finite category.

Mathlib.CategoryTheory.FintypeCat

FintypeCatdefMathlib.CategoryTheory.FintypeCat, type

Wording

finite type category (from the name)

English

A finite type category is a full subcategory of the proposition that $\mathrm{Finite}$.

FintypeCat.SkeletondefMathlib.CategoryTheory.FintypeCat, type

Wording

skeleton (from the name)

English

A skeleton is an element of $\mathrm{ULift}$ applied to $\Natural$.

FintypeCat.Skeleton.equivalencedefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an equivalence of the set of skeletons and the set of finite type categories defined as $\operatorname{asEquivalence}$ applied to the inclusion.

FintypeCat.Skeleton.incldefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

the inclusion (from the name)

English

The inclusion is a functor of the set of skeletons and the set of finite type categories.

FintypeCat.Skeleton.lendefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

no wording

English

Let $x$ be a skeleton. Then $\operatorname{len}$ applied to $x$ is a natural number defined as $\operatorname{down}$ applied to $x$.

FintypeCat.Skeleton.mkdefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\operatorname{mk}$ applied to $x$ is a skeleton defined as $\operatorname{up}$ applied to $x$.

FintypeCat.equivEquivIsodefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

the equivalence equivalence isomorphism (from the name)

English

The equivalence equivalence isomorphism is an equivalence from the set of equivalences from the object of $A$ to the object of $B$ to the set of isomorphisms of $A$ and $B$.

FintypeCat.homMkdefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

the homomorphism of f (from the name)

English

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

FintypeCat.incldefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

the inclusion (from the name)

English

The inclusion is a functor of the set of finite type categories and the set of sets defined as the inclusion of the proposition that $\mathrm{Finite}$.

FintypeCat.ofdefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is a finite type category.

FintypeCat.uSwitchdefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

the switch (from the name)

English

The switch is a functor of the set of finite type categories and the set of finite type categories.

FintypeCat.uSwitchEquivdefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

the switch equivalence of X (from the name)

English

Let $X$ be a finite type category. Then the switch equivalence of $X$ is an equivalence from the object of the action of the switch and $X$ to the object of $X$ defined as the composition of the lift and the inverse of $\operatorname{equivFin}$ applied to the object of $X$.

FintypeCat.uSwitchEquivalencedefMathlib.CategoryTheory.FintypeCat, function or constant

Wording

the switch equivalence (from the name)

English

The switch equivalence is an equivalence of the set of finite type categories and the set of finite type categories.

Mathlib.CategoryTheory.Functor.Basic

CategoryTheory.FunctorstructureMathlib.CategoryTheory.Functor.Basic, type

Wording

functor of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the functors of $C$ and $D$ are a basic type.

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

Wording

the 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 composition of $F$ and $G$ is a functor of $C$ and $E$.

CategoryTheory.Functor.iddefMathlib.CategoryTheory.Functor.Basic, function or constant

Wording

the identity of C (from the name)

English

Let $C$ be a set. Then the identity of $C$ is a functor of $C$ and $C$.

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

Wording

the map of self and x2 (from the name)

English

Let $\mathrm{self}$ be a functor of $C$ and $D$. Let $x_{2}$ be a homomorphism of $X$ and $Y$. Then the map of $\mathrm{self}$ and $x_{2}$ is a homomorphism of the action of $\mathrm{self}$ and $X$ and the action of $\mathrm{self}$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

CategoryTheory.Functor.objdefMathlib.CategoryTheory.Functor.Basic, function or constant

Wording

the action of self and x2 (from the docstring)

English

Let $\mathrm{self}$ be a functor of $C$ and $D$. Let $x_{2}$ be an element of $C$. Then the action of $\mathrm{self}$ and $x_{2}$ is an element of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

CategoryTheory.Functor.toPrefunctordefMathlib.CategoryTheory.Functor.Basic, function or constant

Wording

the prefunctor between the underlying quivers of F (from the docstring)

English

Let $F$ be a functor of $C$ and $D$. Then the prefunctor between the underlying quivers of $F$ is a prefunctor of $C$ and $D$ defined as $\operatorname{mk}$ applied to $\operatorname{obj}$ applied to $F$ and $\operatorname{map}$ applied to $F$.

Mathlib.CategoryTheory.Functor.Category

CategoryTheory.Functor.associatordefMathlib.CategoryTheory.Functor.Category, function or constant

Wording

the associator of G and H (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Let $H$ be a functor of $E$ and $\mathrm{E'}$. Then the associator of $G$ and $H$ is an isomorphism of the composition of the composition of $F$ and $G$ and $H$ and the composition of $F$ and the composition of $G$ and $H$.

CategoryTheory.Functor.flipdefMathlib.CategoryTheory.Functor.Category, function or constant

Wording

the flip of F (from the name)

English

Let $F$ be a functor of $C$ and the set of functors of $D$ and $E$. Then the flip of $F$ is a functor of $D$ and the set of functors of $C$ and $E$.

CategoryTheory.Functor.leftUnitordefMathlib.CategoryTheory.Functor.Category, function or constant

Wording

the left unitor of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the left unitor of $F$ is an isomorphism of the composition of the identity of $C$ and $F$ and $F$.

CategoryTheory.Functor.rightUnitordefMathlib.CategoryTheory.Functor.Category, function or constant

Wording

the right unitor of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the right unitor of $F$ is an isomorphism of the composition of $F$ and the identity of $D$ and $F$.

CategoryTheory.NatTrans.flipAppdefMathlib.CategoryTheory.Functor.Category, function or constant

Wording

the flip application of x3 and Y (from the name)

English

Let $x_{3}$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $Y$ be an element of $D$. Then the flip application of $x_{3}$ and $Y$ is a homomorphism of the action of the flip of $G$ and $Y$ and the action of the flip of $\mathrm{G'}$ and $Y$ defined as the component of the map of the flip functor of $D$ and $E$ and $x_{3}$ and $Y$.

CategoryTheory.NatTrans.hcompdefMathlib.CategoryTheory.Functor.Category, function or constant

Wording

no wording

English

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

CategoryTheory.flipFunctordefMathlib.CategoryTheory.Functor.Category, function or constant

Wording

the flip functor of D and E (from the name)

English

Let $C$, $D$ and $E$ be sets. Then the flip functor of $D$ and $E$ is a functor of the set of functors of $C$ and the set of functors of $D$ and $E$ and the set of functors of $D$ and the set of functors of $C$ and $E$.

Mathlib.CategoryTheory.Functor.Const

CategoryTheory.Functor.compConstIsodefMathlib.CategoryTheory.Functor.Const, function or constant

Wording

the canonical isomorphism of J and F (from the docstring)

English

Let $J$ be a set. Let $F$ be a functor of $C$ and $D$. Then the canonical isomorphism of $J$ and $F$ is an isomorphism of the composition of $F$ and the constant of $J$ and the composition of the constant of $J$ and the action of the right whiskering of $C$ and $D$ and $F$.

CategoryTheory.Functor.constdefMathlib.CategoryTheory.Functor.Const, function or constant

Wording

the constant of J (from the name)

English

Let $J$ be a set. Then the constant of $J$ is a functor of $C$ and the set of functors of $J$ and $C$.

CategoryTheory.Functor.const.opObjOpdefMathlib.CategoryTheory.Functor.Const, function or constant

Wording

the opposite object opposite of X (from the name)

English

Let $X$ be an element of $C$. Then the opposite object opposite of $X$ is an isomorphism of the action of the constant of the set of opposites of $J$ and $\operatorname{op}$ applied to $X$ and the opposite of the action of the constant of $J$ and $X$.

CategoryTheory.Functor.const.opObjUnopdefMathlib.CategoryTheory.Functor.Const, function or constant

Wording

the opposite object opposite of X (from the name)

English

Let $X$ be an opposite of $C$. Then the opposite object opposite of $X$ is an isomorphism of the action of the constant of the set of opposites of $J$ and the opposite of $X$ and the left opposite of the action of the constant of $J$ and $X$.

CategoryTheory.Functor.constCompdefMathlib.CategoryTheory.Functor.Const, function or constant

Wording

the constant composition of X and F (from the name)

English

Let $J$ be a set. Let $X$ be an element of $C$. Let $F$ be a functor of $C$ and $D$. Then the constant composition of $X$ and $F$ is an isomorphism of the composition of the action of the constant of $J$ and $X$ and $F$ and the action of the constant of $J$ and the action of $F$ and $X$.

CategoryTheory.Functor.constCompWhiskeringLeftIsodefMathlib.CategoryTheory.Functor.Const, function or constant

Wording

the canonical isomorphism of J and F (from the docstring)

English

Let $J$ be a set. Let $F$ be a functor of $J$ and $D$. Then the canonical isomorphism of $J$ and $F$ is an isomorphism of the composition of the constant of $D$ and the action of the left whiskering of $D$ and $C$ and $F$ and the constant of $J$.

Mathlib.CategoryTheory.Functor.Currying

CategoryTheory.Functor.compFlipUncurryIsodefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the composition flip uncurrying isomorphism of F and G (from the name)

English

Let $F$ be a functor of $B$ and $D$. Let $G$ be a functor of $D$ and the set of functors of $C$ and $E$. Then the composition flip uncurrying isomorphism of $F$ and $G$ is an isomorphism of the action of $\operatorname{uncurry}$ and the flip of the composition of $F$ and $G$ and the composition of the product of the identity of $C$ and $F$ and the action of $\operatorname{uncurry}$ and the flip of $G$ defined as the identity of the action of $\operatorname{uncurry}$ and the flip of the composition of $F$ and $G$.

CategoryTheory.Functor.currydefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the curry (from the name)

English

The curry is a functor of the set of functors of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$ and the set of functors of $C$ and the set of functors of $D$ and $E$.

CategoryTheory.Functor.curryObjdefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the object level part of the currying functor of F (from the docstring)

English

Let $F$ be a functor of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$. Then the object level part of the currying functor of $F$ is a functor of $C$ and the set of functors of $D$ and $E$.

CategoryTheory.Functor.curryObjCompIsodefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the curry object composition isomorphism of F and G (from the name)

English

Let $F$ be a functor of $\mathrm{Prod}$ applied to $C$ and $B$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the curry object composition isomorphism of $F$ and $G$ is an isomorphism of the flip of the action of the curry and the composition of $F$ and $G$ and the composition of the flip of the action of the curry and $F$ and the action of the right whiskering of $D$ and $E$ and $G$ defined as the identity of the flip of the action of the curry and the composition of $F$ and $G$.

CategoryTheory.Functor.curryObjProdCompdefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the curry object product composition of x6 and G (from the name)

English

Let $x_{5}$ be a functor of $C$ and $D$. Let $x_{6}$ be a functor of $\mathrm{C'}$ and $\mathrm{D'}$. Let $G$ be a functor of $\mathrm{Prod}$ applied to $D$ and $\mathrm{D'}$ and $E$. Then the curry object product composition of $x_{6}$ and $G$ is an isomorphism of the action of the curry and the composition of the product of $x_{5}$ and $x_{6}$ and $G$ and the composition of $x_{5}$ and the composition of the action of the curry and $G$ and the action of the left whiskering of $\mathrm{D'}$ and $E$ and $x_{6}$.

CategoryTheory.Functor.curryingdefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the currying (from the name)

English

The currying is an equivalence of the set of functors of $C$ and the set of functors of $D$ and $E$ and the set of functors of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$.

CategoryTheory.Functor.curryingEquivdefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the currying equivalence (from the name)

English

The currying equivalence is an equivalence from the set of functors of $C$ and the set of functors of $D$ and $E$ to the set of functors of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$ defined as $\operatorname{mk}$ applied to the function that maps $F$ to the action of $\operatorname{uncurry}$ and $F$, the function that maps $G$ to the action of the curry and $G$, $\mathrm{CategoryTheory\_\_Functor\_\_curry\_obj\_uncurry\_obj}$ and $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_obj\_curry\_obj}$.

CategoryTheory.Functor.curryingFlipEquivdefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the currying flip equivalence (from the name)

English

The currying flip equivalence is an equivalence from the set of functors of $D$ and the set of functors of $C$ and $E$ to the set of functors of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$ defined as the composition of $\operatorname{flippingEquiv}$ and the currying equivalence.

CategoryTheory.Functor.flipIsoCurrySwapUncurrydefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and the set of functors of $D$ and $E$. Then $\operatorname{flipIsoCurrySwapUncurry}$ applied to $F$ is an isomorphism of the flip of $F$ and the action of the curry and the composition of the swap of $D$ and $C$ and the action of $\operatorname{uncurry}$ and $F$.

CategoryTheory.Functor.flippingdefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

no wording

English

$\operatorname{flipping}$ is an equivalence of the set of functors of $C$ and the set of functors of $D$ and $E$ and the set of functors of $D$ and the set of functors of $C$ and $E$.

CategoryTheory.Functor.flippingEquivdefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

no wording

English

$\operatorname{flippingEquiv}$ is an equivalence from the set of functors of $C$ and the set of functors of $D$ and $E$ to the set of functors of $D$ and the set of functors of $C$ and $E$.

CategoryTheory.Functor.fullyFaithfulCurrydefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the fully faithful curry (from the name)

English

generation took over the time limit

CategoryTheory.Functor.fullyFaithfulUncurrydefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

no wording

English

$\operatorname{fullyFaithfulUncurry}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{uncurry}$ defined as the functor of the currying.

CategoryTheory.Functor.uncurrydefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

no wording

English

$\operatorname{uncurry}$ is a functor of the set of functors of $C$ and the set of functors of $D$ and $E$ and the set of functors of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$.

CategoryTheory.Functor.uncurryObjFlipdefMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the uncurrying object flip of F (from the name)

English

Let $F$ be a functor of $C$ and the set of functors of $D$ and $E$. Then the uncurrying object flip of $F$ is an isomorphism of the action of $\operatorname{uncurry}$ and the flip of $F$ and the composition of the swap of $D$ and $C$ and the action of $\operatorname{uncurry}$ and $F$.

CategoryTheory.Functor.whiskeringRight₂defMathlib.CategoryTheory.Functor.Currying, function or constant

Wording

the right whiskering of D and E (from the name)

English

Let $B$, $C$, $D$ and $E$ be sets. Then the right whiskering of $D$ and $E$ is a functor of the set of functors of $C$ and the set of functors of $D$ and $E$ and the set of functors of the set of functors of $B$ and $C$ and the set of functors of the set of functors of $B$ and $D$ and the set of functors of $B$ and $E$ defined as the composition of $\operatorname{uncurry}$ and the composition of the right whiskering of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$ and the composition of the action of the left whiskering of the set of functors of $B$ and $\mathrm{Prod}$ applied to $C$ and $D$ and the set of functors of $B$ and $E$ and the product functor to functor product of $C$ and $D$ and the curry.

Mathlib.CategoryTheory.Functor.CurryingFour

CategoryTheory.Functor.currying₄defMathlib.CategoryTheory.Functor.CurryingFour, function or constant

Wording

the currying (from the name)

English

The currying is an equivalence of the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$ and the set of functors of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$ and $E$ defined as the composition of the currying and the composition of the currying and the composition of the currying and the left congruence of the composition of the associativity of $x_{2}$ and $x_{3}$ and the associativity of $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.

CategoryTheory.Functor.curry₄defMathlib.CategoryTheory.Functor.CurryingFour, function or constant

Wording

the curry (from the name)

English

The curry is a functor of the set of functors of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$ and $E$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$ defined as the inverse of the currying.

CategoryTheory.Functor.curry₄ObjProdCompdefMathlib.CategoryTheory.Functor.CurryingFour, function or constant

Wording

the curry object product composition of x20 and G (from the name)

English

Let $x_{17}$ be a functor of $x$ and $x_{4}$. Let $x_{18}$ be a functor of $x_{1}$ and $x_{5}$. Let $x_{19}$ be a functor of $x_{2}$ and $x_{6}$. Let $x_{20}$ be a functor of $x_{3}$ and $x_{7}$. Let $G$ be a functor of $\mathrm{Prod}$ applied to $x_{4}$ and $\mathrm{Prod}$ applied to $x_{5}$ and $\mathrm{Prod}$ applied to $x_{6}$ and $x_{7}$ and $E$. Then the curry object product composition of $x_{20}$ and $G$ is an isomorphism of the action of the curry and the composition of the product of $x_{17}$ and the product of $x_{18}$ and the product of $x_{19}$ and $x_{20}$ and $G$ and the composition of $x_{17}$ and the composition of the action of the curry and $G$ and the action of the action of the action of the left whiskering of $E$ and $x_{18}$ and $x_{19}$ and $x_{20}$.

CategoryTheory.Functor.fullyFaithfulCurry₄defMathlib.CategoryTheory.Functor.CurryingFour, function or constant

Wording

the fully faithful curry (from the name)

English

generation took over the time limit

CategoryTheory.Functor.fullyFaithfulUncurry₄defMathlib.CategoryTheory.Functor.CurryingFour, function or constant

Wording

no wording

English

$\mathrm{CategoryTheory\_\_Functor\_\_fullyFaithfulUncurry\_u2084\_}$ is an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2084\_}$ defined as the functor of the currying.

CategoryTheory.Functor.uncurry₄defMathlib.CategoryTheory.Functor.CurryingFour, function or constant

Wording

no wording

English

$\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2084\_}$ is a functor of the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$ and the set of functors of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$ and $E$ defined as the functor of the currying.

Mathlib.CategoryTheory.Functor.CurryingThree

CategoryTheory.Functor.bifunctorComp₁₂IsodefMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the bifunctor composition isomorphism of x9 and G (from the name)

English

Let $x_{9}$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $G$ be a functor of $x_{2}$ and the set of functors of $x_{3}$ and $E$. Then the bifunctor composition isomorphism of $x_{9}$ and $G$ is an isomorphism of the bifunctor composition of $x_{9}$ and $G$ and the action of the curry and the composition of the action of $\operatorname{uncurry}$ and $x_{9}$ and $G$.

CategoryTheory.Functor.bifunctorComp₂₃IsodefMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the bifunctor composition isomorphism of F and x9 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{3}$ and $E$. Let $x_{9}$ be a functor of $x_{1}$ and the set of functors of $x_{2}$ and $x_{3}$. Then the bifunctor composition isomorphism of $F$ and $x_{9}$ is an isomorphism of the bifunctor composition of $F$ and $x_{9}$ and the action of the curry and the action of the curry and the composition of the associator of $x_{1}$ and $x_{2}$ and the action of $\operatorname{uncurry}$ and the flip of the composition of the action of $\operatorname{uncurry}$ and $x_{9}$ and the flip of $F$.

CategoryTheory.Functor.currying₃defMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the currying (from the name)

English

The currying is an equivalence of the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$ and the set of functors of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $E$ defined as the composition of the currying and the composition of the currying and the left congruence of the associativity of $x_{1}$ and $x_{2}$.

CategoryTheory.Functor.curry₃defMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the curry (from the name)

English

The curry is a functor of the set of functors of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $E$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$ defined as the inverse of the currying.

CategoryTheory.Functor.curry₃ObjProdCompdefMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the curry object product composition of x15 and G (from the name)

English

Let $x_{13}$ be a functor of $x$ and $x_{3}$. Let $x_{14}$ be a functor of $x_{1}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{2}$ and $x_{5}$. Let $G$ be a functor of $\mathrm{Prod}$ applied to $x_{3}$ and $\mathrm{Prod}$ applied to $x_{4}$ and $x_{5}$ and $E$. Then the curry object product composition of $x_{15}$ and $G$ is an isomorphism of the action of the curry and the composition of the product of $x_{13}$ and the product of $x_{14}$ and $x_{15}$ and $G$ and the composition of $x_{13}$ and the composition of the action of the curry and $G$ and the action of the action of the left whiskering of $E$ and $x_{14}$ and $x_{15}$.

CategoryTheory.Functor.flip₁₃defMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the flip of F (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$. Then the flip of $F$ is a functor of $x_{2}$ and the set of functors of $x_{1}$ and the set of functors of $x$ and $E$.

CategoryTheory.Functor.flip₁₃FunctordefMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the flip functor (from the name)

English

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

CategoryTheory.Functor.flip₂₃defMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the flip of F (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$. Then the flip of $F$ is a functor of $x$ and the set of functors of $x_{2}$ and the set of functors of $x_{1}$ and $E$.

CategoryTheory.Functor.flip₂₃FunctordefMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the flip functor (from the name)

English

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

CategoryTheory.Functor.fullyFaithfulCurry₃defMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

the fully faithful curry (from the name)

English

generation took over the time limit

CategoryTheory.Functor.fullyFaithfulUncurry₃defMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

no wording

English

$\mathrm{CategoryTheory\_\_Functor\_\_fullyFaithfulUncurry\_u2083\_}$ is an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2083\_}$ defined as the functor of the currying.

CategoryTheory.Functor.uncurry₃defMathlib.CategoryTheory.Functor.CurryingThree, function or constant

Wording

no wording

English

$\mathrm{CategoryTheory\_\_Functor\_\_uncurry\_u2083\_}$ is a functor of the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$ and the set of functors of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $E$ defined as the functor of the currying.

Mathlib.CategoryTheory.Functor.Derived.Adjunction

CategoryTheory.Adjunction.deriveddefMathlib.CategoryTheory.Functor.Derived.Adjunction, function or constant

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $G$ and $F$. Let $x_{10}$ be a morphism property of $x$. Let $x_{11}$ be a morphism property of $x_{1}$. Let $x_{12}$ be a homomorphism of the composition of $x_{8}$ and $\mathrm{G'}$ and the composition of $G$ and $x_{9}$. Let $x_{13}$ be a homomorphism of the composition of $F$ and $x_{8}$ and the composition of $x_{9}$ and $\mathrm{F'}$. Then $\operatorname{derived}$ applied to $\mathrm{adj}$, $x_{10}$, $x_{11}$, $x_{12}$ and $x_{13}$ is an adjunction of $\mathrm{G'}$ and $\mathrm{F'}$.

CategoryTheory.Adjunction.derivedεdefMathlib.CategoryTheory.Functor.Derived.Adjunction, function or constant

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $G$ and $F$. Let $x_{10}$ be a morphism property of $x_{1}$. Let $x_{11}$ be a homomorphism of the composition of $x_{8}$ and $\mathrm{G'}$ and the composition of $G$ and $x_{9}$. Let $x_{12}$ be a homomorphism of the composition of $F$ and $x_{8}$ and the composition of $x_{9}$ and $\mathrm{F'}$. Then $\mathrm{CategoryTheory\_\_Adjunction\_\_derived\_u3b5\_}$ applied to $\mathrm{adj}$, $x_{10}$, $x_{11}$ and $x_{12}$ is a homomorphism of the composition of $\mathrm{F'}$ and $\mathrm{G'}$ and the identity of $x_{3}$ defined as $\operatorname{rightDerivedDesc}$ applied to the composition of $\mathrm{F'}$ and $\mathrm{G'}$, the composition of the right whisker of $x_{12}$ and $\mathrm{G'}$ and the homomorphism of the associator of $\mathrm{F'}$ and $\mathrm{G'}$, $x_{10}$, the identity of $x_{3}$ and the composition of the homomorphism of the associator of $x_{8}$ and $\mathrm{G'}$ and the composition of the left whisker of $F$ and $x_{11}$ and the composition of the inverse of the associator of $G$ and $x_{9}$ and the composition of the right whisker of the counit of $\mathrm{adj}$ and $x_{9}$ and the composition of the homomorphism of the left unitor of $x_{9}$ and the inverse of the right unitor of $x_{9}$.

CategoryTheory.Adjunction.derivedηdefMathlib.CategoryTheory.Functor.Derived.Adjunction, function or constant

Wording

no wording

English

Let $\mathrm{adj}$ be an adjunction of $G$ and $F$. Let $x_{10}$ be a morphism property of $x$. Let $x_{11}$ be a homomorphism of the composition of $x_{8}$ and $\mathrm{G'}$ and the composition of $G$ and $x_{9}$. Let $x_{12}$ be a homomorphism of the composition of $F$ and $x_{8}$ and the composition of $x_{9}$ and $\mathrm{F'}$. Then $\mathrm{CategoryTheory\_\_Adjunction\_\_derived\_u3b7\_}$ applied to $\mathrm{adj}$, $x_{10}$, $x_{11}$ and $x_{12}$ is a homomorphism of the identity of $x_{2}$ and the composition of $\mathrm{G'}$ and $\mathrm{F'}$ defined as the left derived lift of the identity of $x_{2}$ and the composition of the homomorphism of the right unitor of $x_{8}$ and the composition of the inverse of the left unitor of $x_{8}$ and the composition of the right whisker of the unit of $\mathrm{adj}$ and $x_{8}$ and the composition of the homomorphism of the associator of $F$ and $x_{8}$ and the composition of the left whisker of $G$ and $x_{12}$ and the inverse of the associator of $x_{9}$ and $\mathrm{F'}$.

Mathlib.CategoryTheory.Functor.Derived.LeftDerived

CategoryTheory.Functor.HasLeftDerivedFunctorclassMathlib.CategoryTheory.Functor.Derived.LeftDerived, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $H$. Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{HasLeftDerivedFunctor}$ holds for $F$ and $W$.

CategoryTheory.Functor.IsLeftDerivedFunctorclassMathlib.CategoryTheory.Functor.Derived.LeftDerived, predicate

Wording

no wording

English

Let $\mathrm{LF}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{LF}$ and $F$. Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{IsLeftDerivedFunctor}$ holds for $\mathrm{LF}$, $x_{3}$ and $W$.

CategoryTheory.Functor.leftDerivedLiftdefMathlib.CategoryTheory.Functor.Derived.LeftDerived, function or constant

Wording

the left derived lift of G and x4 (from the name)

English

Let $\mathrm{LF}$ and $G$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{LF}$ and $F$. Let $W$ be a morphism property of $C$. Let $x_{4}$ be a homomorphism of the composition of $L$ and $G$ and $F$. Then the left derived lift of $G$ and $x_{4}$ is a homomorphism of $G$ and $\mathrm{LF}$ defined as the lift of $G$ and $x_{4}$.

CategoryTheory.Functor.leftDerivedNatIsodefMathlib.CategoryTheory.Functor.Derived.LeftDerived, function or constant

Wording

the left derived natural isomorphism of x5 and #6 (from the name)

English

Let $\mathrm{LF'}$ and $\mathrm{LF}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{LF'}$ and $\mathrm{F'}$. Let $x_{4}$ be a homomorphism of the composition of $L$ and $\mathrm{LF}$ and $F$. Let $W$ be a morphism property of $C$. Let $x_{5}$ be an isomorphism of $\mathrm{F'}$ and $F$. Then the left derived natural isomorphism of $W$ and $x_{5}$ is an isomorphism of $\mathrm{LF'}$ and $\mathrm{LF}$.

CategoryTheory.Functor.leftDerivedNatTransdefMathlib.CategoryTheory.Functor.Derived.LeftDerived, function or constant

Wording

the left derived natural transformation of x5 and #6 (from the name)

English

Let $\mathrm{LF'}$ and $\mathrm{LF}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{LF'}$ and $\mathrm{F'}$. Let $x_{4}$ be a homomorphism of the composition of $L$ and $\mathrm{LF}$ and $F$. Let $W$ be a morphism property of $C$. Let $x_{5}$ be a homomorphism of $\mathrm{F'}$ and $F$. Then the left derived natural transformation of $W$ and $x_{5}$ is a homomorphism of $\mathrm{LF'}$ and $\mathrm{LF}$ defined as the left derived lift of $\mathrm{LF'}$ and the composition of $x_{3}$ and $x_{5}$.

CategoryTheory.Functor.leftDerivedUniquedefMathlib.CategoryTheory.Functor.Derived.LeftDerived, function or constant

Wording

no wording

English

Let $\mathrm{LF'}$ and $\mathrm{LF}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{LF}$ and $F$. Let $x_{4}$ be a homomorphism of the composition of $L$ and $\mathrm{LF'}$ and $F$. Let $W$ be a morphism property of $C$. Then $\operatorname{leftDerivedUnique}$ applied to $\mathrm{LF'}$, $\mathrm{LF}$, $x_{3}$, $x_{4}$ and $W$ is an isomorphism of $\mathrm{LF}$ and $\mathrm{LF'}$ defined as the left derived natural isomorphism of $W$ and the identity of $F$.

CategoryTheory.Functor.totalLeftDeriveddefMathlib.CategoryTheory.Functor.Derived.LeftDerived, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $H$. Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then $\operatorname{totalLeftDerived}$ applied to $F$, $L$ and $W$ is a functor of $D$ and $H$ defined as the right Kan extension of $L$ and $F$.

CategoryTheory.Functor.totalLeftDerivedCounitdefMathlib.CategoryTheory.Functor.Derived.LeftDerived, function or constant

Wording

the total left derived counit of L and W (from the name)

English

Let $F$ be a functor of $C$ and $H$. Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then the total left derived counit of $L$ and $W$ is a homomorphism of the composition of $L$ and $\operatorname{totalLeftDerived}$ applied to $F$, $L$ and $W$ and $F$ defined as the counit of the chosen right Kan extension of $L$ and $F$.

Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

CategoryTheory.Functor.HasPointwiseLeftDerivedFunctordefMathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $H$. Let $W$ be a morphism property of $C$. Then $\operatorname{HasPointwiseLeftDerivedFunctor}$ holds for $F$ and $W$, if for all elements $X$ of $C$, $\operatorname{HasPointwiseLeftDerivedFunctorAt}$ holds for $F$, $W$ and $X$.

CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAtclassMathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $H$. Let $W$ be a morphism property of $C$. Let $X$ be an element of $C$. Then we can say that $\operatorname{HasPointwiseLeftDerivedFunctorAt}$ holds for $F$, $W$ and $X$.

CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionOfIsIsoOfIsLocalizationdefMathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $E$ be a right extension of $L$ and $F$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $E$. Proof. Let $W$ be arbitrary. Let $E$ be arbitrary. By W. By E. By CategoryTheory__CostructuredArrow__hom. By CategoryTheory__asIso. By CategoryTheory__Iso__symm. By CategoryTheory__Functor__isPointwiseRightKanExtensionOfIsoOfIsLocalization.

CategoryTheory.Functor.isPointwiseRightKanExtensionAtOfIsoOfIsLocalizationdefMathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $e$ be an isomorphism of $F$ and the composition of $L$ and $G$. Let $Y$ be an element of $C$. Then $\operatorname{isPointwiseRightKanExtensionAtOfIsoOfIsLocalization}$ applied to $W$, $e$ and $Y$ is an element of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $\operatorname{mk}$ applied to $G$ and the inverse of $e$ and the action of $L$ and $Y$.

CategoryTheory.Functor.isPointwiseRightKanExtensionOfHasPointwiseLeftDerivedFunctordefMathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of the composition of $L$ and $\mathrm{F'}$ and $F$. Let $W$ be a morphism property of $C$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{3}$. Proof. Let $\mathrm{F'}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $W$ be arbitrary. By F'. By x3. By CategoryTheory__Functor__isPointwiseRightKanExtensionOfIsRightKanExtension.

CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsoOfIsLocalizationdefMathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $e$ be an isomorphism of $F$ and the composition of $L$ and $G$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $\operatorname{mk}$ applied to $G$ and the inverse of $e$. Proof. Let $W$ be arbitrary. Let $e$ be arbitrary. Let $Y$ be arbitrary. By G. By e. By CategoryTheory__Iso__inv. By CategoryTheory__Functor__RightExtension__mk. By L. By Y. By CategoryTheory__Functor__objObjPreimageIso. By W. By e. By L. By Y. By CategoryTheory__Functor__objPreimage. By CategoryTheory__Functor__isPointwiseRightKanExtensionAtOfIsoOfIsLocalization. By CategoryTheory__Functor__RightExtension__isPointwiseRightKanExtensionAtEquivOfIso'__app.

Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

CategoryTheory.Functor.HasPointwiseRightDerivedFunctordefMathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $H$. Let $W$ be a morphism property of $C$. Then $\operatorname{HasPointwiseRightDerivedFunctor}$ holds for $F$ and $W$, if for all elements $X$ of $C$, $\operatorname{HasPointwiseRightDerivedFunctorAt}$ holds for $F$, $W$ and $X$.

CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAtclassMathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $H$. Let $W$ be a morphism property of $C$. Let $X$ be an element of $C$. Then we can say that $\operatorname{HasPointwiseRightDerivedFunctorAt}$ holds for $F$, $W$ and $X$.

CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionOfIsIsoOfIsLocalizationdefMathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $E$ be a left extension of $L$ and $F$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $E$. Proof. Let $W$ be arbitrary. Let $E$ be arbitrary. By W. By E. By CategoryTheory__StructuredArrow__hom. By CategoryTheory__asIso. By CategoryTheory__Functor__isPointwiseLeftKanExtensionOfIsoOfIsLocalization.

CategoryTheory.Functor.isPointwiseLeftKanExtensionAtOfIsoOfIsLocalizationdefMathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $e$ be an isomorphism of $F$ and the composition of $L$ and $G$. Let $Y$ be an element of $C$. Then $\operatorname{isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization}$ applied to $W$, $e$ and $Y$ is an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $\operatorname{mk}$ applied to $G$ and the homomorphism of $e$ and the action of $L$ and $Y$.

CategoryTheory.Functor.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctordefMathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived, function or constant

Wording

no wording

English

Let $\mathrm{F'}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{F'}$. Let $W$ be a morphism property of $C$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to $\mathrm{F'}$ and $x_{3}$. Proof. Let $\mathrm{F'}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $W$ be arbitrary. By F'. By x3. By CategoryTheory__Functor__isPointwiseLeftKanExtensionOfIsLeftKanExtension.

CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsoOfIsLocalizationdefMathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived, function or constant

Wording

no wording

English

Let $W$ be a morphism property of $C$. Let $e$ be an isomorphism of $F$ and the composition of $L$ and $G$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to $G$ and the homomorphism of $e$. Proof. Let $W$ be arbitrary. Let $e$ be arbitrary. Let $Y$ be arbitrary. By G. By e. By CategoryTheory__Iso__hom. By CategoryTheory__Functor__LeftExtension__mk. By L. By Y. By CategoryTheory__Functor__objObjPreimageIso. By W. By e. By L. By Y. By CategoryTheory__Functor__objPreimage. By CategoryTheory__Functor__isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization. By CategoryTheory__Functor__LeftExtension__isPointwiseLeftKanExtensionAtEquivOfIso'__app.

Mathlib.CategoryTheory.Functor.Derived.RightDerived

CategoryTheory.Functor.HasRightDerivedFunctorclassMathlib.CategoryTheory.Functor.Derived.RightDerived, predicate

Wording

no wording

English

Let $F$ be a functor of $C$ and $H$. Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{HasRightDerivedFunctor}$ holds for $F$ and $W$.

CategoryTheory.Functor.IsRightDerivedFunctorclassMathlib.CategoryTheory.Functor.Derived.RightDerived, predicate

Wording

no wording

English

Let $\mathrm{RF}$ be a functor of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{RF}$. Let $W$ be a morphism property of $C$. Then we can say that $\operatorname{IsRightDerivedFunctor}$ holds for $\mathrm{RF}$, $x_{3}$ and $W$.

CategoryTheory.Functor.rightDerivedDescdefMathlib.CategoryTheory.Functor.Derived.RightDerived, function or constant

Wording

no wording

English

Let $\mathrm{RF}$ and $G$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{RF}$. Let $W$ be a morphism property of $C$. Let $x_{4}$ be a homomorphism of $F$ and the composition of $L$ and $G$. Then $\operatorname{rightDerivedDesc}$ applied to $\mathrm{RF}$, $x_{3}$, $W$, $G$ and $x_{4}$ is a homomorphism of $\mathrm{RF}$ and $G$ defined as $\operatorname{descOfIsLeftKanExtension}$ applied to $\mathrm{RF}$, $x_{3}$, $G$ and $x_{4}$.

CategoryTheory.Functor.rightDerivedNatIsodefMathlib.CategoryTheory.Functor.Derived.RightDerived, function or constant

Wording

the right derived natural isomorphism of x5 and #6 (from the name)

English

Let $\mathrm{RF}$ and $\mathrm{RF'}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{RF}$. Let $x_{4}$ be a homomorphism of $\mathrm{F'}$ and the composition of $L$ and $\mathrm{RF'}$. Let $W$ be a morphism property of $C$. Let $x_{5}$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the right derived natural isomorphism of $W$ and $x_{5}$ is an isomorphism of $\mathrm{RF}$ and $\mathrm{RF'}$.

CategoryTheory.Functor.rightDerivedNatTransdefMathlib.CategoryTheory.Functor.Derived.RightDerived, function or constant

Wording

the right derived natural transformation of x5 and #6 (from the name)

English

Let $\mathrm{RF}$ and $\mathrm{RF'}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{RF}$. Let $x_{4}$ be a homomorphism of $\mathrm{F'}$ and the composition of $L$ and $\mathrm{RF'}$. Let $W$ be a morphism property of $C$. Let $x_{5}$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the right derived natural transformation of $W$ and $x_{5}$ is a homomorphism of $\mathrm{RF}$ and $\mathrm{RF'}$ defined as $\operatorname{rightDerivedDesc}$ applied to $\mathrm{RF}$, $x_{3}$, $W$, $\mathrm{RF'}$ and the composition of $x_{5}$ and $x_{4}$.

CategoryTheory.Functor.rightDerivedUniquedefMathlib.CategoryTheory.Functor.Derived.RightDerived, function or constant

Wording

no wording

English

Let $\mathrm{RF}$ and $\mathrm{RF'}$ be functors of $D$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{RF}$. Let $x_{4}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{RF'}$. Let $W$ be a morphism property of $C$. Then $\operatorname{rightDerivedUnique}$ applied to $\mathrm{RF}$, $\mathrm{RF'}$, $x_{3}$, $x_{4}$ and $W$ is an isomorphism of $\mathrm{RF}$ and $\mathrm{RF'}$ defined as the right derived natural isomorphism of $W$ and the identity of $F$.

CategoryTheory.Functor.totalRightDeriveddefMathlib.CategoryTheory.Functor.Derived.RightDerived, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $H$. Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then $\operatorname{totalRightDerived}$ applied to $F$, $L$ and $W$ is a functor of $D$ and $H$ defined as the left Kan extension of $L$ and $F$.

CategoryTheory.Functor.totalRightDerivedUnitdefMathlib.CategoryTheory.Functor.Derived.RightDerived, function or constant

Wording

the total right derived unit of L and W (from the name)

English

Let $F$ be a functor of $C$ and $H$. Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then the total right derived unit of $L$ and $W$ is a homomorphism of $F$ and the composition of $L$ and $\operatorname{totalRightDerived}$ applied to $F$, $L$ and $W$ defined as the unit of the chosen left Kan extension of $L$ and $F$.

Mathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift

CategoryTheory.Functor.IsRightDerivedFunctor.postcomposeShiftNatTransdefMathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift, function or constant

Wording

the postcomposition shift natural transformation of x3 and a (from the name)

English

Let $\mathrm{RF}$ be a functor of $H$ and $D$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{RF}$. Let $a$ be an element of $A$. Then the postcomposition shift natural transformation of $x_{3}$ and $a$ is a homomorphism of the composition of $F$ and the shift functor of $D$ and $a$ and the composition of $L$ and the composition of $\mathrm{RF}$ and the shift functor of $D$ and $a$ defined as the composition of the right whisker of $x_{3}$ and the shift functor of $D$ and $a$ and the homomorphism of the associator of $\mathrm{RF}$ and the shift functor of $D$ and $a$.

CategoryTheory.Functor.IsRightDerivedFunctor.precomposeShiftNatTransdefMathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift, function or constant

Wording

the precomposition shift natural transformation of x3 and a (from the name)

English

Let $\mathrm{RF}$ be a functor of $H$ and $D$. Let $x_{3}$ be a homomorphism of $F$ and the composition of $L$ and $\mathrm{RF}$. Let $a$ be an element of $A$. Then the precomposition shift natural transformation of $x_{3}$ and $a$ is a homomorphism of the composition of the shift functor of $C$ and $a$ and $F$ and the composition of $L$ and the composition of the shift functor of $H$ and $a$ and $\mathrm{RF}$ defined as the composition of the left whisker of the shift functor of $C$ and $a$ and $x_{3}$ and the composition of the inverse of the associator of $L$ and $\mathrm{RF}$ and the composition of the right whisker of the homomorphism of the commutative shift isomorphism of $L$ and $a$ and $\mathrm{RF}$ and the homomorphism of the associator of the shift functor of $H$ and $a$ and $\mathrm{RF}$.

Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition

CategoryTheory.Functor.natTransOfIsRightDerivedFunctorCompdefMathlib.CategoryTheory.Functor.Derived.RightDerivedComposition, function or constant

Wording

the natural transformation of x23 and x24 (from the name)

English

Let $e$ be an isomorphism of the composition of $x_{12}$ and $x_{13}$ and $x_{14}$. Let $x_{15}$ be a functor of $x$ and $x_{3}$. Let $x_{16}$ be a functor of $x_{1}$ and $x_{4}$. Let $x_{17}$ be a functor of $x_{2}$ and $x_{5}$. Let $x_{18}$ be a morphism property of $x$. Let $x_{22}$ be a homomorphism of the composition of $x_{12}$ and $x_{16}$ and the composition of $x_{15}$ and $x_{19}$. Let $x_{23}$ be a homomorphism of the composition of $x_{13}$ and $x_{17}$ and the composition of $x_{16}$ and $x_{20}$. Let $x_{24}$ be a homomorphism of the composition of $x_{14}$ and $x_{17}$ and the composition of $x_{15}$ and $x_{21}$. Then the natural transformation of $x_{23}$ and $x_{24}$ is a homomorphism of $x_{21}$ and the composition of $x_{19}$ and $x_{20}$ defined as $\operatorname{rightDerivedDesc}$ applied to $x_{21}$, $x_{24}$, $x_{18}$, the composition of $x_{19}$ and $x_{20}$ and the composition of the right whisker of the inverse of $e$ and $x_{17}$ and the composition of the homomorphism of the associator of $x_{13}$ and $x_{17}$ and the composition of the left whisker of $x_{12}$ and $x_{23}$ and the composition of the inverse of the associator of $x_{16}$ and $x_{20}$ and the composition of the right whisker of $x_{22}$ and $x_{20}$ and the homomorphism of the associator of $x_{19}$ and $x_{20}$.

Mathlib.CategoryTheory.Functor.EpiMono

CategoryTheory.Functor.PreservesEpimorphismsclassMathlib.CategoryTheory.Functor.EpiMono, predicate

Wording

F preserves epimorphisms (from the name)

English

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

CategoryTheory.Functor.PreservesMonomorphismsclassMathlib.CategoryTheory.Functor.EpiMono, predicate

Wording

F preserves monomorphisms (from the name)

English

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

CategoryTheory.Functor.ReflectsEpimorphismsclassMathlib.CategoryTheory.Functor.EpiMono, predicate

Wording

F reflects epimorphisms (from the name)

English

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

CategoryTheory.Functor.ReflectsMonomorphismsclassMathlib.CategoryTheory.Functor.EpiMono, predicate

Wording

F reflects monomorphisms (from the name)

English

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

CategoryTheory.Functor.splitEpiEquivdefMathlib.CategoryTheory.Functor.EpiMono, function or constant

Wording

the split epimorphism equivalence of F and f (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the split epimorphism equivalence of $F$ and $f$ is an equivalence from the set of split epimorphisms of $f$ to the set of split epimorphisms of the map of $F$ and $f$.

CategoryTheory.Functor.splitMonoEquivdefMathlib.CategoryTheory.Functor.EpiMono, function or constant

Wording

the split monomorphism equivalence of F and f (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $Y$ and $X$. Then the split monomorphism equivalence of $F$ and $f$ is an equivalence from the set of split monomorphisms of $f$ to the set of split monomorphisms of the map of $F$ and $f$.

Mathlib.CategoryTheory.Functor.Flat

CategoryTheory.PreservesFiniteLimitsOfFlat.liftdefMathlib.CategoryTheory.Functor.Flat, function or constant

Wording

the lift of hc and s (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $s$ be a cone of the composition of $K$ and $F$. Then the lift of $\mathrm{hc}$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and the action of $F$ and $\operatorname{pt}$ applied to $c$.

CategoryTheory.RepresentablyCoflatclassMathlib.CategoryTheory.Functor.Flat, predicate

Wording

no wording

English

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

CategoryTheory.RepresentablyFlatclassMathlib.CategoryTheory.Functor.Flat, predicate

Wording

F is representably flat (from the name)

English

generation took over the time limit

CategoryTheory.lanEvaluationIsoColimdefMathlib.CategoryTheory.Functor.Flat, function or constant

Wording

no wording

English

Let $E$ be a set. Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Then $\operatorname{lanEvaluationIsoColim}$ applied to $E$, $F$ and $X$ is an isomorphism of the composition of $\operatorname{lan}$ applied to $F$ and the action of the evaluation of $D$ and $E$ and $X$ and the composition of the action of the left whiskering of $C$ and $E$ and the projection of $F$ and $X$ and the colimit.

Mathlib.CategoryTheory.Functor.FullyFaithful

CategoryTheory.Functor.FaithfulclassMathlib.CategoryTheory.Functor.FullyFaithful, predicate

Wording

F is faithful (from the name)

English

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

CategoryTheory.Functor.Faithful.divdefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the quotient of obj and map (from the name)

English

Let $F$ be a functor of $C$ and $E$. Let $G$ be a functor of $D$ and $E$. Let $\mathrm{obj}$ be a function from elements of $C$ to elements of $D$ such that for all elements $X_{2}$ of $C$, the action of $G$ and $\mathrm{obj}$ applied to $X_{2}$ is equal to the action of $F$ and $X_{2}$. Let $\mathrm{map}$ be a function from elements $X_{1}$ of $C$ and elements $Y_{1}$ of $C$ and homomorphisms of $X_{1}$ and $Y_{1}$ to homomorphisms of $\mathrm{obj}$ applied to $X_{1}$ and $\mathrm{obj}$ applied to $Y_{1}$ such that for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, $\mathrm{HEq}$ holds for the map of $G$ and $\mathrm{map}$ applied to $X$, $Y$ and $f$ and the map of $F$ and $f$. Then the quotient of $\mathrm{obj}$ and $X_{1}$ is a functor of $C$ and $D$.

CategoryTheory.Functor.FullclassMathlib.CategoryTheory.Functor.FullyFaithful, predicate

Wording

F is full (from the name)

English

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

CategoryTheory.Functor.FullyFaithfulstructureMathlib.CategoryTheory.Functor.FullyFaithful, type

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then the elements of $\operatorname{FullyFaithful}$ applied to $F$ are a basic type.

CategoryTheory.Functor.FullyFaithful.compdefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the composition of hF and hG (from the name)

English

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

CategoryTheory.Functor.FullyFaithful.homEquivdefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the equivalence of hF (from the docstring)

English

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the equivalence of $\mathrm{hF}$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of the action of $F$ and $X$ and the action of $F$ and $Y$.

CategoryTheory.Functor.FullyFaithful.iddefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the identity functor of C (from the docstring)

English

Let $C$ be a set. Then the identity functor of $C$ is an element of $\operatorname{FullyFaithful}$ applied to the identity of $C$.

CategoryTheory.Functor.FullyFaithful.isoEquivdefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the equivalence of hF (from the docstring)

English

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the equivalence of $\mathrm{hF}$ is an equivalence from the set of isomorphisms of $X$ and $Y$ to the set of isomorphisms of the action of $F$ and $X$ and the action of $F$ and $Y$.

CategoryTheory.Functor.FullyFaithful.ofCompFaithfuldefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

no wording

English

Let $\mathrm{hFG}$ be an element of $\operatorname{FullyFaithful}$ applied to the composition of $F$ and $G$. Then $\operatorname{ofCompFaithful}$ applied to $\mathrm{hFG}$ is an element of $\operatorname{FullyFaithful}$ applied to $F$.

CategoryTheory.Functor.FullyFaithful.ofFullyFaithfuldefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{ofFullyFaithful}$ applied to $F$ is an element of $\operatorname{FullyFaithful}$ applied to $F$.

CategoryTheory.Functor.FullyFaithful.ofIsodefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

no wording

English

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Let $e$ be an isomorphism of $F$ and $G$. Then $\operatorname{ofIso}$ applied to $\mathrm{hF}$ and $e$ is an element of $\operatorname{FullyFaithful}$ applied to $G$.

CategoryTheory.Functor.FullyFaithful.preimagedefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the preimage of self and f (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Let $f$ be a homomorphism of the action of $F$ and $X$ and the action of $F$ and $Y$. Then the preimage of $\mathrm{self}$ and $f$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $f$.

CategoryTheory.Functor.FullyFaithful.preimageIsodefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the unique isomorphism of hF and e (from the docstring)

English

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Let $e$ be an isomorphism of the action of $F$ and $X$ and the action of $F$ and $Y$. Then the unique isomorphism of $\mathrm{hF}$ and $e$ is an isomorphism of $X$ and $Y$.

CategoryTheory.Functor.fullyFaithfulCancelRightdefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

no wording

English

Let $H$ be a functor of $D$ and $E$. Let $\mathrm{comp\_iso}$ be an isomorphism of the composition of $F$ and $H$ and the composition of $G$ and $H$. Then $\operatorname{fullyFaithfulCancelRight}$ applied to $H$ and $\mathrm{comp\_iso}$ is an isomorphism of $F$ and $G$.

CategoryTheory.Functor.preimagedefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the choice of F and f (from the docstring)

English

Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of the action of $F$ and $X$ and the action of $F$ and $Y$. Then the choice of $F$ and $f$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_map\_surjective}$ applied to $F$ and $f$.

CategoryTheory.Functor.preimageIsodefMathlib.CategoryTheory.Functor.FullyFaithful, function or constant

Wording

the preimage isomorphism of F and f (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $f$ be an isomorphism of the action of $F$ and $X$ and the action of $F$ and $Y$. Then the preimage isomorphism of $F$ and $f$ is an isomorphism of $X$ and $Y$.