Definitions: Mathlib.RepresentationTheory, part 1 of 2

Representation.LinearizeMonoidal.δdefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $X$ and $Y$ be actions of the set of sets and $G$. Then $\mathrm{Representation\_\_LinearizeMonoidal\_\_\_u3b4\_}$ applied to $X$ and $Y$ is an intertwining map of $\operatorname{linearize}$ applied to $k$, $G$ and the tensor object of $X$ and $Y$ and $\operatorname{tprod}$ applied to $\operatorname{linearize}$ applied to $k$, $G$ and $X$ and $\operatorname{linearize}$ applied to $k$, $G$ and $Y$.

Representation.LinearizeMonoidal.εdefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\mathrm{Representation\_\_LinearizeMonoidal\_\_\_u3b5\_}$ applied to $k$ and $G$ is an intertwining map of $\operatorname{trivial}$ applied to $k$, $G$ and $k$ and $\operatorname{linearize}$ applied to $k$, $G$ and the tensor unity in the monoidal structure of the set of actions of the set of sets and $G$.

Representation.LinearizeMonoidal.ηdefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\mathrm{Representation\_\_LinearizeMonoidal\_\_\_u3b7\_}$ applied to $k$ and $G$ is an intertwining map of $\operatorname{linearize}$ applied to $k$, $G$ and the tensor unity in the monoidal structure of the set of actions of the set of sets and $G$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$.

Representation.LinearizeMonoidal.μdefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $X$ and $Y$ be actions of the set of sets and $G$. Then $\mathrm{Representation\_\_LinearizeMonoidal\_\_\_u3bc\_}$ applied to $X$ and $Y$ is an intertwining map of $\operatorname{tprod}$ applied to $\operatorname{linearize}$ applied to $k$, $G$ and $X$ and $\operatorname{linearize}$ applied to $k$, $G$ and $Y$ and $\operatorname{linearize}$ applied to $k$, $G$ and the tensor object of $X$ and $Y$.

Representation.linearizedefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Let $X$ be an action of the set of sets and $G$. Then $\operatorname{linearize}$ applied to $k$, $G$ and $X$ is a representation of $G$ and the set of monoid algebras of $k$ and $\operatorname{V}$ applied to $X$.

Representation.linearizeDiagonalEquivdefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then $\operatorname{linearizeDiagonalEquiv}$ applied to $k$, $G$ and $n$ is an equivalence of $\operatorname{linearize}$ applied to $k$, $G$ and the diagonal of $G$ and $n$ and the diagonal of $n$ defined as $\operatorname{linearizeOfMulActionIso}$ applied to $k$, $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$.

Representation.linearizeMapdefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{linearizeMap}$ applied to $f$ is an intertwining map of $\operatorname{linearize}$ applied to $k$, $G$ and $X$ and $\operatorname{linearize}$ applied to $k$, $G$ and $Y$.

Representation.linearizeOfMulActionIsodefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $k$, $G$ and $H$ be sets. Then $\operatorname{linearizeOfMulActionIso}$ applied to $k$, $G$ and $H$ is an equivalence of $\operatorname{linearize}$ applied to $k$, $G$ and the action of $G$ and $H$ and the representation of $G$ and $H$.

Representation.linearizeTrivialIsodefMathlib.RepresentationTheory.Action, function or constant

Wording

no wording

English

Let $k$, $G$ and $X$ be sets. Then $\operatorname{linearizeTrivialIso}$ applied to $k$, $G$ and $X$ is an equivalence of $\operatorname{linearize}$ applied to $k$, $G$ and $\operatorname{trivial}$ applied to $G$ and $X$ and $\operatorname{trivial}$ applied to $k$, $G$ and the set of monoid algebras of $k$ and $X$.

Mathlib.RepresentationTheory.Basic

RepresentationdefMathlib.RepresentationTheory.Basic, type

Wording

representation of G and V (from the name)

English

Let $k$, $G$ and $V$ be sets. Then a representation of $G$ and $V$ is an element of the function that maps $k$, $G$ and $V$ to the set of monoid homomorphisms of $G$ and the set of linear maps of $V$ and $V$.

Representation.IsTrivialclassMathlib.RepresentationTheory.Basic, predicate

Wording

x4 is trivial (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Then we can say that $x_{4}$ is trivial.

Representation.asAlgebraHomdefMathlib.RepresentationTheory.Basic, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Then $\operatorname{asAlgebraHom}$ applied to $x_{4}$ is an algebra homomorphism of the set of monoid algebras of $k$ and $G$ and the set of ends of $k$ and $V$ defined as $\operatorname{lift}$ applied to $k$, the set of ends of $k$ and $V$, $G$ and $x_{4}$.

Representation.asGroupHomdefMathlib.RepresentationTheory.Basic, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Then $\operatorname{asGroupHom}$ applied to $x_{4}$ is a monoid homomorphism of $G$ and the set of units of the set of linear maps of $V$ and $V$ defined as the homomorphism unit of $x_{4}$.

Representation.asModuledefMathlib.RepresentationTheory.Basic, type

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Then an element of $\operatorname{asModule}$ applied to $x_{4}$ is an element of the function that maps $x_{4}$ to $V$.

Representation.asModuleEquivdefMathlib.RepresentationTheory.Basic, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Then $\operatorname{asModuleEquiv}$ applied to $x_{4}$ is a linear equivalence of $\operatorname{asModule}$ applied to $x_{4}$ and $V$ defined as the identity map of $k$ and $\operatorname{asModule}$ applied to $x_{4}$.

Representation.diagonaldefMathlib.RepresentationTheory.Basic, function or constant

Wording

the diagonal of n (from the name)

English

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then the diagonal of $n$ is a representation of $G$ and the set of monoid algebras of $k$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ defined as the representation of $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$.

Representation.directSumdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the direct sum of x5 (from the name)

English

Let $x_{5}$ be a function from elements $i_{1}$ of $x_{2}$ to representations of $G$ and $V$ applied to $i_{1}$. Then the direct sum of $i_{1}$ is a representation of $G$ and the set of direct sums of $x_{2}$ and the function that maps $i$ to $V$ applied to $i$.

Representation.dualdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the dual of x4 (from the docstring)

English

Let $x_{4}$ be a representation of $G$ and $V$. Then the dual of $x_{4}$ is a representation of $G$ and the set of duals of $k$ and $V$.

Representation.finsuppdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the finitely supported function of x4 and x5 (from the name)

English

Let $x_{4}$ be a representation of $G$ and $A$. Let $x_{5}$ be a set. Then the finitely supported function of $x_{4}$ and $x_{5}$ is a representation of $G$ and $\FinsuppMACRoQ {x_{5}}{A}$.

Representation.finsuppLEquivFreeAsModuledefMathlib.RepresentationTheory.Basic, function or constant

Wording

the finitely supported function equivalence free as module of G and x2 (from the name)

English

Let $k$, $G$ and $x_{2}$ be sets. Then the finitely supported function equivalence free as module of $G$ and $x_{2}$ is a linear equivalence of the set of finitely supported functions from $x_{2}$ to the set of monoid algebras of $k$ and $G$ and $\operatorname{asModule}$ applied to the free of $G$ and $x_{2}$.

Representation.freedefMathlib.RepresentationTheory.Basic, function or constant

Wording

the free of G and x2 (from the name)

English

Let $k$, $G$ and $x_{2}$ be sets. Then the free of $G$ and $x_{2}$ is a representation of $G$ and the set of finitely supported functions from $x_{2}$ to the set of monoid algebras of $k$ and $G$ defined as the finitely supported function of the left regular of $k$ and $G$ and $x_{2}$.

Representation.freeAsModuleBasisdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the free as module basis of G and x2 (from the name)

English

Let $k$, $G$ and $x_{2}$ be sets. Then the free as module basis of $G$ and $x_{2}$ is a basis of the set of monoid algebras of $k$ and $G$ and $\operatorname{asModule}$ applied to the free of $G$ and $x_{2}$ defined as $\operatorname{ofRepr}$ applied to the inverse of the finitely supported function equivalence free as module of $G$ and $x_{2}$.

Representation.leftRegulardefMathlib.RepresentationTheory.Basic, function or constant

Wording

the left regular of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the left regular of $k$ and $G$ is a representation of $G$ and the set of monoid algebras of $k$ and $G$ defined as the representation of $G$ and $G$.

Representation.linHomdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the linear homomorphism of x6 and x7 (from the name)

English

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the linear homomorphism of $x_{6}$ and $x_{7}$ is a representation of $G$ and the set of linear maps of $V$ and $W$.

Representation.normdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the norm of x5 (from the name)

English

Let $x_{5}$ be a representation of $G$ and $V$. Then the norm of $x_{5}$ is an end of $k$ and $V$ defined as $\FinsetSum {\FinsetunivMACRoAC}{g}{x_{5} (g)}$.

Representation.ofDistribMulActiondefMathlib.RepresentationTheory.Basic, function or constant

Wording

the representation of G and A (from the name)

English

Let $k$, $G$ and $A$ be sets. Then the representation of $G$ and $A$ is a representation of $G$ and $A$.

Representation.ofModuledefMathlib.RepresentationTheory.Basic, function or constant

Wording

the representation of M (from the name)

English

Let $M$ be a set. Then the representation of $M$ is a representation of $G$ and $\mathrm{RestrictScalars}$ applied to $k$, the set of monoid algebras of $k$ and $G$ and $M$ defined as $\operatorname{symm}$ applied to the lift of the set of linear maps of $\mathrm{RestrictScalars}$ applied to $k$, the set of monoid algebras of $k$ and $G$ and $M$ and $\mathrm{RestrictScalars}$ applied to $k$, the set of monoid algebras of $k$ and $G$ and $M$ and $G$ and $\operatorname{lsmul}$ applied to $k$, the set of monoid algebras of $k$ and $G$ and $M$.

Representation.ofModule'defMathlib.RepresentationTheory.Basic, function or constant

Wording

the representation of M (from the name)

English

Let $M$ be a set. Then the representation of $M$ is a representation of $G$ and $M$ defined as $\operatorname{symm}$ applied to the lift of the set of linear maps of $M$ and $M$ and $G$ and $\operatorname{lsmul}$ applied to $k$, $k$ and $M$.

Representation.ofMulActiondefMathlib.RepresentationTheory.Basic, function or constant

Wording

the representation of G and H (from the name)

English

Let $k$, $G$ and $H$ be sets. Then the representation of $G$ and $H$ is a representation of $G$ and the set of monoid algebras of $k$ and $H$.

Representation.ofMulActionSelfAsModuleEquivdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the representation (from the name)

English

The representation is a linear equivalence of $\operatorname{asModule}$ applied to the representation of $G$ and $G$ and the set of monoid algebras of $k$ and $G$.

Representation.ofMulDistribMulActiondefMathlib.RepresentationTheory.Basic, function or constant

Wording

the representation of M and G (from the name)

English

Let $M$ and $G$ be sets. Then the representation of $M$ and $G$ is a representation of $M$ and $\mathrm{Additive}$ applied to $G$ defined as the composition of the monoid homomorphism of the additive monoid end ring isomorphism integer of $\mathrm{Additive}$ applied to $G$ and the composition of the monoid homomorphism of the monoid end of $G$ and the monoid end of $M$ and $G$.

Representation.ofQuotientdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the representation of x4 and S (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $S$ be a subgroup of $G$. Then the representation of $x_{4}$ and $S$ is a representation of the set of quotients of $G$ and $S$ and $V$.

Representation.proddefMathlib.RepresentationTheory.Basic, function or constant

Wording

the product of x6 and x7 (from the name)

English

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the product of $x_{6}$ and $x_{7}$ is a representation of $G$ and $\mathrm{Prod}$ applied to $V$ and $W$.

Representation.quotientdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the quotient of x4 and W (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $W$ be a submodule of $k$ and $V$ such that for all elements $g$ of $G$, $W$ is less than or equal to the preimage of $x_{4}$ applied to $g$ and $W$. Then the quotient of $x_{4}$ and $W$ is a representation of $G$ and the set of quotients of $V$ and $W$.

Representation.subrepresentationdefMathlib.RepresentationTheory.Basic, function or constant

Wording

the subrepresentation of x4 and W (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $W$ be a submodule of $k$ and $V$ such that for all elements $g$ of $G$, $W$ is less than or equal to the preimage of $x_{4}$ applied to $g$ and $W$. Then the subrepresentation of $x_{4}$ and $W$ is a representation of $G$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {W}{x_{5}})}$.

Representation.tproddefMathlib.RepresentationTheory.Basic, function or constant

Wording

no wording

English

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then $\operatorname{tprod}$ applied to $x_{6}$ and $x_{7}$ is a representation of $G$ and the set of tensor products of $V$ and $W$.

Representation.trivialdefMathlib.RepresentationTheory.Basic, function or constant

Wording

no wording

English

Let $k$, $G$ and $V$ be sets. Then $\operatorname{trivial}$ applied to $k$, $G$ and $V$ is a representation of $G$ and $V$ defined as $1$.

Mathlib.RepresentationTheory.Character

FDRep.characterdefMathlib.RepresentationTheory.Character, function or constant

Wording

the character of V and g (from the docstring)

English

Let $V$ be an element of $\mathrm{FDRep}$ applied to $k$ and $G$. Let $g$ be an element of $G$. Then the character of $V$ and $g$ is an element of $k$ defined as $\operatorname{trace}$ applied to $k$, the set of carriers of $\operatorname{V}$ applied to $V$ and $\mathrm{FDRep\_\_\_u3c1\_\_\_app}$ applied to $V$ and $g$.

Representation.characterdefMathlib.RepresentationTheory.Character, function or constant

Wording

the character of x4 and g (from the docstring)

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $g$ be an element of $G$. Then the character of $x_{4}$ and $g$ is an element of $k$ defined as $\operatorname{trace}$ applied to $k$, $V$ and $x_{4}$ applied to $g$.

Mathlib.RepresentationTheory.Coinduced

Rep.coinddefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction of x3 and A (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $A$ be a representation of $k$ and $G$. Then the coinduction of $x_{3}$ and $A$ is a representation of $k$ and $H$ defined as $\operatorname{of}$ applied to the coinduction of $x_{3}$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$.

Rep.coind'defMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction of x3 and A (from the name)

English

Rep.coindFunctordefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction functor of k and x3 (from the name)

English

Let $k$ be a set. Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Then the coinduction functor of $k$ and $x_{3}$ is a functor of the set of representations of $k$ and $G$ and the set of representations of $k$ and $H$.

Rep.coindFunctor'defMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction functor of k and x3 (from the name)

English

Rep.coindFunctorIsodefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction functor isomorphism of x3 (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Then the coinduction functor isomorphism of $x_{3}$ is an isomorphism of the coinduction functor of $k$ and $x_{3}$ and the coinduction functor of $k$ and $x_{3}$.

Rep.coindIsodefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction isomorphism of x3 and A (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $A$ be a representation of $k$ and $G$. Then the coinduction isomorphism of $x_{3}$ and $A$ is an isomorphism of the coinduction of $x_{3}$ and $A$ and the coinduction of $x_{3}$ and $A$.

Rep.coindMapdefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction map of x3 and f (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $f$ be a homomorphism of $A$ and $B$. Then the coinduction map of $x_{3}$ and $f$ is a homomorphism of the coinduction of $x_{3}$ and $A$ and the coinduction of $x_{3}$ and $B$ defined as the representation of the coinduction map of $x_{3}$ and the homomorphism of $f$.

Rep.coindMap'defMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction map of x3 and f (from the name)

English

Rep.coindVEquivdefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction equivalence of x3 and A (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $A$ be a representation of $k$ and $G$. Then the coinduction equivalence of $x_{3}$ and $A$ is a linear equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{coindV} (x_{3} , \mathrm{Rep\_\_\_u3c1\_} (A))}{x_{4}})}$ and the set of homomorphisms of the restriction of $x_{3}$ and the left regular of $k$ and $H$ and $A$.

Rep.resCoindAdjunctiondefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the restriction coinduction adjunction of k and x3 (from the name)

English

Let $k$ be a set. Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Then the restriction coinduction adjunction of $k$ and $x_{3}$ is an adjunction of the restriction functor of $x_{3}$ and the coinduction functor of $k$ and $x_{3}$.

Rep.resCoindHomEquivdefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the restriction coinduction homomorphism equivalence of B and A (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $B$ be a representation of $k$ and $H$. Let $A$ be a representation of $k$ and $G$. Then the restriction coinduction homomorphism equivalence of $B$ and $A$ is a linear equivalence of the set of homomorphisms of the restriction of $x_{3}$ and $B$ and $A$ and the set of homomorphisms of $B$ and the coinduction of $x_{3}$ and $A$.

Rep.resCoindToHomdefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the restriction coinduction to homomorphism of A and f (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $B$ be a representation of $k$ and $H$. Let $A$ be a representation of $k$ and $G$. Let $f$ be a homomorphism of the restriction of $x_{3}$ and $B$ and $A$. Then the restriction coinduction to homomorphism of $A$ and $f$ is a homomorphism of $B$ and the coinduction of $x_{3}$ and $A$.

Representation.coinddefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction of x3 and x6 (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $x_{6}$ be a representation of $G$ and $B$. Then the coinduction of $x_{3}$ and $x_{6}$ is a representation of $H$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{coindV} (x_{3} , x_{6})}{x_{7}})}$.

Representation.coind'defMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction of x3 and A (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $A$ be a representation of $k$ and $G$. Then the coinduction of $x_{3}$ and $A$ is a representation of $H$ and the set of homomorphisms of the restriction of $x_{3}$ and the left regular of $k$ and $H$ and $A$.

Representation.coindMapdefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction map of x3 and f (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $f$ be an intertwining map of $x_{8}$ and $x_{9}$. Then the coinduction map of $x_{3}$ and $f$ is an intertwining map of the coinduction of $x_{3}$ and $x_{8}$ and the coinduction of $x_{3}$ and $x_{9}$.

Representation.coindVdefMathlib.RepresentationTheory.Coinduced, function or constant

Wording

the coinduction of x3 and x6 (from the name)

English

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $x_{6}$ be a representation of $G$ and $A$. Then the coinduction of $x_{3}$ and $x_{6}$ is a submodule of $k$ and the set of functions from elements of $H$ to elements of $A$.

Mathlib.RepresentationTheory.Coinvariants

Rep.coinvariantsAdjunctiondefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\operatorname{coinvariantsAdjunction}$ applied to $k$ and $G$ is an adjunction of $\operatorname{coinvariantsFunctor}$ applied to $k$ and $G$ and the trivial functor of $k$ and $G$.

Rep.coinvariantsFunctordefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\operatorname{coinvariantsFunctor}$ applied to $k$ and $G$ is a functor of the set of representations of $k$ and $G$ and the set of module categories of $k$.

Rep.coinvariantsMkdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\operatorname{coinvariantsMk}$ applied to $k$ and $G$ is a homomorphism of the forgetful functor of the set of representations of $k$ and $G$ and the set of module categories of $k$ and $\operatorname{coinvariantsFunctor}$ applied to $k$ and $G$.

Rep.coinvariantsShortComplexdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then $\operatorname{coinvariantsShortComplex}$ applied to $A$ and $S$ is a short complex of the set of representations of $k$ and $G$.

Rep.coinvariantsTensordefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\operatorname{coinvariantsTensor}$ applied to $k$ and $G$ is a functor of the set of representations of $k$ and $G$ and the set of functors of the set of representations of $k$ and $G$ and the set of module categories of $k$ defined as the action of the action of the postcomposition and $\operatorname{coinvariantsFunctor}$ applied to $k$ and $G$ and the tensor product bifunctor of the set of representations of $k$ and $G$.

Rep.coinvariantsTensorFreeLEquivdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $x_{2}$ be a set. Then $\operatorname{coinvariantsTensorFreeLEquiv}$ applied to $A$ and $x_{2}$ is a linear equivalence of $\operatorname{Coinvariants}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to the tensor object of $A$ and the free of $G$ and $x_{2}$ and $\FinsuppMACRoQ {x_{2}}{\operatorname{V} (A)}$.

Rep.coinvariantsTensorFreeToFinsuppdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $x_{2}$ be a set. Then $\operatorname{coinvariantsTensorFreeToFinsupp}$ applied to $A$ and $x_{2}$ is a linear map of $\operatorname{Coinvariants}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to the tensor object of $A$ and the free of $G$ and $x_{2}$ and $\FinsuppMACRoQ {x_{2}}{\operatorname{V} (A)}$ defined as the composition of $\operatorname{toLinearMap}$ applied to the composition of $\operatorname{coinvariantsFinsuppLEquiv}$ applied to $\operatorname{tprod}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and the left regular of $k$ and $G$ and $x_{2}$ and $\operatorname{lcongr}$ applied to the identity of $x_{2}$ and $\operatorname{coinvariantsTprodLeftRegularLEquiv}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and the map of the finitely supported function of $\operatorname{tprod}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and the left regular of $k$ and $G$ and $x_{2}$ and $\operatorname{toIntertwiningMap}$ applied to the right finitely supported function tensor of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and the left regular of $k$ and $G$.

Rep.coinvariantsTensorMkdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ and $B$ be representations of $k$ and $G$. Then $\operatorname{coinvariantsTensorMk}$ applied to $A$ and $B$ is a linear map of $\operatorname{V}$ applied to $A$ and the set of linear maps of $\operatorname{V}$ applied to $B$ and the set of carriers of the action of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $G$ and $A$ and $B$ defined as $\mathrm{LinearMap\_\_compr\_u2082\_}$ applied to $\operatorname{mk}$ applied to $k$, $\operatorname{V}$ applied to $A$ and $\operatorname{V}$ applied to $B$ and $\operatorname{mk}$ applied to $\operatorname{tprod}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to $B$.

Rep.descdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $A$ and $B$. Then $\operatorname{desc}$ applied to $f$ is a homomorphism of the action of $\operatorname{coinvariantsFunctor}$ applied to $k$ and $G$ and $A$ and $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $B$.

Rep.finsuppToCoinvariantsTensorFreedefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $x_{2}$ be a set. Then $\operatorname{finsuppToCoinvariantsTensorFree}$ applied to $A$ and $x_{2}$ is a linear map of $\FinsuppMACRoQ {x_{2}}{\operatorname{V} (A)}$ and $\operatorname{Coinvariants}$ applied to $\operatorname{tprod}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to the free of $G$ and $x_{2}$ defined as the composition of the map of $\operatorname{tprod}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to the free of $G$ and $x_{2}$ and $\operatorname{toIntertwiningMap}$ applied to the inverse of the right finitely supported function tensor of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and the left regular of $k$ and $G$ and $\operatorname{toLinearMap}$ applied to the inverse of the composition of $\operatorname{coinvariantsFinsuppLEquiv}$ applied to $\operatorname{tprod}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and the left regular of $k$ and $G$ and $x_{2}$ and $\operatorname{lcongr}$ applied to the identity of $x_{2}$ and $\operatorname{coinvariantsTprodLeftRegularLEquiv}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$.

Rep.quotientToCoinvariantsdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then $\operatorname{quotientToCoinvariants}$ applied to $A$ and $S$ is a representation of $k$ and the set of quotients of $G$ and $S$ defined as the representation of $\operatorname{toCoinvariants}$ applied to $A$ and $S$ and $S$.

Rep.quotientToCoinvariantsFunctordefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $k$ be a set. Let $S$ be a subgroup of $G$. Then $\operatorname{quotientToCoinvariantsFunctor}$ applied to $k$ and $S$ is a functor of the set of representations of $k$ and $G$ and the set of representations of $k$ and the set of quotients of $G$ and $S$.

Rep.toCoinvariantsdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then $\operatorname{toCoinvariants}$ applied to $A$ and $S$ is a representation of $k$ and $G$ defined as $\operatorname{of}$ applied to $\operatorname{toCoinvariants}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $S$.

Rep.toCoinvariantsKerdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then $\operatorname{toCoinvariantsKer}$ applied to $A$ and $S$ is a representation of $k$ and $G$ defined as $\operatorname{of}$ applied to $\operatorname{toCoinvariantsKer}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $S$.

Rep.toCoinvariantsMkQdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then $\operatorname{toCoinvariantsMkQ}$ applied to $A$ and $S$ is a homomorphism of $A$ and $\operatorname{toCoinvariants}$ applied to $A$ and $S$ defined as the representation of $\operatorname{toCoinvariantsMkQ}$ applied to $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $S$.

Representation.CoinvariantsdefMathlib.RepresentationTheory.Coinvariants, type

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Then an element of $\operatorname{Coinvariants}$ applied to $x_{4}$ is an element of the function that maps $x_{4}$ to the set of quotients of $V$ and the kernel of $x_{4}$.

Representation.Coinvariants.kerdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

the kernel of x4 (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Then the kernel of $x_{4}$ is a submodule of $k$ and $V$ defined as the span of $k$ and the range of the function that maps $\mathrm{gv}$ to $\operatorname{coe} (x_{4} , \ProdfstMACRoZ {\mathrm{gv}}, \ProdsndMACRoAA {\mathrm{gv}})- \ProdsndMACRoAA {\mathrm{gv}}$.

Representation.Coinvariants.liftdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

the lift of x6 and f (from the name)

English

Let $x_{6}$ be a representation of $G$ and $V$. Let $f$ be a linear map of $V$ and $W$ such that for all elements $x_{7}$ of $G$, the composition of $f$ and $x_{6}$ applied to $x_{7}$ is equal to $f$. Then the lift of $x_{6}$ and $f$ is a linear map of $\operatorname{Coinvariants}$ applied to $x_{6}$ and $W$.

Representation.Coinvariants.mapdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

the map of x7 and f (from the name)

English

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Let $f$ be an intertwining map of $x_{6}$ and $x_{7}$. Then the map of $x_{7}$ and $f$ is a linear map of $\operatorname{Coinvariants}$ applied to $x_{6}$ and $\operatorname{Coinvariants}$ applied to $x_{7}$.

Representation.Coinvariants.mkdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Then $\operatorname{mk}$ applied to $x_{4}$ is a linear map of $V$ and $\operatorname{Coinvariants}$ applied to $x_{4}$ defined as $\operatorname{mkQ}$ applied to the kernel of $x_{4}$.

Representation.coinvariantsFinsuppLEquivdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $x_{5}$ be a set. Then $\operatorname{coinvariantsFinsuppLEquiv}$ applied to $x_{4}$ and $x_{5}$ is a linear equivalence of $\operatorname{Coinvariants}$ applied to the finitely supported function of $x_{4}$ and $x_{5}$ and $\FinsuppMACRoQ {x_{5}}{\operatorname{Coinvariants} (x_{4})}$.

Representation.coinvariantsToFinsuppdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $x_{5}$ be a set. Then $\operatorname{coinvariantsToFinsupp}$ applied to $x_{4}$ and $x_{5}$ is a linear map of $\operatorname{Coinvariants}$ applied to the finitely supported function of $x_{4}$ and $x_{5}$ and $\FinsuppMACRoQ {x_{5}}{\operatorname{Coinvariants} (x_{4})}$.

Representation.coinvariantsTprodLeftRegularLEquivdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Then $\operatorname{coinvariantsTprodLeftRegularLEquiv}$ applied to $x_{4}$ is a linear equivalence of $\operatorname{Coinvariants}$ applied to $\operatorname{tprod}$ applied to $x_{4}$ and the left regular of $k$ and $G$ and $V$.

Representation.finsuppToCoinvariantsdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $x_{5}$ be a set. Then $\operatorname{finsuppToCoinvariants}$ applied to $x_{4}$ and $x_{5}$ is a linear map of $\FinsuppMACRoQ {x_{5}}{\operatorname{Coinvariants} (x_{4})}$ and $\operatorname{Coinvariants}$ applied to the finitely supported function of $x_{4}$ and $x_{5}$.

Representation.ofCoinvariantsTprodLeftRegulardefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

the representation of x4 (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Then the representation of $x_{4}$ is a linear map of $\operatorname{Coinvariants}$ applied to $\operatorname{tprod}$ applied to $x_{4}$ and the left regular of $k$ and $G$ and $V$.

Representation.quotientToCoinvariantsdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $S$ be a subgroup of $G$. Then $\operatorname{quotientToCoinvariants}$ applied to $x_{4}$ and $S$ is a representation of the set of quotients of $G$ and $S$ and $\operatorname{Coinvariants}$ applied to the composition of $x_{4}$ and the subtype of $S$ defined as the representation of $\operatorname{toCoinvariants}$ applied to $x_{4}$ and $S$ and $S$.

Representation.toCoinvariantsdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $S$ be a subgroup of $G$. Then $\operatorname{toCoinvariants}$ applied to $x_{4}$ and $S$ is a representation of $G$ and $\operatorname{Coinvariants}$ applied to the composition of $x_{4}$ and the subtype of $S$ defined as the quotient of $x_{4}$ and the kernel of the composition of $x_{4}$ and the subtype of $S$.

Representation.toCoinvariantsKerdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $S$ be a subgroup of $G$. Then $\operatorname{toCoinvariantsKer}$ applied to $x_{4}$ and $S$ is a representation of $G$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{comp} (x_{4} , \operatorname{subtype} (S)))}{x_{5}})}$ defined as the subrepresentation of $x_{4}$ and the kernel of the composition of $x_{4}$ and the subtype of $S$.

Representation.toCoinvariantsMkQdefMathlib.RepresentationTheory.Coinvariants, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $S$ be a subgroup of $G$. Then $\operatorname{toCoinvariantsMkQ}$ applied to $x_{4}$ and $S$ is an intertwining map of $x_{4}$ and $\operatorname{toCoinvariants}$ applied to $x_{4}$ and $S$.

Mathlib.RepresentationTheory.Continuous.Basic

ContIntertwiningMapstructureMathlib.RepresentationTheory.Continuous.Basic, type

Wording

continuous intertwining map of x8 and x9 (from the name)

English

Let $x_{8}$ be a continuous representation of $G$ and $V$. Let $x_{9}$ be a continuous representation of $G$ and $W$. Then the continuous intertwining maps of $x_{8}$ and $x_{9}$ are a basic type.

ContIntertwiningMap.compdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a continuous intertwining map of $x_{12}$ and $x_{13}$. Let $g$ be a continuous intertwining map of $x_{11}$ and $x_{12}$. Then the composition of $f$ and $g$ is a continuous intertwining map of $x_{11}$ and $x_{13}$.

ContIntertwiningMap.iddefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the identity continuous intertwining map (from the docstring)

English

The identity continuous intertwining map is a continuous intertwining map of $x_{5}$ and $x_{5}$.

ContIntertwiningMap.mapInvariantsdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the map invariant of f (from the name)

English

Let $f$ be a continuous intertwining map of $x_{8}$ and $x_{9}$. Then the map invariant of $f$ is a continuous linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{invariants} (x_{8})}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{invariants} (x_{9})}{x_{11}})}$.

