Definitions: Mathlib.RepresentationTheory, part 2 of 2

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $A$ be a representation of $k$ and $G$. Let $B$ be a representation of $k$ and $H$. Then $\operatorname{coinvariantsTensorIndHom}$ applied to $x_{3}$, $A$ and $B$ is a homomorphism of the action of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $H$ and the ind of $x_{3}$ and $A$ and $B$ and the action of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $G$ and $A$ and the restriction of $x_{3}$ and $B$.

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $A$ be a representation of $k$ and $G$. Let $B$ be a representation of $k$ and $H$. Then $\operatorname{coinvariantsTensorIndInv}$ applied to $x_{3}$, $A$ and $B$ is a homomorphism of the action of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $G$ and $A$ and the restriction of $x_{3}$ and $B$ and the action of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $H$ and the ind of $x_{3}$ and $A$ and $B$.

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $A$ be a representation of $k$ and $G$. Let $B$ be a representation of $k$ and $H$. Then $\operatorname{coinvariantsTensorIndIso}$ applied to $x_{3}$, $A$ and $B$ is an isomorphism of the action of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $H$ and the ind of $x_{3}$ and $A$ and $B$ and the action of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $G$ and $A$ and the restriction of $x_{3}$ and $B$.

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $A$ be a representation of $k$ and $G$. Then $\operatorname{coinvariantsTensorIndNatIso}$ applied to $x_{3}$ and $A$ is an isomorphism of the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $H$ and the ind of $x_{3}$ and $A$ and the composition of the restriction functor of $x_{3}$ and the action of $\operatorname{coinvariantsTensor}$ applied to $k$ and $G$ and $A$.

the ind of x3 and A (from the name)

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

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

Let $k$ be a set. Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Then the ind 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$.

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

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

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

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

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

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

ind of x3 and x6 (from the name)

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $x_{6}$ be a representation of $G$ and $A$. Then an ind of $x_{3}$ and $x_{6}$ is an element of the function that maps $x_{3}$ and $x_{6}$ to $\operatorname{Coinvariants}$ applied to $\operatorname{tprod}$ applied to the composition of the left regular of $k$ and $H$ and $x_{3}$ and $x_{6}$.

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $x_{6}$ be a representation of $G$ and $A$. Let $h$ be an element of $H$. Then $\operatorname{mk}$ applied to $x_{3}$, $x_{6}$ and $h$ is a linear map of $A$ and the set of inds of $x_{3}$ and $x_{6}$ defined as the composition of $\operatorname{mk}$ applied to $\operatorname{tprod}$ applied to the composition of the left regular of $k$ and $H$ and $x_{3}$ and $x_{6}$ and $\operatorname{mk}$ applied to $k$, the set of monoid algebras of $k$ and $H$, $A$ and $\operatorname{single}$ applied to $h$ and $1$.

the ind of x3 and x6 (from the name)

Let $x_{3}$ be a monoid homomorphism of $G$ and $H$. Let $x_{6}$ be a representation of $G$ and $A$. Then the ind of $x_{3}$ and $x_{6}$ is a representation of $H$ and the set of inds of $x_{3}$ and $x_{6}$.

the intertwining map of x7 and f (from the name)

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Let $f$ be a linear map of $V$ and $W$ such that for all elements $g$ of $G$, for all elements $v$ of $V$, $\EqtMACRoH {f (\operatorname{coe} (x_{6} , g , v))}{\operatorname{coe} (x_{7} , g , f (v))}$. Then the intertwining map of $x_{7}$ and $f$ is an intertwining map of $x_{6}$ and $x_{7}$.

equivalence of x6 and x7 (from the name)

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

the dual tensor homomorphism of x6 and x7 (from the name)

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the dual tensor homomorphism of $x_{6}$ and $x_{7}$ is an equivalence of $\operatorname{tprod}$ applied to the dual of $x_{6}$ and $x_{7}$ and the linear homomorphism of $x_{6}$ and $x_{7}$.

the inverse function of self and x8 (from the name)

Let $\mathrm{self}$ be an equivalence of $x_{6}$ and $x_{7}$. Let $x_{8}$ be an element of $W$. Then the inverse function of $\mathrm{self}$ and $x_{8}$ is an element of $V$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{8}$.

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

the identity of x4 (from the name)

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

the inverse of x8 (from the name)

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

the linear equivalence of self (from the name)

Let $\mathrm{self}$ be an equivalence of $x_{6}$ and $x_{7}$. Then the linear equivalence of $\mathrm{self}$ is a linear equivalence of $V$ and $W$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toIntertwiningMap}$ applied to $\mathrm{self}$, $\operatorname{invFun}$ applied to $\mathrm{self}$, $\mathrm{Representation\_\_Equiv\_\_left\_inv}$ applied to $\mathrm{self}$ and $\mathrm{Representation\_\_Equiv\_\_right\_inv}$ applied to $\mathrm{self}$.

the composition of x11 and x12 (from the name)

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

intertwining map of x6 and x7 (from the name)

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

