Definitions: Mathlib.Algebra, part 8 of 17

MonoidWithZeroHom.compdefMathlib.Algebra.GroupWithZero.Hom, function or constant

Wording

the composition of hnp and hmn (from the name)

English

Let $\mathrm{hnp}$ be a monoid with zero homomorphism of $x_{1}$ and $x_{2}$. Let $\mathrm{hmn}$ be a monoid with zero homomorphism of $x$ and $x_{1}$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is a monoid with zero homomorphism of $x$ and $x_{2}$.

MonoidWithZeroHom.copydefMathlib.Algebra.GroupWithZero.Hom, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a monoid with zero homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a monoid homomorphism of $x$ and $x_{1}$.

MonoidWithZeroHom.iddefMathlib.Algebra.GroupWithZero.Hom, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a monoid with zero homomorphism of $x$ and $x$.

MonoidWithZeroHom.ofClassdefMathlib.Algebra.GroupWithZero.Hom, function or constant

Wording

the monoid with zero homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the monoid with zero homomorphism of $f$ is a monoid with zero homomorphism of $x$ and $x_{1}$.

MonoidWithZeroHom.toMonoidHomdefMathlib.Algebra.GroupWithZero.Hom, function or constant

Wording

the monoid homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a monoid with zero homomorphism of $x$ and $x_{1}$. Then the monoid homomorphism of $\mathrm{self}$ is a monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toZeroHom}$ applied to $\mathrm{self}$ and $\mathrm{MonoidWithZeroHom\_\_map\_one'}$ applied to $\mathrm{self}$ and $\mathrm{MonoidWithZeroHom\_\_map\_mul'}$ applied to $\mathrm{self}$.

MonoidWithZeroHomClassclassMathlib.Algebra.GroupWithZero.Hom, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MonoidWithZeroHomClass}$ holds for $F$, $x$ and $x_{1}$.

powMonoidWithZeroHomdefMathlib.Algebra.GroupWithZero.Hom, function or constant

Wording

the power monoid with zero homomorphism of hn (from the name)

English

Assume that $n \neq 0$. Then the power monoid with zero homomorphism of $\mathrm{hn}$ is a monoid with zero homomorphism of $x$ and $x$.

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

associatesNonZeroDivisorsEquivdefMathlib.Algebra.GroupWithZero.NonZeroDivisors, function or constant

Wording

the associate non zero divisor equivalence (from the name)

English

The associate non zero divisor equivalence is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (\mathrm{Associates} (x))}{x_{2}})}$ and the set of associates of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (x)}{x_{3}})}$.

nonZeroDivisorsdefMathlib.Algebra.GroupWithZero.NonZeroDivisors, function or constant

Wording

the non zero divisor of x (from the name)

English

Let $x$ be a set. Then the non zero divisor of $x$ is a submonoid of $x$ defined as the minimum of the left non zero divisor of $x$ and the right non zero divisor of $x$.

nonZeroDivisorsEquivUnitsdefMathlib.Algebra.GroupWithZero.NonZeroDivisors, function or constant

Wording

the non zero divisor equivalence unit (from the name)

English

The non zero divisor equivalence unit is a multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (x)}{x_{2}})}$ and $\UnitsMACRoAO {x}$.

nonZeroDivisorsLeftdefMathlib.Algebra.GroupWithZero.NonZeroDivisors, function or constant

Wording

the left non zero divisor of x (from the name)

English

Let $x$ be a set. Then the left non zero divisor of $x$ is a submonoid of $x$.

nonZeroDivisorsRightdefMathlib.Algebra.GroupWithZero.NonZeroDivisors, function or constant

Wording

the right non zero divisor of x (from the name)

English

Let $x$ be a set. Then the right non zero divisor of $x$ is a submonoid of $x$.

nonZeroSMulDivisorsdefMathlib.Algebra.GroupWithZero.NonZeroDivisors, function or constant

Wording

the non zero multiplicative divisor of x and M (from the name)

English

Let $x$ and $M$ be sets. Then the non zero multiplicative divisor of $x$ and $M$ is a submonoid of $x$.

unitsNonZeroDivisorsEquivdefMathlib.Algebra.GroupWithZero.NonZeroDivisors, function or constant

Wording

the unit non zero divisor equivalence (from the name)

English

The unit non zero divisor equivalence is a multiplicative equivalence of $\UnitsMACRoAO {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (x)}{x_{2}})})}$ and $\UnitsMACRoAO {x}$.

Mathlib.Algebra.GroupWithZero.Pi

MulHom.singledefMathlib.Algebra.GroupWithZero.Pi, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Then $\operatorname{single}$ applied to $i$ is a multiplicative homomorphism of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$.

Mathlib.Algebra.GroupWithZero.Prod

divMonoidWithZeroHomdefMathlib.Algebra.GroupWithZero.Prod, function or constant

Wording

the quotient monoid with zero homomorphism (from the name)

English

The quotient monoid with zero homomorphism is a monoid with zero homomorphism of $\mathrm{Prod}$ applied to $x$ and $x$ and $x$.

mulMonoidWithZeroHomdefMathlib.Algebra.GroupWithZero.Prod, function or constant

Wording

the multiplicative monoid with zero homomorphism (from the name)

English

The multiplicative monoid with zero homomorphism is a monoid with zero homomorphism of $\mathrm{Prod}$ applied to $x$ and $x$ and $x$.

Mathlib.Algebra.GroupWithZero.ProdHom

MonoidWithZeroHom.fstdefMathlib.Algebra.GroupWithZero.ProdHom, function or constant

Wording

the first component of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the first component of $x$ and $x_{1}$ is a monoid with zero homomorphism of $\mathrm{WithZero}$ applied to $\mathrm{Prod}$ applied to $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$ and $x$ defined as $\operatorname{lift'}$ applied to the composition of the coercion homomorphism of $x$ and the first component of $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$.

MonoidWithZeroHom.inldefMathlib.Algebra.GroupWithZero.ProdHom, function or constant

Wording

the left injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the left injection of $x$ and $x_{1}$ is a monoid with zero homomorphism of $x$ and $\mathrm{WithZero}$ applied to $\mathrm{Prod}$ applied to $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$ defined as the composition of the map of the left injection of $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$ and the monoid with zero homomorphism of the inverse of $\operatorname{withZeroUnitsEquiv}$.

MonoidWithZeroHom.inrdefMathlib.Algebra.GroupWithZero.ProdHom, function or constant

Wording

the right injection of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the right injection of $x$ and $x_{1}$ is a monoid with zero homomorphism of $x_{1}$ and $\mathrm{WithZero}$ applied to $\mathrm{Prod}$ applied to $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$ defined as the composition of the map of the right injection of $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$ and the monoid with zero homomorphism of the inverse of $\operatorname{withZeroUnitsEquiv}$.

MonoidWithZeroHom.snddefMathlib.Algebra.GroupWithZero.ProdHom, function or constant

Wording

the second component of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the second component of $x$ and $x_{1}$ is a monoid with zero homomorphism of $\mathrm{WithZero}$ applied to $\mathrm{Prod}$ applied to $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$ and $x_{1}$ defined as $\operatorname{lift'}$ applied to the composition of the coercion homomorphism of $x_{1}$ and the second component of $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$.

Mathlib.Algebra.GroupWithZero.Range

MonoidWithZeroHom.ValueGroup₀defMathlib.Algebra.GroupWithZero.Range, type

Wording

value group of f (from the name)

English

Let $f$ be a monoid with zero homomorphism of $A$ and $B$. Then a value group of $f$ is an element of the function that maps $f$ to $\mathrm{WithZero}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (f)}{x_{2}})}$.

MonoidWithZeroHom.ValueGroup₀.embeddingdefMathlib.Algebra.GroupWithZero.Range, function or constant

Wording

the embedding (from the name)

English

The embedding is a monoid with zero homomorphism of the set of value groups of $f$ and $B$ defined as the composition of the monoid with zero homomorphism of $\operatorname{withZeroUnitsEquiv}$ and the map of the subtype of the value group of $f$.

MonoidWithZeroHom.ValueGroup₀.mkdefMathlib.Algebra.GroupWithZero.Range, function or constant

Wording

no wording

English

Let $f$ be a monoid with zero homomorphism of $A$ and $B$. Let $r$ and $s$ be elements of $A$. Then $\mathrm{MonoidWithZeroHom\_\_ValueGroup\_u2080\_\_\_mk}$ applied to $f$, $r$ and $s$ is a value group of $f$.

MonoidWithZeroHom.ValueGroup₀.restrict₀defMathlib.Algebra.GroupWithZero.Range, function or constant

Wording

no wording

English

Let $f$ be a monoid with zero homomorphism of $A$ and $B$. Then $\mathrm{MonoidWithZeroHom\_\_ValueGroup\_u2080\_\_\_restrict\_u2080\_}$ applied to $f$ is a monoid with zero homomorphism of $A$ and the set of value groups of $f$.

MonoidWithZeroHom.ValueMonoid₀defMathlib.Algebra.GroupWithZero.Range, type

Wording

value monoid of f (from the name)

English

Let $f$ be a monoid with zero homomorphism of $A$ and $B$. Then a value monoid of $f$ is an element of the function that maps $f$ to $\mathrm{WithZero}$ applied to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{valueMonoid} (f)}{x_{2}})}$.

MonoidWithZeroHom.valueGroupdefMathlib.Algebra.GroupWithZero.Range, function or constant

Wording

the value group of f (from the name)

English

Let $f$ be a monoid with zero homomorphism of $A$ and $B$. Then the value group of $f$ is a subgroup of $\UnitsMACRoAO {B}$ defined as the closure of the value monoid of $f$.

MonoidWithZeroHom.valueGroup.mkdefMathlib.Algebra.GroupWithZero.Range, function or constant

Wording

no wording

English

Let $f$ be a monoid with zero homomorphism of $A$ and $B$. Let $r$ and $s$ be elements of $A$ such that $f (r)\neq 0$ and $f (s)\neq 0$. Then $\operatorname{mk}$ applied to $f$, $r$, $s$, $\mathrm{hr}$ and $\mathrm{hs}$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (f)}{x_{2}})}$ defined as $\operatorname{inv} (\operatorname{mk0} (f (r), \mathrm{hr}))\times \operatorname{mk0} (f (s), \mathrm{hs})$.

MonoidWithZeroHom.valueMonoiddefMathlib.Algebra.GroupWithZero.Range, function or constant

Wording

the value monoid of f (from the name)

English

Let $f$ be a monoid with zero homomorphism of $A$ and $B$. Then the value monoid of $f$ is a submonoid of $\UnitsMACRoAO {B}$.

Mathlib.Algebra.GroupWithZero.Submonoid.Primal

Submonoid.isPrimaldefMathlib.Algebra.GroupWithZero.Submonoid.Primal, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{isPrimal}$ applied to $x$ is a submonoid of $x$.

Mathlib.Algebra.GroupWithZero.Units.Basic

Ring.inversedefMathlib.Algebra.GroupWithZero.Units.Basic, function or constant

Wording

the inverse of x2 (from the name)

English

Let $x_{2}$ be an element of $x$. Then the inverse of $x_{2}$ is an element of $x$ defined as $\mathrm{dite}$ applied to the proposition that $x_{2}$ is a unit, the function that maps $h$ to the underlying value in the base of $\operatorname{inv}$ applied to the unit of $h$ and the function that maps $h_{1}$ to $0$.

Units.mk0defMathlib.Algebra.GroupWithZero.Units.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $x$ such that $a \neq 0$. Then $\operatorname{mk0}$ applied to $a$ and $\mathrm{ha}$ is a unit of $x$ defined as $\operatorname{mk}$ applied to $a$, $\operatorname{inv}$ applied to $a$, $\mathrm{mul\_inv\_cancel\_u2080\_}$ applied to $\mathrm{ha}$ and $\mathrm{inv\_mul\_cancel\_u2080\_}$ applied to $\mathrm{ha}$.

Mathlib.Algebra.GroupWithZero.Units.Equiv

Equiv.divLeft₀defMathlib.Algebra.GroupWithZero.Units.Equiv, function or constant

Wording

the left quotient of a and ha (from the name)

English

Let $a$ be an element of $x$ such that $a \neq 0$. Then the left quotient of $a$ and $\mathrm{ha}$ is a permutation of $x$.

Equiv.divRight₀defMathlib.Algebra.GroupWithZero.Units.Equiv, function or constant

Wording

the right quotient of a and ha (from the name)

English

Let $a$ be an element of $x$ such that $a \neq 0$. Then the right quotient of $a$ and $\mathrm{ha}$ is a permutation of $x$.

Equiv.mulLeft₀defMathlib.Algebra.GroupWithZero.Units.Equiv, function or constant

Wording

the left multiplicative of a and ha (from the name)

English

Let $a$ be an element of $x$ such that $a \neq 0$. Then the left multiplicative of $a$ and $\mathrm{ha}$ is a permutation of $x$ defined as the left multiplicative of $\operatorname{mk0}$ applied to $a$ and $\mathrm{ha}$.

Equiv.mulRight₀defMathlib.Algebra.GroupWithZero.Units.Equiv, function or constant

Wording

the right multiplicative of a and ha (from the name)

English

Let $a$ be an element of $x$ such that $a \neq 0$. Then the right multiplicative of $a$ and $\mathrm{ha}$ is a permutation of $x$ defined as the right multiplicative of $\operatorname{mk0}$ applied to $a$ and $\mathrm{ha}$.

unitsEquivNeZerodefMathlib.Algebra.GroupWithZero.Units.Equiv, function or constant

Wording

no wording

English

$\mathrm{unitsEquivNeZero}$ is an equivalence from $\UnitsMACRoAO {x}$ to $\SubtypeSet {a}{\mathrm{Neq} (a , 0)}$.

Mathlib.Algebra.GroupWithZero.Units.Lemmas

MonoidWithZero.inversedefMathlib.Algebra.GroupWithZero.Units.Lemmas, function or constant

Wording

the inverse (from the name)

English

The inverse is a monoid with zero homomorphism of $M$ and $M$.

invMonoidWithZeroHomdefMathlib.Algebra.GroupWithZero.Units.Lemmas, function or constant

Wording

the inverse monoid with zero homomorphism (from the name)

English

The inverse monoid with zero homomorphism is a monoid with zero homomorphism of $x$ and $x$.

Mathlib.Algebra.GroupWithZero.WithZero

MulEquiv.unzerodefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

no wording

English

Let $e$ be a multiplicative equivalence of $\mathrm{WithZero}$ applied to $x$ and $\mathrm{WithZero}$ applied to $x_{1}$. Then $\operatorname{unzero}$ applied to $e$ is a multiplicative equivalence of $x$ and $x_{1}$ defined as $\operatorname{symm}$ applied to $\operatorname{withZero}$ and $e$.

MulEquiv.withZerodefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

no wording

English

$\operatorname{withZero}$ is an equivalence from the set of multiplicative equivalences of $x$ and $x_{1}$ to the set of multiplicative equivalences of $\mathrm{WithZero}$ applied to $x$ and $\mathrm{WithZero}$ applied to $x_{1}$.

WithZero.coeMonoidHomdefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

the coercion monoid homomorphism (from the name)

English

The coercion monoid homomorphism is a monoid homomorphism of $x$ and $\mathrm{WithZero}$ applied to $x$.

WithZero.expdefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

the exponential map of a (from the docstring)

English

Let $a$ be an element of $M$. Then the exponential map of $a$ is an element of $\mathrm{WithZero}$ applied to the set of multiplicatives of $M$ defined as the coercion of $\operatorname{ofAdd}$ applied to $a$.

WithZero.expEquivdefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

the exponential map (from the docstring)

English

The exponential map is an equivalence from $G$ to the set of units of $\mathrm{WithZero}$ applied to the set of multiplicatives of $G$ defined as the composition of the multiplicative and $\operatorname{toEquiv}$ applied to the inverse of the unit with zero equivalence.

WithZero.expRecOndefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{WithZero}$ applied to the set of multiplicatives of $M$. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{exp}$ be a function from elements $a$ of $M$ to elements of $\mathrm{motive}$ applied to the exponential map of $a$. Then $\operatorname{expRecOn}$ applied to $x$, $\mathrm{zero}$, $a$ and $\mathrm{exp}$ is an element of $\mathrm{motive}$ applied to $x$ defined as the function that maps $\mathrm{exp}$ to $\operatorname{recOn}$ applied to $x$, $\mathrm{zero}$, $a$ and $\mathrm{exp}$.

WithZero.lift'defMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

the lift (from the name)

English

The lift is an equivalence from the set of monoid homomorphisms of $x$ and $x_{1}$ to the set of monoid with zero homomorphisms of $\mathrm{WithZero}$ applied to $x$ and $x_{1}$.

WithZero.logdefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

the logarithm of x1 (from the docstring)

English

Let $x_{1}$ be an element of $\mathrm{WithZero}$ applied to the set of multiplicatives of $M$. Then the logarithm of $x_{1}$ is an element of $M$ defined as $\operatorname{recZeroCoe}$ applied to $0$, $\operatorname{coe}$ applied to the sum and $x_{1}$.

WithZero.logEquivdefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

the logarithm (from the docstring)

English

The logarithm is an equivalence from the set of units of $\mathrm{WithZero}$ applied to the set of multiplicatives of $G$ to $G$ defined as the composition of $\operatorname{toEquiv}$ applied to the unit with zero equivalence and the sum.

WithZero.map'defMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a monoid homomorphism of $x$ and $x_{1}$. Then the map of $f$ is a monoid with zero homomorphism of $\mathrm{WithZero}$ applied to $x$ and $\mathrm{WithZero}$ applied to $x_{1}$ defined as $\operatorname{lift'}$ applied to the composition of the coercion monoid homomorphism and $f$.

WithZero.unitsWithZeroEquivdefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

the unit with zero equivalence (from the name)

English

The unit with zero equivalence is a multiplicative equivalence of $\UnitsMACRoAO {\mathrm{WithZero} (x)}$ and $x$.

WithZero.withZeroUnitsEquivdefMathlib.Algebra.GroupWithZero.WithZero, function or constant

Wording

no wording

English

$\operatorname{withZeroUnitsEquiv}$ is a multiplicative equivalence of $\mathrm{WithZero}$ applied to $\UnitsMACRoAO {G}$ and $G$.

Mathlib.Algebra.HierarchyDesign

LibraryNote.commutative_subobjectsdefMathlib.Algebra.HierarchyDesign, function or constant

Wording

the commutative subobject (from the name)

English

The commutative subobject is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

LibraryNote.higher_instance_prioritydefMathlib.Algebra.HierarchyDesign, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_higher\_instance\_priority}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

LibraryNote.implicit_instance_argumentsdefMathlib.Algebra.HierarchyDesign, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_implicit\_instance\_arguments}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

LibraryNote.instance_argument_orderdefMathlib.Algebra.HierarchyDesign, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_instance\_argument\_order}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

LibraryNote.lower_instance_prioritydefMathlib.Algebra.HierarchyDesign, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_lower\_instance\_priority}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

LibraryNote.the_algebraic_hierarchydefMathlib.Algebra.HierarchyDesign, function or constant

Wording

the algebraic hierarchy (from the name)

English

The algebraic hierarchy is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Mathlib.Algebra.Homology.Additive

CategoryTheory.Equivalence.mapHomologicalComplexdefMathlib.Algebra.Homology.Additive, function or constant

Wording

the map homological complex of e and c (from the name)

English

Let $e$ be an equivalence of $x_{1}$ and $x_{2}$. Let $c$ be a complex shape of $x$. Then the map homological complex of $e$ and $c$ is an equivalence of the set of homological complexes of $x_{1}$ and $c$ and the set of homological complexes of $x_{2}$ and $c$.

CategoryTheory.Functor.mapHomologicalComplexdefMathlib.Algebra.Homology.Additive, function or constant

Wording

the map homological complex of F and c (from the name)

English

Let $F$ be a functor of $x_{1}$ and $x_{2}$. Let $c$ be a complex shape of $x$. Then the map homological complex of $F$ and $c$ is a functor of the set of homological complexes of $x_{1}$ and $c$ and the set of homological complexes of $x_{2}$ and $c$.

CategoryTheory.Functor.mapHomologicalComplexCompIsodefMathlib.Algebra.Homology.Additive, function or constant

Wording

the map homological complex composition isomorphism of e and c (from the name)

English

Let $e$ be an isomorphism of the composition of $F$ and $G$ and $H$. Let $c$ be a complex shape of $x$. Then the map homological complex composition isomorphism of $e$ and $c$ is an isomorphism of the composition of the map homological complex of $F$ and $c$ and the map homological complex of $G$ and $c$ and the map homological complex of $H$ and $c$ defined as the map homological complex of $e$ and $c$.

CategoryTheory.Functor.mapHomologicalComplexIdIsodefMathlib.Algebra.Homology.Additive, function or constant

Wording

the map homological complex identity isomorphism of x1 and c (from the name)

English

Let $x_{1}$ be a set. Let $c$ be a complex shape of $x$. Then the map homological complex identity isomorphism of $x_{1}$ and $c$ is an isomorphism of the map homological complex of the identity of $x_{1}$ and $c$ and the identity of the set of homological complexes of $x_{1}$ and $c$.

CategoryTheory.NatIso.mapHomologicalComplexdefMathlib.Algebra.Homology.Additive, function or constant

Wording

the map homological complex of x7 and c (from the name)

English

Let $x_{7}$ be an isomorphism of $F$ and $G$. Let $c$ be a complex shape of $x$. Then the map homological complex of $x_{7}$ and $c$ is an isomorphism of the map homological complex of $F$ and $c$ and the map homological complex of $G$ and $c$.

CategoryTheory.NatTrans.mapHomologicalComplexdefMathlib.Algebra.Homology.Additive, function or constant

Wording

the map homological complex of x7 and c (from the name)

English

Let $x_{7}$ be a homomorphism of $F$ and $G$. Let $c$ be a complex shape of $x$. Then the map homological complex of $x_{7}$ and $c$ is a homomorphism of the map homological complex of $F$ and $c$ and the map homological complex of $G$ and $c$.

HomologicalComplex.Hom.fAddMonoidHomdefMathlib.Algebra.Homology.Additive, function or constant

Wording

the additive monoid homomorphism of i (from the name)

English

Let $i$ be an element of $x$. Then the additive monoid homomorphism of $i$ is an additive monoid homomorphism of the set of homomorphisms of $x_{3}$ and $x_{4}$ and the set of homomorphisms of $\operatorname{X}$ applied to $x_{3}$ and $i$ and $\operatorname{X}$ applied to $x_{4}$ and $i$.

HomologicalComplex.singleMapHomologicalComplexdefMathlib.Algebra.Homology.Additive, function or constant