ContIntertwiningMap.mapInvariantsOfResdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the map invariant of x11 and f (from the name)

English

Let $x_{11}$ be a monoid homomorphism of $H$ and $G$. Let $f$ be a continuous intertwining map of the restriction of $x_{9}$ and $x_{11}$ and $x_{10}$. Then the map invariant of $x_{11}$ and $f$ is a continuous linear map of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{invariants} (x_{9})}{x_{12}})}$ and $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {\operatorname{invariants} (x_{10})}{x_{13}})}$.

ContIntertwiningMap.restrictdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the restriction of x11 and f (from the docstring)

English

Let $x_{11}$ be a monoid homomorphism of $H$ and $G$. Let $f$ be a continuous intertwining map of $x_{9}$ and $x_{10}$. Then the restriction of $x_{11}$ and $f$ is a continuous intertwining map of the restriction of $x_{9}$ and $x_{11}$ and the restriction of $x_{10}$ and $x_{11}$.

ContIntertwiningMap.toIntertwiningMapdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the intertwining map of f (from the name)

English

Let $f$ be a continuous intertwining map of $x_{8}$ and $x_{9}$. Then the intertwining map of $f$ is an intertwining map of the representation of $x_{8}$ and the representation of $x_{9}$.

ContRepresentationstructureMathlib.RepresentationTheory.Continuous.Basic, type

Wording

continuous representation of G and V (from the name)

English

Let $R$, $G$ and $V$ be sets. Then the continuous representations of $G$ and $V$ are a basic type.

ContRepresentation.EquivstructureMathlib.RepresentationTheory.Continuous.Basic, type

Wording

equivalence of x8 and x9 (from the name)

English

Let $x_{8}$ be a continuous representation of $G$ and $V$. Let $x_{9}$ be a continuous representation of $G$ and $W$. Then the equivalences of $x_{8}$ and $x_{9}$ are a basic type.

ContRepresentation.Equiv.mkdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

no wording

English

Let $e$ be a continuous linear equivalence of $V$ and $W$ such that for all elements $g$ of $G$, the composition of the continuous linear map of $e$ and $x_{8}$ applied to $g$ is equal to the composition of $x_{9}$ applied to $g$ and the continuous linear map of $e$. Then $\operatorname{mk}$ applied to $e$ and $\mathrm{he}$ is an equivalence of $x_{8}$ and $x_{9}$.

ContRepresentation.Equiv.refldefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the identity of x5 (from the name)

English

Let $x_{5}$ be a continuous representation of $G$ and $V$. Then the identity of $x_{5}$ is an equivalence of $x_{5}$ and $x_{5}$.

ContRepresentation.Equiv.symmdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the inverse of x10 (from the name)

English

Let $x_{10}$ be an equivalence of $x_{8}$ and $x_{9}$. Then the inverse of $x_{10}$ is an equivalence of $x_{9}$ and $x_{8}$.

ContRepresentation.Equiv.toContIntertwiningMapdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the continuous intertwining map of self (from the name)

English

Let $\mathrm{self}$ be an equivalence of $x_{8}$ and $x_{9}$. Then the continuous intertwining map of $\mathrm{self}$ is a continuous intertwining map of $x_{8}$ and $x_{9}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toLinearEquiv}$ applied to $\operatorname{toContinuousLinearEquiv}$ applied to $\mathrm{self}$ and $\operatorname{cont}$ applied to $\mathrm{self}$ and $\operatorname{isIntertwining'}$ applied to $\mathrm{self}$.

ContRepresentation.Equiv.transdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the composition of x14 and x15 (from the name)

English

Let $x_{14}$ be an equivalence of $x_{11}$ and $x_{12}$. Let $x_{15}$ be an equivalence of $x_{12}$ and $x_{13}$. Then the composition of $x_{14}$ and $x_{15}$ is an equivalence of $x_{11}$ and $x_{13}$.

ContRepresentation.coinddefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the coinduction of x9 and x10 (from the name)

English

Let $x_{9}$ be a continuous monoid homomorphism of $G$ and $H$. Let $x_{10}$ be a continuous representation of $G$ and $V$. Then the coinduction of $x_{9}$ and $x_{10}$ is a continuous representation of $H$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{coindV} (x_{9} , x_{10})}{x_{11}})}$.

ContRepresentation.coindVdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the underlying module of the coinduced continuous representation of x9 and x10 (from the docstring)

English

Let $x_{9}$ be a continuous monoid homomorphism of $G$ and $H$. Let $x_{10}$ be a continuous representation of $G$ and $V$. Then the underlying module of the coinduced continuous representation of $x_{9}$ and $x_{10}$ is a submodule of $R$ and the set of continuous maps of $H$ and $V$.

ContRepresentation.coind₁defMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the coinduction of x7 (from the name)

English

Let $x_{7}$ be a continuous representation of $G$ and $V$. Then the coinduction of $x_{7}$ is a continuous representation of $G$ and the set of continuous maps of $G$ and $V$.

ContRepresentation.coind₁EquivcoinddefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

no wording

English

$\mathrm{ContRepresentation\_\_coind\_u2081\_Equivcoind}$ is an equivalence of the coinduction of $\operatorname{trivial}$ applied to $R$, $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{7}})}$ and $V$ and the coinduction of $1$ and $\operatorname{trivial}$ applied to $R$, $G$ and $V$.

ContRepresentation.coind₁MapdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the coinduction map of f (from the name)

English

Let $f$ be a continuous intertwining map of $x_{10}$ and $x_{11}$. Then the coinduction map of $f$ is a continuous intertwining map of the coinduction of $x_{10}$ and the coinduction of $x_{11}$.

ContRepresentation.coind₁ResdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the coinduction restriction of x9 and x10 (from the name)

English

Let $x_{9}$ be a continuous monoid homomorphism of $H$ and $G$. Let $x_{10}$ be a continuous representation of $G$ and $V$. Then the coinduction restriction of $x_{9}$ and $x_{10}$ is a continuous intertwining map of the restriction of the coinduction of $x_{10}$ and the monoid homomorphism of $x_{9}$ and the coinduction of the restriction of $x_{10}$ and the monoid homomorphism of $x_{9}$.

ContRepresentation.coind₁ResMapdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the coinduction restriction map of x14 and f (from the name)

English

Let $x_{14}$ be a continuous monoid homomorphism of $H$ and $G$. Let $f$ be a continuous intertwining map of the restriction of $x_{12}$ and the monoid homomorphism of $x_{14}$ and $x_{13}$. Then the coinduction restriction map of $x_{14}$ and $f$ is a continuous intertwining map of the restriction of the coinduction of $x_{12}$ and the monoid homomorphism of $x_{14}$ and the coinduction of $x_{13}$ defined as the composition of the coinduction map of $f$ and the coinduction restriction of $x_{14}$ and $x_{12}$.

ContRepresentation.coind₁ιdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the coinduction inclusion of x7 (from the name)

English

Let $x_{7}$ be a continuous representation of $G$ and $V$. Then the coinduction inclusion of $x_{7}$ is a continuous intertwining map of $x_{7}$ and the coinduction of $x_{7}$.

ContRepresentation.invariantsdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the invariant of x5 (from the name)

English

Let $x_{5}$ be a continuous representation of $G$ and $V$. Then the invariant of $x_{5}$ is a submodule of $R$ and $V$.

ContRepresentation.restrictdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the restriction of x6 and x7 (from the docstring)

English

Let $x_{6}$ be a continuous representation of $G$ and $V$. Let $x_{7}$ be a monoid homomorphism of $H$ and $G$. Then the restriction of $x_{6}$ and $x_{7}$ is a continuous representation of $H$ and $V$ defined as $\operatorname{ofMonoidHom}$ applied to the composition of the underlying monoid homomorphism of $x_{6}$ and $x_{7}$.