the central algebra product of x4 and hz (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Assume that $z$ is an element of the center of the set of monoid algebras of $A$ and $G$. Then the central algebra product of $x_{4}$ and $\mathrm{hz}$ is an intertwining map of $x_{4}$ and $x_{4}$.

the central algebra multiplicative homomorphism of x4 (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Then the central algebra multiplicative homomorphism of $x_{4}$ is a monoid homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{MonoidAlgebra} (A , G))}{x_{5}})}$ and the set of intertwining maps of $x_{4}$ and $x_{4}$.

the central product of x4 and g (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Let $g$ be an element of $G$ such that $g$ is an element of the center of $G$. Then the central product of $x_{4}$ and $g$ is an intertwining map of $x_{4}$ and $x_{4}$.

the coercion function additive monoid homomorphism of x6 and x7 (from the name)

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the coercion function additive monoid homomorphism of $x_{6}$ and $x_{7}$ is an additive monoid homomorphism of the set of intertwining maps of $x_{6}$ and $x_{7}$ and the set of functions from elements of $V$ to elements of $W$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ and $\mathrm{Representation\_\_IntertwiningMap\_\_coe\_zero}$ applied to $x_{6}$ and $x_{7}$ and $\mathrm{Representation\_\_IntertwiningMap\_\_coe\_add}$ applied to $x_{6}$ and $x_{7}$.

the composition of f and g (from the name)

Let $f$ be an intertwining map of $x_{9}$ and $x_{10}$. Let $g$ be an intertwining map of $x_{8}$ and $x_{9}$. Then the composition of $f$ and $g$ is an intertwining map of $x_{8}$ and $x_{10}$.

the equivalence algebra end of x4 (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Then the equivalence algebra end of $x_{4}$ is an algebra isomorphism of the set of intertwining maps of $x_{4}$ and $x_{4}$ and the set of ends of the set of monoid algebras of $A$ and $G$ and $\operatorname{asModule}$ applied to $x_{4}$.

the equivalence linear map as module of x6 and x7 (from the name)

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the equivalence linear map as module of $x_{6}$ and $x_{7}$ is a linear equivalence of the set of intertwining maps of $x_{6}$ and $x_{7}$ and the set of linear maps of $\operatorname{asModule}$ applied to $x_{6}$ and $\operatorname{asModule}$ applied to $x_{7}$.

the first component of x6 and x7 (from the name)

Let $A$ be a set. Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the first component of $x_{6}$ and $x_{7}$ is an intertwining map of the product of $x_{6}$ and $x_{7}$ and $x_{6}$.

the identity of x4 (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Then the identity of $x_{4}$ is an intertwining map of $x_{4}$ and $x_{4}$.

the left injection of x6 and x7 (from the name)

Let $A$ be a set. Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the left injection of $x_{6}$ and $x_{7}$ is an intertwining map of $x_{6}$ and the product of $x_{6}$ and $x_{7}$ defined as the product of the identity of $x_{6}$ and $0$.

the right injection of x6 and x7 (from the name)

Let $A$ be a set. Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the right injection of $x_{6}$ and $x_{7}$ is an intertwining map of $x_{7}$ and the product of $x_{6}$ and $x_{7}$ defined as the product of $0$ and the identity of $x_{7}$.

the kernel of x7 and f (from the name)

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 kernel of $x_{7}$ and $f$ is a subrepresentation of $x_{6}$.

the tensor of x8 and f (from the name)

Let $x_{8}$ be a representation of $G$ and $V$. Let $f$ be an intertwining map of $x_{9}$ and $x_{10}$. Then the tensor of $x_{8}$ and $f$ is an intertwining map of $\operatorname{tprod}$ applied to $x_{8}$ and $x_{9}$ and $\operatorname{tprod}$ applied to $x_{8}$ and $x_{10}$ defined as the tensor of the identity of $x_{8}$ and $f$.

Let $x_{8}$ be a representation of $G$ and $V$. Let $x_{9}$ be a representation of $G$ and $W$. Let $x_{10}$ be a representation of $G$ and $U$. Then $\operatorname{llcomp}$ applied to $x_{8}$, $x_{9}$ and $x_{10}$ is a linear map of the set of intertwining maps of $x_{9}$ and $x_{10}$ and the set of linear maps of the set of intertwining maps of $x_{8}$ and $x_{9}$ and the set of intertwining maps of $x_{8}$ and $x_{10}$.

the intertwining map of f and hf (from the name)

Let $f$ be an intertwining map of $x_{6}$ and $x_{7}$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the intertwining map of $f$ and $\mathrm{hf}$ is an equivalence of $x_{6}$ and $x_{7}$.

the product of f and g (from the name)

Let $f$ be an intertwining map of $x_{8}$ and $x_{9}$. Let $g$ be an intertwining map of $x_{8}$ and $x_{10}$. Then the product of $f$ and $g$ is an intertwining map of $x_{8}$ and the product of $x_{9}$ and $x_{10}$.

the tensor of x8 and f (from the name)

Let $x_{8}$ be a representation of $G$ and $V$. Let $f$ be an intertwining map of $x_{9}$ and $x_{10}$. Then the tensor of $x_{8}$ and $f$ is an intertwining map of $\operatorname{tprod}$ applied to $x_{9}$ and $x_{8}$ and $\operatorname{tprod}$ applied to $x_{10}$ and $x_{8}$ defined as the tensor of $f$ and the identity of $x_{8}$.

the range of x7 and f (from the name)

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 range of $x_{7}$ and $f$ is a subrepresentation of $x_{7}$.

the second component of x6 and x7 (from the name)

Let $A$ be a set. Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the second component of $x_{6}$ and $x_{7}$ is an intertwining map of the product of $x_{6}$ and $x_{7}$ and $x_{7}$.

the tensor of f and g (from the name)

Let $f$ be an intertwining map of $x_{8}$ and $x_{9}$. Let $g$ be an intertwining map of $x_{10}$ and $x_{13}$. Then the tensor of $f$ and $g$ is an intertwining map of $\operatorname{tprod}$ applied to $x_{8}$ and $x_{10}$ and $\operatorname{tprod}$ applied to $x_{9}$ and $x_{13}$.

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

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Let $f$ be a linear map of $V$ and $W$. Then we can say that $\operatorname{IsIntertwiningMap}$ holds for $x_{6}$, $x_{7}$ and $f$.

the associator of x9 and x10 (from the name)

Let $x_{8}$ be a representation of $G$ and $V$. Let $x_{9}$ be a representation of $G$ and $W$. Let $x_{10}$ be a representation of $G$ and $U$. Then the associator of $x_{9}$ and $x_{10}$ is an equivalence of $\operatorname{tprod}$ applied to $\operatorname{tprod}$ applied to $x_{8}$ and $x_{9}$ and $x_{10}$ and $\operatorname{tprod}$ applied to $x_{8}$ and $\operatorname{tprod}$ applied to $x_{9}$ and $x_{10}$.

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then $\operatorname{comm}$ applied to $x_{6}$ and $x_{7}$ is an equivalence of $\operatorname{tprod}$ applied to $x_{6}$ and $x_{7}$ and $\operatorname{tprod}$ applied to $x_{7}$ and $x_{6}$.

Let $A$ be a set. Let $x_{4}$ be a representation of $G$ and $W$. Then $\operatorname{lid}$ applied to $A$ and $x_{4}$ is an equivalence of $\operatorname{tprod}$ applied to $\operatorname{trivial}$ applied to $A$, $G$ and $A$ and $x_{4}$ and $x_{4}$.

Let $A$ be a set. Let $x_{4}$ be a representation of $G$ and $W$. Then $\operatorname{rid}$ applied to $A$ and $x_{4}$ is an equivalence of $\operatorname{tprod}$ applied to $x_{4}$ and $\operatorname{trivial}$ applied to $A$, $G$ and $A$ and $x_{4}$.

Let $k$ and $G$ be sets. Then $\operatorname{average}$ applied to $k$ and $G$ is a monoid algebra of $k$ and $G$ defined as $\HSMulhSMulMACRoAL {\operatorname{invOf} (\operatorname{card} (G))}{(\FinsetSum {\FinsetunivMACRoAC}{g}{\operatorname{of} (k , G , g)})}$.

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

Let $k$ and $G$ be sets. Then the invariant adjunction of $k$ and $G$ is an adjunction of the trivial functor of $k$ and $G$ and the invariant functor of $k$ and $G$.

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

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

the quotient to invariant of A and S (from the name)

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

the quotient to invariant functor of k and S (from the name)

Let $k$ be a set. Let $S$ be a subgroup of $G$. Then the quotient to invariant functor of $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$.

the invariant of A and S (from the name)

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

the average map of x4 (from the name)

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

the invariant of x4 (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Then the invariant of $x_{4}$ is a submodule of $k$ and $V$.

the invariant equivalence intertwining map of x6 and x7 (from the name)

Let $x_{6}$ be a representation of $G$ and $V$. Let $x_{7}$ be a representation of $G$ and $W$. Then the invariant equivalence intertwining map of $x_{6}$ and $x_{7}$ is a linear equivalence of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{invariants} (\operatorname{linHom} (x_{6} , x_{7}))}{x_{8}})}$ and the set of intertwining maps of $x_{6}$ and $x_{7}$.

Let $X$ and $Y$ be elements of $\mathrm{FDRep}$ applied to $k$ and $G$. Then $\operatorname{invariantsEquivFDRepHom}$ applied to $X$ and $Y$ is a linear equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{invariants} (\operatorname{linHom} (\mathrm{FDRep\_\_\_u3c1\_} (X), \mathrm{FDRep\_\_\_u3c1\_} (Y)))}{x_{2}})}$ and the set of homomorphisms of $X$ and $Y$.