Wording

the single map homological complex of c and j (from the name)

English

Let $F$ be a functor of $x_{1}$ and $x_{2}$. Let $c$ be a complex shape of $x$. Let $j$ be an element of $x$. Then the single map homological complex of $c$ and $j$ is an isomorphism of the composition of $\operatorname{single}$ applied to $x_{1}$, $c$ and $j$ and the map homological complex of $F$ and $c$ and the composition of $F$ and $\operatorname{single}$ applied to $x_{2}$, $c$ and $j$.

Mathlib.Algebra.Homology.AlternatingConst

AlgebraicTopology.alternatingFaceMapComplexConstdefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

the alternating face complex of the constant complex (from the docstring)

English

The alternating face complex of the constant complex is an isomorphism of the composition of the constant of the set of opposites of the set of simplex categories and the alternating face map complex of $C$ and the alternating constant.

ChainComplex.alternatingConstdefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

the alternating constant (from the name)

English

The alternating constant is a functor of $C$ and the set of chain complexes of $C$ and $\Natural$.

ChainComplex.alternatingConstHomologyDataEvenNEZerodefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Let $n$ be a natural number such that $n$ is even and $n \neq 0$. Then $\operatorname{alternatingConstHomologyDataEvenNEZero}$ applied to $X$, $n$, $\mathrm{hn}$ and $h_{1}$ is a homology data of $\operatorname{sc}$ applied to the action of the alternating constant and $X$ and $n$.

ChainComplex.alternatingConstHomologyDataOdddefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

no wording

English

Let $X$ be an element of $C$. Let $n$ be an odd natural number. Then $\operatorname{alternatingConstHomologyDataOdd}$ applied to $X$, $n$ and $\mathrm{hn}$ is a homology data of $\operatorname{sc}$ applied to the action of the alternating constant and $X$ and $n$.

ChainComplex.alternatingConstHomologyDataZerodefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

the alternating constant homology data zero of X and n (from the name)

English

Let $X$ be an element of $C$. Let $n$ be a natural number such that $n = 0$. Then the alternating constant homology data zero of $X$ and $n$ is a homology data of $\operatorname{sc}$ applied to the action of the alternating constant and $X$ and $n$.

ChainComplex.alternatingConstHomologyZerodefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

the alternating constant homology zero of X (from the name)

English

Let $X$ be an element of $C$. Then the alternating constant homology zero of $X$ is an isomorphism of the homology of the action of the alternating constant and $X$ and $0$ and $X$.

ChainComplex.alternatingConstHomotopyEquivdefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

the alternating constant homotopy equivalence of X (from the name)

English

Let $X$ be an element of $C$. Then the alternating constant homotopy equivalence of $X$ is a homotopy equivalence of the action of the alternating constant and $X$ and the action of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $C$ and $X$ defined as the composition of the homotopy equivalence of the inverse of the application of the alternating face complex of the constant complex and $X$ and the homotopy equivalence of the constant of $X$.

HomologicalComplex.alternatingConstdefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

the alternating constant of A (from the name)

English

HomologicalComplex.alternatingConstHomologyIsoEvendefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

the alternating constant homology isomorphism even of A (from the name)

English

Let $A$ be an element of $C$. Assume that the composition of $x_{2}$ and $x_{3}$ is equal to $0$. Assume that the composition of $x_{3}$ and $x_{2}$ is equal to $0$. Assume that for all natural numbers $i$ and $j_{1}$, if $\operatorname{Rel}$ holds for $c$, $i$ and $j_{1}$, then $i + j_{1}$ is odd. Assume that $\operatorname{Rel}$ holds for $c$, $\operatorname{prev}$ applied to $c$ and $j$ and $j$. Assume that $\operatorname{Rel}$ holds for $c$, $j$ and $\operatorname{next}$ applied to $c$ and $j$. Assume that $j$ is even. Then the alternating constant homology isomorphism even of $A$ is an isomorphism of the homology of the alternating constant of $A$ and $j$ and the homology of $\operatorname{mk}$ applied to $x_{3}$, $x_{2}$ and $\mathrm{hEven}$ defined as the homology isomorphism of $\operatorname{alternatingConstScIsoEven}$ applied to $A$, $\mathrm{hOdd}$, $\mathrm{hEven}$, $\mathrm{hc}$, $\mathrm{hpj}$, $\mathrm{hnj}$ and $h_{1}$.

HomologicalComplex.alternatingConstHomologyIsoOdddefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

no wording

English

Let $A$ be an element of $C$. Assume that the composition of $x_{2}$ and $x_{3}$ is equal to $0$. Assume that the composition of $x_{3}$ and $x_{2}$ is equal to $0$. Assume that for all natural numbers $i$ and $j_{1}$, if $\operatorname{Rel}$ holds for $c$, $i$ and $j_{1}$, then $i + j_{1}$ is odd. Assume that $\operatorname{Rel}$ holds for $c$, $\operatorname{prev}$ applied to $c$ and $j$ and $j$. Assume that $\operatorname{Rel}$ holds for $c$, $j$ and $\operatorname{next}$ applied to $c$ and $j$. Assume that $j$ is odd. Then $\operatorname{alternatingConstHomologyIsoOdd}$ applied to $A$, $\mathrm{hOdd}$, $\mathrm{hEven}$, $\mathrm{hc}$, $\mathrm{hpj}$, $\mathrm{hnj}$ and $h_{1}$ is an isomorphism of the homology of the alternating constant of $A$ and $j$ and the homology of $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$ and $\mathrm{hOdd}$ defined as the homology isomorphism of $\operatorname{alternatingConstScIsoOdd}$ applied to $A$, $\mathrm{hOdd}$, $\mathrm{hEven}$, $\mathrm{hc}$, $\mathrm{hpj}$, $\mathrm{hnj}$ and $h_{1}$.

HomologicalComplex.alternatingConstScIsoEvendefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

no wording

English

Let $A$ be an element of $C$. Assume that the composition of $x_{2}$ and $x_{3}$ is equal to $0$. Assume that the composition of $x_{3}$ and $x_{2}$ is equal to $0$. Assume that for all natural numbers $i_{1}$ and $j_{1}$, if $\operatorname{Rel}$ holds for $c$, $i_{1}$ and $j_{1}$, then $i_{1} + j_{1}$ is odd. Assume that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Assume that $\operatorname{Rel}$ holds for $c$, $j$ and $k$. Assume that $j$ is even. Then $\operatorname{alternatingConstScIsoEven}$ applied to $A$, $\mathrm{hOdd}$, $\mathrm{hEven}$, $\mathrm{hc}$, $\mathrm{hij}$, $\mathrm{hjk}$ and $h$ is an isomorphism of $\operatorname{sc'}$ applied to the alternating constant of $A$, $i$, $j$ and $k$ and $\operatorname{mk}$ applied to $x_{3}$, $x_{2}$ and $\mathrm{hEven}$.

HomologicalComplex.alternatingConstScIsoOdddefMathlib.Algebra.Homology.AlternatingConst, function or constant

Wording

no wording

English

Let $A$ be an element of $C$. Assume that the composition of $x_{2}$ and $x_{3}$ is equal to $0$. Assume that the composition of $x_{3}$ and $x_{2}$ is equal to $0$. Assume that for all natural numbers $i_{1}$ and $j_{1}$, if $\operatorname{Rel}$ holds for $c$, $i_{1}$ and $j_{1}$, then $i_{1} + j_{1}$ is odd. Assume that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Assume that $\operatorname{Rel}$ holds for $c$, $j$ and $k$. Assume that $j$ is odd. Then $\operatorname{alternatingConstScIsoOdd}$ applied to $A$, $\mathrm{hOdd}$, $\mathrm{hEven}$, $\mathrm{hc}$, $\mathrm{hij}$, $\mathrm{hjk}$ and $h$ is an isomorphism of $\operatorname{sc'}$ applied to the alternating constant of $A$, $i$, $j$ and $k$ and $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$ and $\mathrm{hOdd}$.

Mathlib.Algebra.Homology.Augment

ChainComplex.augmentdefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a chain complex of $V$ and $\Natural$. Let $f$ be a homomorphism of $\operatorname{X}$ applied to $C$ and $0$ and $X$ such that the composition of $\operatorname{d}$ applied to $C$, $1$ and $0$ and $f$ is equal to $0$. Then $\operatorname{augment}$ applied to $C$, $f$ and $w$ is a chain complex of $V$ and $\Natural$.

ChainComplex.augmentTruncatedefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a chain complex of $V$ and $\Natural$. Then $\operatorname{augmentTruncate}$ applied to $C$ is an isomorphism of $\operatorname{augment}$ applied to the action of the truncation and $C$, $\operatorname{d}$ applied to $C$, $1$ and $0$ and $\mathrm{HomologicalComplex\_\_d\_comp\_d}$ applied to $C$, $1 + 1$, $0 + 1$ and $0$ and $C$.

ChainComplex.toSingle₀AsComplexdefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a chain complex of $V$ and $\Natural$. Let $X$ be an element of $V$. Let $f$ be a homomorphism of $C$ and the action of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $V$ and $X$. Then $\mathrm{ChainComplex\_\_toSingle\_u2080\_AsComplex}$ applied to $C$, $X$ and $f$ is a chain complex of $V$ and $\Natural$.

ChainComplex.truncatedefMathlib.Algebra.Homology.Augment, function or constant

Wording

the truncation (from the docstring)

English

The truncation is a functor of the set of chain complexes of $V$ and $\Natural$ and the set of chain complexes of $V$ and $\Natural$.

ChainComplex.truncateAugmentdefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a chain complex of $V$ and $\Natural$. Let $f$ be a homomorphism of $\operatorname{X}$ applied to $C$ and $0$ and $X$ such that the composition of $\operatorname{d}$ applied to $C$, $1$ and $0$ and $f$ is equal to $0$. Then $\operatorname{truncateAugment}$ applied to $C$, $f$ and $w$ is an isomorphism of the action of the truncation and $\operatorname{augment}$ applied to $C$, $f$ and $w$ and $C$.

ChainComplex.truncateTodefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a chain complex of $V$ and $\Natural$. Then $\operatorname{truncateTo}$ applied to $C$ is a homomorphism of the action of the truncation and $C$ and the action of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to $V$ and $\operatorname{X}$ applied to $C$ and $0$ defined as $\operatorname{symm}$ applied to the single equivalence of the action of the truncation and $C$ and $\operatorname{X}$ applied to $C$ and $0$ and $\operatorname{d}$ applied to $C$, $1$ and $0$.

CochainComplex.augmentdefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a cochain complex of $V$ and $\Natural$. Let $f$ be a homomorphism of $X$ and $\operatorname{X}$ applied to $C$ and $0$ such that the composition of $f$ and $\operatorname{d}$ applied to $C$, $0$ and $1$ is equal to $0$. Then $\operatorname{augment}$ applied to $C$, $f$ and $w$ is a cochain complex of $V$ and $\Natural$.

CochainComplex.augmentTruncatedefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a cochain complex of $V$ and $\Natural$. Then $\operatorname{augmentTruncate}$ applied to $C$ is an isomorphism of $\operatorname{augment}$ applied to the action of the truncation and $C$, $\operatorname{d}$ applied to $C$, $0$ and $1$ and $\mathrm{HomologicalComplex\_\_d\_comp\_d}$ applied to $C$, $0$, $1$ and $1 + 1$ and $C$.

CochainComplex.fromSingle₀AsComplexdefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a cochain complex of $V$ and $\Natural$. Let $X$ be an element of $V$. Let $f$ be a homomorphism of the action of $\mathrm{CochainComplex\_\_single\_u2080\_}$ applied to $V$ and $X$ and $C$. Then $\mathrm{CochainComplex\_\_fromSingle\_u2080\_AsComplex}$ applied to $C$, $X$ and $f$ is a cochain complex of $V$ and $\Natural$.

CochainComplex.toTruncatedefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a cochain complex of $V$ and $\Natural$. Then $\operatorname{toTruncate}$ applied to $C$ is a homomorphism of the action of $\mathrm{CochainComplex\_\_single\_u2080\_}$ applied to $V$ and $\operatorname{X}$ applied to $C$ and $0$ and the action of the truncation and $C$ defined as $\operatorname{symm}$ applied to $\mathrm{CochainComplex\_\_fromSingle\_u2080\_Equiv}$ applied to the action of the truncation and $C$ and $\operatorname{X}$ applied to $C$ and $0$ and $\operatorname{d}$ applied to $C$, $0$ and $1$.

CochainComplex.truncatedefMathlib.Algebra.Homology.Augment, function or constant

Wording

the truncation (from the docstring)

English

The truncation is a functor of the set of cochain complexes of $V$ and $\Natural$ and the set of cochain complexes of $V$ and $\Natural$.

CochainComplex.truncateAugmentdefMathlib.Algebra.Homology.Augment, function or constant

Wording

no wording

English

Let $C$ be a cochain complex of $V$ and $\Natural$. Let $f$ be a homomorphism of $X$ and $\operatorname{X}$ applied to $C$ and $0$ such that the composition of $f$ and $\operatorname{d}$ applied to $C$, $0$ and $1$ is equal to $0$. Then $\operatorname{truncateAugment}$ applied to $C$, $f$ and $w$ is an isomorphism of the action of the truncation and $\operatorname{augment}$ applied to $C$, $f$ and $w$ and $C$.

Mathlib.Algebra.Homology.Bifunctor

CategoryTheory.Functor.mapBifunctorHomologicalComplexdefMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

the map bifunctor homological complex of x10 and x11 (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $x_{10}$ be a complex shape of $x_{8}$. Let $x_{11}$ be a complex shape of $x_{9}$. Then the map bifunctor homological complex of $x_{10}$ and $x_{11}$ is a functor of the set of homological complexes of $x$ and $x_{10}$ and the set of functors of the set of homological complexes of $x_{1}$ and $x_{11}$ and the set of homological complexes of $x_{10}$ and $x_{11}$.

CategoryTheory.Functor.map₂CochainComplexdefMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

the map cochain complex of F (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Then the map cochain complex of $F$ is a functor of the set of cochain complexes of $x$ and $\Integer$ and the set of functors of the set of cochain complexes of $x_{1}$ and $\Integer$ and the set of cochain complexes of $D$ and $\Integer$ defined as the map homological complex of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$.

CategoryTheory.Functor.map₂HomologicalComplexdefMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

the map homological complex of x11 and c (from the name)

English

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $x_{10}$ be a complex shape of $x_{8}$. Let $x_{11}$ be a complex shape of $x_{9}$. Let $c$ be a complex shape of $J$. Then the map homological complex of $x_{11}$ and $c$ is a functor of the set of homological complexes of $x$ and $x_{10}$ and the set of functors of the set of homological complexes of $x_{1}$ and $x_{11}$ and the set of homological complexes of $D$ and $c$.

HomologicalComplex.HasMapBifunctordefMathlib.Algebra.Homology.Bifunctor, predicate

Wording

no wording

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Then $\operatorname{HasMapBifunctor}$ holds for $x_{12}$, $x_{13}$, $F$ and $c$, if $\mathrm{HomologicalComplex\_u2082\_\_\_HasTotal}$ holds for the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$ and $c$.

HomologicalComplex.mapBifunctordefMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

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

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Then the map bifunctor of $F$ and $c$ is a homological complex of $D$ and $c$ defined as the total complex of the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$ and $c$.

HomologicalComplex.mapBifunctor.D₁defMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

no wording

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Let $j$ and $\mathrm{j'}$ be elements of $J$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_\_D\_u2081\_}$ applied to $x_{12}$, $x_{13}$, $F$, $c$, $j$ and $\mathrm{j'}$ is a homomorphism of $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $j$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $\mathrm{j'}$ defined as $\mathrm{HomologicalComplex\_u2082\_\_\_D\_u2081\_}$ applied to the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$, $c$, $j$ and $\mathrm{j'}$.

HomologicalComplex.mapBifunctor.D₂defMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

no wording

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Let $j$ and $\mathrm{j'}$ be elements of $J$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_\_D\_u2082\_}$ applied to $x_{12}$, $x_{13}$, $F$, $c$, $j$ and $\mathrm{j'}$ is a homomorphism of $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $j$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $\mathrm{j'}$ defined as $\mathrm{HomologicalComplex\_u2082\_\_\_D\_u2082\_}$ applied to the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$, $c$, $j$ and $\mathrm{j'}$.

HomologicalComplex.mapBifunctor.d₁defMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

no wording

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Let $x_{16}$ be an element of $x_{5}$. Let $x_{17}$ be an element of $x_{6}$. Let $j$ be an element of $J$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_\_d\_u2081\_}$ applied to $x_{12}$, $x_{13}$, $F$, $c$, $x_{16}$, $x_{17}$ and $j$ is a homomorphism of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{12}$ and $x_{16}$ and $\operatorname{X}$ applied to $x_{13}$ and $x_{17}$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $j$ defined as $\mathrm{HomologicalComplex\_u2082\_\_\_d\_u2081\_}$ applied to the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$, $c$, $x_{16}$, $x_{17}$ and $j$.

HomologicalComplex.mapBifunctor.d₂defMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

no wording

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Let $x_{16}$ be an element of $x_{5}$. Let $x_{17}$ be an element of $x_{6}$. Let $j$ be an element of $J$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_\_d\_u2082\_}$ applied to $x_{12}$, $x_{13}$, $F$, $c$, $x_{16}$, $x_{17}$ and $j$ is a homomorphism of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{12}$ and $x_{16}$ and $\operatorname{X}$ applied to $x_{13}$ and $x_{17}$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $j$ defined as $\mathrm{HomologicalComplex\_u2082\_\_\_d\_u2082\_}$ applied to the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$, $c$, $x_{16}$, $x_{17}$ and $j$.

HomologicalComplex.mapBifunctorDescdefMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

no wording

English

Let $f$ be a function from elements $x_{16}$ of $x_{5}$ and elements $x_{17}$ of $x_{6}$ and elements of $\mathrm{Proof}$ applied to the proposition that the projection of $c$ and $\ProdmkMACRoU {x_{16}}{x_{17}}$ is equal to $j$ to homomorphisms of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{12}$ and $x_{16}$ and $\operatorname{X}$ applied to $x_{13}$ and $x_{17}$ and $A$. Then $\operatorname{mapBifunctorDesc}$ applied to $x_{16}$, $x_{17}$ and $f$ is a homomorphism of $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $j$ and $A$ defined as the function that maps $x_{17}$ and $f$ to $\mathrm{HomologicalComplex\_u2082\_\_\_totalDesc}$ applied to the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$, $x_{16}$, $x_{17}$ and $f$.

HomologicalComplex.mapBifunctorMapdefMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

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

English

Let $x_{16}$ be a homomorphism of $x_{12}$ and $x_{13}$. Let $x_{17}$ be a homomorphism of $x_{14}$ and $x_{15}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Then the map bifunctor map of $F$ and $c$ is a homomorphism of the map bifunctor of $F$ and $c$ and the map bifunctor of $F$ and $c$ defined as the map of the composition of the component of the map of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{16}$ and $x_{14}$ and the map of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{13}$ and $x_{17}$ and $c$.

HomologicalComplex.ιMapBifunctordefMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

the inclusion of x12 (from the docstring)

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Let $x_{16}$ be an element of $x_{5}$. Let $x_{17}$ be an element of $x_{6}$. Let $j$ be an element of $J$ such that the projection of $c$ and $\ProdmkMACRoU {x_{16}}{x_{17}}$ is equal to $j$. Then the inclusion of $x_{12}$ is a homomorphism of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{12}$ and $x_{16}$ and $\operatorname{X}$ applied to $x_{13}$ and $x_{17}$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $j$ defined as $\mathrm{HomologicalComplex\_u2082\_\_\_\_u3b9\_Total}$ applied to the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$, $c$, $x_{16}$, $x_{17}$, $j$ and $h_{3}$.

HomologicalComplex.ιMapBifunctorOrZerodefMathlib.Algebra.Homology.Bifunctor, function or constant

Wording

the inclusion of x12 (from the docstring)

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Let $x_{16}$ be an element of $x_{5}$. Let $x_{17}$ be an element of $x_{6}$. Let $j$ be an element of $J$. Then the inclusion of $x_{12}$ is a homomorphism of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{12}$ and $x_{16}$ and $\operatorname{X}$ applied to $x_{13}$ and $x_{17}$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $c$ and $j$ defined as $\mathrm{HomologicalComplex\_u2082\_\_\_\_u3b9\_TotalOrZero}$ applied to the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$, $c$, $x_{16}$, $x_{17}$ and $j$.

Mathlib.Algebra.Homology.BifunctorAssociator

HomologicalComplex.HasGoodTrifunctor₁₂ObjdefMathlib.Algebra.Homology.BifunctorAssociator, predicate

Wording

no wording

English

Let $x_{13}$ 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 $x_{4}$. Let $x_{22}$ be a homological complex of $x$ and $x_{19}$. Let $x_{23}$ be a homological complex of $x_{1}$ and $x_{20}$. Let $x_{24}$ be a homological complex of $x_{3}$ and $x_{21}$. Let $x_{25}$ be a complex shape of $x_{17}$. Let $x_{26}$ be a complex shape of $x_{18}$. Then $\mathrm{HomologicalComplex\_\_HasGoodTrifunctor\_u2081\_\_u2082\_Obj}$ holds for $x_{13}$, $G$, $x_{22}$, $x_{23}$, $x_{24}$, $x_{25}$ and $x_{26}$, if $\mathrm{CategoryTheory\_\_GradedObject\_\_HasGoodTrifunctor\_u2081\_\_u2082\_Obj}$ holds for $x_{13}$, $G$, $\mathrm{ComplexShape\_\_\_u3c1\_\_u2081\_\_u2082\_}$ applied to $x_{19}$, $x_{20}$, $x_{21}$, $x_{25}$ and $x_{26}$, $\operatorname{X}$ applied to $x_{22}$, $\operatorname{X}$ applied to $x_{23}$ and $\operatorname{X}$ applied to $x_{24}$.

HomologicalComplex.HasGoodTrifunctor₂₃ObjdefMathlib.Algebra.Homology.BifunctorAssociator, predicate

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{13}$ be a functor of $x_{1}$ and the set of functors of $x_{3}$ and $x_{2}$. Let $x_{23}$ be a homological complex of $x$ and $x_{20}$. Let $x_{24}$ be a homological complex of $x_{1}$ and $x_{21}$. Let $x_{25}$ be a homological complex of $x_{3}$ and $x_{22}$. Let $x_{26}$ be a complex shape of $x_{17}$. Let $x_{27}$ be a complex shape of $x_{18}$. Let $x_{28}$ be a complex shape of $x_{19}$. Then $\mathrm{HomologicalComplex\_\_HasGoodTrifunctor\_u2082\_\_u2083\_Obj}$ holds for $F$, $x_{13}$, $x_{23}$, $x_{24}$, $x_{25}$, $x_{26}$, $x_{27}$ and $x_{28}$, if $\mathrm{CategoryTheory\_\_GradedObject\_\_HasGoodTrifunctor\_u2082\_\_u2083\_Obj}$ holds for $F$, $x_{13}$, $\mathrm{ComplexShape\_\_\_u3c1\_\_u2082\_\_u2083\_}$ applied to $x_{20}$, $x_{21}$, $x_{22}$, $x_{26}$, $x_{27}$ and $x_{28}$, $\operatorname{X}$ applied to $x_{23}$, $\operatorname{X}$ applied to $x_{24}$ and $\operatorname{X}$ applied to $x_{25}$.

HomologicalComplex.mapBifunctorAssociatordefMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

the map bifunctor associator of x34 and x35 (from the name)

English

HomologicalComplex.mapBifunctorAssociatorXdefMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

the map bifunctor associator of x35 and j (from the name)

English

Let $\mathrm{associator}$ be an isomorphism of the bifunctor composition of $x_{18}$ and $G$ and the bifunctor composition of $F$ and $x_{19}$. Let $x_{30}$ be a homological complex of $x$ and $x_{27}$. Let $x_{31}$ be a homological complex of $x_{1}$ and $x_{28}$. Let $x_{32}$ be a homological complex of $x_{4}$ and $x_{29}$. Let $x_{33}$ be a complex shape of $x_{23}$. Let $x_{34}$ be a complex shape of $x_{24}$. Let $x_{35}$ be a complex shape of $x_{25}$. Let $j$ be an element of $x_{25}$. Then the map bifunctor associator of $x_{35}$ and $j$ is an isomorphism of $\operatorname{X}$ applied to the map bifunctor of $G$ and $x_{35}$ and $j$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{35}$ and $j$ defined as the map isomorphism of the evaluation of $j$ and the map bifunctor associator of $\operatorname{X}$ applied to $x_{31}$ and $\operatorname{X}$ applied to $x_{32}$.

HomologicalComplex.mapBifunctor₁₂.D₁defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

HomologicalComplex.mapBifunctor₁₂.D₂defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

HomologicalComplex.mapBifunctor₁₂.D₃defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

HomologicalComplex.mapBifunctor₁₂.d₁defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $x_{15}$ 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 $x_{4}$. Let $x_{25}$ be a homological complex of $x$ and $x_{22}$. Let $x_{26}$ be a homological complex of $x_{1}$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{3}$ and $x_{24}$. Let $x_{28}$ be a complex shape of $x_{19}$. Let $x_{29}$ be a complex shape of $x_{20}$. Let $x_{33}$ be an element of $x_{16}$. Let $x_{34}$ be an element of $x_{17}$. Let $x_{35}$ be an element of $x_{18}$. Let $j$ be an element of $x_{20}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2081\_\_u2082\_\_\_d\_u2081\_}$ applied to $x_{15}$, $G$, $x_{25}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{33}$, $x_{34}$, $x_{35}$ and $j$ is a homomorphism of the action of the action of $G$ and the action of the action of $x_{15}$ and $\operatorname{X}$ applied to $x_{25}$ and $x_{33}$ and $\operatorname{X}$ applied to $x_{26}$ and $x_{34}$ and $\operatorname{X}$ applied to $x_{27}$ and $x_{35}$ and $\operatorname{X}$ applied to the map bifunctor of $G$ and $x_{29}$ and $j$ defined as $\HSMulhSMulMACRoAL {(\mathrm{ComplexShape\_\_\_u3b5\_\_u2081\_} (x_{28} , x_{24} , x_{29} , \ProdmkMACRoU {\mathrm{ComplexShape\_\_\_u3c0\_} (x_{28} , \ProdmkMACRoU {x_{33}}{x_{34}})}{x_{35}})\times \mathrm{ComplexShape\_\_\_u3b5\_\_u2081\_} (x_{22} , x_{23} , x_{28} , \ProdmkMACRoU {x_{33}}{x_{34}}))}{\operatorname{comp} (\operatorname{NatTrans} (\operatorname{map} (G , \operatorname{NatTrans} (\operatorname{map} (x_{15} , \operatorname{d} (x_{25} , x_{33} , \operatorname{next} (x_{22} , x_{33}))), \operatorname{X} (x_{26} , x_{34}))), \operatorname{X} (x_{27} , x_{35})), \mathrm{HomologicalComplex\_\_mapBifunctor\_u2081\_\_u2082\_\_\_\_u3b9\_OrZero} (x_{15}))}$.

HomologicalComplex.mapBifunctor₁₂.d₂defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $x_{15}$ 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 $x_{4}$. Let $x_{25}$ be a homological complex of $x$ and $x_{22}$. Let $x_{26}$ be a homological complex of $x_{1}$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{3}$ and $x_{24}$. Let $x_{28}$ be a complex shape of $x_{19}$. Let $x_{29}$ be a complex shape of $x_{20}$. Let $x_{33}$ be an element of $x_{16}$. Let $x_{34}$ be an element of $x_{17}$. Let $x_{35}$ be an element of $x_{18}$. Let $j$ be an element of $x_{20}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2081\_\_u2082\_\_\_d\_u2082\_}$ applied to $x_{15}$, $G$, $x_{25}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{33}$, $x_{34}$, $x_{35}$ and $j$ is a homomorphism of the action of the action of $G$ and the action of the action of $x_{15}$ and $\operatorname{X}$ applied to $x_{25}$ and $x_{33}$ and $\operatorname{X}$ applied to $x_{26}$ and $x_{34}$ and $\operatorname{X}$ applied to $x_{27}$ and $x_{35}$ and $\operatorname{X}$ applied to the map bifunctor of $G$ and $x_{29}$ and $j$ defined as $\HSMulhSMulMACRoAL {(\mathrm{ComplexShape\_\_\_u3b5\_\_u2081\_} (x_{28} , x_{24} , x_{29} , \ProdmkMACRoU {\mathrm{ComplexShape\_\_\_u3c0\_} (x_{28} , \ProdmkMACRoU {x_{33}}{x_{34}})}{x_{35}})\times \mathrm{ComplexShape\_\_\_u3b5\_\_u2082\_} (x_{22} , x_{23} , x_{28} , \ProdmkMACRoU {x_{33}}{x_{34}}))}{\operatorname{comp} (\operatorname{NatTrans} (\operatorname{map} (G , \operatorname{map} (\operatorname{obj} (x_{15} , \operatorname{X} (x_{25} , x_{33})), \operatorname{d} (x_{26} , x_{34} , \operatorname{next} (x_{23} , x_{34})))), \operatorname{X} (x_{27} , x_{35})), \mathrm{HomologicalComplex\_\_mapBifunctor\_u2081\_\_u2082\_\_\_\_u3b9\_OrZero} (x_{15}))}$.