ContRepresentation.toMonoidHomdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the underlying monoid homomorphism of self (from the docstring)

English

Let $\mathrm{self}$ be a continuous representation of $G$ and $V$. Then the underlying monoid homomorphism of $\mathrm{self}$ is a monoid homomorphism of $G$ and the set of continuous linear maps of $V$ and $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ContRepresentation.toRepresentationdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

the representation of x5 (from the name)

English

Let $R$, $G$ and $V$ be sets. Let $x_{5}$ be a continuous representation of $G$ and $V$. Then the representation of $x_{5}$ is a representation of $G$ and $V$ defined as the composition of $\operatorname{toMonoidHom}$ applied to the linear map ring homomorphism and the underlying monoid homomorphism of $x_{5}$.

ContRepresentation.trivialdefMathlib.RepresentationTheory.Continuous.Basic, function or constant

Wording

no wording

English

Let $R$, $G$ and $V$ be sets. Then $\operatorname{trivial}$ applied to $R$, $G$ and $V$ is a continuous representation of $G$ and $V$ defined as $\operatorname{ofMonoidHom}$ applied to $1$.

Mathlib.RepresentationTheory.Continuous.TopRep

TopRepstructureMathlib.RepresentationTheory.Continuous.TopRep, type

Wording

top representation of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the top representations of $k$ and $G$ are a basic type.

TopRep.HomstructureMathlib.RepresentationTheory.Continuous.TopRep, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be top representations of $k$ and $G$. Then the homomorphisms of $A$ and $B$ are a basic type.

TopRep.Hom.homdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Then the homomorphism of $f$ is a continuous intertwining map of $\mathrm{TopRep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{TopRep\_\_\_u3c1\_}$ applied to $B$ defined as the homomorphism of $f$.

TopRep.Hom.hom'defMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the homomorphism of $\mathrm{self}$ is a continuous intertwining map of $\mathrm{TopRep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{TopRep\_\_\_u3c1\_}$ applied to $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

TopRep.Hom.toTopModuleCatHomdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the top module category homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $A$ and $B$. Then the top module category homomorphism of $f$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $B$ defined as the top module category of $\operatorname{toContinuousLinearMap}$ applied to the homomorphism of $f$.

TopRep.TopRepEquivActionTopdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the top representation equivalence action top (from the name)

English

The top representation equivalence action top is an equivalence of the set of top representations of $k$ and $G$ and the set of actions of the set of top module categories of $k$ and $G$.

TopRep.VdefMathlib.RepresentationTheory.Continuous.TopRep, type

Wording

no wording

English

Let $\mathrm{self}$ be a top representation of $k$ and $G$. Then an element of $\operatorname{V}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

TopRep.coind₁defMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the coinduction of A (from the name)

English

Let $A$ be a top representation of $k$ and $G$. Then the coinduction of $A$ is a top representation of $k$ and $G$ defined as $\operatorname{of}$ applied to the coinduction of $\mathrm{TopRep\_\_\_u3c1\_}$ applied to $A$.

TopRep.coind₁FunctordefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the coinduction functor of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the coinduction functor of $k$ and $G$ is a functor of the set of top representations of $k$ and $G$ and the set of top representations of $k$ and $G$.

TopRep.coind₁ιdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the coinduction inclusion (from the name)

English

The coinduction inclusion is a homomorphism of the identity of the set of top representations of $k$ and $G$ and the coinduction functor of $k$ and $G$.

TopRep.fromActionToActiondefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

no wording

English

Let $X$ be an action of the set of top module categories of $k$ and $G$. Then $\operatorname{fromActionToAction}$ applied to $X$ is an isomorphism of the action of $\operatorname{toActionTopModFunc}$ and the action of $\operatorname{fromActionTopModFunc}$ and $X$ and $X$.

TopRep.fromActionTopModFuncdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

no wording

English

$\operatorname{fromActionTopModFunc}$ is a functor of the set of actions of the set of top module categories of $k$ and $G$ and the set of top representations of $k$ and $G$.

TopRep.invariantsdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the invariant of X (from the name)

English

Let $X$ be a top representation of $k$ and $G$. Then the invariant of $X$ is a top module category of $k$ defined as $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{invariants} (\mathrm{TopRep\_\_\_u3c1\_} (X))}{x_{3}})}$.

TopRep.invariantsFunctordefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the invariant functor of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the invariant functor of $k$ and $G$ is a functor of the set of top representations of $k$ and $G$ and the set of top module categories of $k$.

TopRep.invariantsResMapdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the invariant restriction map of x4 and f (from the name)

English

Let $x_{4}$ be a monoid homomorphism of $H$ and $G$. Let $f$ be a homomorphism of the restriction of $x_{4}$ and $X$ and $Y$. Then the invariant restriction map of $x_{4}$ and $f$ is a homomorphism of the invariant of $X$ and the invariant of $Y$ defined as the top module category of the map invariant of $x_{4}$ and the homomorphism of $f$.

TopRep.ofdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

no wording

English

Let $x_{6}$ be a continuous representation of $G$ and $X$. Then $\operatorname{of}$ applied to $x_{6}$ is a top representation of $k$ and $G$ defined as $\mathrm{TopRep\_\_\_mkInternal}$ applied to $X$ and $x_{6}$.

TopRep.ofHomdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the top representation of f (from the name)

English

Let $f$ be a continuous intertwining map of $x_{9}$ and $x_{10}$. Then the top representation of $f$ is a homomorphism of $\operatorname{of}$ applied to $x_{9}$ and $\operatorname{of}$ applied to $x_{10}$ defined as the concrete category of $f$.

TopRep.resdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the restriction of x4 and A (from the docstring)

English

Let $x_{4}$ be a monoid homomorphism of $H$ and $G$. Let $A$ be a top representation of $k$ and $G$. Then the restriction of $x_{4}$ and $A$ is a top representation of $k$ and $H$ defined as $\operatorname{of}$ applied to the restriction of $\mathrm{TopRep\_\_\_u3c1\_}$ applied to $A$ and $x_{4}$.

TopRep.resFunctordefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the restriction functor of x4 (from the name)

English

Let $x_{4}$ be a monoid homomorphism of $H$ and $G$. Then the restriction functor of $x_{4}$ is a functor of the set of top representations of $k$ and $G$ and the set of top representations of $k$ and $H$.

TopRep.toActionFromActiondefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

the action from action of X (from the name)

English

Let $X$ be a top representation of $k$ and $G$. Then the action from action of $X$ is an isomorphism of the action of $\operatorname{fromActionTopModFunc}$ and the action of $\operatorname{toActionTopModFunc}$ and $X$ and $X$.

TopRep.toActionTopModFuncdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

no wording

English

$\operatorname{toActionTopModFunc}$ is a functor of the set of top representations of $k$ and $G$ and the set of actions of the set of top module categories of $k$ and $G$.

TopRep.ρdefMathlib.RepresentationTheory.Continuous.TopRep, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a top representation of $k$ and $G$. Then $\mathrm{TopRep\_\_\_u3c1\_}$ applied to $\mathrm{self}$ is a continuous representation of $G$ and $\operatorname{V}$ applied to $\mathrm{self}$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$.

Mathlib.RepresentationTheory.Equiv

Representation.diagonalOneEquivLeftRegulardefMathlib.RepresentationTheory.Equiv, function or constant

Wording

the diagonal one equivalence left regular of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the diagonal one equivalence left regular of $k$ and $G$ is an equivalence of the diagonal of $1$ and the left regular of $k$ and $G$.

Representation.finsuppTensorLeftdefMathlib.RepresentationTheory.Equiv, function or constant

Wording

the left finitely supported function tensor of x6 and x7 (from the name)

English

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Let $x_{8}$ be a set. Then the left finitely supported function tensor of $x_{6}$ and $x_{7}$ is an equivalence of $\operatorname{tprod}$ applied to the finitely supported function of $x_{6}$ and $x_{8}$ and $x_{7}$ and the finitely supported function of $\operatorname{tprod}$ applied to $x_{6}$ and $x_{7}$ and $x_{8}$.

Representation.finsuppTensorRightdefMathlib.RepresentationTheory.Equiv, function or constant

Wording

the right finitely supported function tensor of x6 and x7 (from the name)

English

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Let $x_{8}$ be a set. Then the right finitely supported function tensor of $x_{6}$ and $x_{7}$ is an equivalence of $\operatorname{tprod}$ applied to $x_{6}$ and the finitely supported function of $x_{7}$ and $x_{8}$ and the finitely supported function of $\operatorname{tprod}$ applied to $x_{6}$ and $x_{7}$ and $x_{8}$.

Representation.freeLiftdefMathlib.RepresentationTheory.Equiv, function or constant

Wording

the free lift of x4 and f (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $f$ be a function from elements of $x_{5}$ to elements of $V$. Then the free lift of $x_{4}$ and $f$ is an intertwining map of the free of $G$ and $x_{5}$ and $x_{4}$.

Representation.freeLiftLEquivdefMathlib.RepresentationTheory.Equiv, function or constant

Wording

the free lift equivalence of x4 and x5 (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $x_{5}$ be a set. Then the free lift equivalence of $x_{4}$ and $x_{5}$ is a linear equivalence of the set of intertwining maps of the free of $G$ and $x_{5}$ and $x_{4}$ and the set of functions from elements of $x_{5}$ to elements of $V$.

Representation.leftRegularMapEquivdefMathlib.RepresentationTheory.Equiv, function or constant

Wording

the left regular map equivalence of x4 (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Then the left regular map equivalence of $x_{4}$ is a linear equivalence of the set of intertwining maps of the left regular of $k$ and $G$ and $x_{4}$ and $V$.

Representation.leftRegularTensorTrivialIsoFreedefMathlib.RepresentationTheory.Equiv, function or constant

Wording

the left regular tensor trivial isomorphism free of x2 (from the name)

English

Let $x_{2}$ be a set. Then the left regular tensor trivial isomorphism free of $x_{2}$ is an equivalence of $\operatorname{tprod}$ applied to the left regular of $k$ and $G$ and $\operatorname{trivial}$ applied to $k$, $G$ and the set of monoid algebras of $k$ and $x_{2}$ and the free of $G$ and $x_{2}$.

Representation.ofMulActionSubsingletonEquivTrivialdefMathlib.RepresentationTheory.Equiv, function or constant

Wording

the representation of G and H (from the name)

English

Let $k$, $G$ and $H$ be sets. Then the representation of $G$ and $H$ is an equivalence of the representation of $G$ and $H$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$.

Mathlib.RepresentationTheory.FDRep

FDRepdefMathlib.RepresentationTheory.FDRep, type

Wording

no wording

English

Let $R$ and $G$ be sets. Then an element of $\mathrm{FDRep}$ applied to $R$ and $G$ is an element of the function that maps $R$ and $G$ to the set of actions of $\mathrm{FGModuleCat}$ applied to $R$ and $G$.

FDRep.dualTensorIsoLinHomdefMathlib.RepresentationTheory.FDRep, function or constant

Wording

the dual tensor isomorphism linear homomorphism of x4 and W (from the name)

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $W$ be an element of $\mathrm{FDRep}$ applied to $k$ and $G$. Then the dual tensor isomorphism linear homomorphism of $x_{4}$ and $W$ is an isomorphism of the tensor object of $\operatorname{of}$ applied to the dual of $x_{4}$ and $W$ and $\operatorname{of}$ applied to the linear homomorphism of $x_{4}$ and $\mathrm{FDRep\_\_\_u3c1\_}$ applied to $W$.

FDRep.forget₂HomLinearEquivdefMathlib.RepresentationTheory.FDRep, function or constant

Wording

no wording

English

Let $X$ and $Y$ be elements of $\mathrm{FDRep}$ applied to $R$ and $G$. Then $\mathrm{FDRep\_\_forget\_u2082\_HomLinearEquiv}$ applied to $X$ and $Y$ is a linear equivalence of the set of homomorphisms of the action of the forgetful functor of $\mathrm{FDRep}$ applied to $R$ and $G$ and the set of representations of $R$ and $G$ and $X$ and the action of the forgetful functor of $\mathrm{FDRep}$ applied to $R$ and $G$ and the set of representations of $R$ and $G$ and $Y$ and the set of homomorphisms of $X$ and $Y$.

FDRep.isoToLinearEquivdefMathlib.RepresentationTheory.FDRep, function or constant

Wording

the isomorphism to linear equivalence of i (from the name)

English

Let $i$ be an isomorphism of $V$ and $W$. Then the isomorphism to linear equivalence of $i$ is a linear equivalence of the set of carriers of $\operatorname{V}$ applied to $V$ and the set of carriers of $\operatorname{V}$ applied to $W$ defined as the isomorphism to linear equivalence of the map isomorphism of $\operatorname{forget}$ applied to $\mathrm{FGModuleCat}$ applied to $R$ and $G$ and $i$.

FDRep.ofdefMathlib.RepresentationTheory.FDRep, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Then $\operatorname{of}$ applied to $x_{4}$ is an element of $\mathrm{FDRep}$ applied to $R$ and $G$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and $V$ and the composition of the monoid homomorphism of the inverse of the end equivalence and the composition of the monoid homomorphism of the inverse of the end ring isomorphism of $\operatorname{of}$ applied to $R$ and $V$ and $x_{4}$.

FDRep.ρdefMathlib.RepresentationTheory.FDRep, function or constant

Wording

no wording

English

Let $V$ be an element of $\mathrm{FDRep}$ applied to $R$ and $G$. Then $\mathrm{FDRep\_\_\_u3c1\_}$ applied to $V$ is a monoid homomorphism of $G$ and the set of linear maps of the set of carriers of $\operatorname{V}$ applied to $V$ and the set of carriers of $\operatorname{V}$ applied to $V$ defined as the composition of the monoid homomorphism of the end ring isomorphism of the object of $\operatorname{V}$ applied to $V$ and the composition of the monoid homomorphism of the end equivalence and $\mathrm{Action\_\_\_u3c1\_}$ applied to $V$.

Mathlib.RepresentationTheory.FiniteIndex

Rep.coindResAdjunctiondefMathlib.RepresentationTheory.FiniteIndex, function or constant

Wording

the coinduction restriction adjunction of k and S (from the name)

English

Let $k$ be a set. Let $S$ be a subgroup of $G$. Then the coinduction restriction adjunction of $k$ and $S$ is an adjunction of the coinduction functor of $k$ and the subtype of $S$ and the restriction functor of the subtype of $S$ defined as the adjunction of the ind restriction adjunction of $k$ and the subtype of $S$ and the ind coinduction natural isomorphism of $k$ and $S$.

Rep.coindToInddefMathlib.RepresentationTheory.FiniteIndex, function or constant

Wording

the coinduction to ind of A (from the name)

English

Let $A$ be a representation of $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then the coinduction to ind of $A$ is a linear map of $\operatorname{V}$ applied to the coinduction of the subtype of $S$ and $A$ and $\operatorname{V}$ applied to the ind of the subtype of $S$ and $A$.

Rep.indCoindIsodefMathlib.RepresentationTheory.FiniteIndex, function or constant

Wording

the ind coinduction isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then the ind coinduction isomorphism of $A$ is an isomorphism of the ind of the subtype of $S$ and $A$ and the coinduction of the subtype of $S$ and $A$.

Rep.indCoindNatIsodefMathlib.RepresentationTheory.FiniteIndex, function or constant

Wording

the ind coinduction natural isomorphism of k and S (from the name)

English

Let $k$ be a set. Let $S$ be a subgroup of $G$. Then the ind coinduction natural isomorphism of $k$ and $S$ is an isomorphism of the ind functor of $k$ and the subtype of $S$ and the coinduction functor of $k$ and the subtype of $S$.

Rep.indToCoinddefMathlib.RepresentationTheory.FiniteIndex, function or constant

Wording

the ind to coinduction of A (from the name)

English

Let $A$ be a representation of $k$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then the ind to coinduction of $A$ is a linear map of $\operatorname{V}$ applied to the ind of the subtype of $S$ and $A$ and $\operatorname{V}$ applied to the coinduction of the subtype of $S$ and $A$.

Rep.resIndAdjunctiondefMathlib.RepresentationTheory.FiniteIndex, function or constant

Wording

the restriction ind adjunction of k and S (from the name)

English

Let $k$ be a set. Let $S$ be a subgroup of $G$. Then the restriction ind adjunction of $k$ and $S$ is an adjunction of the restriction functor of the subtype of $S$ and the ind functor of $k$ and the subtype of $S$ defined as the adjunction of the restriction coinduction adjunction of $k$ and the subtype of $S$ and the inverse of the ind coinduction natural isomorphism of $k$ and $S$.

Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

ContinuousCohomology.cocyclesdefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the cocycle of A and n (from the name)

English

Let $A$ be a top representation of $k$ and $G$. Let $n$ be a natural number. Then the cocycle of $A$ and $n$ is a top module category of $k$ defined as the cycle of the homogeneous cochain of $A$ and $n$.

ContinuousCohomology.πdefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the projection of A and n (from the name)

English

Let $A$ be a top representation of $k$ and $G$. Let $n$ be a natural number. Then the projection of $A$ and $n$ is a homomorphism of the cycle of the homogeneous cochain of $A$ and $n$ and the homology of the homogeneous cochain of $A$ and $n$ defined as the homology projection of the homogeneous cochain of $A$ and $n$.

TopRep.ddefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

no wording

English

Let $X$ be a top representation of $k$ and $G$. Let $n$ be a natural number. Then $\operatorname{d}$ applied to $X$ and $n$ is a homomorphism of the resolution of $X$ and $n$ and the resolution of $X$ and $n + 1$ defined as $\operatorname{brecOn}$ applied to $n$ and $\mathrm{TopRep\_\_d\_\_\_f}$ applied to $X$.

TopRep.homogeneousCochainsdefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the homogeneous cochain of X (from the name)

English

Let $X$ be a top representation of $k$ and $G$. Then the homogeneous cochain of $X$ is a cochain complex of the set of top module categories of $k$ and $\Natural$ defined as the action of the map homological complex of the invariant functor of $k$ and $G$ and $\operatorname{up}$ applied to $\Natural$ and the shifted resolution of $X$.

TopRep.resolutiondefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the resolution of X (from the name)

English

Let $X$ be a top representation of $k$ and $G$. Then the resolution of $X$ is a cochain complex of the set of top representations of $k$ and $G$ and $\Natural$ defined as $\operatorname{of}$ applied to $\operatorname{resolutionX}$ applied to $X$, $\operatorname{d}$ applied to $X$ and $\mathrm{TopRep\_\_d\_comp\_d}$ applied to $X$.

TopRep.resolution'defMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the shifted resolution of X (from the docstring)

English

Let $X$ be a top representation of $k$ and $G$. Then the shifted resolution of $X$ is a cochain complex of the set of top representations of $k$ and $G$ and $\Natural$.

TopRep.resolution'XdefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the resolution of X and n (from the name)

English

Let $X$ be a top representation of $k$ and $G$. Let $n$ be a natural number. Then the resolution of $X$ and $n$ is a top representation of $k$ and $G$ defined as the resolution of $X$ and $n + 1$.

TopRep.resolution'ddefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the shifted boundary map of the resolution of X and n (from the docstring)

English

Let $X$ be a top representation of $k$ and $G$. Let $n$ be a natural number. Then the shifted boundary map of the resolution of $X$ and $n$ is a homomorphism of the resolution of $X$ and $n$ and the resolution of $X$ and $n + 1$ defined as $\operatorname{d}$ applied to $X$ and $n + 1$.

TopRep.resolutionXdefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the resolution of X and x4 (from the name)

English

Let $X$ be a top representation of $k$ and $G$. Let $x_{4}$ be a natural number. Then the resolution of $X$ and $x_{4}$ is a top representation of $k$ and $G$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{TopRep\_\_resolutionX\_\_\_f}$ applied to $X$.

continuousCohomologydefMathlib.RepresentationTheory.Homological.ContCohomology.Basic, function or constant

Wording

the continuous cohomology of n and A (from the docstring)

English

Let $n$ be a natural number. Let $A$ be a top representation of $k$ and $G$. Then the continuous cohomology of $n$ and $A$ is a top module category of $k$ defined as the homology of the homogeneous cochain of $A$ and $n$.

Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

ContinuousCohomology.cochainsMapdefMathlib.RepresentationTheory.Homological.ContCohomology.Functoriality, function or constant

Wording

the cochain map of x6 and f (from the docstring)

English

Let $x_{6}$ be a continuous monoid homomorphism of $H$ and $G$. Let $f$ be a homomorphism of the restriction of the monoid homomorphism of $x_{6}$ and $X$ and $Y$. Then the cochain map of $x_{6}$ and $f$ is a homomorphism of the homogeneous cochain of $X$ and the homogeneous cochain of $Y$.

ContinuousCohomology.cocyclesMapdefMathlib.RepresentationTheory.Homological.ContCohomology.Functoriality, function or constant

Wording

the cocycle map of f and n (from the name)

English

Let $x_{6}$ be a continuous monoid homomorphism of $H$ and $G$. Let $f$ be a homomorphism of the restriction of the monoid homomorphism of $x_{6}$ and $X$ and $Y$. Let $n$ be a natural number. Then the cocycle map of $f$ and $n$ is a homomorphism of the cocycle of $X$ and $n$ and the cocycle of $Y$ and $n$ defined as the map of the cochain map of $x_{6}$ and $f$ and $n$.

ContinuousCohomology.mapdefMathlib.RepresentationTheory.Homological.ContCohomology.Functoriality, function or constant

Wording

the map of f and n (from the name)

English

Let $x_{6}$ be a continuous monoid homomorphism of $H$ and $G$. Let $f$ be a homomorphism of the restriction of the monoid homomorphism of $x_{6}$ and $X$ and $Y$. Let $n$ be a natural number. Then the map of $f$ and $n$ is a homomorphism of the continuous cohomology of $n$ and $X$ and the continuous cohomology of $n$ and $Y$ defined as the map of the cochain map of $x_{6}$ and $f$ and $n$.

ContinuousCohomology.resolutionMapdefMathlib.RepresentationTheory.Homological.ContCohomology.Functoriality, function or constant

Wording

the resolution map of f and i (from the name)

English

Let $x_{6}$ be a continuous monoid homomorphism of $H$ and $G$. Let $f$ be a homomorphism of the restriction of the monoid homomorphism of $x_{6}$ and $X$ and $Y$. Let $i$ be a natural number. Then the resolution map of $f$ and $i$ is a homomorphism of the restriction of the monoid homomorphism of $x_{6}$ and the resolution of $X$ and $i$ and the resolution of $Y$ and $i$ defined as $\operatorname{brecOn}$ applied to $i$ and $\mathrm{ContinuousCohomology\_\_resolutionMap\_\_\_f}$ applied to $x_{6}$ and $f$.

Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

ContinuousCohomology.cocycles₀IsodefMathlib.RepresentationTheory.Homological.ContCohomology.LowDegree, function or constant

Wording

the cocycle isomorphism of X (from the name)

English

Let $X$ be a top representation of $k$ and $G$. Then the cocycle isomorphism of $X$ is an isomorphism of the cocycle of $X$ and $0$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (\operatorname{hom} (\operatorname{d} (\operatorname{homogeneousCochains} (X), 0 , 1))))}{x_{4}})}$.