the invariant equivalence representation homomorphism of X and Y (from the name)

Let $X$ and $Y$ be representations of $k$ and $G$. Then the invariant equivalence representation homomorphism of $X$ and $Y$ is a linear equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{invariants} (\operatorname{linHom} (\mathrm{Rep\_\_\_u3c1\_} (X), \mathrm{Rep\_\_\_u3c1\_} (Y)))}{x_{2}})}$ and the set of homomorphisms of $X$ and $Y$.

the quotient to invariant of x4 and S (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Let $S$ be a subgroup of $G$. Then the quotient to invariant of $x_{4}$ and $S$ is a representation of the set of quotients of $G$ and $S$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{invariants} (\operatorname{comp} (x_{4} , \operatorname{subtype} (S)))}{x_{5}})}$ defined as the representation of the invariant of $x_{4}$ and $S$ and $S$.

the quotient to invariant lift of x4 and S (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Let $S$ be a subgroup of $G$. Then the quotient to invariant lift of $x_{4}$ and $S$ is an intertwining map of the composition of the quotient to invariant of $x_{4}$ and $S$ and $\operatorname{mk'}$ applied to $S$ and $x_{4}$.

the invariant of x4 and S (from the name)

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

x4 is irreducible (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Then $x_{4}$ is irreducible, if the set of subrepresentations of $x_{4}$ is a simple order.

the conjugate of x8 and g (from the name)

Let $x_{8}$ be a linear map of $W$ and $V$. Let $g$ be an element of $G$. Then the conjugate of $x_{8}$ and $g$ is a linear map of $W$ and $V$ defined as the composition of the linear map of $\operatorname{inv}$ applied to $g$ and the composition of $x_{8}$ and the linear map of $g$.

the equivariant projection of G and x8 (from the name)

Let $G$ be a set. Let $x_{8}$ be a linear map of $W$ and $V$. Then the equivariant projection of $G$ and $x_{8}$ is a linear map of $W$ and $V$ defined as $\HSMulhSMulMACRoAL {\operatorname{inverse} (\operatorname{card} (G))}{\operatorname{sumOfConjugatesEquivariant} (G , x_{8})}$.

the sum of G and x8 (from the name)

Let $G$ be a set. Let $x_{8}$ be a linear map of $W$ and $V$. Then the sum of $G$ and $x_{8}$ is a linear map of $W$ and $V$ defined as $\FinsetSum {\FinsetunivMACRoAC}{g}{\operatorname{conjugate} (x_{8} , g)}$.

the sum of G and x8 (from the name)

Let $G$ be a set. Let $x_{8}$ be a linear map of $W$ and $V$. Then the sum of $G$ and $x_{8}$ is a linear map of $W$ and $V$.

representation of k and G (from the name)

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

the action to representation of k and G (from the name)

Let $k$ and $G$ be sets. Then the action to representation of $k$ and $G$ is a functor of the set of actions of the set of module categories of $k$ and $G$ and the set of representations of $k$ and $G$.

the action to representation representation to action of X (from the name)

Let $k$ and $G$ be sets. Let $X$ be a representation of $k$ and $G$. Then the action to representation representation to action of $X$ is an isomorphism of the action of the action to representation of $k$ and $G$ and the action of the representation to action of $k$ and $G$ and $X$ and $X$.

homomorphism of A and B (from the name)

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

the homomorphism of f (from the name)

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

the homomorphism of self (from the name)

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

the module category homomorphism of f (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Then the 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 module category of $\operatorname{toLinearMap}$ applied to the homomorphism of $f$.

A is trivial (from the name)

Let $A$ be a representation of $k$ and $G$. Then $A$ is trivial, if $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ is trivial.

the linear homomorphism equivalence of B and C (from the name)

Let $A$, $B$ and $C$ be representations of $k$ and $G$. Then the linear homomorphism equivalence of $B$ and $C$ is a linear equivalence of the set of homomorphisms of the tensor object of $A$ and $B$ and $C$ and the set of homomorphisms of $B$ and the action of $\operatorname{ihom}$ applied to $A$ and $C$.

Let $A$, $B$ and $C$ be representations of $k$ and $G$. Then $\operatorname{linearHomEquivComm}$ applied to $A$, $B$ and $C$ is a linear equivalence of the set of homomorphisms of the tensor object of $A$ and $B$ and $C$ and the set of homomorphisms of $A$ and the action of $\operatorname{ihom}$ applied to $B$ and $C$ defined as the composition of the homomorphism congruence of the braiding natural isomorphism of $A$ and $B$ and the identity of $C$ and the linear homomorphism equivalence of $A$ and $C$.

the representation to action of k and G (from the name)

Let $k$ and $G$ be sets. Then the representation to action of $k$ and $G$ is a functor of the set of representations of $k$ and $G$ and the set of actions of the set of module categories of $k$ and $G$.

the representation to action action to representation of A (from the name)

Let $k$ and $G$ be sets. Let $A$ be an action of the set of module categories of $k$ and $G$. Then the representation to action action to representation of $A$ is an isomorphism of the action of the representation to action of $k$ and $G$ and the action of the action to representation of $k$ and $G$ and $A$ and $A$.

Let $\mathrm{self}$ be a 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}$.

Let $A$ be a representation of $k$ and $G$. Let $g$ be an element of $G$. Then $\operatorname{applyAsHom}$ applied to $A$ and $g$ is a homomorphism of $A$ and $A$.

the binary bicone of A and B (from the name)

Let $A$ and $B$ be representations of $k$ and $G$. Then the binary bicone of $A$ and $B$ is a binary bicone of $A$ and $B$.

Let $A$ and $B$ be representations of $k$ and $G$. Then $\operatorname{binaryBiconeIsBilimit}$ applied to $A$ and $B$ is an element of $\operatorname{IsBilimit}$ applied to the binary bicone of $A$ and $B$.

the diagonal of n (from the name)

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

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

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

the finitely supported function of x2 and A (from the name)

Let $x_{2}$ be a set. Let $A$ be a representation of $k$ and $G$. Then the finitely supported function of $x_{2}$ and $A$ is a representation of $k$ and $G$ defined as $\operatorname{of}$ applied to the finitely supported function of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $x_{2}$.

the left finitely supported function tensor of A and B (from the name)

Let $k$, $G$ and $x_{2}$ be sets. Let $A$ and $B$ be representations of $k$ and $G$. Then the left finitely supported function tensor of $A$ and $B$ is an isomorphism of the tensor object of the finitely supported function of $x_{2}$ and $A$ and $B$ and the finitely supported function of $x_{2}$ and the tensor object of $A$ and $B$ defined as the isomorphism of the left finitely supported function tensor of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to $B$.

the right finitely supported function tensor of A and B (from the name)

Let $k$, $G$ and $x_{2}$ be sets. Let $A$ and $B$ be representations of $k$ and $G$. Then the right finitely supported function tensor of $A$ and $B$ is an isomorphism of the tensor object of $A$ and the finitely supported function of $x_{2}$ and $B$ and the finitely supported function of $x_{2}$ and the tensor object of $A$ and $B$ defined as the isomorphism of the right finitely supported function tensor of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to $B$.

Let $k$ and $G$ be sets. Then $\operatorname{forgetNatIsoActionForget}$ applied to $k$ and $G$ is an isomorphism of the forgetful functor of the set of representations of $k$ and $G$ and the set of module categories of $k$ and the composition of the representation to action of $k$ and $G$ and $\operatorname{forget}$ applied to the set of module categories of $k$ and $G$ defined as the identity of the forgetful functor of the set of representations of $k$ and $G$ and the set of module categories of $k$.

the free of G and x2 (from the name)

Let $k$, $G$ and $x_{2}$ be sets. Then the free of $G$ and $x_{2}$ is a representation of $k$ and $G$ defined as $\operatorname{of}$ applied to the free of $G$ and $x_{2}$.

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

Let $k$ and $G$ be sets. Let $A$ be a representation of $k$ and $G$. Let $f$ be a function from elements of $x_{2}$ to elements of $\operatorname{V}$ applied to $A$. Then the free lift of $A$ and $f$ is a homomorphism of the free of $G$ and $x_{2}$ and $A$ defined as the representation of the free lift of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $f$.

the free lift equivalence of A (from the name)

Let $k$, $G$ and $x_{2}$ be sets. Let $A$ be a representation of $k$ and $G$. Then the free lift equivalence of $A$ is a linear equivalence of the set of homomorphisms of the free of $G$ and $x_{2}$ and $A$ and the set of functions from elements of $x_{2}$ to elements of $\operatorname{V}$ applied to $A$ defined as the composition of the homomorphism linear equivalence of the free of $G$ and $x_{2}$ and $A$ and the free lift equivalence of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $x_{2}$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of homomorphisms of $A$ and $B$ to the set of intertwining maps of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to $B$.

the homomorphism linear equivalence of X and Y (from the name)

Let $X$ and $Y$ be representations of $k$ and $G$. Then the homomorphism linear equivalence of $X$ and $Y$ is a linear equivalence of the set of homomorphisms of $X$ and $Y$ and the set of intertwining maps of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $X$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to $Y$.

Let $A$ be a representation of $k$ and $G$. Then $\operatorname{ihom}$ applied to $A$ is a functor of the set of representations of $k$ and $G$ and the set of representations of $k$ and $G$.

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

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

the left regular homomorphism of A and x2 (from the name)

Let $A$ be a representation of $k$ and $G$. Let $x_{2}$ be an element of $\operatorname{V}$ applied to $A$. Then the left regular homomorphism of $A$ and $x_{2}$ is a homomorphism of the left regular of $k$ and $G$ and $A$.

the left regular homomorphism equivalence of A (from the name)

Let $A$ be a representation of $k$ and $G$. Then the left regular homomorphism equivalence of $A$ is a linear equivalence of the set of homomorphisms of the left regular of $k$ and $G$ and $A$ and $\operatorname{V}$ applied to $A$ defined as the composition of the homomorphism linear equivalence of the left regular of $k$ and $G$ and $A$ and the left regular map equivalence of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$.

the left regular tensor trivial isomorphism free of G and x (from the name)

Let $k$, $G$ and $x$ be sets. Then the left regular tensor trivial isomorphism free of $G$ and $x$ is an isomorphism of the tensor object of the left regular of $k$ and $G$ and $\operatorname{trivial}$ applied to $k$, $G$ and the set of monoid algebras of $k$ and $x$ and the free of $G$ and $x$ defined as the isomorphism of the left regular tensor trivial isomorphism free of $x$.

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

Let $k$, $G$ and $H$ be sets. Then $\operatorname{linearizationOfMulActionIso}$ applied to $k$, $G$ and $H$ is an isomorphism of the action of $\operatorname{linearization}$ applied to $k$ and $G$ and the action of $G$ and $H$ and the representation of $G$ and $H$ defined as the isomorphism of $\operatorname{linearizeOfMulActionIso}$ applied to $k$, $G$ and $H$.

Let $k$, $G$ and $X$ be sets. Then $\operatorname{linearizationTrivialIso}$ applied to $k$, $G$ and $X$ is an isomorphism of the action of $\operatorname{linearization}$ applied to $k$ and $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$ defined as the isomorphism of $\operatorname{linearizeTrivialIso}$ applied to $k$, $G$ and $X$.

the isomorphism of e (from the name)

Let $e$ be an equivalence of $x_{6}$ and $x_{7}$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{of}$ applied to $x_{6}$ and $\operatorname{of}$ applied to $x_{7}$.

Let $A$ be a representation of $k$ and $G$. Let $W$ be a submodule of $k$ and $\operatorname{V}$ applied to $A$ such that for all elements $g$ of $G$, $W$ is less than or equal to the preimage of $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $g$ and $W$. Then $\operatorname{mkQ}$ applied to $A$, $W$ and $\mathrm{le\_comap}$ is a homomorphism of $A$ and the quotient of $A$ and $W$.

the norm of A (from the name)

Let $A$ be a representation of $k$ and $G$. Then the norm of $A$ is an end of $A$.

the norm natural transformation (from the name)

The norm natural transformation is an end of the identity of the set of representations of $k$ and $G$ defined as $\operatorname{of}$ applied to $\operatorname{mk}$ applied to the function that maps $A$ to $\operatorname{asHom}$ applied to the norm of $A$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Rep\_\_norm\_comm}$.

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

the representation of R and S (from the name)

Let $R$ and $S$ be sets. Then the representation of $R$ and $S$ is a representation of $\Integer$ and the set of algebra isomorphisms of $S$ and $S$ defined as the representation of the set of algebra isomorphisms of $S$ and $S$ and $S$.

the representation of R and S (from the name)

Let $R$ and $S$ be sets. Then the representation of $R$ and $S$ is a representation of $\Integer$ and the set of algebra isomorphisms of $S$ and $S$ defined as the representation of the set of algebra isomorphisms of $S$ and $S$ and $\UnitsMACRoAO {S}$.

the representation of G and A (from the name)

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

the representation of f (from the name)

Let $f$ be an intertwining map of $x_{6}$ and $x_{7}$. Then the representation of $f$ is a homomorphism of $\operatorname{of}$ applied to $x_{6}$ and $\operatorname{of}$ applied to $x_{7}$ defined as the concrete category of $f$.

the representation of G and H (from the name)

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

the representation of G and H (from the name)

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

the representation of M and G (from the name)

Let $M$ and $G$ be sets. Then the representation of $M$ and $G$ is a representation of $\Integer$ and $M$ defined as $\operatorname{of}$ applied to the representation of $M$ and $G$.

the product isomorphism product of A and B (from the name)

Let $A$ and $B$ be representations of $k$ and $G$. Then the product isomorphism product of $A$ and $B$ is an isomorphism of $\operatorname{of}$ applied to the product of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to $B$ and the product of $A$ and $B$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to $\operatorname{binaryBiconeIsBilimit}$ applied to $A$ and $B$ and $\operatorname{isLimit}$ applied to the pair of $A$ and $B$.

the quotient of A and W (from the name)

Let $A$ be a representation of $k$ and $G$. Let $W$ be a submodule of $k$ and $\operatorname{V}$ applied to $A$ such that for all elements $g$ of $G$, $W$ is less than or equal to the preimage of $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $g$ and $W$. Then the quotient of $A$ and $W$ is a representation of $k$ and $G$ defined as $\operatorname{of}$ applied to the quotient of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $W$.

the representation isomorphism action of k and G (from the name)

Let $k$ and $G$ be sets. Then the representation isomorphism action of $k$ and $G$ is an equivalence of the set of representations of $k$ and $G$ and the set of actions of the set of module categories of $k$ and $G$.

the subrepresentation of A and W (from the name)

Let $A$ be a representation of $k$ and $G$. Let $W$ be a submodule of $k$ and $\operatorname{V}$ applied to $A$ such that for all elements $g$ of $G$, $W$ is less than or equal to the preimage of $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $g$ and $W$. Then the subrepresentation of $A$ and $W$ is a representation of $k$ and $G$ defined as $\operatorname{of}$ applied to the subrepresentation of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $W$.

the subtype of A and W (from the name)

Let $A$ be a representation of $k$ and $G$. Let $W$ be a submodule of $k$ and $\operatorname{V}$ applied to $A$ such that for all elements $g$ of $G$, $W$ is less than or equal to the preimage of $\mathrm{Rep\_\_\_u3c1\_\_\_app}$ applied to $A$ and $g$ and $W$. Then the subtype of $A$ and $W$ is a homomorphism of the subrepresentation of $A$ and $W$ and $A$.

the tensor homomorphism equivalence of B and C (from the name)

Let $A$, $B$ and $C$ be representations of $k$ and $G$. Then the tensor homomorphism equivalence of $B$ and $C$ is an equivalence from the set of homomorphisms of the tensor object of $A$ and $B$ and $C$ to the set of homomorphisms of $B$ and the action of $\operatorname{ihom}$ applied to $A$ and $C$.

$\operatorname{toAdditive}$ is an additive equivalence of $\operatorname{V}$ applied to the representation of $M$ and $G$ and $\mathrm{Additive}$ applied to $G$ defined as the identity map of $\operatorname{V}$ applied to the representation of $M$ and $G$.

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

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

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

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

the equivalence of i (from the name)

Let $i$ be an isomorphism of $A$ and $B$. Then the equivalence of $i$ is an equivalence of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $A$ and $\mathrm{Rep\_\_\_u3c1\_}$ applied to $B$.

the diagonal homomorphism equivalence of n and A (from the name)

Let $k$ and $G$ be sets. Let $n$ be a natural number. Let $A$ be a representation of $k$ and $G$. Then the diagonal homomorphism equivalence of $n$ and $A$ is a linear equivalence of the set of homomorphisms of the diagonal of $n + 1$ and $A$ 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$ defined as the composition of the homomorphism congruence of the diagonal successor isomorphism free of $n$ and the identity of $A$ and the free lift equivalence of $A$.

the diagonal successor isomorphism free of n (from the name)

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then the diagonal successor isomorphism free of $n$ is an isomorphism of the diagonal of $n + 1$ 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 composition of $\operatorname{diagonalSuccIsoTensorTrivial}$ applied to $k$, $G$ and $n$ and the left regular tensor trivial isomorphism free of $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$.

Let $k$ and $G$ be sets. Let $n$ be a natural number. Then $\operatorname{diagonalSuccIsoTensorTrivial}$ applied to $k$, $G$ and $n$ is an isomorphism of the diagonal of $n + 1$ and the tensor object of the left regular of $k$ and $G$ and $\operatorname{trivial}$ applied to $k$, $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{linearizationOfMulActionIso}$ applied to $k$, $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $G$ and the composition of the map isomorphism of $\operatorname{linearization}$ applied to $k$ and $G$ and $\operatorname{diagonalSuccIsoTensorTrivial}$ applied to $G$ and $n$ and the composition of the inverse of the isomorphism of the left regular of $G$ and $\operatorname{trivial}$ applied to $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$ and the tensor isomorphism of $\operatorname{linearizationOfMulActionIso}$ applied to $k$, $G$ and $G$ and $\operatorname{linearizationTrivialIso}$ applied to $k$, $G$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $G$.

the categorical equivalence (from the docstring)

The categorical equivalence is an equivalence of the set of representations of $k$ and $G$ and the set of module categories of the set of monoid algebras of $k$ and $G$.

the representation (from the name)

The representation is a functor of the set of module categories of the set of monoid algebras of $k$ and $G$ and the set of representations of $k$ and $G$.

the module monoid algebra (from the name)

The module monoid algebra is a functor of the set of representations of $k$ and $G$ and the set of module categories of the set of monoid algebras of $k$ and $G$.

the lift homomorphism of f and #3 (from the name)

Let $f$ be a monoid homomorphism of $H$ and $G$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Let $\mathrm{f'}$ be a homomorphism of the restriction of $f$ and $X$ and the restriction of $f$ and $Y$. Then the lift homomorphism of $f$ and $\mathrm{f'}$ is a homomorphism of $X$ and $Y$.

the representation of A and S (from the name)

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

the restriction of f and M (from the name)

Let $f$ be a monoid homomorphism of $H$ and $G$. Let $M$ be a representation of $k$ and $G$. Then the restriction of $f$ and $M$ is a representation of $k$ and $H$ defined as the action of the restriction functor of $f$ and $M$.

the restriction functor of f (from the docstring)

Let $f$ be a monoid homomorphism of $H$ and $G$. Then the restriction functor of $f$ is a functor of the set of representations of $k$ and $G$ and the set of representations of $k$ and $H$.

the map induced by a monoid homomorphism of f and p (from the docstring)

Let $f$ be a monoid homomorphism of $H$ and $G$. Let $p$ be a homomorphism of $X$ and $Y$. Then the map induced by a monoid homomorphism of $f$ and $p$ is a homomorphism of $\operatorname{of}$ applied to the composition of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $X$ and $f$ and $\operatorname{of}$ applied to the composition of $\mathrm{Rep\_\_\_u3c1\_}$ applied to $Y$ and $f$.

the restriction of A and S (from the name)

Let $A$ be a representation of $k$ and $G$. Let $S$ be a subgroup of $G$. Then the restriction of $A$ and $S$ is an isomorphism of the restriction of $\operatorname{mk'}$ applied to $S$ and the representation of $A$ and $S$ and $A$ defined as the identity of the restriction of $\operatorname{mk'}$ applied to $S$ and the representation of $A$ and $S$.

x4 is a semisimple representation (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Then $x_{4}$ is a semisimple representation, if the set of subrepresentations of $x_{4}$ is a complemented lattice.

the stabilizer of x4 and v (from the docstring)

Let $x_{4}$ be a representation of $G$ and $V$. Let $v$ be an element of $V$. Then the stabilizer of $x_{4}$ and $v$ is a subgroup of $G$.

Let $x_{4}$ be a representation of $G$ and $V$. Then $\operatorname{invtSubmodule}$ applied to $x_{4}$ is a sublattice of the set of submodules of $k$ and $V$ defined as the infimum of the function that maps $g$ to $\operatorname{invtSubmodule}$ applied to $x_{4}$ applied to $g$.

the map submodule of x4 (from the name)

Let $x_{4}$ be a representation of $G$ and $V$. Then the map submodule of $x_{4}$ is an order isomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{invtSubmodule} (x_{4})}{x_{5}})}$ and the set of submodules of the set of monoid algebras of $k$ and $G$ and $\operatorname{asModule}$ applied to $x_{4}$.