HomologicalComplex.mapBifunctor₁₂.d₃defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $x_{15}$ 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 $x_{4}$. Let $x_{25}$ be a homological complex of $x$ and $x_{22}$. Let $x_{26}$ be a homological complex of $x_{1}$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{3}$ and $x_{24}$. Let $x_{28}$ be a complex shape of $x_{19}$. Let $x_{29}$ be a complex shape of $x_{20}$. Let $x_{33}$ be an element of $x_{16}$. Let $x_{34}$ be an element of $x_{17}$. Let $x_{35}$ be an element of $x_{18}$. Let $j$ be an element of $x_{20}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2081\_\_u2082\_\_\_d\_u2083\_}$ applied to $x_{15}$, $G$, $x_{25}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{33}$, $x_{34}$, $x_{35}$ and $j$ is a homomorphism of the action of the action of $G$ and the action of the action of $x_{15}$ and $\operatorname{X}$ applied to $x_{25}$ and $x_{33}$ and $\operatorname{X}$ applied to $x_{26}$ and $x_{34}$ and $\operatorname{X}$ applied to $x_{27}$ and $x_{35}$ and $\operatorname{X}$ applied to the map bifunctor of $G$ and $x_{29}$ and $j$ defined as $\HSMulhSMulMACRoAL {\mathrm{ComplexShape\_\_\_u3b5\_\_u2082\_} (x_{28} , x_{24} , x_{29} , \ProdmkMACRoU {\mathrm{ComplexShape\_\_\_u3c0\_} (x_{28} , \ProdmkMACRoU {x_{33}}{x_{34}})}{x_{35}})}{\operatorname{comp} (\operatorname{map} (\operatorname{obj} (G , \operatorname{obj} (\operatorname{obj} (x_{15} , \operatorname{X} (x_{25} , x_{33})), \operatorname{X} (x_{26} , x_{34}))), \operatorname{d} (x_{27} , x_{35} , \operatorname{next} (x_{24} , x_{35}))), \mathrm{HomologicalComplex\_\_mapBifunctor\_u2081\_\_u2082\_\_\_\_u3b9\_OrZero} (x_{15}))}$.

HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂DescdefMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $f$ be a function from elements $x_{33}$ of $x_{16}$ and elements $x_{34}$ of $x_{17}$ and elements $x_{35}$ of $x_{18}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{r} (x_{22} , x_{23} , x_{24} , x_{28} , x_{29} , \ProdmkMACRoU {x_{33}}{(\ProdmkMACRoU {x_{34}}{x_{35}})})}{j}$ to homomorphisms of the action of the action of $G$ and the action of the action of $x_{15}$ and $\operatorname{X}$ applied to $x_{25}$ and $x_{33}$ and $\operatorname{X}$ applied to $x_{26}$ and $x_{34}$ and $\operatorname{X}$ applied to $x_{27}$ and $x_{35}$ and $A$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2081\_\_u2082\_\_\_mapBifunctor\_u2081\_\_u2082\_Desc}$ applied to $x_{33}$, $x_{34}$, $x_{35}$ and $f$ is a homomorphism of $\operatorname{X}$ applied to the map bifunctor of $G$ and $x_{29}$ and $j$ and $A$ defined as the function that maps $x_{34}$, $x_{35}$ and $f$ to $\mathrm{CategoryTheory\_\_GradedObject\_\_mapBifunctor\_u2081\_\_u2082\_BifunctorDesc}$ applied to $x_{33}$, $x_{34}$, $x_{35}$ and $f$.

HomologicalComplex.mapBifunctor₁₂.ιdefMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

the inclusion in x15 (from the docstring)

English

HomologicalComplex.mapBifunctor₁₂.ιOrZerodefMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

the inclusion in x15 (from the docstring)

English

HomologicalComplex.mapBifunctor₂₃.D₁defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{1}$ and the set of functors of $x_{3}$ and $x_{2}$. Let $x_{25}$ be a homological complex of $x$ and $x_{22}$. Let $x_{26}$ be a homological complex of $x_{1}$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{3}$ and $x_{24}$. Let $x_{28}$ be a complex shape of $x_{19}$. Let $x_{29}$ be a complex shape of $x_{20}$. Let $j$ and $\mathrm{j'}$ be elements of $x_{20}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_D\_u2081\_}$ applied to $F$, $x_{15}$, $x_{25}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $j$ and $\mathrm{j'}$ is a homomorphism of $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{29}$ and $j$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{29}$ and $\mathrm{j'}$ defined as $\mathrm{HomologicalComplex\_\_mapBifunctor\_\_D\_u2081\_}$ applied to $x_{25}$, the map bifunctor of $x_{15}$ and $x_{28}$, $F$, $x_{29}$, $j$ and $\mathrm{j'}$.

HomologicalComplex.mapBifunctor₂₃.D₂defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{1}$ and the set of functors of $x_{3}$ and $x_{2}$. Let $x_{26}$ be a homological complex of $x$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{1}$ and $x_{24}$. Let $x_{28}$ be a homological complex of $x_{3}$ and $x_{25}$. Let $x_{29}$ be a complex shape of $x_{19}$. Let $x_{30}$ be a complex shape of $x_{20}$. Let $x_{31}$ be a complex shape of $x_{21}$. Let $j$ and $\mathrm{j'}$ be elements of $x_{21}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_D\_u2082\_}$ applied to $F$, $x_{15}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{30}$, $x_{31}$, $j$ and $\mathrm{j'}$ is a homomorphism of $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{31}$ and $j$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{31}$ and $\mathrm{j'}$ defined as $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_mapBifunctor\_u2082\_\_u2083\_Desc}$ applied to $x_{29}$ and the function that maps $x_{37}$, $x_{38}$, $x_{39}$ and $h_{8}$ to $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_d\_u2082\_}$ applied to $F$, $x_{15}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{30}$, $x_{31}$, $x_{37}$, $x_{38}$, $x_{39}$ and $\mathrm{j'}$.

HomologicalComplex.mapBifunctor₂₃.D₃defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{1}$ and the set of functors of $x_{3}$ and $x_{2}$. Let $x_{26}$ be a homological complex of $x$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{1}$ and $x_{24}$. Let $x_{28}$ be a homological complex of $x_{3}$ and $x_{25}$. Let $x_{29}$ be a complex shape of $x_{19}$. Let $x_{30}$ be a complex shape of $x_{20}$. Let $x_{31}$ be a complex shape of $x_{21}$. Let $j$ and $\mathrm{j'}$ be elements of $x_{21}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_D\_u2083\_}$ applied to $F$, $x_{15}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{30}$, $x_{31}$, $j$ and $\mathrm{j'}$ is a homomorphism of $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{31}$ and $j$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{31}$ and $\mathrm{j'}$ defined as $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_mapBifunctor\_u2082\_\_u2083\_Desc}$ applied to $x_{29}$ and the function that maps $x_{37}$, $x_{38}$, $x_{39}$ and $h_{8}$ to $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_d\_u2083\_}$ applied to $F$, $x_{15}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{30}$, $x_{31}$, $x_{37}$, $x_{38}$, $x_{39}$ and $\mathrm{j'}$.

HomologicalComplex.mapBifunctor₂₃.d₁defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{1}$ and the set of functors of $x_{3}$ and $x_{2}$. Let $x_{26}$ be a homological complex of $x$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{1}$ and $x_{24}$. Let $x_{28}$ be a homological complex of $x_{3}$ and $x_{25}$. Let $x_{29}$ be a complex shape of $x_{19}$. Let $x_{30}$ be a complex shape of $x_{20}$. Let $x_{31}$ be a complex shape of $x_{21}$. Let $x_{37}$ be an element of $x_{16}$. Let $x_{38}$ be an element of $x_{17}$. Let $x_{39}$ be an element of $x_{18}$. Let $j$ be an element of $x_{21}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_d\_u2081\_}$ applied to $F$, $x_{15}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{30}$, $x_{31}$, $x_{37}$, $x_{38}$, $x_{39}$ and $j$ is a homomorphism of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{26}$ and $x_{37}$ and the action of the action of $x_{15}$ and $\operatorname{X}$ applied to $x_{27}$ and $x_{38}$ and $\operatorname{X}$ applied to $x_{28}$ and $x_{39}$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{31}$ and $j$ defined as $\HSMulhSMulMACRoAL {\mathrm{ComplexShape\_\_\_u3b5\_\_u2081\_} (x_{23} , x_{30} , x_{31} , \ProdmkMACRoU {x_{37}}{\mathrm{ComplexShape\_\_\_u3c0\_} (x_{30} , \ProdmkMACRoU {x_{38}}{x_{39}})})}{\operatorname{comp} (\operatorname{NatTrans} (\operatorname{map} (F , \operatorname{d} (x_{26} , x_{37} , \operatorname{next} (x_{23} , x_{37}))), \operatorname{obj} (\operatorname{obj} (x_{15} , \operatorname{X} (x_{27} , x_{38})), \operatorname{X} (x_{28} , x_{39}))), \mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_\_u3b9\_OrZero} (F))}$.

HomologicalComplex.mapBifunctor₂₃.d₂defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{1}$ and the set of functors of $x_{3}$ and $x_{2}$. Let $x_{26}$ be a homological complex of $x$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{1}$ and $x_{24}$. Let $x_{28}$ be a homological complex of $x_{3}$ and $x_{25}$. Let $x_{29}$ be a complex shape of $x_{19}$. Let $x_{30}$ be a complex shape of $x_{20}$. Let $x_{31}$ be a complex shape of $x_{21}$. Let $x_{37}$ be an element of $x_{16}$. Let $x_{38}$ be an element of $x_{17}$. Let $x_{39}$ be an element of $x_{18}$. Let $j$ be an element of $x_{21}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_d\_u2082\_}$ applied to $F$, $x_{15}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{30}$, $x_{31}$, $x_{37}$, $x_{38}$, $x_{39}$ and $j$ is a homomorphism of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{26}$ and $x_{37}$ and the action of the action of $x_{15}$ and $\operatorname{X}$ applied to $x_{27}$ and $x_{38}$ and $\operatorname{X}$ applied to $x_{28}$ and $x_{39}$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{31}$ and $j$ defined as $\HSMulhSMulMACRoAL {(\mathrm{ComplexShape\_\_\_u3b5\_\_u2082\_} (x_{23} , x_{30} , x_{31} , \ProdmkMACRoU {x_{37}}{\mathrm{ComplexShape\_\_\_u3c0\_} (x_{30} , \ProdmkMACRoU {x_{38}}{x_{39}})})\times \mathrm{ComplexShape\_\_\_u3b5\_\_u2081\_} (x_{24} , x_{25} , x_{30} , \ProdmkMACRoU {x_{38}}{x_{39}}))}{\operatorname{comp} (\operatorname{map} (\operatorname{obj} (F , \operatorname{X} (x_{26} , x_{37})), \operatorname{NatTrans} (\operatorname{map} (x_{15} , \operatorname{d} (x_{27} , x_{38} , \operatorname{next} (x_{24} , x_{38}))), \operatorname{X} (x_{28} , x_{39}))), \mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_\_u3b9\_OrZero} (F))}$.

HomologicalComplex.mapBifunctor₂₃.d₃defMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $F$ be a functor of $x$ and the set of functors of $x_{2}$ and $x_{4}$. Let $x_{15}$ be a functor of $x_{1}$ and the set of functors of $x_{3}$ and $x_{2}$. Let $x_{26}$ be a homological complex of $x$ and $x_{23}$. Let $x_{27}$ be a homological complex of $x_{1}$ and $x_{24}$. Let $x_{28}$ be a homological complex of $x_{3}$ and $x_{25}$. Let $x_{29}$ be a complex shape of $x_{19}$. Let $x_{30}$ be a complex shape of $x_{20}$. Let $x_{31}$ be a complex shape of $x_{21}$. Let $x_{37}$ be an element of $x_{16}$. Let $x_{38}$ be an element of $x_{17}$. Let $x_{39}$ be an element of $x_{18}$. Let $j$ be an element of $x_{21}$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_d\_u2083\_}$ applied to $F$, $x_{15}$, $x_{26}$, $x_{27}$, $x_{28}$, $x_{29}$, $x_{30}$, $x_{31}$, $x_{37}$, $x_{38}$, $x_{39}$ and $j$ is a homomorphism of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{26}$ and $x_{37}$ and the action of the action of $x_{15}$ and $\operatorname{X}$ applied to $x_{27}$ and $x_{38}$ and $\operatorname{X}$ applied to $x_{28}$ and $x_{39}$ and $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{31}$ and $j$ defined as $\HSMulhSMulMACRoAL {(\mathrm{ComplexShape\_\_\_u3b5\_\_u2082\_} (x_{23} , x_{30} , x_{31} , \ProdmkMACRoU {x_{37}}{\mathrm{ComplexShape\_\_\_u3c0\_} (x_{30} , \ProdmkMACRoU {x_{38}}{x_{39}})})\times \mathrm{ComplexShape\_\_\_u3b5\_\_u2082\_} (x_{24} , x_{25} , x_{30} , \ProdmkMACRoU {x_{38}}{x_{39}}))}{\operatorname{comp} (\operatorname{map} (\operatorname{obj} (F , \operatorname{X} (x_{26} , x_{37})), \operatorname{map} (\operatorname{obj} (x_{15} , \operatorname{X} (x_{27} , x_{38})), \operatorname{d} (x_{28} , x_{39} , \operatorname{next} (x_{25} , x_{39})))), \mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_\_u3b9\_OrZero} (F))}$.

HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃DescdefMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

no wording

English

Let $x_{29}$ be a complex shape of $x_{19}$. Let $f$ be a function from elements $x_{37}$ of $x_{16}$ and elements $x_{38}$ of $x_{17}$ and elements $x_{39}$ of $x_{18}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{r} (x_{23} , x_{24} , x_{25} , x_{29} , x_{31} , \ProdmkMACRoU {x_{37}}{(\ProdmkMACRoU {x_{38}}{x_{39}})})}{j}$ to homomorphisms of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{26}$ and $x_{37}$ and the action of the action of $x_{15}$ and $\operatorname{X}$ applied to $x_{27}$ and $x_{38}$ and $\operatorname{X}$ applied to $x_{28}$ and $x_{39}$ and $A$. Then $\mathrm{HomologicalComplex\_\_mapBifunctor\_u2082\_\_u2083\_\_\_mapBifunctor\_u2082\_\_u2083\_Desc}$ applied to $x_{29}$, $x_{37}$, $x_{38}$, $x_{39}$ and $f$ is a homomorphism of $\operatorname{X}$ applied to the map bifunctor of $F$ and $x_{31}$ and $j$ and $A$ defined as the function that maps $x_{38}$, $x_{39}$ and $f$ to $\mathrm{CategoryTheory\_\_GradedObject\_\_mapBifunctorBifunctor\_u2082\_\_u2083\_Desc}$ applied to $x_{37}$, $x_{38}$, $x_{39}$ and $f$.

HomologicalComplex.mapBifunctor₂₃.ιdefMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

the inclusion in F (from the docstring)

English

HomologicalComplex.mapBifunctor₂₃.ιOrZerodefMathlib.Algebra.Homology.BifunctorAssociator, function or constant

Wording

the inclusion in F (from the docstring)

English

Mathlib.Algebra.Homology.BifunctorFlip

HomologicalComplex.mapBifunctorFlipIsodefMathlib.Algebra.Homology.BifunctorFlip, function or constant

Wording

the map bifunctor flip isomorphism of F and c (from the name)

English

Let $x_{12}$ be a homological complex of $x$ and $x_{7}$. Let $x_{13}$ be a homological complex of $x_{1}$ and $x_{8}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Then the map bifunctor flip isomorphism of $F$ and $c$ is an isomorphism of the map bifunctor of the flip of $F$ and $c$ and the map bifunctor of $F$ and $c$ defined as the symmetry isomorphism of the action of the action of the map bifunctor homological complex of $x_{7}$ and $x_{8}$ and $x_{12}$ and $x_{13}$ and $c$.