ContinuousCohomology.d₀kerIsodefMathlib.RepresentationTheory.Homological.ContCohomology.LowDegree, function or constant

Wording

the kernel isomorphism of X (from the name)

English

Let $X$ be a top representation of $k$ and $G$. Then the kernel isomorphism of $X$ is a continuous linear equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (\operatorname{hom} (\operatorname{d} (\operatorname{homogeneousCochains} (X), 0 , 1))))}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{invariants} (\mathrm{TopRep\_\_\_u3c1\_} (X))}{x_{5}})}$.

ContinuousCohomology.zeroIsodefMathlib.RepresentationTheory.Homological.ContCohomology.LowDegree, function or constant

Wording

the zero isomorphism of A (from the name)

English

Let $A$ be a top representation of $k$ and $G$. Then the zero isomorphism of $A$ is an isomorphism of the continuous cohomology of $0$ and $A$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{invariants} (\mathrm{TopRep\_\_\_u3c1\_} (A))}{x_{4}})}$ defined as the composition of the inverse of the canonical isomorphism of the homogeneous cochain of $A$ and the composition of the cocycle isomorphism of $A$ and the top module category of the kernel isomorphism of $A$.

Mathlib.RepresentationTheory.Homological.ContCohomology.Sha

ContinuousCohomology.tateShafarevichdefMathlib.RepresentationTheory.Homological.ContCohomology.Sha, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $V$ to sets. Let $A$ be a top representation of $\Integer$ and the set of absolute Galois groups of $K$. Let $n$ be a natural number. Then $\operatorname{tateShafarevich}$ applied to $f$, $A$ and $n$ is an additive subgroup of the set of carriers of $\operatorname{toModuleCat}$ applied to the continuous cohomology of $n$ and $A$ defined as the infimum of the function that maps $v$ to the additive kernel of the additive monoid homomorphism of $\operatorname{toLinearMap}$ applied to the homomorphism of the map of the identity morphism of the restriction of the monoid homomorphism of the map of the algebra map of $K$ and $f$ applied to $v$ and $A$ and $n$.

Mathlib.RepresentationTheory.Homological.FiniteCyclic

Rep.FiniteCyclicGroup.chainComplexFunctordefMathlib.RepresentationTheory.Homological.FiniteCyclic, function or constant

Wording

the chain complex functor of k and g (from the name)

English

Let $k$ be a set. Let $g$ be an element of $G$. Then the chain complex functor of $k$ and $g$ is a functor of the set of representations of $k$ and $G$ and the set of chain complexes of the set of representations of $k$ and $G$ and $\Natural$.

Rep.FiniteCyclicGroup.moduleCatChainComplexdefMathlib.RepresentationTheory.Homological.FiniteCyclic, function or constant

Wording

the module category chain complex of A and g (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$. Then the module category chain complex of $A$ and $g$ is a chain complex of the set of module categories of $k$ and $\Natural$.

Rep.FiniteCyclicGroup.moduleCatCochainComplexdefMathlib.RepresentationTheory.Homological.FiniteCyclic, function or constant

Wording

the module category cochain complex of A and g (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$. Then the module category cochain complex of $A$ and $g$ is a cochain complex of the set of module categories of $k$ and $\Natural$.

Rep.FiniteCyclicGroup.normHomCompSubdefMathlib.RepresentationTheory.Homological.FiniteCyclic, function or constant

Wording

the norm homomorphism composition difference of A and g (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$. Then the norm homomorphism composition difference of $A$ and $g$ is a short complex of the set of module categories of $k$.

Rep.FiniteCyclicGroup.resolutiondefMathlib.RepresentationTheory.Homological.FiniteCyclic, function or constant

Wording

the resolution of g (from the name)

English

Let $k$ be a set. Let $g$ be an element of $G$ such that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Then the resolution of $g$ is a projective resolution of $\operatorname{trivial}$ applied to $k$, $G$ and $k$.

Rep.FiniteCyclicGroup.resolution.πdefMathlib.RepresentationTheory.Homological.FiniteCyclic, function or constant

Wording

the projection of k and g (from the name)

English

Let $k$ be a set. Let $g$ be an element of $G$. Then the projection of $k$ and $g$ is a homomorphism of the action of the chain complex functor of $k$ and $g$ and the left regular of $k$ and $G$ and the action of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to the set of representations of $k$ and $G$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$ defined as $\operatorname{symm}$ applied to the single equivalence of the action of the chain complex functor of $k$ and $g$ and the left regular of $k$ and $G$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$ and the left regular homomorphism of $\operatorname{trivial}$ applied to $k$, $G$ and $k$ and $1$.

Rep.FiniteCyclicGroup.subCompNormHomdefMathlib.RepresentationTheory.Homological.FiniteCyclic, function or constant

Wording

the difference composition norm homomorphism of A and g (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$. Then the difference composition norm homomorphism of $A$ and $g$ is a short complex of the set of module categories of $k$.

Representation.FiniteCyclicGroup.coinvariantsEquivdefMathlib.RepresentationTheory.Homological.FiniteCyclic, function or constant

Wording

no wording

English

Let $x_{4}$ be a representation of $G$ and $V$. Let $g$ be an element of $G$ such that for all elements $x_{6}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{6}}$. Then $\operatorname{coinvariantsEquiv}$ applied to $x_{4}$, $g$ and $\mathrm{hg}$ is a linear equivalence of $\operatorname{Coinvariants}$ applied to $x_{4}$ and the set of quotients of $V$ and the range of the difference between $x_{4}$ applied to $g$ and the identity.

Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

groupCohomologydefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the group cohomology of A and n (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the group cohomology of $A$ and $n$ is a module category of $k$ defined as the homology of the inhomogeneous cochain of $A$ and $n$.

groupCohomology.cocyclesdefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the cocycle of A and n (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the cocycle of $A$ and $n$ is a module category of $k$ defined as the cycle of the inhomogeneous cochain of $A$ and $n$.

groupCohomology.cocyclesMkdefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the cocycle of f and h (from the name)

English

Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ to elements of $\operatorname{V}$ applied to $A$ such that $\EqtMACRoH {\operatorname{hom} (\operatorname{d} (A , n), f)}{0}$. Then the cocycle of $f$ and $h$ is a carrier of the cocycle of $A$ and $n$.

groupCohomology.iCocyclesdefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the cocycle of A and n (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the cocycle of $A$ and $n$ is a homomorphism of the cocycle of $A$ and $n$ and $\operatorname{X}$ applied to the inhomogeneous cochain of $A$ and $n$ defined as the inclusion of the cycles of the inhomogeneous cochain of $A$ and $n$.

groupCohomology.inhomogeneousCochainsdefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the inhomogeneous cochain of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the inhomogeneous cochain of $A$ is a cochain complex of the set of module categories of $k$ and $\Natural$.

groupCohomology.inhomogeneousCochainsIsodefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the inhomogeneous cochain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the inhomogeneous cochain isomorphism of $A$ is an isomorphism of the inhomogeneous cochain of $A$ and the linear Yoneda object of the bar complex of $k$ and $G$ and $A$.

groupCohomology.toCocyclesdefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the cocycle of i and j (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $i$ and $j$ be natural numbers. Then the cocycle of $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to the inhomogeneous cochain of $A$ and $i$ and the cocycle of $A$ and $j$ defined as the cycle of $i$ and $j$.

groupCohomology.πdefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the projection of A and n (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the projection of $A$ and $n$ is a homomorphism of the cocycle of $A$ and $n$ and the group cohomology of $A$ and $n$ defined as the homology projection of the inhomogeneous cochain of $A$ and $n$.

groupCohomologyIsodefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the group cohomology isomorphism of n and P (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Let $P$ be a projective resolution of $\operatorname{trivial}$ applied to $k$, $G$ and $k$. Then the group cohomology isomorphism of $n$ and $P$ is an isomorphism of the group cohomology of $A$ and $n$ and the homology of the linear Yoneda object of the complex of $P$ and $A$ and $n$ defined as the composition of the group cohomology isomorphism extension of $A$ and $n$ and the isomorphism extension of $n$ and $A$.

groupCohomologyIsoExtdefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

the group cohomology isomorphism extension of A and n (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the group cohomology isomorphism extension of $A$ and $n$ is an isomorphism of the group cohomology of $A$ and $n$ and the action of the action of the extension of $n$ and $\operatorname{op}$ applied to $\operatorname{trivial}$ applied to $k$, $G$ and $k$ and $A$ defined as the composition of the isomorphism of the homomorphism of the homotopy equivalence of the inhomogeneous cochain isomorphism of $A$ and $n$ and the inverse of the extension isomorphism of $A$ and $n$.

inhomogeneousCochains.ddefMathlib.RepresentationTheory.Homological.GroupCohomology.Basic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then $\operatorname{d}$ applied to $A$ and $n$ is a homomorphism of $\operatorname{of}$ applied to $k$ and the set of functions from functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ to elements of $\operatorname{V}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and the set of functions from functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $G$ to elements of $\operatorname{V}$ applied to $A$.

Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Rep.FiniteCyclicGroup.groupCohomologyIsoEvendefMathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic, function or constant

Wording

the group cohomology isomorphism even of g and i (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Let $i$ be an even natural number. Then the group cohomology isomorphism even of $g$ and $i$ is an isomorphism of the group cohomology of $A$ and $i$ and the homology of the norm homomorphism composition difference of $A$ and $g$.

Rep.FiniteCyclicGroup.groupCohomologyIsoOdddefMathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Let $i$ be an odd natural number. Then $\operatorname{groupCohomologyIsoOdd}$ applied to $A$, $g$, $\mathrm{hg}$, $i$ and $\mathrm{hi}$ is an isomorphism of the group cohomology of $A$ and $i$ and the homology of the difference composition norm homomorphism of $A$ and $g$.

Rep.FiniteCyclicGroup.groupCohomologyIso₀defMathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic, function or constant

Wording

the group cohomology isomorphism of A and g (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Then the group cohomology isomorphism of $A$ and $g$ is an isomorphism of the group cohomology of $A$ and $0$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (\operatorname{hom} (\operatorname{applyAsHom} (A , g)- \operatorname{id} (A))))}{x_{2}})}$.

Rep.FiniteCyclicGroup.groupCohomologyπEvendefMathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic, function or constant

Wording

the group cohomology projection even of g and i (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{4}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{4}}$. Let $i$ be an even element of $\Natural$. Then the group cohomology projection even of $g$ and $i$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (\operatorname{hom} (\operatorname{applyAsHom} (A , g)- \operatorname{id} (A))))}{x_{3}})}$ and the group cohomology of $A$ and $i$ defined as the composition of the inverse of the module category cycle isomorphism of the norm homomorphism composition difference of $A$ and $g$ and the composition of the homology projection of the norm homomorphism composition difference of $A$ and $g$ and the inverse of the group cohomology isomorphism even of $g$ and $i$.

Rep.FiniteCyclicGroup.groupCohomologyπOdddefMathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{4}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{4}}$. Let $i$ be an odd element of $\Natural$. Then $\mathrm{Rep\_\_FiniteCyclicGroup\_\_groupCohomology\_u3c0\_Odd}$ applied to $A$, $g$, $\mathrm{hg}$, $i$ and $\mathrm{hi}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (\operatorname{hom} (\operatorname{asHom} (\operatorname{norm} (A)))))}{x_{3}})}$ and the group cohomology of $A$ and $i$ defined as the composition of the inverse of the module category cycle isomorphism of the difference composition norm homomorphism of $A$ and $g$ and the composition of the homology projection of the difference composition norm homomorphism of $A$ and $g$ and the inverse of $\operatorname{groupCohomologyIsoOdd}$ applied to $A$, $g$, $\mathrm{hg}$, $i$ and $\mathrm{hi}$.

Rep.FiniteCyclicGroup.homResolutionIsodefMathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic, function or constant

Wording

the homomorphism resolution isomorphism of A and g (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Then the homomorphism resolution isomorphism of $A$ and $g$ is an isomorphism of the linear Yoneda object of the complex of the resolution of $g$ and $A$ and the module category cochain complex of $A$ and $g$.

Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

groupCohomology.H1InfResdefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the infimum restriction of A and S (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then the infimum restriction of $A$ and $S$ is a short complex of the set of module categories of $k$ defined as the infimum restriction of $S$ and $1$.

groupCohomology.HInfResdefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the infimum restriction of S and n (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Let $n$ be a natural number. Then the infimum restriction of $S$ and $n$ is a short complex of the set of module categories of $k$.

groupCohomology.cochainsFunctordefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the cochain functor of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the cochain functor of $k$ and $G$ is a functor of the set of representations of $k$ and $G$ and the set of cochain complexes of the set of module categories of $k$ and $\Natural$.

groupCohomology.cochainsMapdefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the cochain map of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of the restriction of $f$ and $A$ and $B$. Then the cochain map of $f$ and $x_{3}$ is a homomorphism of the inhomogeneous cochain of $A$ and the inhomogeneous cochain of $B$.

groupCohomology.cochainsMap₁defMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the cochain map of f and x3 (from the name)

English

groupCohomology.cochainsMap₂defMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the cochain map of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of the restriction of $f$ and $A$ and $B$. Then the cochain map of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $H$ and $H$ to elements of $\operatorname{V}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $B$ defined as the module category of the composition of the left composition of $\operatorname{toLinearMap}$ applied to the homomorphism of $x_{3}$ and $\mathrm{Prod}$ applied to $G$ and $G$ and the left function of $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $f$.

groupCohomology.cochainsMap₃defMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the cochain map of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of the restriction of $f$ and $A$ and $B$. Then the cochain map of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $H$ and $\mathrm{Prod}$ applied to $H$ and $H$ to elements of $\operatorname{V}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $B$ defined as the module category of the composition of the left composition of $\operatorname{toLinearMap}$ applied to the homomorphism of $x_{3}$ and $\mathrm{Prod}$ applied to $G$ and $\mathrm{Prod}$ applied to $G$ and $G$ and the left function of $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $f$.

groupCohomology.cocyclesMapdefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the cocycle map of x3 and n (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of the restriction of $f$ and $A$ and $B$. Let $n$ be a natural number. Then the cocycle map of $x_{3}$ and $n$ is a homomorphism of the cocycle of $A$ and $n$ and the cocycle of $B$ and $n$ defined as the map of the cochain map of $f$ and $x_{3}$ and $n$.

groupCohomology.functordefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the functor of n (from the name)

English

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then the functor of $n$ is a functor of the set of representations of $k$ and $G$ and the set of module categories of $k$.

groupCohomology.infNatTransdefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the infimum natural transformation of S and n (from the name)

English

Let $k$ be a set. Let $S$ be a subgroup of $G$. Let $n$ be a natural number. Then the infimum natural transformation of $S$ and $n$ is a homomorphism of the composition of the quotient to invariant functor of $k$ and $S$ and the functor of $n$ and the functor of $n$.

groupCohomology.mapdefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the map of x3 and n (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of the restriction of $f$ and $A$ and $B$. Let $n$ be a natural number. Then the map of $x_{3}$ and $n$ is a homomorphism of the group cohomology of $A$ and $n$ and the group cohomology of $B$ and $n$ defined as the map of the cochain map of $f$ and $x_{3}$ and $n$.

groupCohomology.mapCocycles₁defMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the map cocycle of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of the restriction of $f$ and $A$ and $B$. Then the map cocycle of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2081\_} (A)}{x_{4}})}$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2081\_} (B)}{x_{5}})}$ defined as the cycle map of the explicit left homology data of the short complex of $A$ and the explicit left homology data of the short complex of $B$.