subrepresentation of x4 (from the name)

Let $x_{4}$ be a representation of $G$ and $W$. Then the subrepresentations of $x_{4}$ are a basic type.

Let $x_{5}$ be a subrepresentation of $x_{4}$. Then $\operatorname{asSubmodule}$ applied to $x_{5}$ is a submodule of the set of monoid algebras of $A$ and $G$ and $\operatorname{asModule}$ applied to $x_{4}$.

Let $x_{4}$ be a subrepresentation of the representation of $M$. Then $\operatorname{asSubmodule'}$ applied to $x_{4}$ is a submodule of the set of monoid algebras of $A$ and $G$ and $M$.

the subrepresentation of N (from the name)

Let $N$ be a submodule of the set of monoid algebras of $A$ and $G$ and $M$. Then the subrepresentation of $N$ is a subrepresentation of the representation of $M$.

the subrepresentation of N (from the name)

Let $N$ be a submodule of the set of monoid algebras of $A$ and $G$ and $\operatorname{asModule}$ applied to $x_{4}$. Then the subrepresentation of $N$ is a subrepresentation of $x_{4}$.

the quotient of x5 (from the name)

Let $x_{5}$ be a subrepresentation of $x_{4}$. Then the quotient of $x_{5}$ is a representation of $G$ and the set of quotients of $W$ and the submodule of $x_{5}$.

the submodule subrepresentation order isomorphism (from the name)

The submodule subrepresentation order isomorphism is an order isomorphism of the set of submodules of the set of monoid algebras of $A$ and $G$ and $M$ and the set of subrepresentations of the representation of $M$.

the subrepresentation submodule order isomorphism (from the name)

The subrepresentation submodule order isomorphism is an order isomorphism of the set of subrepresentations of $x_{4}$ and the set of submodules of the set of monoid algebras of $A$ and $G$ and $\operatorname{asModule}$ applied to $x_{4}$.

the representation of x5 (from the name)

Let $x_{5}$ be a subrepresentation of $x_{4}$. Then the representation of $x_{5}$ is a representation of $G$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{toSubmodule} (x_{5})}{x_{6}})}$.