Mathlib.Algebra.Homology.BifunctorHomotopy

HomologicalComplex.mapBifunctorMapHomotopy₁defMathlib.Algebra.Homology.BifunctorHomotopy, function or constant

Wording

the map bifunctor map homotopy of F and c (from the name)

English

Let $x_{16}$ be a homotopy of $x_{14}$ and $x_{15}$. Let $x_{19}$ be a homomorphism of $x_{17}$ and $x_{18}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Then the map bifunctor map homotopy of $F$ and $c$ is a homotopy of the map bifunctor map of $F$ and $c$ and the map bifunctor map of $F$ and $c$ defined as $\operatorname{mk}$ applied to $\mathrm{HomologicalComplex\_\_mapBifunctorMapHomotopy\_\_hom\_u2081\_}$ applied to $x_{16}$, $x_{19}$, $F$ and $c$, $\mathrm{HomologicalComplex\_\_mapBifunctorMapHomotopy\_\_zero\_u2081\_}$ applied to $x_{16}$, $x_{19}$, $F$ and $c$ and $\mathrm{HomologicalComplex\_\_mapBifunctorMapHomotopy\_\_comm\_u2081\_}$ applied to $x_{16}$, $x_{19}$, $F$ and $c$.

HomologicalComplex.mapBifunctorMapHomotopy₂defMathlib.Algebra.Homology.BifunctorHomotopy, function or constant

Wording

the map bifunctor map homotopy of F and c (from the name)

English

Let $x_{14}$ be a homomorphism of $x_{12}$ and $x_{13}$. Let $x_{19}$ be a homotopy of $x_{17}$ and $x_{18}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $c$ be a complex shape of $J$. Then the map bifunctor map homotopy of $F$ and $c$ is a homotopy of the map bifunctor map of $F$ and $c$ and the map bifunctor map of $F$ and $c$.

Mathlib.Algebra.Homology.BifunctorShift

CochainComplex.HasMapBifunctordefMathlib.Algebra.Homology.BifunctorShift, predicate

Wording

no wording

English

Let $x_{7}$ be a cochain complex of $x$ and $\Integer$. Let $x_{8}$ be a cochain complex of $x_{1}$ and $\Integer$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Then $\operatorname{HasMapBifunctor}$ holds for $x_{7}$, $x_{8}$ and $F$, if $\operatorname{HasMapBifunctor}$ holds for $x_{7}$, $x_{8}$, $F$ and $\operatorname{up}$ applied to $\Integer$.

CochainComplex.mapBifunctordefMathlib.Algebra.Homology.BifunctorShift, function or constant

Wording

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

English

Let $x_{7}$ be a cochain complex of $x$ and $\Integer$. Let $x_{8}$ be a cochain complex of $x_{1}$ and $\Integer$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Then the map bifunctor of $x_{8}$ and $F$ is a cochain complex of $D$ and $\Integer$ defined as the map bifunctor of $F$ and $\operatorname{up}$ applied to $\Integer$.

CochainComplex.mapBifunctorShift₁IsodefMathlib.Algebra.Homology.BifunctorShift, function or constant

Wording

the map bifunctor shift isomorphism of F and x10 (from the name)

English

Let $x_{8}$ be a cochain complex of $x$ and $\Integer$. Let $x_{9}$ be a cochain complex of $x_{1}$ and $\Integer$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $x_{10}$ be an integer. Then the map bifunctor shift isomorphism of $F$ and $x_{10}$ is an isomorphism of the map bifunctor of $x_{9}$ and $F$ and the action of the shift functor of the set of cochain complexes of $D$ and $\Integer$ and $x_{10}$ and the map bifunctor of $x_{9}$ and $F$ defined as the composition of the isomorphism of $\mathrm{CochainComplex\_\_mapBifunctorHomologicalComplexShift\_u2081\_Iso}$ applied to $x_{8}$, $x_{9}$, $F$ and $x_{10}$ and $\operatorname{up}$ applied to $\Integer$ and the isomorphism of the action of the action of the map bifunctor homological complex of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$ and $x_{8}$ and $x_{9}$ and $x_{10}$.

CochainComplex.mapBifunctorShift₂IsodefMathlib.Algebra.Homology.BifunctorShift, function or constant

Wording

the map bifunctor shift isomorphism of F and y (from the name)

English

Let $x_{8}$ be a cochain complex of $x$ and $\Integer$. Let $x_{9}$ be a cochain complex of $x_{1}$ and $\Integer$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $y$ be an integer. Then the map bifunctor shift isomorphism of $F$ and $y$ is an isomorphism of the map bifunctor of the action of the shift functor of the set of cochain complexes of $x_{1}$ and $\Integer$ and $y$ and $x_{9}$ and $F$ and the action of the shift functor of the set of cochain complexes of $D$ and $\Integer$ and $y$ and the map bifunctor of $x_{9}$ and $F$ defined as the composition of the isomorphism of $\mathrm{CochainComplex\_\_mapBifunctorHomologicalComplexShift\_u2082\_Iso}$ applied to $x_{8}$, $x_{9}$, $F$ and $y$ and $\operatorname{up}$ applied to $\Integer$ and the isomorphism of the action of the action of the map bifunctor homological complex of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$ and $x_{8}$ and $x_{9}$ and $y$.

CochainComplex.ιMapBifunctordefMathlib.Algebra.Homology.BifunctorShift, function or constant

Wording

the inclusion map bifunctor of x11 and n (from the name)

English

Let $x_{7}$ be a cochain complex of $x$ and $\Integer$. Let $x_{8}$ be a cochain complex of $x_{1}$ and $\Integer$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $D$. Let $x_{10}$, $x_{11}$ and $n$ be integers such that $x_{10} + x_{11} = n$. Then the inclusion map bifunctor of $x_{11}$ and $n$ is a homomorphism of the action of the action of $F$ and $\operatorname{X}$ applied to $x_{7}$ and $x_{10}$ and $\operatorname{X}$ applied to $x_{8}$ and $x_{11}$ and $\operatorname{X}$ applied to the map bifunctor of $x_{8}$ and $F$ and $n$ defined as the inclusion of $x_{7}$.

Mathlib.Algebra.Homology.CochainComplexOpposite

ChainComplex.cochainComplexEquivalencedefMathlib.Algebra.Homology.CochainComplexOpposite, function or constant

Wording

the cochain complex equivalence of C (from the name)

English

Let $C$ be a set. Then the cochain complex equivalence of $C$ is an equivalence of the set of chain complexes of $C$ and $\Integer$ and the set of cochain complexes of $C$ and $\Integer$.

CochainComplex.homotopyOpdefMathlib.Algebra.Homology.CochainComplexOpposite, function or constant

Wording

the homotopy opposite of h (from the name)

English

Let $h$ be a homotopy of $f$ and $g$. Then the homotopy opposite of $h$ is a homotopy of the map of the functor of the opposite equivalence of $C$ and the opposite in $f$ and the map of the functor of the opposite equivalence of $C$ and the opposite in $g$.

CochainComplex.homotopyOpEquivdefMathlib.Algebra.Homology.CochainComplexOpposite, function or constant

Wording

the homotopy opposite equivalence (from the name)

English

The homotopy opposite equivalence is an equivalence from the set of homotopies of $f$ and $g$ to the set of homotopies of the map of the functor of the opposite equivalence of $C$ and the opposite in $f$ and the map of the functor of the opposite equivalence of $C$ and the opposite in $g$.

CochainComplex.homotopyUnopdefMathlib.Algebra.Homology.CochainComplexOpposite, function or constant

Wording

the homotopy opposite of h (from the name)

English

Let $h$ be a homotopy of the map of the functor of the opposite equivalence of $C$ and the opposite in $f$ and the map of the functor of the opposite equivalence of $C$ and the opposite in $g$. Then the homotopy opposite of $h$ is a homotopy of $f$ and $g$.

CochainComplex.opEquivalencedefMathlib.Algebra.Homology.CochainComplexOpposite, function or constant

Wording

the opposite equivalence of C (from the name)

English

Let $C$ be a set. Then the opposite equivalence of $C$ is an equivalence of the set of opposites of the set of cochain complexes of $C$ and $\Integer$ and the set of cochain complexes of the set of opposites of $C$ and $\Integer$ defined as the composition of the opposite equivalence of $C$ and $\operatorname{up}$ applied to $\Integer$ and the cochain complex equivalence of the set of opposites of $C$.

ComplexShape.embeddingDownIntUpIntdefMathlib.Algebra.Homology.CochainComplexOpposite, function or constant

Wording

the embedding of the complex shape (from the docstring)

English

The embedding of the complex shape is an embedding of $\operatorname{down}$ applied to $\Integer$ and $\operatorname{up}$ applied to $\Integer$.

ComplexShape.embeddingUpIntDownIntdefMathlib.Algebra.Homology.CochainComplexOpposite, function or constant

Wording

the embedding of the complex shape (from the docstring)

English

The embedding of the complex shape is an embedding of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{down}$ applied to $\Integer$.

Mathlib.Algebra.Homology.CochainComplexPlus

CategoryTheory.Functor.mapCochainComplexPlusdefMathlib.Algebra.Homology.CochainComplexPlus, function or constant

Wording

the map cochain complex plus of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the map cochain complex plus of $F$ is a functor of the set of pluses of $C$ and the set of pluses of $D$.

CategoryTheory.Functor.mapCochainComplexPlusCompιdefMathlib.Algebra.Homology.CochainComplexPlus, function or constant

Wording

the map cochain complex plus composition inclusion of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the map cochain complex plus composition inclusion of $F$ is an isomorphism of the composition of the map cochain complex plus of $F$ and the inclusion of the full subcategory of bounded below cochain complexes of $D$ and the composition of the inclusion of the full subcategory of bounded below cochain complexes of $C$ and the map homological complex of $F$ and $\operatorname{up}$ applied to $\Integer$ defined as the identity of the composition of the map cochain complex plus of $F$ and the inclusion of the full subcategory of bounded below cochain complexes of $D$.

CategoryTheory.NatTrans.mapCochainComplexPlusdefMathlib.Algebra.Homology.CochainComplexPlus, function or constant

Wording

the map cochain complex plus of x6 (from the name)

English

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{5}$. Then the map cochain complex plus of $x_{6}$ is a homomorphism of the map cochain complex plus of $x_{4}$ and the map cochain complex plus of $x_{5}$.

CochainComplex.PlusdefMathlib.Algebra.Homology.CochainComplexPlus, type

Wording

plus of C (from the name)

English

Let $C$ be a set. Then a plus of $C$ is an element of the function that maps $C$ to the set of full subcategories of the plus of $C$.

CochainComplex.Plus.fullyFaithfulιdefMathlib.Algebra.Homology.CochainComplexPlus, function or constant

Wording

the inclusion of the full subcategory of bounded below cochain complexes of C (from the docstring)

English

Let $C$ be a set. Then the inclusion of the full subcategory of bounded below cochain complexes of $C$ is an element of $\operatorname{FullyFaithful}$ applied to the inclusion of the full subcategory of bounded below cochain complexes of $C$ defined as the inclusion of the plus of $C$.

CochainComplex.Plus.quasiIsodefMathlib.Algebra.Homology.CochainComplexPlus, function or constant

Wording

no wording

English

Let $C$ be a set. Then there is a morphism property of the set of pluses of $C$. Proof. Let $C$ be arbitrary. By C. By Int. By ComplexShape__up. By HomologicalComplex__quasiIso. By C. By CochainComplex__Plus___u3b9_. By CategoryTheory__MorphismProperty__inverseImage.

CochainComplex.Plus.ιdefMathlib.Algebra.Homology.CochainComplexPlus, function or constant

Wording

the inclusion of the full subcategory of bounded below cochain complexes of C (from the docstring)

English

Let $C$ be a set. Then the inclusion of the full subcategory of bounded below cochain complexes of $C$ is a functor of the set of pluses of $C$ and the set of cochain complexes of $C$ and $\Integer$ defined as the inclusion of the plus of $C$.

CochainComplex.plusdefMathlib.Algebra.Homology.CochainComplexPlus, function or constant

Wording

the plus of C (from the name)

English

Let $C$ be a set. Then the plus of $C$ is an object property of the set of cochain complexes of $C$ and $\Integer$ defined as the function that maps $K$ to the proposition that there exists an integer $n$, such that $\operatorname{IsStrictlyGE}$ holds for $K$ and $n$.

Mathlib.Algebra.Homology.CommSq

CategoryTheory.CommSq.cokernelCoforkdefMathlib.Algebra.Homology.CommSq, function or constant

Wording

the cokernel cofork of sq (from the name)

English

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Then the cokernel cofork of $\mathrm{sq}$ is a cokernel cofork of the lift of $f$ and $\operatorname{neg}$ applied to $g$.

CategoryTheory.CommSq.isColimitEquivIsColimitCokernelCoforkdefMathlib.Algebra.Homology.CommSq, function or constant

Wording

no wording

English

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Then $\operatorname{isColimitEquivIsColimitCokernelCofork}$ applied to $\mathrm{sq}$ is an equivalence from $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\mathrm{inl}$, $\mathrm{inr}$ and $\operatorname{w}$ applied to $\mathrm{sq}$ to $\operatorname{IsColimit}$ applied to the cokernel cofork of $\mathrm{sq}$.

CategoryTheory.CommSq.isLimitEquivIsLimitKernelForkdefMathlib.Algebra.Homology.CommSq, function or constant

Wording

no wording

English

Assume that $\operatorname{CommSq}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Then $\operatorname{isLimitEquivIsLimitKernelFork}$ applied to $\mathrm{sq}$ is an equivalence from $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $\mathrm{fst}$, $\mathrm{snd}$ and $\operatorname{w}$ applied to $\mathrm{sq}$ to $\operatorname{IsLimit}$ applied to the kernel fork of $\mathrm{sq}$.

CategoryTheory.CommSq.kernelForkdefMathlib.Algebra.Homology.CommSq, function or constant

Wording

the kernel fork of sq (from the name)

English

Assume that $\operatorname{CommSq}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Then the kernel fork of $\mathrm{sq}$ is a kernel fork of $\operatorname{desc}$ applied to $f$ and $\operatorname{neg}$ applied to $g$.

CategoryTheory.CommSq.shortComplexdefMathlib.Algebra.Homology.CommSq, function or constant

Wording

the short complex attached to the cokernel cofork of sq (from the docstring)

English

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Then the short complex attached to the cokernel cofork of $\mathrm{sq}$ is a short complex of $C$.

CategoryTheory.CommSq.shortComplex'defMathlib.Algebra.Homology.CommSq, function or constant

Wording

the short complex attached to the kernel fork of sq (from the docstring)

English

Assume that $\operatorname{CommSq}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Then the short complex attached to the kernel fork of $\mathrm{sq}$ is a short complex of $C$.

CategoryTheory.IsPullback.isLimitKernelForkdefMathlib.Algebra.Homology.CommSq, function or constant

Wording

the limit kernel fork attached to a pullback square of h1 (from the docstring)

English

Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Then the limit kernel fork attached to a pullback square of $h_{1}$ is an element of $\operatorname{IsLimit}$ applied to the kernel fork of $\operatorname{toCommSq}$ applied to $h_{1}$ defined as $\operatorname{isLimitEquivIsLimitKernelFork}$ applied to $\operatorname{toCommSq}$ applied to $h_{1}$ and $\operatorname{isLimit}$ applied to $h_{1}$.

CategoryTheory.IsPushout.isColimitCokernelCoforkdefMathlib.Algebra.Homology.CommSq, function or constant

Wording

the colimit cokernel cofork attached to a pushout square of h1 (from the docstring)

English

Assume that $\operatorname{IsPushout}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Then the colimit cokernel cofork attached to a pushout square of $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork of $\operatorname{toCommSq}$ applied to $h_{1}$ defined as $\operatorname{isColimitEquivIsColimitCokernelCofork}$ applied to $\operatorname{toCommSq}$ applied to $h_{1}$ and $\operatorname{isColimit}$ applied to $h_{1}$.

Mathlib.Algebra.Homology.ComplexShape

ComplexShapestructureMathlib.Algebra.Homology.ComplexShape, type

Wording

complex shape of x (from the name)

English

Let $x$ be a set. Then the complex shapes of $x$ are a basic type.

ComplexShape.ReldefMathlib.Algebra.Homology.ComplexShape, predicate

Wording

no wording

English

Let $\mathrm{self}$ be a complex shape of $x$. Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\operatorname{Rel}$ holds for $\mathrm{self}$, $x_{1}$ and $x_{2}$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $x_{1}$ and $x_{2}$.

ComplexShape.downdefMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{down}$ applied to $x$ is a complex shape of $x$ defined as $\operatorname{down'}$ applied to $1$.

ComplexShape.down'defMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{down'}$ applied to $a$ is a complex shape of $x$.

ComplexShape.nextdefMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then $\operatorname{next}$ applied to $c$ and $i$ is an element of $x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $j$ of $x$, such that $\operatorname{Rel}$ holds for $c$, $i$ and $j$, the function that maps $h$ to $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $i$.

ComplexShape.prevdefMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $x$. Let $i$ be an element of $x$. Then $\operatorname{prev}$ applied to $c$ and $i$ is an element of $x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $j$ of $x$, such that $\operatorname{Rel}$ holds for $c$, $j$ and $i$, the function that maps $h$ to $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $i$.

ComplexShape.refldefMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a complex shape of $x$.

ComplexShape.symmdefMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

the inverse of c (from the name)

English

Let $c$ be a complex shape of $x$. Then the inverse of $c$ is a complex shape of $x$ defined as $\operatorname{mk}$ applied to the function that maps $i$ and $j$ to $\operatorname{Rel}$ applied to $c$, $j$ and $i$, the function that maps $x_{1}$, $x_{2}$, $x_{3}$, $w$ and $\mathrm{w'}$ to $\mathrm{ComplexShape\_\_prev\_eq}$ applied to $c$, $w$ and $\mathrm{w'}$ and the function that maps $x_{4}$, $x_{5}$, $x_{6}$, $w_{1}$ and $\mathrm{w'1}$ to $\mathrm{ComplexShape\_\_next\_eq}$ applied to $c$, $w_{1}$ and $\mathrm{w'1}$.

ComplexShape.transdefMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

the composition of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be complex shapes of $x$. Then the composition of $x_{1}$ and $x_{2}$ is a complex shape of $x$.

ComplexShape.updefMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{up}$ applied to $x$ is a complex shape of $x$ defined as $\operatorname{up'}$ applied to $1$.

ComplexShape.up'defMathlib.Algebra.Homology.ComplexShape, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{up'}$ applied to $a$ is a complex shape of $x$.

Mathlib.Algebra.Homology.ComplexShapeSigns

ComplexShape.AssociativeclassMathlib.Algebra.Homology.ComplexShapeSigns, predicate

Wording

no wording

English

Let $x_{5}$ be a complex shape of $x$. Let $x_{6}$ be a complex shape of $x_{1}$. Let $x_{7}$ be a complex shape of $x_{2}$. Let $x_{8}$ be a complex shape of $x_{3}$. Let $x_{9}$ be a complex shape of $x_{4}$. Let $c$ be a complex shape of $J$. Then we can say that $\operatorname{Associative}$ holds for $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $c$.

ComplexShape.TensorSignsclassMathlib.Algebra.Homology.ComplexShapeSigns, predicate

Wording

no wording

English

Let $c$ be a complex shape of $I$. Then we can say that $\operatorname{TensorSigns}$ holds for $c$.

ComplexShape.TensorSigns.ε'defMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $I$. Then $\mathrm{ComplexShape\_\_TensorSigns\_\_\_u3b5\_'}$ applied to $c$ is a monoid homomorphism of the set of multiplicatives of $I$ and $\UnitsMACRoAO {\Integer}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ComplexShape.rdefMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{4}$ be a complex shape of $x$. Let $x_{5}$ be a complex shape of $x_{1}$. Let $x_{6}$ be a complex shape of $x_{2}$. Let $x_{7}$ be a complex shape of $x_{3}$. Let $c$ be a complex shape of $J$. Let $x_{10}$ be an element of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then $\operatorname{r}$ applied to $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $c$ and $x_{10}$ is an element of $J$.

ComplexShape.symmetryEquivdefMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

the symmetry equivalence of x5 and j (from the name)

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $j$ be an element of $x_{2}$. Then the symmetry equivalence of $x_{5}$ and $j$ is an equivalence from the set of elements of the preimage of $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{5}$ and $\operatorname{singleton}$ applied to $j$ to the set of elements of the preimage of $\mathrm{ComplexShape\_\_\_u3c0\_}$ applied to $x_{5}$ and $\operatorname{singleton}$ applied to $j$.