groupCohomology.mapCocycles₂defMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the map cocycle of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of the restriction of $f$ and $A$ and $B$. Then the map cocycle of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2082\_} (A)}{x_{4}})}$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2082\_} (B)}{x_{5}})}$ defined as the cycle map of the explicit left homology data of the short complex of $A$ and the explicit left homology data of the short complex of $B$.

groupCohomology.mapIsodefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the map isomorphism of he and #4 (from the name)

English

Let $e$ be a multiplicative equivalence of $G$ and $H$. Let $\mathrm{e'}$ be a linear equivalence of $\operatorname{V}$ applied to $B$ and $\operatorname{V}$ applied to $A$ such that for all elements $g$ of $G$, the composition of $\operatorname{toLinearMap}$ applied to $\mathrm{e'}$ and $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $B$ and $g$ is equal to the composition of $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $e$ applied to $g$ and $\operatorname{toLinearMap}$ applied to $\mathrm{e'}$. Let $n$ be a natural number. Then the map isomorphism of $\mathrm{e'}$ and $n$ is an isomorphism of the group cohomology of $B$ and $n$ and the group cohomology of $A$ and $n$.

groupCohomology.mapShortComplexH1defMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the map short complex of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of the restriction of $f$ and $A$ and $B$. Then the map short complex of $f$ and $x_{3}$ is a homomorphism of the short complex of $A$ and the short complex of $B$.

groupCohomology.mapShortComplexH2defMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the map short complex of f and x3 (from the name)

English

groupCohomology.resNatTransdefMathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality, function or constant

Wording

the restriction natural transformation of f and n (from the name)

English

Let $k$ be a set. Let $f$ be a monoid homomorphism of $G$ and $H$. Let $n$ be a natural number. Then the restriction natural transformation of $f$ and $n$ is a homomorphism of the functor of $n$ and the composition of the restriction functor of $f$ and the functor of $n$.

Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

groupCohomology.cocyclesMkOfCompEqDdefMathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence, function or constant

Wording

the cocycle of hX and hx (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $X$. Assume that $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the homomorphism of $\operatorname{f}$ applied to $X$ and $x_{2}$ is equal to $\operatorname{hom}$ applied to $\operatorname{d}$ applied to the inhomogeneous cochain of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $X$, $i$ and $j$ and $y$. Then the cocycle of $\mathrm{hX}$ and $\mathrm{hx}$ is a carrier of the cocycle of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $X$ and $j$.

groupCohomology.mapShortComplex₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence, function or constant

Wording

the short complex of hX and hij (from the docstring)

English

Assume that $\operatorname{ShortExact}$ holds for $X$. Assume that $i + 1 = j$. Then the short complex of $\mathrm{hX}$ and $\mathrm{hij}$ is a short complex of the set of module categories of $k$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_'}$ applied to the snake input of $i$ and $j$.

groupCohomology.mapShortComplex₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence, function or constant

Wording

the short complex of X and i (from the docstring)

English

Let $X$ be a short complex of the set of representations of $k$ and $G$. Let $i$ be a natural number. Then the short complex of $X$ and $i$ is a short complex of the set of module categories of $k$ defined as the map of $X$ and the functor of $i$.

groupCohomology.mapShortComplex₃defMathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence, function or constant

Wording

the short complex of hX and hij (from the docstring)

English

groupCohomology.δdefMathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence, function or constant

Wording

no wording

English

Assume that $\operatorname{ShortExact}$ holds for $X$. Let $i$ and $j$ be natural numbers such that $i + 1 = j$. Then $\mathrm{groupCohomology\_\_\_u3b4\_}$ applied to $\mathrm{hX}$, $i$, $j$ and $\mathrm{hij}$ is a homomorphism of the group cohomology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $X$ and $i$ and the group cohomology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $X$ and $j$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_ShortExact\_\_\_u3b4\_}$ applied to $\mathrm{groupCohomology\_\_map\_cochainsFunctor\_shortExact}$ applied to $\mathrm{hX}$, $i$, $j$ and $\mathrm{hij}$.

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

groupCohomology.H0defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{H0}$ applied to $A$ is a module category of $k$ defined as the group cohomology of $A$ and $0$.

groupCohomology.H0IsodefMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism of $A$ is an isomorphism of $\operatorname{H0}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{invariants} (\mathrm{Rep\_\_\_u3c1\_} (A))}{x_{2}})}$ defined as the composition of the inverse of the canonical isomorphism of the inhomogeneous cochain of $A$ and the cocycle isomorphism of $A$.

groupCohomology.H0IsoOfIsTrivialdefMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism of $A$ is an isomorphism of $\operatorname{H0}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $A$.

groupCohomology.H1defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{H1}$ applied to $A$ is a module category of $k$ defined as the group cohomology of $A$ and $1$.

groupCohomology.H1IsodefMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism of $A$ is an isomorphism of $\operatorname{H1}$ applied to $A$ and $\operatorname{H}$ applied to the explicit left homology data of the short complex of $A$ defined as the composition of the inverse of the left homology isomorphism of $\operatorname{sc}$ applied to the inhomogeneous cochain of $A$ and $1$ and the left homology map isomorphism of the left homology data of $\operatorname{sc}$ applied to the inhomogeneous cochain of $A$ and $1$ and the explicit left homology data of the short complex of $A$.

groupCohomology.H1IsoOfIsTrivialdefMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism of $A$ is an isomorphism of $\operatorname{H1}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and the set of additive monoid homomorphisms of $\mathrm{Additive}$ applied to $G$ and $\operatorname{V}$ applied to $A$.

groupCohomology.H1πdefMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the projection of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the projection of $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2081\_} (A)}{x_{2}})}$ and $\operatorname{H1}$ applied to $A$ defined as the composition of the inverse of the isomorphism cocycle of $A$ and the projection of $A$ and $1$.

groupCohomology.H2defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{H2}$ applied to $A$ is a module category of $k$ defined as the group cohomology of $A$ and $2$.

groupCohomology.H2IsodefMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism of $A$ is an isomorphism of $\operatorname{H2}$ applied to $A$ and $\operatorname{H}$ applied to the explicit left homology data of the short complex of $A$ defined as the composition of the inverse of the left homology isomorphism of $\operatorname{sc}$ applied to the inhomogeneous cochain of $A$ and $2$ and the left homology map isomorphism of the left homology data of $\operatorname{sc}$ applied to the inhomogeneous cochain of $A$ and $2$ and the explicit left homology data of the short complex of $A$.

groupCohomology.H2πdefMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the projection of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the projection of $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2082\_} (A)}{x_{2}})}$ and $\operatorname{H2}$ applied to $A$ defined as the composition of the inverse of the isomorphism cocycle of $A$ and the projection of $A$ and $2$.

groupCohomology.IsCoboundary₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, predicate

Wording

f is coboundary (from the name)

English

Let $f$ be a function from elements of $G$ to elements of $A$. Then $f$ is coboundary, if there exists an element $x_{2}$ of $A$, such that for all elements $g$ of $G$, $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{x_{2}}- x_{2}}{f (g)}$.

groupCohomology.IsCoboundary₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, predicate

Wording

f is coboundary (from the name)

English

Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $A$. Then $f$ is coboundary, if there exists a function $x_{3}$ from elements of $G$ to elements of $A$, such that for all elements $g$ and $h$ of $G$, $\EqtMACRoH {\HSMulhSMulMACRoAL {g}{x_{3} (h)}- x_{3} (g \times h)+ x_{3} (g)}{f (\ProdmkMACRoU {g}{h})}$.

groupCohomology.IsCocycle₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, predicate

Wording

f is a cocycle (from the name)

English

Let $f$ be a function from elements of $G$ to elements of $A$. Then $f$ is a cocycle, if for all elements $g$ and $h$ of $G$, $\EqtMACRoH {f (g \times h)}{\HSMulhSMulMACRoAL {g}{f (h)}+ f (g)}$.

groupCohomology.IsCocycle₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, predicate

Wording

f is a cocycle (from the name)

English

Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $A$. Then $f$ is a cocycle, if for all elements $g$, $h$ and $j$ of $G$, $\EqtMACRoH {f (\ProdmkMACRoU {(g \times h)}{j})+ f (\ProdmkMACRoU {g}{h})}{\HSMulhSMulMACRoAL {g}{f (\ProdmkMACRoU {h}{j})}+ f (\ProdmkMACRoU {g}{(h \times j)})}$.

groupCohomology.IsMulCoboundary₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, predicate

Wording

no wording

English

Let $f$ be a function from elements of $G$ to elements of $M$. Then $\mathrm{groupCohomology\_\_IsMulCoboundary\_u2081\_}$ holds for $f$, if there exists an element $x_{2}$ of $M$, such that for all elements $g$ of $G$, $\EqtMACRoH {\frac{ \HSMulhSMulMACRoAL {g}{x_{2}}}{x_{2}}}{f (g)}$.

groupCohomology.IsMulCoboundary₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, predicate

Wording

no wording

English

Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $M$. Then $\mathrm{groupCohomology\_\_IsMulCoboundary\_u2082\_}$ holds for $f$, if there exists a function $x_{3}$ from elements of $G$ to elements of $M$, such that for all elements $g$ and $h$ of $G$, $\EqtMACRoH {\frac{ \HSMulhSMulMACRoAL {g}{x_{3} (h)}}{x_{3} (g \times h)}\times x_{3} (g)}{f (\ProdmkMACRoU {g}{h})}$.

groupCohomology.IsMulCocycle₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, predicate

Wording

f is a multiplicative cocycle (from the name)

English

Let $f$ be a function from elements of $G$ to elements of $M$. Then $f$ is a multiplicative cocycle, if for all elements $g$ and $h$ of $G$, $\EqtMACRoH {f (g \times h)}{\HSMulhSMulMACRoAL {g}{f (h)}\times f (g)}$.

groupCohomology.IsMulCocycle₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, predicate

Wording

f is a multiplicative cocycle (from the name)

English

Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $M$. Then $f$ is a multiplicative cocycle, if for all elements $g$, $h$ and $j$ of $G$, $\EqtMACRoH {f (\ProdmkMACRoU {(g \times h)}{j})\times f (\ProdmkMACRoU {g}{h})}{\HSMulhSMulMACRoAL {g}{f (\ProdmkMACRoU {h}{j})}\times f (\ProdmkMACRoU {g}{(h \times j)})}$.

groupCohomology.coboundariesOfIsCoboundary₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Assume that $f$ is coboundary. Then $\mathrm{groupCohomology\_\_coboundariesOfIsCoboundary\_u2081\_}$ applied to $\mathrm{hf}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_coboundaries\_u2081\_} (\operatorname{ofDistribMulAction} (G , A))}{x_{5}})}$ defined as $f$.

groupCohomology.coboundariesOfIsCoboundary₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Assume that $f$ is coboundary. Then $\mathrm{groupCohomology\_\_coboundariesOfIsCoboundary\_u2082\_}$ applied to $\mathrm{hf}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_coboundaries\_u2082\_} (\operatorname{ofDistribMulAction} (G , A))}{x_{5}})}$ defined as $f$.

groupCohomology.coboundariesOfIsMulCoboundary₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Assume that $\mathrm{groupCohomology\_\_IsMulCoboundary\_u2081\_}$ holds for $f$. Then $\mathrm{groupCohomology\_\_coboundariesOfIsMulCoboundary\_u2081\_}$ applied to $\mathrm{hf}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_coboundaries\_u2081\_} (\operatorname{ofMulDistribMulAction} (G , M))}{x_{3}})}$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofMul}$ and $f$.

groupCohomology.coboundariesOfIsMulCoboundary₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Assume that $\mathrm{groupCohomology\_\_IsMulCoboundary\_u2082\_}$ holds for $f$. Then $\mathrm{groupCohomology\_\_coboundariesOfIsMulCoboundary\_u2082\_}$ applied to $\mathrm{hf}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_coboundaries\_u2082\_} (\operatorname{ofMulDistribMulAction} (G , M))}{x_{3}})}$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofMul}$ and $f$.

groupCohomology.coboundariesToCocycles₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupCohomology\_\_coboundariesToCocycles\_u2081\_}$ applied to $A$ is a linear map of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_coboundaries\_u2081\_} (A)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2081\_} (A)}{x_{3}})}$ defined as the inclusion of $\mathrm{groupCohomology\_\_coboundaries\_u2081\_\_le\_cocycles\_u2081\_}$ applied to $A$.

groupCohomology.coboundariesToCocycles₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupCohomology\_\_coboundariesToCocycles\_u2082\_}$ applied to $A$ is a linear map of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_coboundaries\_u2082\_} (A)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2082\_} (A)}{x_{3}})}$ defined as the inclusion of $\mathrm{groupCohomology\_\_coboundaries\_u2082\_\_le\_cocycles\_u2082\_}$ applied to $A$.

groupCohomology.coboundaries₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupCohomology\_\_coboundaries\_u2081\_}$ applied to $A$ is a submodule of $k$ and the set of functions from elements of $G$ to elements of $\operatorname{V}$ applied to $A$ defined as the range of the homomorphism of $\mathrm{groupCohomology\_\_d\_u2080\_\_u2081\_}$ applied to $A$.

groupCohomology.coboundaries₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupCohomology\_\_coboundaries\_u2082\_}$ applied to $A$ is a submodule of $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $A$ defined as the range of the homomorphism of $\mathrm{groupCohomology\_\_d\_u2081\_\_u2082\_}$ applied to $A$.

groupCohomology.cochainsIso₀defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cochain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cochain isomorphism of $A$ is an isomorphism of $\operatorname{X}$ applied to the inhomogeneous cochain of $A$ and $0$ and $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $A$ defined as the module isomorphism of $\operatorname{funUnique}$ applied to the set of functions from elements of $\mathrm{Fin}$ applied to $0$ to elements of $G$, $k$ and $\operatorname{V}$ applied to $A$.

groupCohomology.cochainsIso₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cochain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cochain isomorphism of $A$ is an isomorphism of $\operatorname{X}$ applied to the inhomogeneous cochain of $A$ and $1$ and $\operatorname{of}$ applied to $k$ and the set of functions from elements of $G$ to elements of $\operatorname{V}$ applied to $A$ defined as the inverse of the module isomorphism of the left function congruence of $\operatorname{funUnique}$ applied to $\mathrm{Fin}$ applied to $1$ and $G$.

groupCohomology.cochainsIso₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cochain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cochain isomorphism of $A$ is an isomorphism of $\operatorname{X}$ applied to the inhomogeneous cochain of $A$ and $2$ and $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $A$ defined as the inverse of the module isomorphism of the left function congruence of $\mathrm{piFinTwoEquiv}$ applied to the function that maps $x_{2}$ to $G$.

groupCohomology.cochainsIso₃defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cochain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cochain isomorphism of $A$ is an isomorphism of $\operatorname{X}$ applied to the inhomogeneous cochain of $A$ and $3$ and $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $A$ defined as the inverse of the module isomorphism of the left function congruence of the composition of the inverse of $\operatorname{consEquiv}$ applied to the function that maps $x_{2}$ to $G$ and the product congruence of the identity of $G$ and $\mathrm{piFinTwoEquiv}$ applied to the function that maps $x_{3}$ to $G$.

groupCohomology.cocyclesIso₀defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cocycle isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cocycle isomorphism of $A$ is an isomorphism of the cocycle of $A$ and $0$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{invariants} (\mathrm{Rep\_\_\_u3c1\_} (A))}{x_{2}})}$.

groupCohomology.cocyclesOfIsCocycle₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cocycle of hf (from the name)

English

Assume that $f$ is a cocycle. Then the cocycle of $\mathrm{hf}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2081\_} (\operatorname{ofDistribMulAction} (G , A))}{x_{5}})}$ defined as $f$.

groupCohomology.cocyclesOfIsCocycle₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cocycle of hf (from the name)

English

Assume that $f$ is a cocycle. Then the cocycle of $\mathrm{hf}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2082\_} (\operatorname{ofDistribMulAction} (G , A))}{x_{5}})}$ defined as $f$.

groupCohomology.cocyclesOfIsMulCocycle₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cocycle of hf (from the name)

English

Assume that $f$ is a multiplicative cocycle. Then the cocycle of $\mathrm{hf}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2081\_} (\operatorname{ofMulDistribMulAction} (G , M))}{x_{3}})}$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofMul}$ and $f$.

groupCohomology.cocyclesOfIsMulCocycle₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cocycle of hf (from the name)

English

Assume that $f$ is a multiplicative cocycle. Then the cocycle of $\mathrm{hf}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2082\_} (\operatorname{ofMulDistribMulAction} (G , M))}{x_{3}})}$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofMul}$ and $f$.

groupCohomology.cocycles₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cocycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cocycle of $A$ is a submodule of $k$ and the set of functions from elements of $G$ to elements of $\operatorname{V}$ applied to $A$ defined as the kernel of the homomorphism of $\mathrm{groupCohomology\_\_d\_u2081\_\_u2082\_}$ applied to $A$.

groupCohomology.cocycles₁IsoOfIsTrivialdefMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cocycle isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cocycle isomorphism of $A$ is an isomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2081\_} (A)}{x_{2}})}$ and $\operatorname{of}$ applied to $k$ and the set of additive monoid homomorphisms of $\mathrm{Additive}$ applied to $G$ and $\operatorname{V}$ applied to $A$.

groupCohomology.cocycles₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the cocycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cocycle of $A$ is a submodule of $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $A$ defined as the kernel of the homomorphism of $\mathrm{groupCohomology\_\_d\_u2082\_\_u2083\_}$ applied to $A$.

groupCohomology.dArrowIso₀₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the arrow of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the arrow of $A$ is an isomorphism of $\operatorname{mk}$ applied to $\operatorname{d}$ applied to the inhomogeneous cochain of $A$, $0$ and $1$ and $\operatorname{mk}$ applied to $\mathrm{groupCohomology\_\_d\_u2080\_\_u2081\_}$ applied to $A$ defined as the isomorphism of the cochain isomorphism of $A$ and the cochain isomorphism of $A$.

groupCohomology.d₀₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupCohomology\_\_d\_u2080\_\_u2081\_}$ applied to $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and the set of functions from elements of $G$ to elements of $\operatorname{V}$ applied to $A$.

groupCohomology.d₁₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupCohomology\_\_d\_u2081\_\_u2082\_}$ applied to $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and the set of functions from elements of $G$ to elements of $\operatorname{V}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $A$.

groupCohomology.d₂₃defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupCohomology\_\_d\_u2082\_\_u2083\_}$ applied to $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $A$ and $\operatorname{of}$ applied to $k$ and the set of functions from elements of $\mathrm{Prod}$ applied to $G$ and $\mathrm{Prod}$ applied to $G$ and $G$ to elements of $\operatorname{V}$ applied to $A$.