the submodule of self (from the name)

Let $\mathrm{self}$ be a subrepresentation of $x_{4}$. Then the submodule of $\mathrm{self}$ is a submodule of $A$ and $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the algebra homomorphism of x2 (from the name)

Let $x_{2}$ be an automorphism of $\operatorname{forget}$ applied to $k$ and $G$. Then the algebra homomorphism of $x_{2}$ is an algebra homomorphism of the set of functions from elements of $G$ to elements of $k$ and the set of functions from elements of $G$ to elements of $k$.

the equivalence of k and G (from the name)

Let $k$ and $G$ be sets. Then the equivalence of $k$ and $G$ is a multiplicative equivalence of $G$ and the set of automorphisms of $\operatorname{forget}$ applied to $k$ and $G$.

the equivalence application of g and X (from the name)

Let $g$ be an element of $G$. Let $X$ be an element of $\mathrm{FDRep}$ applied to $k$ and $G$. Then the equivalence application of $g$ and $X$ is an isomorphism of $\operatorname{V}$ applied to $X$ and $\operatorname{V}$ applied to $X$.

the group homomorphism of k and G (from the docstring)

Let $k$ and $G$ be sets. Then the group homomorphism of $k$ and $G$ is a monoid homomorphism of $G$ and the set of automorphisms of $\operatorname{forget}$ applied to $k$ and $G$.