ComplexShape.εdefMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $I$. Let $i$ be an element of $I$. Then $\mathrm{ComplexShape\_\_\_u3b5\_}$ applied to $c$ and $i$ is a unit of $\Integer$ defined as $\mathrm{ComplexShape\_\_TensorSigns\_\_\_u3b5\_'\_\_app}$ applied to $c$ and $i$.

ComplexShape.ε₁defMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $i$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then $\mathrm{ComplexShape\_\_\_u3b5\_\_u2081\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$ and $i$ is a unit of $\Integer$ defined as $\mathrm{TotalComplexShape\_\_\_u3b5\_\_u2081\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$ and $i$.

ComplexShape.ε₂defMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $i$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then $\mathrm{ComplexShape\_\_\_u3b5\_\_u2082\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$ and $i$ is a unit of $\Integer$ defined as $\mathrm{TotalComplexShape\_\_\_u3b5\_\_u2082\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$ and $i$.

ComplexShape.πdefMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

the projection of x5 and i (from the name)

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $i$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the projection of $x_{5}$ and $i$ is an element of $x_{2}$ defined as the projection of $x_{5}$ and $i$.

ComplexShape.ρ₁₂defMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{4}$ be a complex shape of $x$. Let $x_{5}$ be a complex shape of $x_{1}$. Let $x_{6}$ be a complex shape of $x_{2}$. Let $x_{7}$ be a complex shape of $x_{3}$. Let $c$ be a complex shape of $J$. Then $\mathrm{ComplexShape\_\_\_u3c1\_\_u2081\_\_u2082\_}$ applied to $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $c$ is a bifunctor composition index data of $\operatorname{r}$ applied to $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $c$.

ComplexShape.ρ₂₃defMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{5}$ be a complex shape of $x$. Let $x_{6}$ be a complex shape of $x_{1}$. Let $x_{7}$ be a complex shape of $x_{2}$. Let $x_{8}$ be a complex shape of $x_{3}$. Let $x_{9}$ be a complex shape of $x_{4}$. Let $c$ be a complex shape of $J$. Then $\mathrm{ComplexShape\_\_\_u3c1\_\_u2082\_\_u2083\_}$ applied to $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $c$ is a bifunctor composition index data of $\operatorname{r}$ applied to $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$ and $c$.

ComplexShape.σdefMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $x_{9}$ be an element of $x$. Let $x_{10}$ be an element of $x_{1}$. Then $\mathrm{ComplexShape\_\_\_u3c3\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$, $x_{9}$ and $x_{10}$ is a unit of $\Integer$ defined as $\mathrm{TotalComplexShapeSymmetry\_\_\_u3c3\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$, $x_{9}$ and $x_{10}$.

TotalComplexShapeclassMathlib.Algebra.Homology.ComplexShapeSigns, predicate

Wording

no wording

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Then we can say that $\mathrm{TotalComplexShape}$ holds for $x_{3}$, $x_{4}$ and $x_{5}$.

TotalComplexShape.ε₁defMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $x_{6}$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then $\mathrm{TotalComplexShape\_\_\_u3b5\_\_u2081\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ is a unit of $\Integer$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{6}$.

TotalComplexShape.ε₂defMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $x_{6}$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then $\mathrm{TotalComplexShape\_\_\_u3b5\_\_u2082\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ is a unit of $\Integer$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{6}$.

TotalComplexShape.πdefMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

the projection of x5 and x6 (from the name)

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $x_{6}$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the projection of $x_{5}$ and $x_{6}$ is an element of $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{6}$.

TotalComplexShapeSymmetryclassMathlib.Algebra.Homology.ComplexShapeSigns, predicate

Wording

no wording

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Then we can say that $\mathrm{TotalComplexShapeSymmetry}$ holds for $x_{3}$, $x_{4}$ and $x_{5}$.

TotalComplexShapeSymmetry.σdefMathlib.Algebra.Homology.ComplexShapeSigns, function or constant

Wording

no wording

English

Let $x_{3}$ be a complex shape of $x$. Let $x_{4}$ be a complex shape of $x_{1}$. Let $x_{5}$ be a complex shape of $x_{2}$. Let $x_{8}$ be an element of $x$. Let $x_{9}$ be an element of $x_{1}$. Then $\mathrm{TotalComplexShapeSymmetry\_\_\_u3c3\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$, $x_{8}$ and $x_{9}$ is a unit of $\Integer$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{8}$ and $x_{9}$.

TotalComplexShapeSymmetrySymmetryclassMathlib.Algebra.Homology.ComplexShapeSigns, predicate

Wording

no wording

English

Mathlib.Algebra.Homology.ConcreteCategory

HomologicalComplex.cyclesMkdefMathlib.Algebra.Homology.ConcreteCategory, function or constant

Wording

the cycle of x6 and j (from the name)

English

Let $K$ be a homological complex of $C$ and $c$. Let $x_{6}$ be a carrier of the action of the forgetful functor of $C$ and the set of abelian groups and $\operatorname{X}$ applied to $K$ and $i$. Let $j$ be an element of $x_{5}$ such that $\EqtMACRoH {\operatorname{next} (c , i)}{j}$ and $\operatorname{hom}$ applied to the map of the forgetful functor of $C$ and the set of abelian groups and $\operatorname{d}$ applied to $K$, $i$ and $j$ and $x_{6}$ is equal to $0$. Then the cycle of $x_{6}$ and $j$ is a carrier of the action of the forgetful functor of $C$ and the set of abelian groups and the cycle of $K$ and $i$.

Mathlib.Algebra.Homology.DerivedCategory.Basic

DerivedCategorydefMathlib.Algebra.Homology.DerivedCategory.Basic, type

Wording

derived category of C (from the name)

English

Let $C$ be a set. Then a derived category of $C$ is an element of the function that maps $C$ to $\mathrm{HomologicalComplexUpToQuasiIso}$ applied to $C$ and $\operatorname{up}$ applied to $\Integer$.

DerivedCategory.QdefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

no wording

English

$\operatorname{Q}$ is a functor of the set of cochain complexes of $C$ and $\Integer$ and the set of derived categories of $C$ defined as $\operatorname{Q}$.

DerivedCategory.QhdefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

no wording

English

$\operatorname{Qh}$ is a functor of the set of homotopy categories of $C$ and $\operatorname{up}$ applied to $\Integer$ and the set of derived categories of $C$ defined as $\operatorname{Qh}$.

DerivedCategory.quotientCompQhIsodefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

the natural isomorphism of C (from the docstring)

English

Let $C$ be a set. Then the natural isomorphism of $C$ is an isomorphism of the composition of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Qh}$ and $\operatorname{Q}$ defined as the canonical isomorphism of $C$ and $\operatorname{up}$ applied to $\Integer$.

DerivedCategory.singleFunctordefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

the single functor of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the single functor of $C$ and $n$ is a functor of $C$ and the set of derived categories of $C$ defined as the functor of the single functor of $C$ and $n$.

DerivedCategory.singleFunctorIsoCompQdefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

the isomorphism of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the isomorphism of $C$ and $n$ is an isomorphism of the single functor of $C$ and $n$ and the composition of the single functor of $C$ and $n$ and $\operatorname{Q}$ defined as the identity of the single functor of $C$ and $n$.

DerivedCategory.singleFunctorIsoCompQhdefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

the isomorphism of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the isomorphism of $C$ and $n$ is an isomorphism of the single functor of $C$ and $n$ and the composition of the single functor of $C$ and $n$ and $\operatorname{Qh}$ defined as the map isomorphism of the evaluation of $n$ and the isomorphism of $C$.

DerivedCategory.singleFunctorsdefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

the single functor of C (from the name)

English

Let $C$ be a set. Then the single functor of $C$ is a single functor of the set of derived categories of $C$ and $\Integer$ defined as the postcomposition of the collection of all single functors of $C$ and $\operatorname{Q}$.

DerivedCategory.singleFunctorsPostcompQIsodefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

the isomorphism of C (from the docstring)

English

DerivedCategory.singleFunctorsPostcompQhIsodefMathlib.Algebra.Homology.DerivedCategory.Basic, function or constant

Wording

the isomorphism of C (from the docstring)

English

Let $C$ be a set. Then the isomorphism of $C$ is an isomorphism of the single functor of $C$ and the postcomposition of the collection of all single functors of $C$ and $\operatorname{Qh}$ defined as the composition of the isomorphism of the collection of all single functors of $C$ and the inverse of the natural isomorphism of $C$ and the inverse of the postcomposition postcomposition isomorphism of the quotient of $C$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Qh}$.

HasDerivedCategorydefMathlib.Algebra.Homology.DerivedCategory.Basic, type

Wording

no wording

English

Let $C$ be a set. Then an element of $\mathrm{HasDerivedCategory}$ applied to $C$ is an element of the function that maps $C$ to the proposition that $\operatorname{quasiIso}$ applied to $C$ and $\operatorname{up}$ applied to $\Integer$ has localizations.

Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

CochainComplex.Plus.fibrantObjectEquivalencedefMathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives, function or constant

Wording

the fibrant object equivalence of C (from the name)

English

Let $C$ be a set. Then the fibrant object equivalence of $C$ is an equivalence of the set of pluses of the set of injective objects of $C$ and the set of fibrant objects of the set of pluses of $C$.

CochainComplex.Plus.fibrantObjectLocalizerMorphismdefMathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives, function or constant

Wording

the fibrant object localizer morphism of C (from the name)

English

Let $C$ be a set. Then the fibrant object localizer morphism of $C$ is a localizer morphism of the inverse image of $\operatorname{quasiIso}$ applied to $C$ and the map cochain complex plus of the inclusion of $C$ and the weak equivalence of the set of fibrant objects of the set of pluses of $C$.

CochainComplex.Plus.localizerMorphismdefMathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives, function or constant

Wording

the localizer morphism of C (from the name)

English

Let $C$ be a set. Then the localizer morphism of $C$ is a localizer morphism of the inverse image of $\operatorname{quasiIso}$ applied to $C$ and the map cochain complex plus of the inclusion of $C$ and $\operatorname{quasiIso}$ applied to $C$.

HomotopyCategory.Plus.localizerMorphismdefMathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives, function or constant

Wording

the localizer morphism of C (from the name)

English

Let $C$ be a set. Then the localizer morphism of $C$ is a localizer morphism of the isomorphism of the set of pluses of the set of injective objects of $C$ and $\operatorname{quasiIso}$ applied to $C$.

Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

CategoryTheory.Functor.mapDerivedCategorydefMathlib.Algebra.Homology.DerivedCategory.ExactFunctor, function or constant

Wording

the map derived category of F (from the name)

English

Let $F$ be a functor of $x$ and $x_{4}$. Then the map derived category of $F$ is a functor of the set of derived categories of $x$ and the set of derived categories of $x_{4}$ defined as $\operatorname{mapHomologicalComplexUpToQuasiIso}$ applied to $F$ and $\operatorname{up}$ applied to $\Integer$.

CategoryTheory.Functor.mapDerivedCategoryCompIsodefMathlib.Algebra.Homology.DerivedCategory.ExactFunctor, function or constant

Wording

the map derived category composition isomorphism of F and G (from the name)

English

Let $F$ be a functor of $x$ and $x_{4}$. Let $G$ be a functor of $x_{4}$ and $x_{8}$. Then the map derived category composition isomorphism of $F$ and $G$ is an isomorphism of the composition of the map derived category of $F$ and the map derived category of $G$ and the map derived category of the composition of $F$ and $G$ defined as the lift natural isomorphism of the map derived category of the composition of $F$ and $G$ and the composition of the inverse of the associator of the map homological complex of $G$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Q}$ and the right isomorphism whisker of the map homological complex composition isomorphism of the identity of the composition of $F$ and $G$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Q}$.

CategoryTheory.Functor.mapDerivedCategoryFactorsdefMathlib.Algebra.Homology.DerivedCategory.ExactFunctor, function or constant

Wording

the map derived category factor of F (from the name)

English

Let $F$ be a functor of $x$ and $x_{4}$. Then the map derived category factor of $F$ is an isomorphism of the composition of $\operatorname{Q}$ and the map derived category of $F$ and the composition of the map homological complex of $F$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Q}$ defined as $\operatorname{mapHomologicalComplexUpToQuasiIsoFactors}$ applied to $F$ and $\operatorname{up}$ applied to $\Integer$.

CategoryTheory.Functor.mapDerivedCategoryFactorshdefMathlib.Algebra.Homology.DerivedCategory.ExactFunctor, function or constant

Wording

no wording

English

Let $F$ be a functor of $x$ and $x_{4}$. Then $\operatorname{mapDerivedCategoryFactorsh}$ applied to $F$ is an isomorphism of the composition of $\operatorname{Qh}$ and the map derived category of $F$ and the composition of the map homotopy category of $F$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Qh}$ defined as $\operatorname{mapHomologicalComplexUpToQuasiIsoFactorsh}$ applied to $F$ and $\operatorname{up}$ applied to $\Integer$.

CategoryTheory.Functor.mapDerivedCategoryIdIsodefMathlib.Algebra.Homology.DerivedCategory.ExactFunctor, function or constant

Wording

the map derived category identity isomorphism of x (from the name)

English

Let $x$ be a set. Then the map derived category identity isomorphism of $x$ is an isomorphism of the map derived category of the identity of $x$ and the identity of the set of derived categories of $x$ defined as the lift natural isomorphism of the identity of the set of derived categories of $x$ and the identity of $\operatorname{Q}$.

CategoryTheory.Functor.mapDerivedCategorySingleFunctordefMathlib.Algebra.Homology.DerivedCategory.ExactFunctor, function or constant

Wording

the map derived category single functor of F and n (from the name)

English

Let $F$ be a functor of $x$ and $x_{4}$. Let $n$ be an integer. Then the map derived category single functor of $F$ and $n$ is an isomorphism of the composition of the single functor of $x$ and $n$ and the map derived category of $F$ and the composition of $F$ and the single functor of $x_{4}$ and $n$ defined as the composition of the right isomorphism whisker of the isomorphism of $x$ and $n$ and the map derived category of $F$ and the composition of the associator of $\operatorname{Q}$ and the map derived category of $F$ and the composition of the left isomorphism whisker of the single functor of $x$ and $n$ and the map derived category factor of $F$ and the composition of the inverse of the associator of the map homological complex of $F$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Q}$ and the composition of the right isomorphism whisker of the single map homological complex of $\operatorname{up}$ applied to $\Integer$ and $n$ and $\operatorname{Q}$ and the composition of the associator of $\operatorname{single}$ applied to $x_{4}$, $\operatorname{up}$ applied to $\Integer$ and $n$ and $\operatorname{Q}$ and the inverse of the left isomorphism whisker of $F$ and the isomorphism of $x_{4}$ and $n$.

CategoryTheory.NatTrans.mapDerivedCategorydefMathlib.Algebra.Homology.DerivedCategory.ExactFunctor, function or constant

Wording

the map derived category of x8 (from the name)

English

Let $x_{8}$ be a homomorphism of $F$ and $G$. Then the map derived category of $x_{8}$ is a homomorphism of the map derived category of $F$ and the map derived category of $G$ defined as the lift natural transformation of the map derived category of $G$ and the right whisker of the map homological complex of $x_{8}$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Q}$.

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

CategoryTheory.Abelian.ExtdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, type

Wording

extension of Y and n (from the name)

English

Let $X$ and $Y$ be elements of $C$. Let $n$ be a natural number. Then an extension of $Y$ and $n$ is an element of the function that maps $X$, $Y$ and $n$ to the set of small shifted homomorphisms of the action of the single functor of $C$ and $0$ and $Y$ and $n$.

CategoryTheory.Abelian.Ext.addEquivBiproddefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the additive equivalence biproduct (from the name)

English

The additive equivalence biproduct is an additive equivalence of the set of extensions of the biproduct of $x_{2}$ and $x_{3}$ and $n$ and $\mathrm{Prod}$ applied to the set of extensions of $x_{2}$ and $n$ and the set of extensions of $x_{3}$ and $n$.

CategoryTheory.Abelian.Ext.addEquivBiproductdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the additive equivalence biproduct of hc and n (from the name)

English

Let $X$ be an element of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsBilimit}$ applied to $c$. Let $n$ be a natural number. Then the additive equivalence biproduct of $\mathrm{hc}$ and $n$ is an additive equivalence of the set of extensions of $\operatorname{pt}$ applied to $c$ and $n$ and the set of functions from elements $i$ of $J$ to extensions of $Y$ applied to $i$ and $n$.

CategoryTheory.Abelian.Ext.addEquiv₀defMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the additive bijection (from the docstring)

English

The additive bijection is an additive equivalence of the set of extensions of $Y$ and $0$ and the set of homomorphisms of $X$ and $Y$.

CategoryTheory.Abelian.Ext.bilinearCompdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the composition of X (from the docstring)

English

Let $X$, $Y$ and $Z$ be elements of $C$. Let $a$, $b$ and $c$ be natural numbers such that $a + b = c$. Then the composition of $X$ is an additive monoid homomorphism of the set of extensions of $Y$ and $a$ and the set of additive monoid homomorphisms of the set of extensions of $Z$ and $b$ and the set of extensions of $Z$ and $c$.

CategoryTheory.Abelian.Ext.biprodAddEquivdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the biproduct additive equivalence (from the name)

English

The biproduct additive equivalence is an additive equivalence of the set of extensions of $Y$ and $n$ and $\mathrm{Prod}$ applied to the set of extensions of $Y$ and $n$ and the set of extensions of $Y$ and $n$.

CategoryTheory.Abelian.Ext.biproductAddEquivdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the biproduct additive equivalence of Y and n (from the name)

English

Let $\mathrm{hc}$ be an element of $\operatorname{IsBilimit}$ applied to $c$. Let $Y$ be an element of $C$. Let $n$ be a natural number. Then the biproduct additive equivalence of $Y$ and $n$ is an additive equivalence of the set of extensions of $Y$ and $n$ and the set of functions from elements $i$ of $J$ to extensions of $Y$ and $n$.

CategoryTheory.Abelian.Ext.chgUnivdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

no wording

English

$\operatorname{chgUniv}$ is an equivalence from the set of extensions of $Y$ and $n$ to the set of extensions of $Y$ and $n$ defined as $\operatorname{chgUniv}$.

CategoryTheory.Abelian.Ext.compdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the composition of x2 (from the docstring)

English

Let $x_{2}$ be an extension of $Y$ and $a$. Let $x_{3}$ be an extension of $Z$ and $b$. Assume that $a + b = c$. Then the composition of $x_{2}$ is an extension of $Z$ and $c$.

CategoryTheory.Abelian.Ext.homdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the homomorphism of x3 (from the name)

English

Let $x_{3}$ be an extension of $Y$ and $a$. Then the homomorphism of $x_{3}$ is a shifted homomorphism of the action of the single functor of $C$ and $0$ and $Y$ and $a$ defined as $\operatorname{homEquiv}$ applied to $x_{3}$.

CategoryTheory.Abelian.Ext.hom'defMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the homomorphism of x2 (from the name)

English

Let $x_{2}$ be an extension of $Y$ and $n$. Then the homomorphism of $x_{2}$ is a shifted homomorphism of the action of the single functor of $C$ and $0$ and $Y$ and $n$ defined as the homomorphism of $x_{2}$.

CategoryTheory.Abelian.Ext.homAddEquivdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the homomorphism additive equivalence (from the name)

English

The homomorphism additive equivalence is an additive equivalence of the set of extensions of $Y$ and $n$ and the set of shifted homomorphisms of the action of the single functor of $C$ and $0$ and $Y$ and $n$.

CategoryTheory.Abelian.Ext.homEquivdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the homomorphism equivalence (from the name)

English

The homomorphism equivalence is an equivalence from the set of extensions of $Y$ and $n$ to the set of shifted homomorphisms of the action of the single functor of $C$ and $0$ and $Y$ and $n$ defined as the equivalence of $\operatorname{quasiIso}$ applied to $C$ and $\operatorname{up}$ applied to $\Integer$ and $\operatorname{Q}$.

CategoryTheory.Abelian.Ext.homEquiv₀defMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the homomorphism equivalence (from the name)

English

The homomorphism equivalence is an equivalence from the set of extensions of $Y$ and $0$ to the set of homomorphisms of $X$ and $Y$ defined as the inverse of the equivalence of $\mathrm{CategoryTheory\_\_Abelian\_\_Ext\_\_mk\_u2080\_}$ and $\mathrm{CategoryTheory\_\_Abelian\_\_Ext\_\_mk\_u2080\_\_bijective}$ applied to $X$ and $Y$.

CategoryTheory.Abelian.Ext.mk₀defMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_Ext\_\_mk\_u2080\_}$ applied to $f$ is an extension of $Y$ and $0$.

CategoryTheory.Abelian.Ext.postcompdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the postcomposition of x2 and X (from the name)

English

Let $x_{2}$ be an extension of $Z$ and $n$. Let $X$ be an element of $C$. Assume that $a + n = b$. Then the postcomposition of $x_{2}$ and $X$ is an additive monoid homomorphism of the set of extensions of $Y$ and $a$ and the set of extensions of $Z$ and $b$ defined as $\operatorname{flip}$ applied to the composition of $X$ and $x_{2}$.

CategoryTheory.Abelian.Ext.precompdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the precomposition of x2 and Z (from the name)

English

Let $x_{2}$ be an extension of $Y$ and $n$. Let $Z$ be an element of $C$. Assume that $n + a = b$. Then the precomposition of $x_{2}$ and $Z$ is an additive monoid homomorphism of the set of extensions of $Z$ and $a$ and the set of extensions of $Z$ and $b$ defined as $\operatorname{bilinearComp}$ applied to $X$, $Y$, $Z$, $n$, $a$, $b$, $h_{1}$ and $x_{2}$.

CategoryTheory.Abelian.extFunctordefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, function or constant

Wording

the functor of n (from the docstring)

English

Let $n$ be a natural number. Then the functor of $n$ is a functor of the set of opposites of $C$ and the set of functors of $C$ and the set of additive commutative group categories.

CategoryTheory.HasExtdefMathlib.Algebra.Homology.DerivedCategory.Ext.Basic, predicate

Wording

C has extensions (from the name)

English

Let $C$ be a set. Then $C$ has extensions, if for all elements $X$ and $Y$ of $C$, $\operatorname{HasSmallLocalizedShiftedHom}$ holds for $\operatorname{quasiIso}$ applied to $C$ and $\operatorname{up}$ applied to $\Integer$, $\Integer$, the action of the single functor of $C$ and $0$ and $X$ and the action of the single functor of $C$ and $0$ and $Y$.

Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

CategoryTheory.Abelian.Ext.contravariantSequencedefMathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences, function or constant

Wording