groupCohomology.isoCocycles₁defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the isomorphism cocycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism cocycle of $A$ is an isomorphism of the cocycle of $A$ and $1$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2081\_} (A)}{x_{2}})}$ defined as the cycle map isomorphism of the left homology data of $\operatorname{sc}$ applied to the inhomogeneous cochain of $A$ and $1$ and the explicit left homology data of the short complex of $A$.

groupCohomology.isoCocycles₂defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the isomorphism cocycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism cocycle of $A$ is an isomorphism of the cocycle of $A$ and $2$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupCohomology\_\_cocycles\_u2082\_} (A)}{x_{2}})}$ defined as the cycle map isomorphism of the left homology data of $\operatorname{sc}$ applied to the inhomogeneous cochain of $A$ and $2$ and the explicit left homology data of the short complex of $A$.

groupCohomology.isoShortComplexH1defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the short complex of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is an isomorphism of $\operatorname{sc}$ applied to the inhomogeneous cochain of $A$ and $1$ and the short complex of $A$.

groupCohomology.isoShortComplexH2defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the short complex of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is an isomorphism of $\operatorname{sc}$ applied to the inhomogeneous cochain of $A$ and $2$ and the short complex of $A$.

groupCohomology.shortComplexH0defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the short complex of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is a short complex of the set of module categories of $k$ defined as $\operatorname{mk}$ applied to the module category of the subtype of the invariant of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$, $\mathrm{groupCohomology\_\_d\_u2080\_\_u2081\_}$ applied to $A$ and $\mathrm{groupCohomology\_\_subtype\_comp\_d\_u2080\_\_u2081\_}$ applied to $A$.

groupCohomology.shortComplexH1defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the short complex of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is a short complex of the set of module categories of $k$ defined as $\operatorname{mk}$ applied to $\mathrm{groupCohomology\_\_d\_u2080\_\_u2081\_}$ applied to $A$, $\mathrm{groupCohomology\_\_d\_u2081\_\_u2082\_}$ applied to $A$ and $\mathrm{groupCohomology\_\_d\_u2080\_\_u2081\_\_comp\_d\_u2081\_\_u2082\_}$ applied to $A$.

groupCohomology.shortComplexH2defMathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree, function or constant

Wording

the short complex of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is a short complex of the set of module categories of $k$ defined as $\operatorname{mk}$ applied to $\mathrm{groupCohomology\_\_d\_u2081\_\_u2082\_}$ applied to $A$, $\mathrm{groupCohomology\_\_d\_u2082\_\_u2083\_}$ applied to $A$ and $\mathrm{groupCohomology\_\_d\_u2081\_\_u2082\_\_comp\_d\_u2082\_\_u2083\_}$ applied to $A$.

Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro

groupCohomology.coindIsodefMathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro, function or constant

Wording

the coinduction isomorphism of A and n (from the name)

English

Let $A$ be a representation of $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Let $n$ be a natural number. Then the coinduction isomorphism of $A$ and $n$ is an isomorphism of the group cohomology of the coinduction of the subtype of $S$ and $A$ and $n$ and the group cohomology of $A$ and $n$ defined as the composition of the map isomorphism of the homology functor of $\operatorname{up}$ applied to $\Natural$ and $n$ and the composition of the inhomogeneous cochain isomorphism of the coinduction of the subtype of $S$ and $A$ and the inverse of the linear Yoneda object restriction projective resolution isomorphism of the bar resolution of $k$ and $G$ and $A$ and the inverse of the group cohomology isomorphism of $n$ and the map projective resolution of the restriction functor of the subtype of $S$ and the bar resolution of $k$ and $G$.

groupCohomology.linearYonedaObjResProjectiveResolutionIsodefMathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro, function or constant

Wording

the linear Yoneda object restriction projective resolution isomorphism of P and A (from the name)

English

Let $P$ be a projective resolution of $\operatorname{trivial}$ applied to $k$, $G$ and $k$. Let $A$ be a representation of $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Then the linear Yoneda object restriction projective resolution isomorphism of $P$ and $A$ is an isomorphism of the linear Yoneda object of the complex of the map projective resolution of the restriction functor of the subtype of $S$ and $P$ and $A$ and the linear Yoneda object of the complex of $P$ and the coinduction of the subtype of $S$ and $A$.

Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

HomologicalComplex.coinvariantsTensorObjdefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $P$ be a chain complex of the set of representations of $k$ and $G$ and $x_{2}$. Then $\operatorname{coinvariantsTensorObj}$ applied to $A$ and $P$ is a chain complex of the set of module categories of $k$ and $x_{2}$ defined as the action of the map homological complex of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $G$ and $A$ and $\operatorname{down}$ applied to $x_{2}$ and $P$.

Rep.TordefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then $\operatorname{Tor}$ applied to $k$, $G$ and $n$ is a functor of the set of representations of $k$ and $G$ and the set of functors of the set of representations of $k$ and $G$ and the set of module categories of $k$.

Rep.torIsodefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $P$ be a projective resolution of $B$. Let $n$ be a natural number. Then $\operatorname{torIso}$ applied to $A$, $P$ and $n$ is an isomorphism of the action of the action of $\operatorname{Tor}$ applied to $k$, $G$ and $n$ and $A$ and $B$ and the homology of $\operatorname{coinvariantsTensorObj}$ applied to $A$ and the complex of $P$ and $n$ defined as the isomorphism left derived object of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $G$ and $A$ and $n$.

groupHomologydefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the group homology of A and n (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the group homology of $A$ and $n$ is a module category of $k$ defined as the homology of the inhomogeneous chain of $A$ and $n$.

groupHomology.cyclesdefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the cycle of A and n (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the cycle of $A$ and $n$ is a module category of $k$ defined as the cycle of the inhomogeneous chain of $A$ and $n$.

groupHomology.cyclesMkdefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the cycle of n and f (from the name)

English

Let $m$ and $n$ be natural numbers such that $\operatorname{next} (\operatorname{down} (\Natural), m)= n$. Let $f$ be an element of $\FinsuppMACRoQ {(\mathrm{Elem} (\mathrm{Fin} (m))\rightarrow G)}{\operatorname{V} (A)}$ such that $\operatorname{hom}$ applied to $\operatorname{d}$ applied to the inhomogeneous chain of $A$, $m$ and $n$ and $f$ is equal to $0$. Then the cycle of $n$ and $f$ is a carrier of the cycle of $A$ and $m$ defined as the cycle of $f$ and $n$.

groupHomology.iCyclesdefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the cycle of A and n (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the cycle of $A$ and $n$ is a homomorphism of the cycle of $A$ and $n$ and $\operatorname{X}$ applied to the inhomogeneous chain of $A$ and $n$ defined as the inclusion of the cycles of the inhomogeneous chain of $A$ and $n$.

groupHomology.inhomogeneousChainsdefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the inhomogeneous chain of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the inhomogeneous chain of $A$ is a chain complex of the set of module categories of $k$ and $\Natural$.

groupHomology.inhomogeneousChains.ddefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then $\operatorname{d}$ applied to $A$ and $n$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {(\mathrm{Elem} (\mathrm{Fin} (n + 1))\rightarrow G)}{\operatorname{V} (A)}$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {(\mathrm{Elem} (\mathrm{Fin} (n))\rightarrow G)}{\operatorname{V} (A)}$ defined as the module category of $\operatorname{lsum}$ applied to $k$ and the function that maps $g_{1}$ to the sum of the composition of $\operatorname{lsingle}$ applied to the function that maps $i$ to $g_{1}$ applied to $\operatorname{succ}$ applied to $i$ and $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $\operatorname{inv}$ applied to $g_{1}$ applied to $0$ and $\FinsetSum {\FinsetunivMACRoAC}{j}{(\HSMulhSMulMACRoAL {(\operatorname{neg} (1)^ {(\operatorname{val} (j)+ 1)})}{\operatorname{lsingle} (\operatorname{contractNth} (j , \lambda x_{6} . \lambda x_{7} . x_{6} \times x_{7} , g_{1}))})}$.

groupHomology.inhomogeneousChainsIsodefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the inhomogeneous chain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the inhomogeneous chain isomorphism of $A$ is an isomorphism of the inhomogeneous chain of $A$ and $\operatorname{coinvariantsTensorObj}$ applied to $A$ and the bar complex of $k$ and $G$.

groupHomology.toCyclesdefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the cycle of i and j (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $i$ and $j$ be natural numbers. Then the cycle of $i$ and $j$ is a homomorphism of $\operatorname{X}$ applied to the inhomogeneous chain of $A$ and $i$ and the cycle of $A$ and $j$ defined as the cycle of $i$ and $j$.

groupHomology.πdefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the projection of A and n (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the projection of $A$ and $n$ is a homomorphism of the cycle of $A$ and $n$ and the group homology of $A$ and $n$ defined as the homology projection of the inhomogeneous chain of $A$ and $n$.

groupHomologyIsodefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

the group homology isomorphism of n and P (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Let $P$ be a projective resolution of $\operatorname{trivial}$ applied to $k$, $G$ and $k$. Then the group homology isomorphism of $n$ and $P$ is an isomorphism of the group homology of $A$ and $n$ and the homology of $\operatorname{coinvariantsTensorObj}$ applied to $A$ and the complex of $P$ and $n$ defined as the composition of $\mathrm{groupHomologyIsoTor}$ applied to $A$ and $n$ and $\operatorname{torIso}$ applied to $A$, $P$ and $n$.

groupHomologyIsoTordefMathlib.RepresentationTheory.Homological.GroupHomology.Basic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then $\mathrm{groupHomologyIsoTor}$ applied to $A$ and $n$ is an isomorphism of the group homology of $A$ and $n$ and the action of the action of $\operatorname{Tor}$ applied to $k$, $G$ and $n$ and $A$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$ defined as the composition of the isomorphism of the homomorphism of the homotopy equivalence of the inhomogeneous chain isomorphism of $A$ and $n$ and the inverse of $\operatorname{torIso}$ applied to $A$, the bar resolution of $k$ and $G$ and $n$.

Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIsodefMathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Then $\operatorname{coinvariantsTensorResolutionIso}$ applied to $A$, $g$ and $\mathrm{hg}$ is an isomorphism of $\operatorname{coinvariantsTensorObj}$ applied to $A$ and the complex of the resolution of $\operatorname{inv}$ applied to $g$ and the module category chain complex of $A$ and $g$.

Rep.FiniteCyclicGroup.groupHomologyIsoEvendefMathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic, function or constant

Wording

the group homology isomorphism even of g and i (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{4}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{4}}$. Let $i$ be an even natural number. Then the group homology isomorphism even of $g$ and $i$ is an isomorphism of the group homology of $A$ and $i$ and the homology of the difference composition norm homomorphism of $A$ and $g$.

Rep.FiniteCyclicGroup.groupHomologyIsoOdddefMathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{4}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{4}}$. Let $i$ be an odd natural number. Then $\operatorname{groupHomologyIsoOdd}$ applied to $A$, $g$, $\mathrm{hg}$, $i$ and $\mathrm{hi}$ is an isomorphism of the group homology of $A$ and $i$ and the homology of the norm homomorphism composition difference of $A$ and $g$.

Rep.FiniteCyclicGroup.groupHomologyIso₀defMathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic, function or constant

Wording

the group homology isomorphism of A and g (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{3}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{3}}$. Then the group homology isomorphism of $A$ and $g$ is an isomorphism of the group homology of $A$ and $0$ and $\operatorname{of}$ applied to $k$ and the set of quotients of $\operatorname{V}$ applied to $A$ and the range of $\operatorname{toLinearMap}$ applied to the homomorphism of the difference between $\operatorname{applyAsHom}$ applied to $A$ and $g$ and the identity morphism of $A$.

Rep.FiniteCyclicGroup.groupHomologyπEvendefMathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic, function or constant

Wording

the group homology projection even of g and i (from the name)

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{5}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{5}}$. Let $i$ be an even element of $\Natural$. Then the group homology projection even of $g$ and $i$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{norm} (\mathrm{Rep\_\_\_u3c1\_} (A)))}{x_{4}})}$ and the group homology of $A$ and $i$ defined as the composition of the inverse of the module category cycle isomorphism of the difference composition norm homomorphism of $A$ and $g$ and the composition of the homology projection of the difference composition norm homomorphism of $A$ and $g$ and the inverse of the group homology isomorphism even of $g$ and $i$.

Rep.FiniteCyclicGroup.groupHomologyπOdddefMathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$ such that for all elements $x_{5}$ of $G$, $\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{5}}$. Let $i$ be an odd element of $\Natural$. Then $\mathrm{Rep\_\_FiniteCyclicGroup\_\_groupHomology\_u3c0\_Odd}$ applied to $A$, $g$, $\mathrm{hg}$, $i$ and $\mathrm{hi}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (\operatorname{hom} (\operatorname{applyAsHom} (A , g)- \operatorname{id} (A))))}{x_{4}})}$ and the group homology of $A$ and $i$ defined as the composition of the inverse of the module category cycle isomorphism of the norm homomorphism composition difference of $A$ and $g$ and the composition of the homology projection of the norm homomorphism composition difference of $A$ and $g$ and the inverse of $\operatorname{groupHomologyIsoOdd}$ applied to $A$, $g$, $\mathrm{hg}$, $i$ and $\mathrm{hi}$.

Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

groupHomology.H1CoresCoinfdefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then $\operatorname{H1CoresCoinf}$ applied to $A$ and $S$ is a short complex of the set of module categories of $k$.

groupHomology.H1CoresCoinfOfTrivialdefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then $\operatorname{H1CoresCoinfOfTrivial}$ applied to $A$ and $S$ is a short complex of the set of module categories of $k$.

groupHomology.chainsFunctordefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the chain functor of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the chain functor of $k$ and $G$ is a functor of the set of representations of $k$ and $G$ and the set of chain complexes of the set of module categories of $k$ and $\Natural$.

groupHomology.chainsMapdefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the chain map of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Then the chain map of $f$ and $x_{3}$ is a homomorphism of the inhomogeneous chain of $A$ and the inhomogeneous chain of $B$.

groupHomology.chainsMap₁defMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the chain map of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Then the chain map of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {G}{\operatorname{V} (A)}$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {H}{\operatorname{V} (B)}$ defined as the module category of the composition of the linear map of $\operatorname{toLinearMap}$ applied to the homomorphism of $x_{3}$ and $\operatorname{lmapDomain}$ applied to $\operatorname{V}$ applied to $A$, $k$ and $\operatorname{coe}$ applied to $f$.

groupHomology.chainsMap₂defMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the chain map of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Then the chain map of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{\operatorname{V} (A)}$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (H , H)}{\operatorname{V} (B)}$ defined as the module category of the composition of the linear map of $\operatorname{toLinearMap}$ applied to the homomorphism of $x_{3}$ and $\operatorname{lmapDomain}$ applied to $\operatorname{V}$ applied to $A$, $k$ and $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $f$.

groupHomology.chainsMap₃defMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the chain map of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Then the chain map of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , \mathrm{Prod} (G , G))}{\operatorname{V} (A)}$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (H , \mathrm{Prod} (H , H))}{\operatorname{V} (B)}$ defined as the module category of the composition of the linear map of $\operatorname{toLinearMap}$ applied to the homomorphism of $x_{3}$ and $\operatorname{lmapDomain}$ applied to $\operatorname{V}$ applied to $A$, $k$ and $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{map}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $f$.

groupHomology.coinfNatTransdefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

no wording

English

Let $k$ be a set. Let $S$ be a subgroup of $G$. Let $n$ be a natural number. Then $\operatorname{coinfNatTrans}$ applied to $k$, $S$ and $n$ is a homomorphism of the functor of $n$ and the composition of $\operatorname{quotientToCoinvariantsFunctor}$ applied to $k$ and $S$ and the functor of $n$.

groupHomology.coresNatTransdefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the core natural transformation of f and n (from the name)

English

Let $k$ be a set. Let $f$ be a monoid homomorphism of $G$ and $H$. Let $n$ be a natural number. Then the core natural transformation of $f$ and $n$ is a homomorphism of the composition of the restriction functor of $f$ and the functor of $n$ and the functor of $n$.

groupHomology.cyclesMapdefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the cycle map of x3 and n (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Let $n$ be a natural number. Then the cycle map of $x_{3}$ and $n$ is a homomorphism of the cycle of $A$ and $n$ and the cycle of $B$ and $n$ defined as the map of the chain map of $f$ and $x_{3}$ and $n$.

groupHomology.functordefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the functor of n (from the name)

English

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then the functor of $n$ is a functor of the set of representations of $k$ and $G$ and the set of module categories of $k$.

groupHomology.mapdefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the map of x3 and n (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Let $n$ be a natural number. Then the map of $x_{3}$ and $n$ is a homomorphism of the group homology of $A$ and $n$ and the group homology of $B$ and $n$ defined as the map of the chain map of $f$ and $x_{3}$ and $n$.

groupHomology.mapCycles₁defMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the map cycle of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Then the map cycle of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2081\_} (A)}{x_{4}})}$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2081\_} (B)}{x_{5}})}$ defined as the cycle map of the explicit left homology data of the short complex of $A$ and the explicit left homology data of the short complex of $B$.

groupHomology.mapCycles₂defMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the map cycle of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Then the map cycle of $f$ and $x_{3}$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2082\_} (A)}{x_{4}})}$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2082\_} (B)}{x_{5}})}$ defined as the cycle map of the explicit left homology data of the short complex of $A$ and the explicit left homology data of the short complex of $B$.

groupHomology.mapIsodefMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the map isomorphism of he and #4 (from the name)

English

Let $e$ be a multiplicative equivalence of $G$ and $H$. Let $\mathrm{e'}$ be a linear equivalence of $\operatorname{V}$ applied to $A$ and $\operatorname{V}$ applied to $B$ such that for all elements $g$ of $G$, the composition of $\operatorname{toLinearMap}$ applied to $\mathrm{e'}$ and $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $g$ is equal to the composition of $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $B$ and $e$ applied to $g$ and $\operatorname{toLinearMap}$ applied to $\mathrm{e'}$. Let $n$ be a natural number. Then the map isomorphism of $\mathrm{e'}$ and $n$ is an isomorphism of the group homology of $A$ and $n$ and the group homology of $B$ and $n$.

groupHomology.mapShortComplexH1defMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the map short complex of f and x3 (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $H$. Let $x_{3}$ be a homomorphism of $A$ and the restriction of $f$ and $B$. Then the map short complex of $f$ and $x_{3}$ is a homomorphism of the short complex of $A$ and the short complex of $B$.

groupHomology.mapShortComplexH2defMathlib.RepresentationTheory.Homological.GroupHomology.Functoriality, function or constant

Wording

the map short complex of f and x3 (from the name)

English

Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

groupHomology.cyclesMkOfCompEqDdefMathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence, function or constant

Wording

the cycle of hX and hx (from the name)

English

Assume that $\operatorname{ShortExact}$ holds for $X$. Assume that $\operatorname{linearMap}$ applied to $\operatorname{toLinearMap}$ applied to the homomorphism of $\operatorname{f}$ applied to $X$ and $x_{2}$ is equal to $\operatorname{hom}$ applied to $\operatorname{d}$ applied to the inhomogeneous chain of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2082\_}$ applied to $X$, $i$ and $j$ and $y$. Then the cycle of $\mathrm{hX}$ and $\mathrm{hx}$ is a carrier of the cycle of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $X$ and $j$.