Let $k$ and $G$ be sets. Then $\operatorname{forget}$ applied to $k$ and $G$ is an element of $\operatorname{LaxMonoidalFunctor}$ applied to $\mathrm{FDRep}$ applied to $k$ and $G$ and $\mathrm{FGModuleCat}$ applied to $k$ defined as $\operatorname{of}$ applied to the forgetful functor of $\mathrm{FDRep}$ applied to $k$ and $G$ and $\mathrm{FGModuleCat}$ applied to $k$.

the left regular (from the name)

The left regular is a representation of $G$ and the set of functions from elements of $G$ to elements of $k$.

Let $s$ be an element of $G$. Then $\operatorname{leftRegularFDRepHom}$ applied to $s$ is an end of the right regular representation.

the multiplicative representation homomorphism (from the name)

The multiplicative representation homomorphism is a homomorphism of the tensor object of the right regular representation and the right regular representation and the right regular representation.

the finite group of X and v (from the name)

Let $X$ be an element of $\mathrm{FDRep}$ applied to $k$ and $G$. Let $v$ be a carrier of $\operatorname{V}$ applied to $X$. Then the finite group of $X$ and $v$ is a homomorphism of the right regular representation and $X$.

the right regular representation (from the docstring)

The right regular representation is an element of $\mathrm{FDRep}$ applied to $k$ and $G$ defined as $\operatorname{of}$ applied to the right regular.

the right regular (from the name)

The right regular is a representation of $G$ and the set of functions from elements of $G$ to elements of $k$.

the sum multiplicative inverse of v (from the name)

Let $v$ be a carrier of $\operatorname{V}$ applied to $X$. Then the sum multiplicative inverse of $v$ is a linear map of the set of functions from elements of $G$ to elements of $k$ and the set of carriers of $\operatorname{V}$ applied to $X$.