the contravariant sequence of x2 and x3 (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Let $Y$ be an element of $C$. Let $x_{2}$ and $x_{3}$ be natural numbers such that $1 + x_{2} = x_{3}$. Then the contravariant sequence of $x_{2}$ and $x_{3}$ is a composable arrow of the set of additive commutative group categories and $5$.

CategoryTheory.Abelian.Ext.covariantSequencedefMathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences, function or constant

Wording

the covariant sequence of x2 and x3 (from the name)

English

Let $X$ be an element of $C$. Assume that $\operatorname{ShortExact}$ holds for $S$. Let $x_{2}$ and $x_{3}$ be natural numbers such that $x_{2} + 1 = x_{3}$. Then the covariant sequence of $x_{2}$ and $x_{3}$ is a composable arrow of the set of additive commutative group categories and $5$.

CategoryTheory.Abelian.Ext.δdefMathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences, function or constant

Wording

no wording

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Let $x_{2}$ and $x_{3}$ be natural numbers such that $x_{2} + 1 = x_{3}$. Then $\mathrm{CategoryTheory\_\_Abelian\_\_Ext\_\_\_u3b4\_}$ applied to $\mathrm{hS}$, $x_{2}$, $x_{3}$ and $h_{1}$ is an additive monoid homomorphism of the set of extensions of $Y$ and $x_{2}$ and the set of extensions of $Y$ and $x_{3}$.

Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

CategoryTheory.ShortComplex.ShortExact.extClassdefMathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass, function or constant

Wording

the class in hS (from the docstring)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Then the class in $\mathrm{hS}$ is an extension of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $1$.

Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

CategoryTheory.Abelian.Ext.bilinearCompOfLineardefMathlib.Algebra.Homology.DerivedCategory.Ext.Linear, function or constant

Wording

the composition of R (from the docstring)

English

Let $R$ be a set. Let $X$, $Y$ and $Z$ be elements of $C$. Let $a$, $b$ and $c$ be natural numbers such that $a + b = c$. Then the composition of $R$ is a linear map of the set of extensions of $Y$ and $a$ and the set of linear maps of the set of extensions of $Z$ and $b$ and the set of extensions of $Z$ and $c$.

CategoryTheory.Abelian.Ext.homLinearEquivdefMathlib.Algebra.Homology.DerivedCategory.Ext.Linear, function or constant

Wording

the homomorphism linear equivalence (from the name)

English

The homomorphism linear equivalence is a linear equivalence of the set of extensions of $Y$ and $n$ and the set of shifted homomorphisms of the action of the single functor of $C$ and $0$ and $Y$ and $n$.

CategoryTheory.Abelian.Ext.linearEquiv₀defMathlib.Algebra.Homology.DerivedCategory.Ext.Linear, function or constant

Wording

the linear equivalence (from the docstring)

English

The linear equivalence is a linear equivalence of the set of extensions of $Y$ and $0$ and the set of homomorphisms of $X$ and $Y$.

CategoryTheory.Abelian.Ext.postcompOfLineardefMathlib.Algebra.Homology.DerivedCategory.Ext.Linear, function or constant

Wording

the postcomposition of x2 and X (from the name)

English

Let $x_{2}$ be an extension of $Z$ and $n$. Let $R$ be a set. Let $X$ be an element of $C$. Assume that $a + n = b$. Then the postcomposition of $x_{2}$ and $X$ is a linear map of the set of extensions of $Y$ and $a$ and the set of extensions of $Z$ and $b$ defined as $\operatorname{flip}$ applied to the composition of $R$ and $x_{2}$.

CategoryTheory.Abelian.Ext.precompOfLineardefMathlib.Algebra.Homology.DerivedCategory.Ext.Linear, function or constant

Wording

the precomposition of x2 and Z (from the name)

English

Let $x_{2}$ be an extension of $Y$ and $n$. Let $R$ be a set. Let $Z$ be an element of $C$. Assume that $n + a = b$. Then the precomposition of $x_{2}$ and $Z$ is a linear map of the set of extensions of $Z$ and $a$ and the set of extensions of $Z$ and $b$ defined as $\operatorname{bilinearCompOfLinear}$ applied to $R$, $X$, $Y$, $Z$, $n$, $a$, $b$, $h_{1}$ and $x_{2}$.

CategoryTheory.Abelian.linearExtFunctordefMathlib.Algebra.Homology.DerivedCategory.Ext.Linear, function or constant

Wording

the linear extension functor of n (from the name)

English

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

Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

CategoryTheory.Abelian.Ext.mapExactFunctordefMathlib.Algebra.Homology.DerivedCategory.Ext.Map, function or constant

Wording

the map exact functor of F and f (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $f$ be an extension of $Y$ and $n$. Then the map exact functor of $F$ and $f$ is an extension of the action of $F$ and $Y$ and $n$ defined as the small shifted homomorphism map of the application of the map cochain complex single functor of $F$ and $0$ and $Y$ and $f$.

CategoryTheory.Functor.mapExtAddHomdefMathlib.Algebra.Homology.DerivedCategory.Ext.Map, function or constant

Wording

the map extension additive homomorphism of Y and n (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Let $n$ be a natural number. Then the map extension additive homomorphism of $Y$ and $n$ is an additive monoid homomorphism of the set of extensions of $Y$ and $n$ and the set of extensions of the action of $F$ and $Y$ and $n$.

CategoryTheory.Functor.mapExtLinearMapdefMathlib.Algebra.Homology.DerivedCategory.Ext.Map, function or constant

Wording

the map extension linear map of Y and n (from the name)

English

Let $F$ be a functor of $C$ and $D$. Let $R$ be a set. Let $X$ and $Y$ be elements of $C$. Let $n$ be a natural number. Then the map extension linear map of $Y$ and $n$ is a linear map of the set of extensions of $Y$ and $n$ and the set of extensions of the action of $F$ and $Y$ and $n$.

Mathlib.Algebra.Homology.DerivedCategory.Ext.MapAdjunction

CategoryTheory.Adjunction.extEquivdefMathlib.Algebra.Homology.DerivedCategory.Ext.MapAdjunction, function or constant

Wording

the extension equivalence of adj (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the extension equivalence of $\mathrm{adj}$ is an additive equivalence of the set of extensions of $Y$ and $n$ and the set of extensions of the action of $G$ and $Y$ and $n$.

CategoryTheory.Adjunction.extLinearEquivdefMathlib.Algebra.Homology.DerivedCategory.Ext.MapAdjunction, function or constant

Wording

the extension linear equivalence of adj and R (from the name)

English

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Let $R$ be a set. Then the extension linear equivalence of $\mathrm{adj}$ and $R$ is a linear equivalence of the set of extensions of $Y$ and $n$ and the set of extensions of the action of $G$ and $Y$ and $n$.

Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

DerivedCategory.singleFunctorCompHomologyFunctorIsodefMathlib.Algebra.Homology.DerivedCategory.FullyFaithful, function or constant

Wording

the canonical isomorphism of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the canonical isomorphism of $C$ and $n$ is an isomorphism of the composition of the single functor of $C$ and $n$ and the homology functor of $C$ and $n$ and the identity of $C$ defined as the composition of the right isomorphism whisker of the map isomorphism of the evaluation of $n$ and the isomorphism of $C$ and the homology functor of $C$ and $n$ and the composition of the associator of $\operatorname{Q}$ and the homology functor of $C$ and $n$ and the composition of the left isomorphism whisker of the functor of the collection of all single functors of $C$ and $n$ and the homology functor on the derived category of $C$ and $n$ and the homology functor single isomorphism of $\operatorname{up}$ applied to $\Integer$ and $n$.

Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

CochainComplex.homologyδOfTriangledefMathlib.Algebra.Homology.DerivedCategory.HomologySequence, function or constant

Wording

the homology of x2 and x3 (from the name)

English

Let $T$ be a triangle of the set of cochain complexes of $C$ and $\Integer$. Let $x_{2}$ and $x_{3}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{2} + 1 , x_{3})$ and $\mathrm{CochainComplex\_\_homology\_u3b4\_OfTriangle\_\_\_auto\_1}$. Then the homology of $x_{2}$ and $x_{3}$ is a homomorphism of the homology of the third object of $T$ and $x_{2}$ and the homology of the first object of $T$ and $x_{3}$.

DerivedCategory.HomologySequence.δdefMathlib.Algebra.Homology.DerivedCategory.HomologySequence, function or constant

Wording

no wording

English

Let $T$ be a triangle of the set of derived categories of $C$. Let $x_{3}$ and $x_{4}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{3} + 1 , x_{4})$ and $\mathrm{DerivedCategory\_\_HomologySequence\_\_\_u3b4\_\_\_\_auto\_1}$. Then $\mathrm{DerivedCategory\_\_HomologySequence\_\_\_u3b4\_}$ applied to $T$, $x_{3}$, $x_{4}$ and $h$ is a homomorphism of the action of the homology functor of $C$ and $x_{3}$ and the third object of $T$ and the action of the homology functor of $C$ and $x_{4}$ and the first object of $T$.

DerivedCategory.homologyFunctordefMathlib.Algebra.Homology.DerivedCategory.HomologySequence, function or constant

Wording

the homology functor of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the homology functor of $C$ and $n$ is a functor of the set of derived categories of $C$ and $C$ defined as the homology functor of $\operatorname{up}$ applied to $\Integer$ and $n$.

DerivedCategory.homologyFunctorFactorsdefMathlib.Algebra.Homology.DerivedCategory.HomologySequence, function or constant

Wording

the homology functor on the derived category of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the homology functor on the derived category of $C$ and $n$ is an isomorphism of the composition of $\operatorname{Q}$ and the homology functor of $C$ and $n$ and the homology functor of $\operatorname{up}$ applied to $\Integer$ and $n$ defined as the homology functor factor of $\operatorname{up}$ applied to $\Integer$ and $n$.

DerivedCategory.homologyFunctorFactorshdefMathlib.Algebra.Homology.DerivedCategory.HomologySequence, function or constant

Wording

the homology functor on the derived category of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the homology functor on the derived category of $C$ and $n$ is an isomorphism of the composition of $\operatorname{Qh}$ and the homology functor of $C$ and $n$ and the homology functor of $\operatorname{up}$ applied to $\Integer$ and $n$ defined as $\operatorname{homologyFunctorFactorsh}$ applied to $C$, $\operatorname{up}$ applied to $\Integer$ and $n$.

Mathlib.Algebra.Homology.DerivedCategory.KInjective

CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjectivedefMathlib.Algebra.Homology.DerivedCategory.KInjective, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an equivalence from the set of cohomology classes of $L$ and $n$ to the set of small shifted homomorphisms of $L$ and $n$ defined as the equivalence of $\operatorname{toSmallShiftedHom}$ and $\mathrm{CochainComplex\_\_HomComplex\_\_CohomologyClass\_\_bijective\_toSmallShiftedHom\_of\_isKInjective}$ applied to $K$, $L$ and $n$.

Mathlib.Algebra.Homology.DerivedCategory.KProjective

CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjectivedefMathlib.Algebra.Homology.DerivedCategory.KProjective, function or constant

Wording

the equivalence (from the name)

English

Mathlib.Algebra.Homology.DerivedCategory.Plus

DerivedCategory.Plus.IsGEdefMathlib.Algebra.Homology.DerivedCategory.Plus, predicate

Wording

no wording

English

Let $X$ be a plus of $C$. Let $n$ be an integer. Then $\operatorname{IsGE}$ holds for $X$ and $n$, if $\operatorname{IsGE}$ holds for $\operatorname{t}$, $X$ and $n$.

DerivedCategory.Plus.IsLEdefMathlib.Algebra.Homology.DerivedCategory.Plus, predicate

Wording

no wording

English

Let $X$ be a plus of $C$. Let $n$ be an integer. Then $\operatorname{IsLE}$ holds for $X$ and $n$, if $\operatorname{IsLE}$ holds for $\operatorname{t}$, $X$ and $n$.

DerivedCategory.Plus.QdefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

no wording

English

$\operatorname{Q}$ is a functor of the set of pluses of $C$ and the set of pluses of $C$.

DerivedCategory.Plus.QCompιIsodefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

the composition inclusion isomorphism of C (from the name)

English

Let $C$ be a set. Then the composition inclusion isomorphism of $C$ is an isomorphism of the composition of $\operatorname{Q}$ and the inclusion of the bounded below derived category and the composition of the inclusion of the full subcategory of bounded below cochain complexes of $C$ and $\operatorname{Q}$.

DerivedCategory.Plus.QhdefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

no wording

English

$\operatorname{Qh}$ is a functor of the set of pluses of $C$ and the set of pluses of $C$.

DerivedCategory.Plus.QhCompιIsoιCompQhdefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

no wording

English

Let $C$ be a set. Then $\mathrm{DerivedCategory\_\_Plus\_\_QhComp\_u3b9\_Iso\_u3b9\_CompQh}$ applied to $C$ is an isomorphism of the composition of $\operatorname{Qh}$ and the inclusion of the bounded below derived category and the composition of the inclusion of $C$ and $\operatorname{Qh}$ defined as the identity of the composition of $\operatorname{Qh}$ and the inclusion of the bounded below derived category.

DerivedCategory.Plus.TStructure.tdefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

no wording

English

$\operatorname{t}$ is a structure of the set of pluses of $C$ defined as the structure of the plus of $\operatorname{t}$ and $\operatorname{t}$.

DerivedCategory.Plus.homologyFunctordefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

the homology functor of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the homology functor of $C$ and $n$ is a functor of the set of pluses of $C$ and $C$ defined as the composition of the inclusion of the bounded below derived category and the homology functor of $C$ and $n$.

DerivedCategory.Plus.quotientCompQhIsodefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

the natural isomorphism of C (from the docstring)

English

Let $C$ be a set. Then the natural isomorphism of $C$ is an isomorphism of the composition of the quotient of $C$ and $\operatorname{Qh}$ and $\operatorname{Q}$.

DerivedCategory.Plus.singleFunctordefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

the single functor of C and n (from the docstring)

English

Let $C$ be a set. Let $n$ be an integer. Then the single functor of $C$ and $n$ is a functor of $C$ and the set of pluses of $C$ defined as the functor of the single functor of $C$ and $n$.

DerivedCategory.Plus.singleFunctorsdefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

the single functor of C (from the name)

English

Let $C$ be a set. Then the single functor of $C$ is a single functor of the set of pluses of $C$ and $\Integer$.

DerivedCategory.Plus.singleFunctorιIsodefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

the single functor inclusion isomorphism of C and n (from the name)

English

Let $C$ be a set. Let $n$ be an integer. Then the single functor inclusion isomorphism of $C$ and $n$ is an isomorphism of the composition of the single functor of $C$ and $n$ and the inclusion of the bounded below derived category and the single functor of $C$ and $n$ defined as the identity of the composition of the single functor of $C$ and $n$ and the inclusion of the bounded below derived category.

HomotopyCategory.Plus.subcategoryAcyclicdefMathlib.Algebra.Homology.DerivedCategory.Plus, function or constant

Wording

no wording

English

Let $C$ be a set. Then there is an object property of the set of pluses of $C$. Proof. Let $C$ be arbitrary. By C. By HomotopyCategory__subcategoryAcyclic. By C. By HomotopyCategory__Plus___u3b9_. By CategoryTheory__ObjectProperty__inverseImage.

Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus

CategoryTheory.Functor.rightDerivedFunctorPlusdefMathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus, function or constant

Wording

the right derived functor of F (from the docstring)

English

Let $F$ be a functor of $C$ and $D$. Then the right derived functor of $F$ is a functor of the set of pluses of $C$ and the set of pluses of $D$ defined as $\operatorname{totalRightDerived}$ applied to the composition of the map homotopy category plus of $F$ and $\operatorname{Qh}$, $\operatorname{Qh}$ and $\operatorname{quasiIso}$ applied to $C$.

CategoryTheory.Functor.rightDerivedFunctorPlusUnitdefMathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus, function or constant

Wording

the right derived functor plus unit of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the right derived functor plus unit of $F$ is a homomorphism of the composition of the map cochain complex plus of $F$ and $\operatorname{Q}$ and the composition of $\operatorname{Q}$ and the right derived functor of $F$ defined as the composition of the left whisker of the map cochain complex plus of $F$ and the inverse of the natural isomorphism of $D$ and the composition of the inverse of the associator of the quotient of $D$ and $\operatorname{Qh}$ and the composition of the right whisker of the inverse of the quotient composition map homotopy category plus isomorphism of $F$ and $\operatorname{Qh}$ and the composition of the homomorphism of the associator of the map homotopy category plus of $F$ and $\operatorname{Qh}$ and the composition of the left whisker of the quotient of $C$ and $\operatorname{rightDerivedFunctorPlusUnith}$ applied to $F$ and the composition of the inverse of the associator of $\operatorname{Qh}$ and the right derived functor of $F$ and the right whisker of the homomorphism of the natural isomorphism of $C$ and the right derived functor of $F$.

CategoryTheory.Functor.rightDerivedFunctorPlusUnithdefMathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus, function or constant

Wording

no wording

English

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{rightDerivedFunctorPlusUnith}$ applied to $F$ is a homomorphism of the composition of the map homotopy category plus of $F$ and $\operatorname{Qh}$ and the composition of $\operatorname{Qh}$ and the right derived functor of $F$ defined as the total right derived unit of $\operatorname{Qh}$ and $\operatorname{quasiIso}$ applied to $C$.

CategoryTheory.NatTrans.rightDerivedFunctorPlusdefMathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus, function or constant

Wording

the right derived functor plus of x8 (from the name)

English

Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Then the right derived functor plus of $x_{8}$ is a homomorphism of the right derived functor of $x_{6}$ and the right derived functor of $x_{7}$ defined as the right derived natural transformation of $\operatorname{quasiIso}$ applied to $C$ and the right whisker of the map homotopy category plus of $x_{8}$ and $\operatorname{Qh}$.

CategoryTheory.NatTrans.rightDerivedFunctorPlusAddMonoidHomdefMathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus, function or constant

Wording

the right derived functor plus additive monoid homomorphism (from the name)

English

The right derived functor plus additive monoid homomorphism is an additive monoid homomorphism of the set of homomorphisms of $x_{6}$ and $x_{7}$ and the set of homomorphisms of the right derived functor of $x_{6}$ and the right derived functor of $x_{7}$.

Mathlib.Algebra.Homology.DerivedCategory.ShortExact

DerivedCategory.triangleOfSESdefMathlib.Algebra.Homology.DerivedCategory.ShortExact, function or constant

Wording

the triangle of hS (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Then the triangle of $\mathrm{hS}$ is a triangle of the set of derived categories of $C$ defined as $\operatorname{mk}$ applied to the map of $\operatorname{Q}$ and $\operatorname{f}$ applied to $S$, the map of $\operatorname{Q}$ and $\operatorname{g}$ applied to $S$ and the triangle of $\mathrm{hS}$.

DerivedCategory.triangleOfSES.mapdefMathlib.Algebra.Homology.DerivedCategory.ShortExact, function or constant

Wording

the map of f (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $x_{3}$. Assume that $\operatorname{ShortExact}$ holds for $x_{4}$. Let $f$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the map of $f$ is a homomorphism of the triangle of $h$ and the triangle of $h_{1}$.

DerivedCategory.triangleOfSESIsodefMathlib.Algebra.Homology.DerivedCategory.ShortExact, function or constant

Wording

the triangle of hS (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Then the triangle of $\mathrm{hS}$ is an isomorphism of the triangle of $\mathrm{hS}$ and the action of the map triangle of $\operatorname{Q}$ and the standard triangle of $\operatorname{f}$ applied to $S$.

DerivedCategory.triangleOfSESδdefMathlib.Algebra.Homology.DerivedCategory.ShortExact, function or constant

Wording

the triangle of hS (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Then the triangle of $\mathrm{hS}$ is a homomorphism of the action of $\operatorname{Q}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and the action of the shift functor of the set of derived categories of $C$ and $1$ and the action of $\operatorname{Q}$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ defined as the composition of the inverse of the map of $\operatorname{Q}$ and $\operatorname{descShortComplex}$ applied to $S$ and the composition of the map of $\operatorname{Q}$ and the third morphism of the standard triangle of $\operatorname{f}$ applied to $S$ and the component of the homomorphism of the commutative shift isomorphism of $\operatorname{Q}$ and $1$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$.

Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

CategoryTheory.ShortComplex.ShortExact.singleTriangledefMathlib.Algebra.Homology.DerivedCategory.SingleTriangle, function or constant

Wording

the single triangle of hS (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Then the single triangle of $\mathrm{hS}$ is a triangle of the set of derived categories of $C$ defined as $\operatorname{mk}$ applied to the map of the single functor of $C$ and $0$ and $\operatorname{f}$ applied to $S$, the map of the single functor of $C$ and $0$ and $\operatorname{g}$ applied to $S$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_ShortExact\_\_single\_u3b4\_}$ applied to $\mathrm{hS}$.

CategoryTheory.ShortComplex.ShortExact.singleTriangle.mapdefMathlib.Algebra.Homology.DerivedCategory.SingleTriangle, function or constant

Wording

the map of f (from the name)

English

CategoryTheory.ShortComplex.ShortExact.singleTriangleIsodefMathlib.Algebra.Homology.DerivedCategory.SingleTriangle, function or constant

Wording

the single triangle isomorphism of hS (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Then the single triangle isomorphism of $\mathrm{hS}$ is an isomorphism of the single triangle of $\mathrm{hS}$ and the triangle of $\mathrm{CategoryTheory\_\_ShortComplex\_\_ShortExact\_\_map\_of\_exact}$ applied to $\mathrm{hS}$ and $\operatorname{single}$ applied to $C$, $\operatorname{up}$ applied to $\Integer$ and $0$.

CategoryTheory.ShortComplex.ShortExact.singleδdefMathlib.Algebra.Homology.DerivedCategory.SingleTriangle, function or constant

Wording

no wording

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Then $\mathrm{CategoryTheory\_\_ShortComplex\_\_ShortExact\_\_single\_u3b4\_}$ applied to $\mathrm{hS}$ is a homomorphism of the action of the single functor of $C$ and $0$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and the action of the shift functor of the set of derived categories of $C$ and $1$ and the action of the single functor of $C$ and $0$ and $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$.

Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

CochainComplex.HomComplex.CohomologyClass.toShiftedHomdefMathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom, function or constant

Wording

the shifted homomorphism of x3 (from the name)

English

Let $x_{3}$ be a cohomology class of $L$ and $n$. Then the shifted homomorphism of $x_{3}$ is a homomorphism of the action of $\operatorname{Q}$ and $K$ and the action of the shift functor of the set of derived categories of $C$ and $n$ and the action of $\operatorname{Q}$ and $L$.

CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHomdefMathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom, function or constant

Wording

the small shifted homomorphism of x2 (from the name)

English

Let $x_{2}$ be a cohomology class of $L$ and $n$. Then the small shifted homomorphism of $x_{2}$ is a small shifted homomorphism of $L$ and $n$.

Mathlib.Algebra.Homology.DerivedCategory.TStructure

DerivedCategory.BoundeddefMathlib.Algebra.Homology.DerivedCategory.TStructure, type

Wording

no wording

English

Let $C$ be a set. Then an element of $\operatorname{Bounded}$ applied to $C$ is an element of the function that maps $C$ to the set of full subcategories of $\operatorname{bounded}$ applied to $\operatorname{t}$.

DerivedCategory.Bounded.ιdefMathlib.Algebra.Homology.DerivedCategory.TStructure, function or constant

Wording

the inclusion of the bounded derived category (from the docstring)

English

The inclusion of the bounded derived category is a functor of $\operatorname{Bounded}$ applied to $C$ and the set of derived categories of $C$ defined as the inclusion of $\operatorname{bounded}$ applied to $\operatorname{t}$.

DerivedCategory.IsGEdefMathlib.Algebra.Homology.DerivedCategory.TStructure, predicate

Wording

no wording

English

Let $X$ be a derived category of $C$. Let $n$ be an integer. Then $\operatorname{IsGE}$ holds for $X$ and $n$, if $\operatorname{IsGE}$ holds for $\operatorname{t}$, $X$ and $n$.

DerivedCategory.IsLEdefMathlib.Algebra.Homology.DerivedCategory.TStructure, predicate

Wording

no wording

English

Let $X$ be a derived category of $C$. Let $n$ be an integer. Then $\operatorname{IsLE}$ holds for $X$ and $n$, if $\operatorname{IsLE}$ holds for $\operatorname{t}$, $X$ and $n$.

DerivedCategory.MinusdefMathlib.Algebra.Homology.DerivedCategory.TStructure, type

Wording

minus of C (from the name)

English

Let $C$ be a set. Then a minus of $C$ is an element of the function that maps $C$ to the set of full subcategories of the minus of $\operatorname{t}$.

DerivedCategory.Minus.ιdefMathlib.Algebra.Homology.DerivedCategory.TStructure, function or constant

Wording

the inclusion of the bounded above derived category (from the docstring)

English

The inclusion of the bounded above derived category is a functor of the set of minuses of $C$ and the set of derived categories of $C$ defined as the inclusion of the minus of $\operatorname{t}$.

DerivedCategory.PlusdefMathlib.Algebra.Homology.DerivedCategory.TStructure, type

Wording

plus of C (from the name)

English

Let $C$ be a set. Then a plus of $C$ is an element of the function that maps $C$ to the set of full subcategories of the plus of $\operatorname{t}$.

DerivedCategory.Plus.ιdefMathlib.Algebra.Homology.DerivedCategory.TStructure, function or constant

Wording

the inclusion of the bounded below derived category (from the docstring)

English

The inclusion of the bounded below derived category is a functor of the set of pluses of $C$ and the set of derived categories of $C$ defined as the inclusion of the plus of $\operatorname{t}$.

DerivedCategory.TStructure.tdefMathlib.Algebra.Homology.DerivedCategory.TStructure, function or constant

Wording

no wording

English

$\operatorname{t}$ is a structure of the set of derived categories of $C$.

Mathlib.Algebra.Homology.DifferentialObject

CategoryTheory.DifferentialObject.objEqToHomdefMathlib.Algebra.Homology.DifferentialObject, function or constant

Wording

no wording

English

Let $X$ be a differential object of $\Integer$ and the set of graded objects with shift of $b$ and $V$. Assume that $\EqtMACRoH {i}{j}$. Then $\operatorname{objEqToHom}$ applied to $X$ and $h$ is a homomorphism of the underlying object of $X$ and the underlying object of $X$.

HomologicalComplex.dgoEquivHomologicalComplexdefMathlib.Algebra.Homology.DifferentialObject, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Let $V$ be a set. Then $\operatorname{dgoEquivHomologicalComplex}$ applied to $b$ and $V$ is an equivalence of the set of differential objects of $\Integer$ and the set of graded objects with shift of $b$ and $V$ and the set of homological complexes of $V$ and $\operatorname{up'}$ applied to $b$.

HomologicalComplex.dgoEquivHomologicalComplexCounitIsodefMathlib.Algebra.Homology.DifferentialObject, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Let $V$ be a set. Then $\operatorname{dgoEquivHomologicalComplexCounitIso}$ applied to $b$ and $V$ is an isomorphism of the composition of $\operatorname{homologicalComplexToDGO}$ applied to $b$ and $V$ and $\operatorname{dgoToHomologicalComplex}$ applied to $b$ and $V$ and the identity of the set of homological complexes of $V$ and $\operatorname{up'}$ applied to $b$.

HomologicalComplex.dgoEquivHomologicalComplexUnitIsodefMathlib.Algebra.Homology.DifferentialObject, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Let $V$ be a set. Then $\operatorname{dgoEquivHomologicalComplexUnitIso}$ applied to $b$ and $V$ is an isomorphism of the identity of the set of differential objects of $\Integer$ and the set of graded objects with shift of $b$ and $V$ and the composition of $\operatorname{dgoToHomologicalComplex}$ applied to $b$ and $V$ and $\operatorname{homologicalComplexToDGO}$ applied to $b$ and $V$.

HomologicalComplex.dgoToHomologicalComplexdefMathlib.Algebra.Homology.DifferentialObject, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Let $V$ be a set. Then $\operatorname{dgoToHomologicalComplex}$ applied to $b$ and $V$ is a functor of the set of differential objects of $\Integer$ and the set of graded objects with shift of $b$ and $V$ and the set of homological complexes of $V$ and $\operatorname{up'}$ applied to $b$.

HomologicalComplex.homologicalComplexToDGOdefMathlib.Algebra.Homology.DifferentialObject, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Let $V$ be a set. Then $\operatorname{homologicalComplexToDGO}$ applied to $b$ and $V$ is a functor of the set of homological complexes of $V$ and $\operatorname{up'}$ applied to $b$ and the set of differential objects of $\Integer$ and the set of graded objects with shift of $b$ and $V$.

Mathlib.Algebra.Homology.Double

HomologicalComplex.doubledefMathlib.Algebra.Homology.Double, function or constant

Wording

the double of f and h1 (from the name)

English

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Assume that $\operatorname{Rel}$ holds for $c$, $x_{5}$ and $x_{6}$. Then the double of $f$ and $h_{1}$ is a homological complex of $C$ and $c$.

HomologicalComplex.doubleXIso₀defMathlib.Algebra.Homology.Double, function or constant

Wording

the isomorphism of f and h1 (from the docstring)

English

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Assume that $\operatorname{Rel}$ holds for $c$, $x_{5}$ and $x_{6}$. Then the isomorphism of $f$ and $h_{1}$ is an isomorphism of $\operatorname{X}$ applied to the double of $f$ and $h_{1}$ and $x_{5}$ and $x_{2}$.

HomologicalComplex.doubleXIso₁defMathlib.Algebra.Homology.Double, function or constant

Wording

the double isomorphism of f (from the name)

English

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Assume that $\operatorname{Rel}$ holds for $c$, $x_{5}$ and $x_{6}$. Assume that $x_{5} \neq x_{6}$. Then the double isomorphism of $f$ is an isomorphism of $\operatorname{X}$ applied to the double of $f$ and $h_{1}$ and $x_{6}$ and $x_{3}$.

HomologicalComplex.evalCompCoyonedaCorepresentabledefMathlib.Algebra.Homology.Double, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $x_{2}$. Let $X$ be an element of $C$. Let $j$ be an element of $x_{2}$. Then $\operatorname{evalCompCoyonedaCorepresentable}$ applied to $c$, $X$ and $j$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the evaluation of $c$ and $j$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and $\operatorname{evalCompCoyonedaCorepresentative}$ applied to $c$, $X$ and $j$.

HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleIddefMathlib.Algebra.Homology.Double, function or constant

Wording

the evaluation composition Coyoneda corepresentable by double identity of X (from the name)

English

Assume that $\operatorname{Rel}$ holds for $c$, $x_{3}$ and $x_{4}$. Assume that $x_{3} \neq x_{4}$. Let $X$ be an element of $C$. Then the evaluation composition Coyoneda corepresentable by double identity of $X$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the evaluation of $c$ and $x_{3}$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and the double of the identity morphism of $X$ and $h_{1}$.

HomologicalComplex.evalCompCoyonedaCorepresentableBySingledefMathlib.Algebra.Homology.Double, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $x_{2}$. Let $i$ be an element of $x_{2}$ such that for all elements $j$ of $x_{2}$, it is not the case that $\operatorname{Rel}$ holds for $c$, $i$ and $j$. Let $X$ be an element of $C$. Then $\operatorname{evalCompCoyonedaCorepresentableBySingle}$ applied to $c$, $i$, $\mathrm{hi}$ and $X$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the evaluation of $c$ and $i$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and the action of $\operatorname{single}$ applied to $C$, $c$ and $i$ and $X$.

HomologicalComplex.evalCompCoyonedaCorepresentativedefMathlib.Algebra.Homology.Double, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $x_{2}$. Let $X$ be an element of $C$. Let $j$ be an element of $x_{2}$. Then $\operatorname{evalCompCoyonedaCorepresentative}$ applied to $c$, $X$ and $j$ is a homological complex of $C$ and $c$.

HomologicalComplex.mkHomFromDoubledefMathlib.Algebra.Homology.Double, function or constant

Wording

the homomorphism from double of x7 and x8 (from the name)

English

Assume that $\operatorname{Rel}$ holds for $c$, $x_{5}$ and $x_{6}$. Assume that $x_{5} \neq x_{6}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $\operatorname{X}$ applied to $K$ and $x_{5}$. Let $x_{8}$ be a homomorphism of $x_{3}$ and $\operatorname{X}$ applied to $K$ and $x_{6}$ such that the composition of $x_{7}$ and $\operatorname{d}$ applied to $K$, $x_{5}$ and $x_{6}$ is equal to the composition of $f$ and $x_{8}$ and for all elements $k$ of $x_{4}$, if $\operatorname{Rel}$ holds for $c$, $x_{6}$ and $k$, then the composition of $x_{8}$ and $\operatorname{d}$ applied to $K$, $x_{6}$ and $k$ is equal to $0$. Then the homomorphism from double of $x_{7}$ and $x_{8}$ is a homomorphism of the double of $f$ and $h_{1}$ and $K$.

Mathlib.Algebra.Homology.Embedding.AreComplementary

ComplexShape.Embedding.AreComplementarystructureMathlib.Algebra.Homology.Embedding.AreComplementary, predicate

Wording

no wording

English

Let $x_{5}$ be an embedding of $x_{3}$ and $c$. Let $x_{6}$ be an embedding of $x_{4}$ and $c$. Then we can say that $\operatorname{AreComplementary}$ holds for $x_{5}$ and $x_{6}$.

ComplexShape.Embedding.AreComplementary.BoundarydefMathlib.Algebra.Homology.Embedding.AreComplementary, predicate

Wording

no wording

English

Assume that $\operatorname{AreComplementary}$ holds for $x_{5}$ and $x_{6}$. Let $x_{7}$ be an element of $x_{1}$. Let $x_{8}$ be an element of $x_{2}$. Then $\operatorname{Boundary}$ holds for $h$, $x_{7}$ and $x_{8}$, if $\operatorname{Rel}$ holds for $c$, $\operatorname{f}$ applied to $x_{5}$ and $x_{7}$ and $\operatorname{f}$ applied to $x_{6}$ and $x_{8}$.

ComplexShape.Embedding.AreComplementary.Boundary.equivdefMathlib.Algebra.Homology.Embedding.AreComplementary, function or constant

Wording

the equivalence of ac (from the name)

English

Assume that $\operatorname{AreComplementary}$ holds for $x_{5}$ and $x_{6}$. Then the equivalence of $\mathrm{ac}$ is an equivalence from $\SubtypeSet {j}{\operatorname{BoundaryLE} (x_{5} , j)}$ to $\SubtypeSet {j_{1}}{\operatorname{BoundaryGE} (x_{6} , j_{1})}$.

ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryGEdefMathlib.Algebra.Homology.Embedding.AreComplementary, function or constant

Wording

the index of ac and h (from the name)

English

Assume that $\operatorname{AreComplementary}$ holds for $x_{5}$ and $x_{6}$. Assume that $\operatorname{BoundaryGE}$ holds for $x_{6}$ and $x_{7}$. Then the index of $\mathrm{ac}$ and $h$ is an element of $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{ComplexShape\_\_Embedding\_\_AreComplementary\_\_Boundary\_\_exists\_u2082\_}$ applied to $\mathrm{ac}$ and $h$.

ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryLEdefMathlib.Algebra.Homology.Embedding.AreComplementary, function or constant

Wording

the index of ac and h (from the name)

English

Assume that $\operatorname{AreComplementary}$ holds for $x_{5}$ and $x_{6}$. Assume that $\operatorname{BoundaryLE}$ holds for $x_{5}$ and $x_{7}$. Then the index of $\mathrm{ac}$ and $h$ is an element of $x_{2}$ defined as $\operatorname{choose}$ applied to $\mathrm{ComplexShape\_\_Embedding\_\_AreComplementary\_\_Boundary\_\_exists\_u2081\_}$ applied to $\mathrm{ac}$ and $h$.

ComplexShape.Embedding.AreComplementary.descdefMathlib.Algebra.Homology.Embedding.AreComplementary, function or constant

Wording

no wording

English

Assume that $\operatorname{AreComplementary}$ holds for $x_{5}$ and $x_{6}$. Let $x_{7}$ be a function from elements $x_{10}$ of $x_{1}$ to elements of $X$ applied to $\operatorname{f}$ applied to $x_{5}$ and $x_{10}$. Let $x_{8}$ be a function from elements $x_{9}$ of $x_{2}$ to elements of $X$ applied to $\operatorname{f}$ applied to $x_{6}$ and $x_{9}$. Let $i$ be an element of $x$. Then $\operatorname{desc}$ applied to $\mathrm{ac}$, $x_{10}$, $x_{7}$, $x_{9}$, $x_{8}$ and $i$ is an element of $X$ applied to $i$.

ComplexShape.Embedding.AreComplementary.equivdefMathlib.Algebra.Homology.Embedding.AreComplementary, function or constant

Wording

the equivalence of ac (from the name)

English

Assume that $\operatorname{AreComplementary}$ holds for $x_{5}$ and $x_{6}$. Then the equivalence of $\mathrm{ac}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (x_{1} , x_{2})}{x}$ defined as the equivalence of $\operatorname{fromSum}$ applied to $x_{5}$ and $x_{6}$ and $\mathrm{ComplexShape\_\_Embedding\_\_AreComplementary\_\_fromSum\_bijective}$ applied to $\mathrm{ac}$.

ComplexShape.Embedding.AreComplementary.fromSumdefMathlib.Algebra.Homology.Embedding.AreComplementary, function or constant

Wording

no wording

English

Let $x_{5}$ be an embedding of $x_{3}$ and $c$. Let $x_{6}$ be an embedding of $x_{4}$ and $c$. Let $x_{7}$ be an element of $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$. Then $\operatorname{fromSum}$ applied to $x_{5}$, $x_{6}$ and $x_{7}$ is an element of $x$.

HomologicalComplex.shortComplexTruncLEX₃ToTruncGEdefMathlib.Algebra.Homology.Embedding.AreComplementary, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $c$. Assume that $\operatorname{AreComplementary}$ holds for $x_{7}$ and $x_{8}$. Then $\mathrm{HomologicalComplex\_\_shortComplexTruncLEX\_u2083\_ToTruncGE}$ applied to $K$ and $\mathrm{ac}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $\operatorname{shortComplexTruncLE}$ applied to $K$ and $x_{7}$ and the canonical truncation of $K$ and $x_{8}$.

Mathlib.Algebra.Homology.Embedding.Basic

ComplexShape.EmbeddingstructureMathlib.Algebra.Homology.Embedding.Basic, type

Wording

embedding of c and #2 (from the name)

English

Let $c$ be a complex shape of $x$. Let $\mathrm{c'}$ be a complex shape of $x_{1}$. Then the embeddings of $c$ and $\mathrm{c'}$ are a basic type.

ComplexShape.Embedding.IsRelIffclassMathlib.Algebra.Homology.Embedding.Basic, predicate

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then we can say that $\operatorname{IsRelIff}$ holds for $e$.

ComplexShape.Embedding.IsTruncGEclassMathlib.Algebra.Homology.Embedding.Basic, predicate

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then we can say that $\operatorname{IsTruncGE}$ holds for $e$.

ComplexShape.Embedding.IsTruncLEclassMathlib.Algebra.Homology.Embedding.Basic, predicate

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then we can say that $\operatorname{IsTruncLE}$ holds for $e$.

ComplexShape.Embedding.fdefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an embedding of $c$ and $\mathrm{c'}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

ComplexShape.Embedding.mk'defMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

Let $c$ be a complex shape of $x$. Let $\mathrm{c'}$ be a complex shape of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is injective and for all elements $x_{2}$ of $x$, for all elements $x_{3}$ of $x$, $\operatorname{Rel}$ holds for $c$, $x_{2}$ and $x_{3}$, if and only if $\operatorname{Rel}$ holds for $\mathrm{c'}$, $f$ applied to $x_{2}$ and $f$ applied to $x_{3}$. Then $\operatorname{mk'}$ applied to $c$, $\mathrm{c'}$, $f$, $\mathrm{hf}$ and $\mathrm{iff}$ is an embedding of $c$ and $\mathrm{c'}$.

ComplexShape.Embedding.opdefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

the opposite embedding in e (from the docstring)

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the opposite embedding in $e$ is an embedding of the inverse of $c$ and the inverse of $\mathrm{c'}$ defined as $\operatorname{mk}$ applied to $\operatorname{f}$ applied to $e$, $\mathrm{ComplexShape\_\_Embedding\_\_injective\_f}$ applied to $e$ and the function that maps $x_{2}$, $x_{3}$ and $h$ to $\operatorname{rel}$ applied to $e$ and $h$.

ComplexShape.Embedding.rdefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $\mathrm{i'}$ be an element of $x_{1}$. Then $\operatorname{r}$ applied to $e$ and $\mathrm{i'}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $i$ of $x$, such that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$, the function that maps $h$ to $\operatorname{some}$ applied to $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $\operatorname{none}$.

ComplexShape.embeddingDown'AdddefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $A$. Then $\operatorname{embeddingDown'Add}$ applied to $a$ and $b$ is an embedding of $\operatorname{down'}$ applied to $a$ and $\operatorname{down'}$ applied to $a$.

ComplexShape.embeddingDownNatdefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

$\operatorname{embeddingDownNat}$ is an embedding of $\operatorname{down}$ applied to $\Natural$ and $\operatorname{up}$ applied to $\Integer$.

ComplexShape.embeddingUp'AdddefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $A$. Then $\operatorname{embeddingUp'Add}$ applied to $a$ and $b$ is an embedding of $\operatorname{up'}$ applied to $a$ and $\operatorname{up'}$ applied to $a$.

ComplexShape.embeddingUpIntGEdefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

Let $p$ be an integer. Then $\operatorname{embeddingUpIntGE}$ applied to $p$ is an embedding of $\operatorname{up}$ applied to $\Natural$ and $\operatorname{up}$ applied to $\Integer$.

ComplexShape.embeddingUpIntLEdefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

Let $p$ be an integer. Then $\operatorname{embeddingUpIntLE}$ applied to $p$ is an embedding of $\operatorname{down}$ applied to $\Natural$ and $\operatorname{up}$ applied to $\Integer$.

ComplexShape.embeddingUpNatdefMathlib.Algebra.Homology.Embedding.Basic, function or constant

Wording

no wording

English

$\operatorname{embeddingUpNat}$ is an embedding of $\operatorname{up}$ applied to $\Natural$ and $\operatorname{up}$ applied to $\Integer$.

Mathlib.Algebra.Homology.Embedding.Boundary

ComplexShape.Embedding.BoundaryGEdefMathlib.Algebra.Homology.Embedding.Boundary, predicate

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $j$ be an element of $x$. Then $\operatorname{BoundaryGE}$ holds for $e$ and $j$, if $\operatorname{Rel}$ holds for $\mathrm{c'}$, $\operatorname{prev}$ applied to $\mathrm{c'}$ and $\operatorname{f}$ applied to $e$ and $j$ and $\operatorname{f}$ applied to $e$ and $j$ and for all elements $i$ of $x$, it is not the case that $\operatorname{Rel}$ holds for $\mathrm{c'}$, $\operatorname{f}$ applied to $e$ and $i$ and $\operatorname{f}$ applied to $e$ and $j$.

ComplexShape.Embedding.BoundaryLEdefMathlib.Algebra.Homology.Embedding.Boundary, predicate

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $j$ be an element of $x$. Then $\operatorname{BoundaryLE}$ holds for $e$ and $j$, if $\operatorname{Rel}$ holds for $\mathrm{c'}$, $\operatorname{f}$ applied to $e$ and $j$ and $\operatorname{next}$ applied to $\mathrm{c'}$ and $\operatorname{f}$ applied to $e$ and $j$ and for all elements $k$ of $x$, it is not the case that $\operatorname{Rel}$ holds for $\mathrm{c'}$, $\operatorname{f}$ applied to $e$ and $j$ and $\operatorname{f}$ applied to $e$ and $k$.

Mathlib.Algebra.Homology.Embedding.CochainComplex

CochainComplex.IsGEdefMathlib.Algebra.Homology.Embedding.CochainComplex, predicate

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{IsGE}$ holds for $K$ and $n$, if $\operatorname{IsSupported}$ holds for $K$ and $\operatorname{embeddingUpIntGE}$ applied to $n$.

CochainComplex.IsLEdefMathlib.Algebra.Homology.Embedding.CochainComplex, predicate

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{IsLE}$ holds for $K$ and $n$, if $\operatorname{IsSupported}$ holds for $K$ and $\operatorname{embeddingUpIntLE}$ applied to $n$.

CochainComplex.IsStrictlyGEdefMathlib.Algebra.Homology.Embedding.CochainComplex, predicate

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{IsStrictlyGE}$ holds for $K$ and $n$, if $\operatorname{IsStrictlySupported}$ holds for $K$ and $\operatorname{embeddingUpIntGE}$ applied to $n$.

CochainComplex.IsStrictlyLEdefMathlib.Algebra.Homology.Embedding.CochainComplex, predicate

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{IsStrictlyLE}$ holds for $K$ and $n$, if $\operatorname{IsStrictlySupported}$ holds for $K$ and $\operatorname{embeddingUpIntLE}$ applied to $n$.

CochainComplex.shortComplexTruncLEdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{shortComplexTruncLE}$ applied to $K$ and $n$ is a short complex of the set of cochain complexes of $C$ and $\Integer$ defined as $\operatorname{shortComplexTruncLE}$ applied to $K$ and $\operatorname{embeddingUpIntLE}$ applied to $n$.

CochainComplex.shortComplexTruncLEX₃ToTruncGEdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $x_{2}$ and $x_{3}$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (x_{2} + 1 , x_{3})$ and $\mathrm{CochainComplex\_\_shortComplexTruncLEX\_u2083\_ToTruncGE\_\_\_auto\_1}$. Then $\mathrm{CochainComplex\_\_shortComplexTruncLEX\_u2083\_ToTruncGE}$ applied to $K$, $x_{2}$, $x_{3}$ and $h$ is a homomorphism of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $\operatorname{shortComplexTruncLE}$ applied to $K$ and $x_{2}$ and $\operatorname{truncGE}$ applied to $K$ and $x_{3}$ defined as $\mathrm{HomologicalComplex\_\_shortComplexTruncLEX\_u2083\_ToTruncGE}$ applied to $K$ and $\mathrm{ComplexShape\_\_Embedding\_\_embeddingUpInt\_areComplementary}$ applied to $x_{2}$, $x_{3}$ and $h$.

CochainComplex.truncGEdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{truncGE}$ applied to $K$ and $n$ is a cochain complex of $C$ and $\Integer$ defined as the canonical truncation of $K$ and $\operatorname{embeddingUpIntGE}$ applied to $n$.

CochainComplex.truncGEMapdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $n$ be an integer. Then $\operatorname{truncGEMap}$ applied to $x_{2}$ and $n$ is a homomorphism of $\operatorname{truncGE}$ applied to $K$ and $n$ and $\operatorname{truncGE}$ applied to $L$ and $n$ defined as $\operatorname{truncGEMap}$ applied to $x_{2}$ and $\operatorname{embeddingUpIntGE}$ applied to $n$.

CochainComplex.truncGEXIsodefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ and $i$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Lt} (n , i)$ and $\mathrm{CochainComplex\_\_truncGEXIso\_\_\_auto\_1}$. Then $\operatorname{truncGEXIso}$ applied to $K$, $n$, $i$ and $\mathrm{hi}$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{truncGE}$ applied to $K$ and $n$ and $i$ and $\operatorname{X}$ applied to $K$ and $i$.

CochainComplex.truncGEXIsoOpcyclesdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{truncGEXIsoOpcycles}$ applied to $K$ and $n$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{truncGE}$ applied to $K$ and $n$ and $n$ and $\operatorname{opcycles}$ applied to $K$ and $n$.

CochainComplex.truncLEdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\operatorname{truncLE}$ applied to $K$ and $n$ is a cochain complex of $C$ and $\Integer$ defined as the canonical truncation of $K$ and $\operatorname{embeddingUpIntLE}$ applied to $n$.

CochainComplex.truncLEMapdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $K$ and $L$. Let $n$ be an integer. Then $\operatorname{truncLEMap}$ applied to $x_{2}$ and $n$ is a homomorphism of $\operatorname{truncLE}$ applied to $K$ and $n$ and $\operatorname{truncLE}$ applied to $L$ and $n$ defined as $\operatorname{truncLEMap}$ applied to $x_{2}$ and $\operatorname{embeddingUpIntLE}$ applied to $n$.

CochainComplex.truncLEXIsodefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

the truncation lexicographic isomorphism of n and i (from the name)

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ and $i$ be integers such that $\mathrm{autoParam}$ holds for $\mathrm{Lt} (i , n)$ and $\mathrm{CochainComplex\_\_truncLEXIso\_\_\_auto\_1}$. Then the truncation lexicographic isomorphism of $n$ and $i$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{truncLE}$ applied to $K$ and $n$ and $i$ and $\operatorname{X}$ applied to $K$ and $i$.

CochainComplex.truncLEXIsoCyclesdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

the truncation lexicographic isomorphism cycle of K and n (from the name)

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then the truncation lexicographic isomorphism cycle of $K$ and $n$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{truncLE}$ applied to $K$ and $n$ and $n$ and the cycle of $K$ and $n$.

CochainComplex.ιTruncLEdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\mathrm{CochainComplex\_\_\_u3b9\_TruncLE}$ applied to $K$ and $n$ is a homomorphism of $\operatorname{truncLE}$ applied to $K$ and $n$ and $K$ defined as $\mathrm{HomologicalComplex\_\_\_u3b9\_TruncLE}$ applied to $K$ and $\operatorname{embeddingUpIntLE}$ applied to $n$.

CochainComplex.πTruncGEdefMathlib.Algebra.Homology.Embedding.CochainComplex, function or constant

Wording

no wording

English

Let $K$ be a cochain complex of $C$ and $\Integer$. Let $n$ be an integer. Then $\mathrm{CochainComplex\_\_\_u3c0\_TruncGE}$ applied to $K$ and $n$ is a homomorphism of $K$ and $\operatorname{truncGE}$ applied to $K$ and $n$ defined as $\mathrm{HomologicalComplex\_\_\_u3c0\_TruncGE}$ applied to $K$ and $\operatorname{embeddingUpIntGE}$ applied to $n$.

Mathlib.Algebra.Homology.Embedding.Connect

CochainComplex.ConnectDatastructureMathlib.Algebra.Homology.Embedding.Connect, type

Wording

no wording

English

Let $K$ be a chain complex of $C$ and $\Natural$. Let $L$ be a cochain complex of $C$ and $\Natural$. Then the elements of $\operatorname{ConnectData}$ applied to $K$ and $L$ are a basic type.

CochainComplex.ConnectData.cochainComplexdefMathlib.Algebra.Homology.Embedding.Connect, function or constant

Wording

the cochain complex of h (from the name)

English

Let $h$ be an element of $\operatorname{ConnectData}$ applied to $K$ and $L$. Then the cochain complex of $h$ is a cochain complex of $C$ and $\Integer$.

CochainComplex.ConnectData.d₀defMathlib.Algebra.Homology.Embedding.Connect, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ConnectData}$ applied to $K$ and $L$. Then $\mathrm{CochainComplex\_\_ConnectData\_\_d\_u2080\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{X}$ applied to $K$ and $0$ and $\operatorname{X}$ applied to $L$ and $0$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CochainComplex.ConnectData.homologyIsoNegdefMathlib.Algebra.Homology.Embedding.Connect, function or constant

Wording

the homology isomorphism negation of n and m (from the name)

English

Let $h$ be an element of $\operatorname{ConnectData}$ applied to $K$ and $L$. Let $n$ be a natural number. Let $m$ be an integer such that $m = \operatorname{neg} (n + 1)$. Then the homology isomorphism negation of $n$ and $m$ is an isomorphism of the homology of the cochain complex of $h$ and $m$ and the homology of $K$ and $n$.

CochainComplex.ConnectData.homologyIsoPosdefMathlib.Algebra.Homology.Embedding.Connect, function or constant

Wording

the homology isomorphism positive part of n and m (from the name)

English

Let $h$ be an element of $\operatorname{ConnectData}$ applied to $K$ and $L$. Let $n$ be a natural number. Let $m$ be an integer such that $m = n$. Then the homology isomorphism positive part of $n$ and $m$ is an isomorphism of the homology of the cochain complex of $h$ and $m$ and the homology of $L$ and $n$.

CochainComplex.ConnectData.mapdefMathlib.Algebra.Homology.Embedding.Connect, function or constant

Wording

the map of fL and f_comm (from the name)

English

Let $h$ be an element of $\operatorname{ConnectData}$ applied to $K$ and $L$. Let $\mathrm{h'}$ be an element of $\operatorname{ConnectData}$ applied to $\mathrm{K'}$ and $\mathrm{L'}$. Let $\mathrm{fK}$ be a homomorphism of $K$ and $\mathrm{K'}$. Let $\mathrm{fL}$ be a homomorphism of $L$ and $\mathrm{L'}$ such that the composition of $\operatorname{f}$ applied to $\mathrm{fK}$ and $0$ and $\mathrm{CochainComplex\_\_ConnectData\_\_d\_u2080\_}$ applied to $\mathrm{h'}$ is equal to the composition of $\mathrm{CochainComplex\_\_ConnectData\_\_d\_u2080\_}$ applied to $h$ and $\operatorname{f}$ applied to $\mathrm{fL}$ and $0$. Then the map of $\mathrm{fK}$ and $\mathrm{fL}$ is a homomorphism of the cochain complex of $h$ and the cochain complex of $\mathrm{h'}$.

CochainComplex.ConnectData.restrictionGEIsodefMathlib.Algebra.Homology.Embedding.Connect, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{ConnectData}$ applied to $K$ and $L$. Then $\operatorname{restrictionGEIso}$ applied to $h$ is an isomorphism of the restriction of the cochain complex of $h$ and $\operatorname{embeddingUpIntGE}$ applied to $0$ and $L$.

CochainComplex.ConnectData.restrictionLEIsodefMathlib.Algebra.Homology.Embedding.Connect, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{ConnectData}$ applied to $K$ and $L$. Then $\operatorname{restrictionLEIso}$ applied to $h$ is an isomorphism of the restriction of the cochain complex of $h$ and $\operatorname{embeddingUpIntLE}$ applied to $\operatorname{neg}$ applied to $1$ and $K$.

Mathlib.Algebra.Homology.Embedding.Extend

ComplexShape.Embedding.extendFunctordefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then $\operatorname{extendFunctor}$ applied to $e$ and $C$ is a functor of the set of homological complexes of $C$ and $c$ and the set of homological complexes of $C$ and $\mathrm{c'}$.

ComplexShape.Embedding.extendFunctorCompEvalIsodefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Assume that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$. Then $\operatorname{extendFunctorCompEvalIso}$ applied to $e$, $C$ and $h_{1}$ is an isomorphism of the composition of $\operatorname{extendFunctor}$ applied to $e$ and $C$ and the evaluation of $\mathrm{c'}$ and $\mathrm{i'}$ and the evaluation of $c$ and $i$.

ComplexShape.Embedding.fullyFaithfulExtendFunctordefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

the extension functor attached to an embedding of complex shapes of e and C (from the docstring)

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then the extension functor attached to an embedding of complex shapes of $e$ and $C$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{extendFunctor}$ applied to $e$ and $C$.

HomologicalComplex.extenddefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{extend}$ applied to $K$ and $e$ is a homological complex of $C$ and $\mathrm{c'}$.

HomologicalComplex.extend.XIsodefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

the isomorphism of K and hj (from the docstring)

English

Let $K$ be a homological complex of $C$ and $c$. Assume that $\EqtMACRoH {i}{\operatorname{some} (j)}$. Then the isomorphism of $K$ and $\mathrm{hj}$ is an isomorphism of $\operatorname{X}$ applied to $K$ and $i$ and $\operatorname{X}$ applied to $K$ and $j$.

HomologicalComplex.extend.XOpIsodefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

the canonical isomorphism of K and i (from the docstring)

English

Let $K$ be a homological complex of $C$ and $c$. Let $i$ be an element of $\mathrm{Option}$ applied to $x$. Then the canonical isomorphism of $K$ and $i$ is an isomorphism of $\operatorname{X}$ applied to the opposite of $K$ and $i$ and $\operatorname{op}$ applied to $\operatorname{X}$ applied to $K$ and $i$.

HomologicalComplex.extendMapdefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

no wording

English

Let $x_{4}$ be a homomorphism of $K$ and $L$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{extendMap}$ applied to $x_{4}$ and $e$ is a homomorphism of $\operatorname{extend}$ applied to $K$ and $e$ and $\operatorname{extend}$ applied to $L$ and $e$.

HomologicalComplex.extendOpIsodefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

the canonical isomorphism of K and e (from the docstring)

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then the canonical isomorphism of $K$ and $e$ is an isomorphism of $\operatorname{extend}$ applied to the opposite of $K$ and the opposite embedding in $e$ and the opposite of $\operatorname{extend}$ applied to $K$ and $e$.

HomologicalComplex.extendSingleIsodefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $X$ be an element of $C$. Let $i$ be an element of $x$. Let $\mathrm{i'}$ be an element of $x_{1}$ such that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$. Then $\operatorname{extendSingleIso}$ applied to $e$, $X$, $i$, $\mathrm{i'}$ and $h_{1}$ is an isomorphism of $\operatorname{extend}$ applied to the action of $\operatorname{single}$ applied to $C$, $c$ and $i$ and $X$ and $e$ and the action of $\operatorname{single}$ applied to $C$, $\mathrm{c'}$ and $\mathrm{i'}$ and $X$.

HomologicalComplex.extendXIsodefMathlib.Algebra.Homology.Embedding.Extend, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , i)}{\mathrm{i'}}$. Then $\operatorname{extendXIso}$ applied to $K$, $e$ and $h_{1}$ is an isomorphism of $\operatorname{X}$ applied to $\operatorname{extend}$ applied to $K$ and $e$ and $\mathrm{i'}$ and $\operatorname{X}$ applied to $K$ and $i$ defined as the isomorphism of $K$ and $\mathrm{ComplexShape\_\_Embedding\_\_r\_eq\_some}$ applied to $e$ and $h_{1}$.

Mathlib.Algebra.Homology.Embedding.ExtendHomology

HomologicalComplex.extend.homologyDatadefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

the homology data of K (from the docstring)

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Assume that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$. Assume that $\EqtMACRoH {\operatorname{prev} (\mathrm{c'} , \mathrm{j'})}{\mathrm{i'}}$. Assume that $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Assume that $\EqtMACRoH {\operatorname{next} (\mathrm{c'} , \mathrm{j'})}{\mathrm{k'}}$. Let $h_{1}$ be a homology data of $\operatorname{sc'}$ applied to $K$, $i$, $j$ and $k$. Then the homology data of $K$ is a homology data of $\operatorname{sc'}$ applied to $\operatorname{extend}$ applied to $K$ and $e$, $\mathrm{i'}$, $\mathrm{j'}$ and $\mathrm{k'}$.

HomologicalComplex.extend.homologyData'defMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

the homology data of K (from the docstring)

English

HomologicalComplex.extend.leftHomologyDatadefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

the left homology data of K (from the docstring)

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Assume that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$. Assume that $\EqtMACRoH {\operatorname{prev} (\mathrm{c'} , \mathrm{j'})}{\mathrm{i'}}$. Assume that $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Assume that $\EqtMACRoH {\operatorname{next} (\mathrm{c'} , \mathrm{j'})}{\mathrm{k'}}$. Let $h_{1}$ be a left homology data of $\operatorname{sc'}$ applied to $K$, $i$, $j$ and $k$. Then the left homology data of $K$ is a left homology data of $\operatorname{sc'}$ applied to $\operatorname{extend}$ applied to $K$ and $e$, $\mathrm{i'}$, $\mathrm{j'}$ and $\mathrm{k'}$.

HomologicalComplex.extend.leftHomologyData.isLimitKernelForkdefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

the limit kernel fork of K (from the docstring)

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Assume that $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Assume that $\EqtMACRoH {\operatorname{next} (\mathrm{c'} , \mathrm{j'})}{\mathrm{k'}}$. Let $\mathrm{cone}$ be a kernel fork of $\operatorname{d}$ applied to $K$, $j$ and $k$. Let $\mathrm{hcone}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{cone}$. Then the limit kernel fork of $K$ is an element of $\operatorname{IsLimit}$ applied to the kernel fork of $K$ defined as $\operatorname{isLimitOfIsLimitOfIff}$ applied to $\mathrm{hcone}$, $\operatorname{d}$ applied to $\operatorname{extend}$ applied to $K$ and $e$, $\mathrm{j'}$ and $\mathrm{k'}$, the inverse of $\operatorname{extendXIso}$ applied to $K$, $e$ and $\mathrm{hj'}$ and $\mathrm{HomologicalComplex\_\_extend\_\_comp\_d\_eq\_zero\_iff}$ applied to $K$, $e$, $\mathrm{hj'}$, $\mathrm{hk}$ and $\mathrm{hk'}$.

HomologicalComplex.extend.leftHomologyData.kernelForkdefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

the kernel fork of K (from the docstring)

English

HomologicalComplex.extend.rightHomologyDatadefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

the right homology data of K (from the docstring)

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Assume that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$. Assume that $\EqtMACRoH {\operatorname{prev} (\mathrm{c'} , \mathrm{j'})}{\mathrm{i'}}$. Assume that $\EqtMACRoH {\operatorname{next} (c , j)}{k}$. Assume that $\EqtMACRoH {\operatorname{next} (\mathrm{c'} , \mathrm{j'})}{\mathrm{k'}}$. Let $h_{1}$ be a right homology data of $\operatorname{sc'}$ applied to $K$, $i$, $j$ and $k$. Then the right homology data of $K$ is a right homology data of $\operatorname{sc'}$ applied to $\operatorname{extend}$ applied to $K$ and $e$, $\mathrm{i'}$, $\mathrm{j'}$ and $\mathrm{k'}$.

HomologicalComplex.extend.rightHomologyData.cokernelCoforkdefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

the cokernel cofork of K (from the docstring)

English

HomologicalComplex.extend.rightHomologyData.isColimitCokernelCoforkdefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

the colimit cokernel cofork of K (from the docstring)

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Assume that $\EqtMACRoH {\operatorname{prev} (c , j)}{i}$. Assume that $\EqtMACRoH {\operatorname{prev} (\mathrm{c'} , \mathrm{j'})}{\mathrm{i'}}$. Let $\mathrm{cocone}$ be a cokernel cofork of $\operatorname{d}$ applied to $K$, $i$ and $j$. Let $\mathrm{hcocone}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cocone}$. Then the colimit cokernel cofork of $K$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork of $K$ defined as $\operatorname{isColimitOfIsColimitOfIff}$ applied to $\mathrm{hcocone}$, $\operatorname{d}$ applied to $\operatorname{extend}$ applied to $K$ and $e$, $\mathrm{i'}$ and $\mathrm{j'}$, $\operatorname{extendXIso}$ applied to $K$, $e$ and $\mathrm{hj'}$ and $\mathrm{HomologicalComplex\_\_extend\_\_d\_comp\_eq\_zero\_iff}$ applied to $K$, $e$, $\mathrm{hj'}$, $\mathrm{hi}$ and $\mathrm{hi'}$.

HomologicalComplex.extendCyclesIsodefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Then $\operatorname{extendCyclesIso}$ applied to $K$, $e$ and $\mathrm{hj'}$ is an isomorphism of the cycle of $\operatorname{extend}$ applied to $K$ and $e$ and $\mathrm{j'}$ and the cycle of $K$ and $j$.

HomologicalComplex.extendHomologyIsodefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Then $\operatorname{extendHomologyIso}$ applied to $K$, $e$ and $\mathrm{hj'}$ is an isomorphism of the homology of $\operatorname{extend}$ applied to $K$ and $e$ and $\mathrm{j'}$ and the homology of $K$ and $j$.

HomologicalComplex.extendOpcyclesIsodefMathlib.Algebra.Homology.Embedding.ExtendHomology, function or constant

Wording

no wording

English

Let $K$ be a homological complex of $C$ and $c$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$ such that $\EqtMACRoH {\operatorname{f} (e , j)}{\mathrm{j'}}$. Then $\operatorname{extendOpcyclesIso}$ applied to $K$, $e$ and $\mathrm{hj'}$ is an isomorphism of $\operatorname{opcycles}$ applied to $\operatorname{extend}$ applied to $K$ and $e$ and $\mathrm{j'}$ and $\operatorname{opcycles}$ applied to $K$ and $j$.

Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

ComplexShape.Embedding.extendHomotopyFunctordefMathlib.Algebra.Homology.Embedding.ExtendHomotopy, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then $\operatorname{extendHomotopyFunctor}$ applied to $e$ and $C$ is a functor of the set of homotopy categories of $C$ and $c$ and the set of homotopy categories of $C$ and $\mathrm{c'}$.

ComplexShape.Embedding.extendHomotopyFunctorFactorsdefMathlib.Algebra.Homology.Embedding.ExtendHomotopy, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Let $C$ be a set. Then $\operatorname{extendHomotopyFunctorFactors}$ applied to $e$ and $C$ is an isomorphism of the composition of the quotient of $C$ and $c$ and $\operatorname{extendHomotopyFunctor}$ applied to $e$ and $C$ and the composition of $\operatorname{extendFunctor}$ applied to $e$ and $C$ and the quotient of $C$ and $\mathrm{c'}$ defined as the identity of the composition of the quotient of $C$ and $c$ and $\operatorname{extendHomotopyFunctor}$ applied to $e$ and $C$.

Homotopy.extenddefMathlib.Algebra.Homology.Embedding.ExtendHomotopy, function or constant

Wording

no wording

English

Let $h_{1}$ be a homotopy of $f$ and $g$. Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{extend}$ applied to $h_{1}$ and $e$ is a homotopy of $\operatorname{extendMap}$ applied to $f$ and $e$ and $\operatorname{extendMap}$ applied to $g$ and $e$.

Homotopy.extendEquivdefMathlib.Algebra.Homology.Embedding.ExtendHomotopy, function or constant

Wording

no wording

English

Let $e$ be an embedding of $c$ and $\mathrm{c'}$. Then $\operatorname{extendEquiv}$ applied to $e$ is an equivalence from the set of homotopies of $f$ and $g$ to the set of homotopies of $\operatorname{extendMap}$ applied to $f$ and $e$ and $\operatorname{extendMap}$ applied to $g$ and $e$.

Mathlib.Algebra.GroupWithZero.Associated

Mathlib.Algebra.GroupWithZero.Basic

Mathlib.Algebra.GroupWithZero.Defs

Mathlib.Algebra.GroupWithZero.Divisibility

Mathlib.Algebra.GroupWithZero.Equiv

Mathlib.Algebra.GroupWithZero.Hom

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Mathlib.Algebra.GroupWithZero.Pi

Mathlib.Algebra.GroupWithZero.Prod

Mathlib.Algebra.GroupWithZero.ProdHom

Mathlib.Algebra.GroupWithZero.Range

Mathlib.Algebra.GroupWithZero.Submonoid.Primal

Mathlib.Algebra.GroupWithZero.Units.Basic

Mathlib.Algebra.GroupWithZero.Units.Equiv

Mathlib.Algebra.GroupWithZero.Units.Lemmas

Mathlib.Algebra.GroupWithZero.WithZero

Mathlib.Algebra.HierarchyDesign

Mathlib.Algebra.Homology.Additive

Mathlib.Algebra.Homology.AlternatingConst

Mathlib.Algebra.Homology.Augment

Mathlib.Algebra.Homology.Bifunctor

Mathlib.Algebra.Homology.BifunctorAssociator

Mathlib.Algebra.Homology.BifunctorFlip

Mathlib.Algebra.Homology.BifunctorHomotopy

Mathlib.Algebra.Homology.BifunctorShift

Mathlib.Algebra.Homology.CochainComplexOpposite

Mathlib.Algebra.Homology.CochainComplexPlus

Mathlib.Algebra.Homology.CommSq

Mathlib.Algebra.Homology.ComplexShape

Mathlib.Algebra.Homology.ComplexShapeSigns

Mathlib.Algebra.Homology.ConcreteCategory

Mathlib.Algebra.Homology.DerivedCategory.Basic

Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Mathlib.Algebra.Homology.DerivedCategory.Ext.MapAdjunction

Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Mathlib.Algebra.Homology.DerivedCategory.KInjective

Mathlib.Algebra.Homology.DerivedCategory.KProjective

Mathlib.Algebra.Homology.DerivedCategory.Plus

Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus

Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

Mathlib.Algebra.Homology.DerivedCategory.TStructure

Mathlib.Algebra.Homology.DifferentialObject

Mathlib.Algebra.Homology.Double

Mathlib.Algebra.Homology.Embedding.AreComplementary

Mathlib.Algebra.Homology.Embedding.Basic

Mathlib.Algebra.Homology.Embedding.Boundary

Mathlib.Algebra.Homology.Embedding.CochainComplex

Mathlib.Algebra.Homology.Embedding.Connect

Mathlib.Algebra.Homology.Embedding.Extend

Mathlib.Algebra.Homology.Embedding.ExtendHomology

Mathlib.Algebra.Homology.Embedding.ExtendHomotopy