groupHomology.mapShortComplex₁defMathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence, function or constant

Wording

the short complex of hX and hij (from the docstring)

English

Assume that $\operatorname{ShortExact}$ holds for $X$. Assume that $j + 1 = i$. Then the short complex of $\mathrm{hX}$ and $\mathrm{hij}$ is a short complex of the set of module categories of $k$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_SnakeInput\_\_L\_u2082\_'}$ applied to the snake input of $i$ and $j$.

groupHomology.mapShortComplex₂defMathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence, function or constant

Wording

the short complex of X and i (from the docstring)

English

groupHomology.mapShortComplex₃defMathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence, function or constant

Wording

the short complex of hX and hij (from the docstring)

English

groupHomology.δdefMathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence, function or constant

Wording

no wording

English

Assume that $\operatorname{ShortExact}$ holds for $X$. Let $i$ and $j$ be natural numbers such that $j + 1 = i$. Then $\mathrm{groupHomology\_\_\_u3b4\_}$ applied to $\mathrm{hX}$, $i$, $j$ and $\mathrm{hij}$ is a homomorphism of the group homology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $X$ and $i$ and the group homology of $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $X$ and $j$ defined as $\mathrm{CategoryTheory\_\_ShortComplex\_\_ShortExact\_\_\_u3b4\_}$ applied to $\mathrm{groupHomology\_\_map\_chainsFunctor\_shortExact}$ applied to $\mathrm{hX}$, $i$, $j$ and $\mathrm{hij}$.

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

groupHomology.H0defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{H0}$ applied to $A$ is a module category of $k$ defined as the group homology of $A$ and $0$.

groupHomology.H0IsodefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism of $A$ is an isomorphism of $\operatorname{H0}$ applied to $A$ and the action of $\operatorname{coinvariantsFunctor}$ applied to $k$ and $G$ and $A$ defined as the composition of the canonical isomorphism of the inhomogeneous chain of $A$ and $\mathrm{groupHomology\_\_opcyclesIso\_u2080\_}$ applied to $A$.

groupHomology.H0IsoOfIsTrivialdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

groupHomology.H0πdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the projection of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the projection of $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $A$ and $\operatorname{H0}$ applied to $A$ defined as the composition of the inverse of the cycle isomorphism of $A$ and the projection of $A$ and $0$.

groupHomology.H1defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{H1}$ applied to $A$ is a module category of $k$ defined as the group homology of $A$ and $1$.

groupHomology.H1AddEquivOfIsTrivialdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the additive equivalence of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the additive equivalence of $A$ is an additive equivalence of the set of carriers of $\operatorname{H1}$ applied to $A$ and the set of tensor products of $\mathrm{Additive}$ applied to the set of abelianizations of $G$ and $\operatorname{V}$ applied to $A$.

groupHomology.H1IsodefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism of $A$ is an isomorphism of $\operatorname{H1}$ applied to $A$ and $\operatorname{H}$ applied to the explicit left homology data of the short complex of $A$ defined as the composition of the inverse of the left homology isomorphism of $\operatorname{sc}$ applied to the inhomogeneous chain of $A$ and $1$ and the left homology map isomorphism of the left homology data of $\operatorname{sc}$ applied to the inhomogeneous chain of $A$ and $1$ and the explicit left homology data of the short complex of $A$.

groupHomology.H1ToTensorOfIsTrivialdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{H1ToTensorOfIsTrivial}$ applied to $A$ is a linear map of the set of carriers of $\operatorname{H1}$ applied to $A$ and the set of tensor products of $\mathrm{Additive}$ applied to the set of abelianizations of $G$ and $\operatorname{V}$ applied to $A$.

groupHomology.H1πdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the projection of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the projection of $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2081\_} (A)}{x_{2}})}$ and $\operatorname{H1}$ applied to $A$ defined as the composition of the inverse of the isomorphism cycle of $A$ and the projection of $A$ and $1$.

groupHomology.H2defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{H2}$ applied to $A$ is a module category of $k$ defined as the group homology of $A$ and $2$.

groupHomology.H2IsodefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism of $A$ is an isomorphism of $\operatorname{H2}$ applied to $A$ and $\operatorname{H}$ applied to the explicit left homology data of the short complex of $A$ defined as the composition of the inverse of the left homology isomorphism of $\operatorname{sc}$ applied to the inhomogeneous chain of $A$ and $2$ and the left homology map isomorphism of the left homology data of $\operatorname{sc}$ applied to the inhomogeneous chain of $A$ and $2$ and the explicit left homology data of the short complex of $A$.

groupHomology.H2πdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the projection of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the projection of $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2082\_} (A)}{x_{2}})}$ and $\operatorname{H2}$ applied to $A$ defined as the composition of the inverse of the isomorphism cycle of $A$ and the projection of $A$ and $2$.

groupHomology.IsBoundary₀defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, predicate

Wording

a is a boundary (from the name)

English

Let $G$ be a set. Let $a$ be an element of $A$. Then $a$ is a boundary, if there exists an element $x_{3}$ of $\FinsuppMACRoQ {G}{A}$, such that the sum of $x_{3}$ and the function that maps $g$ and $z$ to $\HSMulhSMulMACRoAL {\operatorname{inv} (g)}{z}- z$ is equal to $a$.

groupHomology.IsBoundary₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, predicate

Wording

x4 is a boundary (from the name)

English

Let $x_{4}$ be an element of $\FinsuppMACRoQ {G}{A}$. Then $x_{4}$ is a boundary, if there exists an element $y$ of $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{A}$, such that the sum of $y$ and the function that maps $g$ and $a$ to $\FinsuppsingleMACRoS {\ProdsndMACRoAA {g}}{(\HSMulhSMulMACRoAL {\operatorname{inv} (\ProdfstMACRoZ {g})}{a})}- \FinsuppsingleMACRoS {(\ProdfstMACRoZ {g}\times \ProdsndMACRoAA {g})}{a}+ \FinsuppsingleMACRoS {\ProdfstMACRoZ {g}}{a}$ is equal to $x_{4}$.

groupHomology.IsBoundary₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, predicate

Wording

x4 is a boundary (from the name)

English

Let $x_{4}$ be an element of $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{A}$. Then $x_{4}$ is a boundary, if there exists an element $y$ of $\FinsuppMACRoQ {\mathrm{Prod} (G , \mathrm{Prod} (G , G))}{A}$, such that the sum of $y$ and the function that maps $g$ and $a$ to $\FinsuppsingleMACRoS {(\ProdmkMACRoU {\ProdfstMACRoZ {\ProdsndMACRoAA {g}}}{\ProdsndMACRoAA {\ProdsndMACRoAA {g}}})}{(\HSMulhSMulMACRoAL {\operatorname{inv} (\ProdfstMACRoZ {g})}{a})}- \FinsuppsingleMACRoS {(\ProdmkMACRoU {(\ProdfstMACRoZ {g}\times \ProdfstMACRoZ {\ProdsndMACRoAA {g}})}{\ProdsndMACRoAA {\ProdsndMACRoAA {g}}})}{a}+ \FinsuppsingleMACRoS {(\ProdmkMACRoU {\ProdfstMACRoZ {g}}{(\ProdfstMACRoZ {\ProdsndMACRoAA {g}}\times \ProdsndMACRoAA {\ProdsndMACRoAA {g}})})}{a}- \FinsuppsingleMACRoS {(\ProdmkMACRoU {\ProdfstMACRoZ {g}}{\ProdfstMACRoZ {\ProdsndMACRoAA {g}}})}{a}$ is equal to $x_{4}$.

groupHomology.IsCycle₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, predicate

Wording

x3 is a cycle (from the name)

English

Let $x_{3}$ be an element of $\FinsuppMACRoQ {G}{A}$. Then $x_{3}$ is a cycle, if the sum of $x_{3}$ and the function that maps $g$ and $a$ to $\HSMulhSMulMACRoAL {\operatorname{inv} (g)}{a}$ is equal to the sum of $x_{3}$ and the function that maps $x_{4}$ and $a_{1}$ to $a_{1}$.

groupHomology.IsCycle₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, predicate

Wording

x4 is a cycle (from the name)

English

Let $x_{4}$ be an element of $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{A}$. Then $x_{4}$ is a cycle, if the sum of $x_{4}$ and the function that maps $g$ and $a$ to $\FinsuppsingleMACRoS {\ProdsndMACRoAA {g}}{(\HSMulhSMulMACRoAL {\operatorname{inv} (\ProdfstMACRoZ {g})}{a})}+ \FinsuppsingleMACRoS {\ProdfstMACRoZ {g}}{a}$ is equal to the sum of $x_{4}$ and the function that maps $g_{1}$ and $a_{1}$ to $\FinsuppsingleMACRoS {(\ProdfstMACRoZ {g_{1}}\times \ProdsndMACRoAA {g_{1}})}{a_{1}}$.

groupHomology.boundariesOfIsBoundary₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the boundary of x5 and hx (from the name)

English

Let $x_{5}$ be an element of $\FinsuppMACRoQ {G}{A}$ such that $x_{5}$ is a boundary. Then the boundary of $x_{5}$ and $\mathrm{hx}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_boundaries\_u2081\_} (\operatorname{ofDistribMulAction} (G , A))}{x_{6}})}$ defined as $x_{5}$.

groupHomology.boundariesOfIsBoundary₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the boundary of x5 and hx (from the name)

English

Let $x_{5}$ be an element of $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{A}$ such that $x_{5}$ is a boundary. Then the boundary of $x_{5}$ and $\mathrm{hx}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_boundaries\_u2082\_} (\operatorname{ofDistribMulAction} (G , A))}{x_{6}})}$ defined as $x_{5}$.

groupHomology.boundariesToCycles₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the boundary to cycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the boundary to cycle of $A$ is a linear map of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_boundaries\_u2081\_} (A)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2081\_} (A)}{x_{3}})}$ defined as the inclusion of $\mathrm{groupHomology\_\_boundaries\_u2081\_\_le\_cycles\_u2081\_}$ applied to $A$.

groupHomology.boundariesToCycles₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the boundary to cycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the boundary to cycle of $A$ is a linear map of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_boundaries\_u2082\_} (A)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2082\_} (A)}{x_{3}})}$ defined as the inclusion of $\mathrm{groupHomology\_\_boundaries\_u2082\_\_le\_cycles\_u2082\_}$ applied to $A$.

groupHomology.boundaries₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the boundary of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the boundary of $A$ is a submodule of $k$ and $\FinsuppMACRoQ {G}{\operatorname{V} (A)}$ defined as the range of the homomorphism of $\mathrm{groupHomology\_\_d\_u2082\_\_u2081\_}$ applied to $A$.

groupHomology.boundaries₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the boundary of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the boundary of $A$ is a submodule of $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{\operatorname{V} (A)}$ defined as the range of the homomorphism of $\mathrm{groupHomology\_\_d\_u2083\_\_u2082\_}$ applied to $A$.

groupHomology.chainsIso₀defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the chain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the chain isomorphism of $A$ is an isomorphism of $\operatorname{X}$ applied to the inhomogeneous chain of $A$ and $0$ and $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $A$ defined as the module isomorphism of the unique linear equivalence of $\operatorname{default}$.

groupHomology.chainsIso₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the chain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the chain isomorphism of $A$ is an isomorphism of $\operatorname{X}$ applied to the inhomogeneous chain of $A$ and $1$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {G}{\operatorname{V} (A)}$ defined as the module isomorphism of the domain congruence of $\operatorname{funUnique}$ applied to $\mathrm{Fin}$ applied to $1$ and $G$.

groupHomology.chainsIso₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the chain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the chain isomorphism of $A$ is an isomorphism of $\operatorname{X}$ applied to the inhomogeneous chain of $A$ and $2$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{\operatorname{V} (A)}$ defined as the module isomorphism of the domain congruence of $\mathrm{piFinTwoEquiv}$ applied to the function that maps $x_{2}$ to $G$.

groupHomology.chainsIso₃defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the chain isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the chain isomorphism of $A$ is an isomorphism of $\operatorname{X}$ applied to the inhomogeneous chain of $A$ and $3$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , \mathrm{Prod} (G , G))}{\operatorname{V} (A)}$ defined as the module isomorphism of the domain congruence of the composition of the inverse of $\operatorname{consEquiv}$ applied to the function that maps $i$ to $G$ and the product congruence of the identity of $G$ and $\mathrm{piFinTwoEquiv}$ applied to the function that maps $x_{2}$ to $G$.

groupHomology.chains₁ToCoinvariantsKerdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupHomology\_\_chains\_u2081\_ToCoinvariantsKer}$ applied to $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {G}{\operatorname{V} (A)}$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{ker} (\mathrm{Rep\_\_\_u3c1\_} (A))}{x_{2}})}$.

groupHomology.coinvariantsKerOfIsBoundary₀defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $x_{5}$ be an element of $A$ such that $x_{5}$ is a boundary. Then $\mathrm{groupHomology\_\_coinvariantsKerOfIsBoundary\_u2080\_}$ applied to $x_{5}$ and $\mathrm{hx}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{ofDistribMulAction} (G , A))}{x_{6}})}$ defined as $x_{5}$.

groupHomology.cyclesIso₀defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the cycle isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cycle isomorphism of $A$ is an isomorphism of the cycle of $A$ and $0$ and $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $A$.

groupHomology.cyclesOfIsCycle₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the cycle of x5 and hx (from the name)

English

Let $x_{5}$ be an element of $\FinsuppMACRoQ {G}{A}$ such that $x_{5}$ is a cycle. Then the cycle of $x_{5}$ and $\mathrm{hx}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2081\_} (\operatorname{ofDistribMulAction} (G , A))}{x_{6}})}$ defined as $x_{5}$.

groupHomology.cyclesOfIsCycle₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the cycle of x5 and hx (from the name)

English

Let $x_{5}$ be an element of $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{A}$ such that $x_{5}$ is a cycle. Then the cycle of $x_{5}$ and $\mathrm{hx}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2082\_} (\operatorname{ofDistribMulAction} (G , A))}{x_{6}})}$ defined as $x_{5}$.

groupHomology.cycles₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the cycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cycle of $A$ is a submodule of $k$ and $\FinsuppMACRoQ {G}{\operatorname{V} (A)}$ defined as the kernel of the homomorphism of $\mathrm{groupHomology\_\_d\_u2081\_\_u2080\_}$ applied to $A$.

groupHomology.cycles₁IsoOfIsTrivialdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the cycle isomorphism of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cycle isomorphism of $A$ is an isomorphism of $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2081\_} (A)}{x_{2}})}$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {G}{\operatorname{V} (A)}$ defined as the module isomorphism of the linear equivalence of the cycle of $A$ and $\mathrm{groupHomology\_\_cycles\_u2081\_\_eq\_top\_of\_isTrivial}$ applied to $A$.

groupHomology.cycles₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the cycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the cycle of $A$ is a submodule of $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{\operatorname{V} (A)}$ defined as the kernel of the homomorphism of $\mathrm{groupHomology\_\_d\_u2082\_\_u2081\_}$ applied to $A$.

groupHomology.d₁₀defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupHomology\_\_d\_u2081\_\_u2080\_}$ applied to $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {G}{\operatorname{V} (A)}$ and $\operatorname{of}$ applied to $k$ and $\operatorname{V}$ applied to $A$ defined as the module category of $\operatorname{lsum}$ applied to $k$ and the function that maps $g_{1}$ to the difference between $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $\operatorname{inv}$ applied to $g_{1}$ and the identity.

groupHomology.d₁₀ArrowIsodefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the arrow of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the arrow of $A$ is an isomorphism of $\operatorname{mk}$ applied to $\operatorname{d}$ applied to the inhomogeneous chain of $A$, $1$ and $0$ and $\operatorname{mk}$ applied to $\mathrm{groupHomology\_\_d\_u2081\_\_u2080\_}$ applied to $A$ defined as the isomorphism of the chain isomorphism of $A$ and the chain isomorphism of $A$.

groupHomology.d₂₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupHomology\_\_d\_u2082\_\_u2081\_}$ applied to $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{\operatorname{V} (A)}$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {G}{\operatorname{V} (A)}$ defined as the module category of $\operatorname{lsum}$ applied to $k$ and the function that maps $g_{1}$ to the sum of the difference between the composition of $\operatorname{lsingle}$ applied to $\ProdsndMACRoAA {g_{1}}$ and $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $\operatorname{inv}$ applied to $\ProdfstMACRoZ {g_{1}}$ and $\operatorname{lsingle}$ applied to $\ProdfstMACRoZ {g_{1}}\times \ProdsndMACRoAA {g_{1}}$ and $\operatorname{lsingle}$ applied to $\ProdfstMACRoZ {g_{1}}$.

groupHomology.d₃₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupHomology\_\_d\_u2083\_\_u2082\_}$ applied to $A$ is a homomorphism of $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , \mathrm{Prod} (G , G))}{\operatorname{V} (A)}$ and $\operatorname{of}$ applied to $k$ and $\FinsuppMACRoQ {\mathrm{Prod} (G , G)}{\operatorname{V} (A)}$ defined as the module category of $\operatorname{lsum}$ applied to $k$ and the function that maps $g_{1}$ to the difference between the sum of the difference between the composition of $\operatorname{lsingle}$ applied to $\ProdmkMACRoU {\ProdfstMACRoZ {\ProdsndMACRoAA {g_{1}}}}{\ProdsndMACRoAA {\ProdsndMACRoAA {g_{1}}}}$ and $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $\operatorname{inv}$ applied to $\ProdfstMACRoZ {g_{1}}$ and $\operatorname{lsingle}$ applied to $\ProdmkMACRoU {(\ProdfstMACRoZ {g_{1}}\times \ProdfstMACRoZ {\ProdsndMACRoAA {g_{1}}})}{\ProdsndMACRoAA {\ProdsndMACRoAA {g_{1}}}}$ and $\operatorname{lsingle}$ applied to $\ProdmkMACRoU {\ProdfstMACRoZ {g_{1}}}{(\ProdfstMACRoZ {\ProdsndMACRoAA {g_{1}}}\times \ProdsndMACRoAA {\ProdsndMACRoAA {g_{1}}})}$ and $\operatorname{lsingle}$ applied to $\ProdmkMACRoU {\ProdfstMACRoZ {g_{1}}}{\ProdfstMACRoZ {\ProdsndMACRoAA {g_{1}}}}$.

groupHomology.isoCycles₁defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the isomorphism cycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism cycle of $A$ is an isomorphism of the cycle of $A$ and $1$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2081\_} (A)}{x_{2}})}$ defined as the cycle map isomorphism of the left homology data of $\operatorname{sc}$ applied to the inhomogeneous chain of $A$ and $1$ and the explicit left homology data of the short complex of $A$.

groupHomology.isoCycles₂defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the isomorphism cycle of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the isomorphism cycle of $A$ is an isomorphism of the cycle of $A$ and $2$ and $\operatorname{of}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{groupHomology\_\_cycles\_u2082\_} (A)}{x_{2}})}$ defined as the cycle map isomorphism of the left homology data of $\operatorname{sc}$ applied to the inhomogeneous chain of $A$ and $2$ and the explicit left homology data of the short complex of $A$.

groupHomology.isoShortComplexH1defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the short complex of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is an isomorphism of $\operatorname{sc}$ applied to the inhomogeneous chain of $A$ and $1$ and the short complex of $A$.

groupHomology.isoShortComplexH2defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the short complex of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is an isomorphism of $\operatorname{sc}$ applied to the inhomogeneous chain of $A$ and $2$ and the short complex of $A$.

groupHomology.mkH1OfIsTrivialdefMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{mkH1OfIsTrivial}$ applied to $A$ is a linear map of $\mathrm{Additive}$ applied to the set of abelianizations of $G$ and the set of linear maps of $\operatorname{V}$ applied to $A$ and the set of carriers of $\operatorname{H1}$ applied to $A$.

groupHomology.opcyclesIso₀defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

no wording

English

Let $A$ be a representation of $k$ and $G$. Then $\mathrm{groupHomology\_\_opcyclesIso\_u2080\_}$ applied to $A$ is an isomorphism of $\operatorname{opcycles}$ applied to the inhomogeneous chain of $A$ and $0$ and the action of $\operatorname{coinvariantsFunctor}$ applied to $k$ and $G$ and $A$.

groupHomology.shortComplexH0defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the short complex of A (from the name)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is a short complex of the set of module categories of $k$ defined as $\operatorname{mk}$ applied to $\mathrm{groupHomology\_\_d\_u2081\_\_u2080\_}$ applied to $A$, the component of $\operatorname{coinvariantsMk}$ applied to $k$ and $G$ and $A$ and $\mathrm{groupHomology\_\_d\_u2081\_\_u2080\_\_comp\_coinvariantsMk}$ applied to $A$.

groupHomology.shortComplexH1defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the short complex of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is a short complex of the set of module categories of $k$ defined as $\operatorname{mk}$ applied to $\mathrm{groupHomology\_\_d\_u2082\_\_u2081\_}$ applied to $A$, $\mathrm{groupHomology\_\_d\_u2081\_\_u2080\_}$ applied to $A$ and $\mathrm{groupHomology\_\_d\_u2082\_\_u2081\_\_comp\_d\_u2081\_\_u2080\_}$ applied to $A$.

groupHomology.shortComplexH2defMathlib.RepresentationTheory.Homological.GroupHomology.LowDegree, function or constant

Wording

the short complex of A (from the docstring)

English

Let $A$ be a representation of $k$ and $G$. Then the short complex of $A$ is a short complex of the set of module categories of $k$ defined as $\operatorname{mk}$ applied to $\mathrm{groupHomology\_\_d\_u2083\_\_u2082\_}$ applied to $A$, $\mathrm{groupHomology\_\_d\_u2082\_\_u2081\_}$ applied to $A$ and $\mathrm{groupHomology\_\_d\_u2083\_\_u2082\_\_comp\_d\_u2082\_\_u2081\_}$ applied to $A$.

Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro

groupHomology.coinvariantsTensorResProjectiveResolutionIsodefMathlib.RepresentationTheory.Homological.GroupHomology.Shapiro, function or constant

Wording

no wording

English

Let $S$ be a subgroup of $G$. Let $A$ be a representation of $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$. Let $P$ be a projective resolution of $\operatorname{trivial}$ applied to $k$, $G$ and $k$. Then $\operatorname{coinvariantsTensorResProjectiveResolutionIso}$ applied to $S$, $A$ and $P$ is an isomorphism of $\operatorname{coinvariantsTensorObj}$ applied to $A$ and the complex of the map projective resolution of the restriction functor of the subtype of $S$ and $P$ and $\operatorname{coinvariantsTensorObj}$ applied to the ind of the subtype of $S$ and $A$ and the complex of $P$ defined as the application of the map homological complex of the inverse of $\operatorname{coinvariantsTensorIndNatIso}$ applied to the subtype of $S$ and $A$ and $\operatorname{down}$ applied to $\Natural$ and the complex of $P$.

groupHomology.indIsodefMathlib.RepresentationTheory.Homological.GroupHomology.Shapiro, function or constant

Wording

the ind isomorphism of A and n (from the name)

English

Let $S$ be a subgroup of $G$. Let $A$ be a representation of $k$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Let $n$ be a natural number. Then the ind isomorphism of $A$ and $n$ is an isomorphism of the group homology of the ind of the subtype of $S$ and $A$ and $n$ and the group homology of $A$ and $n$ defined as the composition of the map isomorphism of the homology functor of $\operatorname{down}$ applied to $\Natural$ and $n$ and the composition of the inhomogeneous chain isomorphism of the ind of the subtype of $S$ and $A$ and the inverse of $\operatorname{coinvariantsTensorResProjectiveResolutionIso}$ applied to $S$, $A$ and the bar resolution of $k$ and $G$ and the inverse of the group homology isomorphism of $n$ and the map projective resolution of the restriction functor of the subtype of $S$ and the bar resolution of $k$ and $G$.

Mathlib.RepresentationTheory.Homological.Resolution

Rep.barComplexdefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the bar complex of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the bar complex of $k$ and $G$ is a chain complex of the set of representations of $k$ and $G$ and $\Natural$.

Rep.barComplex.ddefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then $\operatorname{d}$ applied to $k$, $G$ and $n$ is a homomorphism of the free of $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $G$ and the free of $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ defined as the free lift of the free of $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ and the function that maps $g$ to $\FinsuppsingleMACRoS {i}{g (\operatorname{succ} (i))}{\operatorname{single} (g (0), 1)}+ \FinsetSum {\FinsetunivMACRoAC}{j}{(\FinsuppsingleMACRoS {\operatorname{contractNth} (j , \lambda x_{3} . \lambda x_{4} . x_{3} \times x_{4} , g)}{\operatorname{single} (1 , \operatorname{neg} (1)^ {(\operatorname{val} (j)+ 1)})})}$.

Rep.barComplex.isoStandardComplexdefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the isomorphism standard complex of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the isomorphism standard complex of $k$ and $G$ is an isomorphism of the bar complex of $k$ and $G$ and the standard complex of $k$ and $G$.

Rep.barResolutiondefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the bar resolution of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the bar resolution of $k$ and $G$ is a projective resolution of $\operatorname{trivial}$ applied to $k$, $G$ and $k$.

Rep.barResolution.extIsodefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the extension isomorphism of V and n (from the name)

English

Let $k$ and $G$ be sets. Let $V$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the extension isomorphism of $V$ and $n$ is an isomorphism of the action of the action of the extension of $n$ and $\operatorname{op}$ applied to $\operatorname{trivial}$ applied to $k$, $G$ and $k$ and $V$ and the homology of the linear Yoneda object of the bar complex of $k$ and $G$ and $V$ and $n$ defined as the isomorphism extension of $n$ and $V$.

Rep.standardComplexdefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the standard complex of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the standard complex of $k$ and $G$ is a chain complex of the set of representations of $k$ and $G$ and $\Natural$ defined as the action of the alternating face map complex of the set of representations of $k$ and $G$ and the composition of the classifying space universal cover of $G$ and $\operatorname{linearization}$ applied to $k$ and $G$.

Rep.standardComplex.compForgetAugmentedIsodefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\operatorname{compForgetAugmentedIso}$ applied to $k$ and $G$ is an isomorphism of the object of the action of $\operatorname{drop}$ and the module of $k$ and $G$ and $\mathrm{Rep\_\_standardComplex\_\_forget\_u2082\_ToModuleCat}$ applied to $k$ and $G$.

Rep.standardComplex.ddefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then $\operatorname{d}$ applied to $k$, $G$ and $n$ is a linear map of the set of monoid algebras of $k$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $G$ and the set of monoid algebras of $k$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ defined as the composition of $\operatorname{lift}$ applied to the set of monoid algebras of $k$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$, $k$, the set of functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $G$ and the function that maps $g_{1}$ to $\FinsetSum {\FinsetunivMACRoAC}{p}{\operatorname{single} (\operatorname{comp} (g_{1} , \operatorname{succAbove} (p)), \operatorname{neg} (1)^ {\operatorname{val} (p)})}$ and $\operatorname{toLinearMap}$ applied to the coefficient linear equivalence of $k$.

Rep.standardComplex.forget₂ToModuleCatdefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\mathrm{Rep\_\_standardComplex\_\_forget\_u2082\_ToModuleCat}$ applied to $k$ and $G$ is a homological complex of the set of module categories of $k$ and $\operatorname{down}$ applied to $\Natural$ defined as the action of the map homological complex of the forgetful functor of the set of representations of $k$ and $G$ and the set of module categories of $k$ and $\operatorname{down}$ applied to $\Natural$ and the standard complex of $k$ and $G$.

Rep.standardComplex.forget₂ToModuleCatHomotopyEquivdefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\mathrm{Rep\_\_standardComplex\_\_forget\_u2082\_ToModuleCatHomotopyEquiv}$ applied to $k$ and $G$ is a homotopy equivalence of $\mathrm{Rep\_\_standardComplex\_\_forget\_u2082\_ToModuleCat}$ applied to $k$ and $G$ and the action of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to the set of module categories of $k$ and the action of the forgetful functor of the set of representations of $k$ and $G$ and the set of module categories of $k$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$ defined as the composition of the homotopy equivalence of the inverse of $\operatorname{compForgetAugmentedIso}$ applied to $k$ and $G$ and the composition of the homotopy equivalence of $\operatorname{extraDegeneracyCompForgetAugmentedToModule}$ applied to $k$ and $G$ and the homotopy equivalence of the map isomorphism of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to the set of module categories of $k$ and the module isomorphism of the composition of the coefficient linear equivalence of $k$ and the unique linear equivalence of $\operatorname{default}$.

Rep.standardComplex.xIsodefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the isomorphism of n (from the name)

English

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then the isomorphism of $n$ is an isomorphism of $\operatorname{X}$ applied to the standard complex of $k$ and $G$ and $n$ and the representation of $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $G$ defined as the identity of $\operatorname{X}$ applied to the standard complex of $k$ and $G$ and $n$.

Rep.standardComplex.εdefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\mathrm{Rep\_\_standardComplex\_\_\_u3b5\_}$ applied to $k$ and $G$ is a homomorphism of the representation of $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $1$ to elements of $G$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$.

Rep.standardComplex.εToSingle₀defMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\mathrm{Rep\_\_standardComplex\_\_\_u3b5\_ToSingle\_u2080\_}$ applied to $k$ and $G$ is a homomorphism of the standard complex of $k$ and $G$ and the action of $\mathrm{ChainComplex\_\_single\_u2080\_}$ applied to the set of representations of $k$ and $G$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$ defined as $\operatorname{symm}$ applied to the single equivalence of the standard complex of $k$ and $G$ and $\operatorname{trivial}$ applied to $k$, $G$ and $k$ and $\mathrm{Rep\_\_standardComplex\_\_\_u3b5\_}$ applied to $k$ and $G$.

Rep.standardResolutiondefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the standard resolution of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the standard resolution of $k$ and $G$ is a projective resolution of $\operatorname{trivial}$ applied to $k$, $G$ and $k$.

Rep.standardResolution.extIsodefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the extension isomorphism of V and n (from the name)

English

Let $k$ and $G$ be sets. Let $V$ be a representation of $k$ and $G$. Let $n$ be a natural number. Then the extension isomorphism of $V$ and $n$ is an isomorphism of the action of the action of the extension of $n$ and $\operatorname{op}$ applied to $\operatorname{trivial}$ applied to $k$, $G$ and $k$ and $V$ and the homology of the linear Yoneda object of the standard complex of $k$ and $G$ and $V$ and $n$ defined as the isomorphism extension of $n$ and $V$.

classifyingSpaceUniversalCoverdefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the classifying space universal cover of G (from the name)

English

Let $G$ be a set. Then the classifying space universal cover of $G$ is a simplicial object of the set of actions of the set of sets and $G$.

classifyingSpaceUniversalCover.cechNerveTerminalFromIsodefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the Cech nerve terminal from isomorphism of G (from the name)

English

Let $G$ be a set. Then the Cech nerve terminal from isomorphism of $G$ is an isomorphism of $\operatorname{cechNerveTerminalFrom}$ applied to the action of $G$ and $G$ and the classifying space universal cover of $G$.

classifyingSpaceUniversalCover.cechNerveTerminalFromIsoCompForgetdefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{cechNerveTerminalFromIsoCompForget}$ applied to $G$ is an isomorphism of $\operatorname{cechNerveTerminalFrom}$ applied to $G$ and the composition of the classifying space universal cover of $G$ and the forgetful functor of the set of actions of the set of sets and $G$.

classifyingSpaceUniversalCover.compForgetAugmenteddefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{compForgetAugmented}$ applied to $G$ is an element of $\operatorname{Augmented}$ applied to the set of sets.

classifyingSpaceUniversalCover.compForgetAugmented.toModuledefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the module of k and G (from the name)

English

Let $k$ and $G$ be sets. Then the module of $k$ and $G$ is an element of $\operatorname{Augmented}$ applied to the set of module categories of $k$ defined as the action of the action of the whiskering of the set of sets and the set of module categories of $k$ and the free functor of $k$ and $\operatorname{compForgetAugmented}$ applied to $G$.

classifyingSpaceUniversalCover.extraDegeneracyAugmentedCechNervedefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

the extra degeneracy augmented Cech nerve of G (from the name)

English

Let $G$ be a set. Then the extra degeneracy augmented Cech nerve of $G$ is an extra degeneracy of the augmented Cech nerve of $\operatorname{mk}$ applied to the map of $G$.

classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmenteddefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{extraDegeneracyCompForgetAugmented}$ applied to $G$ is an extra degeneracy of $\operatorname{compForgetAugmented}$ applied to $G$.

classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmentedToModuledefMathlib.RepresentationTheory.Homological.Resolution, function or constant

Wording

no wording

English

Let $k$ and $G$ be sets. Then $\operatorname{extraDegeneracyCompForgetAugmentedToModule}$ applied to $k$ and $G$ is an extra degeneracy of the module of $k$ and $G$ defined as the map of $\operatorname{extraDegeneracyCompForgetAugmented}$ applied to $G$ and the free functor of $k$.

Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Rep.tateNormdefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

no wording

English

Let $M$ be a representation of $R$ and $G$. Then $\operatorname{tateNorm}$ applied to $M$ is a homomorphism of $\operatorname{X}$ applied to the inhomogeneous chain of $M$ and $0$ and $\operatorname{X}$ applied to the inhomogeneous cochain of $M$ and $0$ defined as the composition of the homomorphism of the chain isomorphism of $M$ and the composition of the module category homomorphism of $\operatorname{asHom}$ applied to the norm of $M$ and the inverse of the cochain isomorphism of $M$.

TateCohomology.isoGroupCohomologydefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

the isomorphism group cohomology of n (from the name)

English

Let $n$ be a natural number. Then the isomorphism group cohomology of $n$ is an isomorphism of $\mathrm{tateCohomologyFunctor}$ applied to $n$ and the functor of $n$.

TateCohomology.isoGroupHomologydefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

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

English

Let $m$ be an integer. Let $n$ be a natural number such that $m = \operatorname{neg} (n + 1)$. Then the isomorphism group homology of $m$ and $n$ is an isomorphism of $\mathrm{tateCohomologyFunctor}$ applied to $m$ and the functor of $n$.

TateCohomology.tateComplex.evalNegdefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

the evaluation negation of n (from the name)

English

Let $n$ be a natural number. Then the evaluation negation of $n$ is an isomorphism of the composition of $\mathrm{tateComplexFunctor}$ applied to $R$ and $G$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{negSucc}$ applied to $n$ and the composition of the chain functor of $R$ and $G$ and the evaluation of $\operatorname{down}$ applied to $\Natural$ and $n$ defined as the identity of the composition of $\mathrm{tateComplexFunctor}$ applied to $R$ and $G$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $\operatorname{negSucc}$ applied to $n$.

TateCohomology.tateComplex.evalNonnegdefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{evalNonneg}$ applied to $n$ is an isomorphism of the composition of $\mathrm{tateComplexFunctor}$ applied to $R$ and $G$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$ and the composition of the cochain functor of $R$ and $G$ and the evaluation of $\operatorname{up}$ applied to $\Natural$ and $n$ defined as the identity of the composition of $\mathrm{tateComplexFunctor}$ applied to $R$ and $G$ and the evaluation of $\operatorname{up}$ applied to $\Integer$ and $n$.

TateCohomology.δdefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

no wording

English

Assume that $\operatorname{ShortExact}$ holds for $S$. Let $n$ be an integer. Then $\mathrm{TateCohomology\_\_\_u3b4\_}$ applied to $\mathrm{hS}$ and $n$ is a homomorphism of $\mathrm{tateCohomology}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2083\_}$ applied to $S$ and $n$ and $\mathrm{tateCohomology}$ applied to $\mathrm{CategoryTheory\_\_ShortComplex\_\_X\_u2081\_}$ applied to $S$ and $n + 1$.

tateCohomologydefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

no wording

English

Let $M$ be a representation of $R$ and $G$. Let $n$ be an integer. Then $\mathrm{tateCohomology}$ applied to $M$ and $n$ is a module category of $R$ defined as the action of $\mathrm{tateCohomologyFunctor}$ applied to $n$ and $M$.

tateCohomologyFunctordefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

no wording

English

Let $n$ be an integer. Then $\mathrm{tateCohomologyFunctor}$ applied to $n$ is a functor of the set of representations of $R$ and $G$ and the set of module categories of $R$ defined as the composition of $\mathrm{tateComplexFunctor}$ applied to $R$ and $G$ and the homology functor of $\operatorname{up}$ applied to $\Integer$ and $n$.

tateComplexdefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

no wording

English

Let $M$ be a representation of $R$ and $G$. Then $\mathrm{tateComplex}$ applied to $M$ is a cochain complex of the set of module categories of $R$ and $\Integer$ defined as the cochain complex of $\mathrm{tateComplexConnectData}$ applied to $M$.

tateComplex.mapdefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

the map of x3 (from the name)

English

Let $x_{3}$ be a homomorphism of $X$ and $Y$. Then the map of $x_{3}$ is a homomorphism of $\mathrm{tateComplex}$ applied to $X$ and $\mathrm{tateComplex}$ applied to $Y$.

tateComplexConnectDatadefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

no wording

English

Let $M$ be a representation of $R$ and $G$. Then $\mathrm{tateComplexConnectData}$ applied to $M$ is an element of $\operatorname{ConnectData}$ applied to the inhomogeneous chain of $M$ and the inhomogeneous cochain of $M$ defined as $\operatorname{mk}$ applied to $\operatorname{tateNorm}$ applied to $M$, $\mathrm{Rep\_\_d\_comp\_tateNorm}$ applied to $M$ and $\mathrm{Rep\_\_tateNorm\_comp\_d}$ applied to $M$.

tateComplexFunctordefMathlib.RepresentationTheory.Homological.TateCohomology.Basic, function or constant

Wording

no wording

English

Let $R$ and $G$ be sets. Then $\mathrm{tateComplexFunctor}$ applied to $R$ and $G$ is a functor of the set of representations of $R$ and $G$ and the set of cochain complexes of the set of module categories of $R$ and $\Integer$.