Coinvariants

📁 Source: Mathlib/RepresentationTheory/Coinvariants.lean

Statistics

Metric	Count
Definitions coinvariantsAdjunction, coinvariantsFunctor, coinvariantsMk, coinvariantsShortComplex, coinvariantsTensor, coinvariantsTensorFreeLEquiv, coinvariantsTensorFreeToFinsupp, coinvariantsTensorMk, desc, finsuppToCoinvariantsTensorFree, quotientToCoinvariants, quotientToCoinvariantsFunctor, toCoinvariants, toCoinvariantsKer, toCoinvariantsMkQ, Coinvariants, instAddCommGroup, instModule, ker, map, mk, coinvariantsFinsuppLEquiv, coinvariantsToFinsupp, coinvariantsTprodLeftRegularLEquiv, finsuppToCoinvariants, ofCoinvariantsTprodLeftRegular, quotientToCoinvariants, toCoinvariants, toCoinvariantsKer	29
Theorems coinvariantsAdjunction_counit_app, coinvariantsAdjunction_homEquiv_apply_hom, coinvariantsAdjunction_homEquiv_symm_apply_hom, coinvariantsAdjunction_unit_app_hom, coinvariantsFunctor_hom_ext, coinvariantsFunctor_hom_ext_iff, coinvariantsFunctor_map_hom, coinvariantsFunctor_obj_carrier, coinvariantsMk_app_hom, coinvariantsShortComplex_X₁, coinvariantsShortComplex_X₂, coinvariantsShortComplex_X₃, coinvariantsShortComplex_f, coinvariantsShortComplex_g, coinvariantsShortComplex_shortExact, coinvariantsTensorFreeLEquiv_apply, coinvariantsTensorFreeLEquiv_symm_apply, coinvariantsTensorFreeToFinsupp_mk_tmul_single, coinvariantsTensorMk_apply, coinvariantsTensor_hom_ext, coinvariantsTensor_hom_ext_iff, finsuppToCoinvariantsTensorFree_single, instAdditiveModuleCatCoinvariantsFunctor, instAdditiveModuleCatObjFunctorCoinvariantsTensor, instEpiModuleCatAppActionCoinvariantsMk, instIsLeftAdjointModuleCatCoinvariantsFunctor, instLinearModuleCatCoinvariantsFunctor, instLinearModuleCatObjFunctorCoinvariantsTensor, instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, quotientToCoinvariantsFunctor_map_hom, quotientToCoinvariantsFunctor_obj_V, toCoinvariantsMkQ_hom, hom_ext, hom_ext_iff, induction_on, le_comap_ker, lift_comp_mk, lift_mk, map_comp, map_comp_mk, map_id, map_mk, mem_ker_of_eq, mk_eq_iff, mk_eq_zero, mk_inv_tmul, mk_self_apply, mk_surjective, mk_tmul_inv, sub_mem_ker, coinvariantsFinsuppLEquiv_apply, coinvariantsFinsuppLEquiv_symm_apply, coinvariantsToFinsupp_mk_single, coinvariantsTprodLeftRegularLEquiv_apply, coinvariantsTprodLeftRegularLEquiv_symm_apply, finsuppToCoinvariants_single_mk, instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, ofCoinvariantsTprodLeftRegular_mk_tmul_single, toCoinvariants_mk	59
Total	88

Rep

Definitions

Name	Category	Theorems
coinvariantsAdjunction 📖	CompOp	4 math math: coinvariantsAdjunction_counit_app, coinvariantsAdjunction_homEquiv_symm_apply_hom, coinvariantsAdjunction_unit_app_hom, coinvariantsAdjunction_homEquiv_apply_hom
coinvariantsFunctor 📖	CompOp	36 math math: groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, coinvariantsAdjunction_counit_app, groupHomology.π_comp_H0Iso_hom_assoc, coinvariantsAdjunction_homEquiv_symm_apply_hom, groupHomology.d₁₀_comp_coinvariantsMk_apply, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, coinvariantsFunctor_obj_carrier, groupHomology.coinvariantsMk_comp_H0Iso_inv, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coinvariantsFunctor_hom_ext_iff, instLinearModuleCatCoinvariantsFunctor, groupHomology.π_comp_H0Iso_hom_apply, instEpiModuleCatAppActionCoinvariantsMk, groupHomology.d₁₀_comp_coinvariantsMk, quotientToCoinvariantsFunctor_map_hom, instIsLeftAdjointModuleCatCoinvariantsFunctor, groupHomology.map_id_comp_H0Iso_hom_assoc, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, coinvariantsMk_app_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, groupHomology.map_id_comp_H0Iso_hom_apply, groupHomology.π_comp_H0Iso_hom, groupHomology.H0π_comp_H0Iso_hom, groupHomology.map_id_comp_H0Iso_hom, groupHomology.shortComplexH0_g, coinvariantsAdjunction_unit_app_hom, groupHomology.d₁₀_comp_coinvariantsMk_assoc, groupHomology.H0π_comp_H0Iso_hom_assoc, coinvariantsAdjunction_homEquiv_apply_hom, instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, coinvariantsFunctor_map_hom, groupHomology.H0π_comp_H0Iso_hom_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, instAdditiveModuleCatCoinvariantsFunctor
coinvariantsMk 📖	CompOp	18 math math: groupHomology.π_comp_H0Iso_hom_assoc, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupHomology.coinvariantsMk_comp_H0Iso_inv, coinvariantsFunctor_hom_ext_iff, instEpiModuleCatAppActionCoinvariantsMk, groupHomology.d₁₀_comp_coinvariantsMk, coinvariantsMk_app_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, groupHomology.π_comp_H0Iso_hom, groupHomology.H0π_comp_H0Iso_hom, groupHomology.shortComplexH0_g, coinvariantsAdjunction_unit_app_hom, groupHomology.d₁₀_comp_coinvariantsMk_assoc, groupHomology.H0π_comp_H0Iso_hom_assoc, coinvariantsAdjunction_homEquiv_apply_hom, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc
coinvariantsShortComplex 📖	CompOp	7 math math: groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, coinvariantsShortComplex_g, coinvariantsShortComplex_f, coinvariantsShortComplex_X₁, coinvariantsShortComplex_X₂, coinvariantsShortComplex_X₃, coinvariantsShortComplex_shortExact
coinvariantsTensor 📖	CompOp	12 math math: instLinearModuleCatObjFunctorCoinvariantsTensor, coinvariantsTensorIndIso_inv, coinvariantsTensorIndIso_hom, coinvariantsTensorIndNatIso_inv_app, instAdditiveModuleCatObjFunctorCoinvariantsTensor, Tor_map, coinvariantsTensorIndNatIso_hom_app, coinvariantsTensor_hom_ext_iff, coinvariantsTensorMk_apply, coinvariantsTensorIndHom_mk_tmul_indVMk, coinvariantsTensorIndInv_mk_tmul_indMk, Tor_obj
coinvariantsTensorFreeLEquiv 📖	CompOp	2 math math: coinvariantsTensorFreeLEquiv_symm_apply, groupHomology.inhomogeneousChains.d_eq
coinvariantsTensorFreeToFinsupp 📖	CompOp	2 math math: coinvariantsTensorFreeLEquiv_apply, coinvariantsTensorFreeToFinsupp_mk_tmul_single
coinvariantsTensorMk 📖	CompOp	4 math math: coinvariantsTensor_hom_ext_iff, coinvariantsTensorMk_apply, coinvariantsTensorIndHom_mk_tmul_indVMk, coinvariantsTensorIndInv_mk_tmul_indMk
desc 📖	CompOp	2 math math: coinvariantsAdjunction_counit_app, coinvariantsAdjunction_homEquiv_symm_apply_hom
finsuppToCoinvariantsTensorFree 📖	CompOp	2 math math: finsuppToCoinvariantsTensorFree_single, coinvariantsTensorFreeLEquiv_symm_apply
quotientToCoinvariants 📖	CompOp	3 math math: groupHomology.H1CoresCoinf_X₃, groupHomology.H1CoresCoinf_g, quotientToCoinvariantsFunctor_map_hom
quotientToCoinvariantsFunctor 📖	CompOp	3 math math: groupHomology.coinfNatTrans_app, quotientToCoinvariantsFunctor_map_hom, quotientToCoinvariantsFunctor_obj_V
toCoinvariants 📖	CompOp	3 math math: toCoinvariantsMkQ_hom, coinvariantsShortComplex_X₃, quotientToCoinvariantsFunctor_obj_V
toCoinvariantsKer 📖	CompOp	1 math math: coinvariantsShortComplex_X₁
toCoinvariantsMkQ 📖	CompOp	3 math math: groupHomology.H1CoresCoinf_g, coinvariantsShortComplex_g, toCoinvariantsMkQ_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinvariantsAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.comp Rep Action.instCategory trivialFunctor coinvariantsFunctor CategoryTheory.Functor.id CategoryTheory.Adjunction.counit coinvariantsAdjunction desc CategoryTheory.Functor.obj trivial ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coinvariantsAdjunction_homEquiv_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Action.instCategory trivialFunctor DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct coinvariantsFunctor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv coinvariantsAdjunction CategoryTheory.CategoryStruct.comp Action Action.forget CategoryTheory.NatTrans.app coinvariantsMk	—	—
coinvariantsAdjunction_homEquiv_symm_apply_hom 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj trivialFunctor coinvariantsFunctor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv coinvariantsAdjunction desc instIsTrivialObjModuleCatTrivialFunctor	—	coinvariantsFunctor_hom_ext instIsTrivialObjModuleCatTrivialFunctor ModuleCat.hom_ext LinearMap.ext
coinvariantsAdjunction_unit_app_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp coinvariantsFunctor trivialFunctor CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit coinvariantsAdjunction Action Action.forget coinvariantsMk	—	—
coinvariantsFunctor_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.forget coinvariantsFunctor CategoryTheory.NatTrans.app coinvariantsMk	—	—	CategoryTheory.cancel_epi instEpiModuleCatAppActionCoinvariantsMk
coinvariantsFunctor_hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.forget coinvariantsFunctor CategoryTheory.NatTrans.app coinvariantsMk	—	coinvariantsFunctor_hom_ext
coinvariantsFunctor_map_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of Representation.Coinvariants ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory ModuleCat.isAddCommGroup ModuleCat.isModule ρ Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule CategoryTheory.Functor.map Rep Action.instCategory coinvariantsFunctor Representation.Coinvariants.map Action.Hom.hom	—	—
coinvariantsFunctor_obj_carrier 📖	mathematical	—	ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj Rep Action.instCategory ModuleCat ModuleCat.moduleCategory coinvariantsFunctor Representation.Coinvariants Action.V ModuleCat.isAddCommGroup ModuleCat.isModule ρ	—	—
coinvariantsMk_app_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule Representation.Coinvariants Action.V ModuleCat ModuleCat.moduleCategory ρ Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule CategoryTheory.NatTrans.app Action Action.instCategory Action.forget coinvariantsFunctor coinvariantsMk	—	—
coinvariantsShortComplex_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive coinvariantsShortComplex toCoinvariantsKer	—	—
coinvariantsShortComplex_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive coinvariantsShortComplex	—	—
coinvariantsShortComplex_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive coinvariantsShortComplex toCoinvariants	—	—
coinvariantsShortComplex_f 📖	mathematical	—	CategoryTheory.ShortComplex.f Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive coinvariantsShortComplex subtype Representation.Coinvariants.ker Subgroup SetLike.instMembership Subgroup.instSetLike ModuleCat.carrier Action.V Subgroup.toGroup ModuleCat.isAddCommGroup ModuleCat.isModule MonoidHom.comp LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ Subgroup.subtype	—	—
coinvariantsShortComplex_g 📖	mathematical	—	CategoryTheory.ShortComplex.g Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive coinvariantsShortComplex toCoinvariantsMkQ	—	—
coinvariantsShortComplex_shortExact 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive coinvariantsShortComplex	—	CategoryTheory.Functor.reflects_exact_of_faithful Action.forget₂_preservesZeroMorphisms CategoryTheory.forget₂_faithful CategoryTheory.ShortComplex.moduleCat_exact_iff Submodule.Quotient.mk_eq_zero mono_iff_injective epi_iff_surjective Submodule.mkQ_surjective
coinvariantsTensorFreeLEquiv_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants TensorProduct ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instZero AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ModuleCat.isModule Finsupp.module Semiring.toModule TensorProduct.addCommGroup ModuleCat.isAddCommGroup TensorProduct.instModule Representation.tprod ρ Representation.free NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory free LinearMap.instFunLike coinvariantsTensorFreeToFinsupp	—	—
coinvariantsTensorFreeLEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupCarrierVModuleCat Representation.Coinvariants CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory free ModuleCat.isAddCommGroup ModuleCat.isModule ρ Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Representation.Coinvariants.instAddCommGroup Finsupp.module Representation.Coinvariants.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm coinvariantsTensorFreeLEquiv LinearMap ModuleCat.of MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero Finsupp.instAddCommGroup Ring.toAddCommGroup NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Representation.tprod Representation.free LinearMap.instFunLike finsuppToCoinvariantsTensorFree	—	RingHomInvPair.ids
coinvariantsTensorFreeToFinsupp_mk_tmul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants TensorProduct ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instZero AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ModuleCat.isModule Finsupp.module Semiring.toModule TensorProduct.addCommGroup ModuleCat.isAddCommGroup TensorProduct.instModule Representation.tprod ρ Representation.free NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap.instFunLike coinvariantsTensorFreeToFinsupp TensorProduct.tmul Finsupp.single SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	RingHomCompTriple.ids TensorProduct.finsuppRight_tmul_single RingHomInvPair.ids Representation.coinvariantsFinsuppLEquiv_apply Representation.coinvariantsToFinsupp_mk_single Finsupp.lcongr_single Representation.coinvariantsTprodLeftRegularLEquiv_apply Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single
coinvariantsTensorMk_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring coinvariantsTensorMk TensorProduct Representation.Coinvariants TensorProduct.addCommGroup CategoryTheory.MonoidalCategory.curriedTensor Action.instMonoidalCategory ModuleCat.monoidalCategory ρ Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule TensorProduct.tmul	—	smulCommClass_self
coinvariantsTensor_hom_ext 📖	—	LinearMap.compr₂ CommRing.toCommSemiring CommSemiring.toSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero coinvariantsTensorMk ModuleCat.Hom.hom	—	—	smulCommClass_self IsScalarTower.left coinvariantsFunctor_hom_ext ModuleCat.hom_ext TensorProduct.ext
coinvariantsTensor_hom_ext_iff 📖	mathematical	—	LinearMap.compr₂ CommRing.toCommSemiring CommSemiring.toSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero coinvariantsTensorMk ModuleCat.Hom.hom	—	smulCommClass_self IsScalarTower.left coinvariantsTensor_hom_ext
finsuppToCoinvariantsTensorFree_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupCarrierVModuleCat Representation.Coinvariants TensorProduct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instZero AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ModuleCat.isModule Finsupp.module Semiring.toModule TensorProduct.addCommGroup ModuleCat.isAddCommGroup TensorProduct.instModule Representation.tprod ρ Representation.free Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule LinearMap.instFunLike finsuppToCoinvariantsTensorFree Finsupp.single NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TensorProduct.tmul InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomCompTriple.ids LinearMap.comp.congr_simp LinearEquiv.trans.congr_simp Finsupp.lcongr_symm Finsupp.lcongr_single TensorProduct.finsuppRight_symm_apply_single
instAdditiveModuleCatCoinvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive Rep CommRing.toRing ModuleCat Action.instCategory ModuleCat.moduleCategory Action.instPreadditive ModuleCat.instPreadditive coinvariantsFunctor	—	coinvariantsFunctor_hom_ext ModuleCat.hom_ext LinearMap.ext map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass RingHomCompTriple.ids CategoryTheory.Preadditive.comp_add
instAdditiveModuleCatObjFunctorCoinvariantsTensor 📖	mathematical	—	CategoryTheory.Functor.Additive Rep CommRing.toRing ModuleCat Action.instCategory ModuleCat.moduleCategory Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor	—	CategoryTheory.MonoidalPreadditive.whiskerLeft_add Action.instMonoidalPreadditive ModuleCat.instMonoidalPreadditive CategoryTheory.Functor.map_add instAdditiveModuleCatCoinvariantsFunctor
instEpiModuleCatAppActionCoinvariantsMk 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.forget coinvariantsFunctor CategoryTheory.NatTrans.app coinvariantsMk	—	ModuleCat.epi_iff_surjective Representation.Coinvariants.mk_surjective
instIsLeftAdjointModuleCatCoinvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory coinvariantsFunctor	—	CategoryTheory.Adjunction.isLeftAdjoint
instLinearModuleCatCoinvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Rep CommRing.toRing ModuleCat Action.instCategory ModuleCat.moduleCategory Action.instPreadditive ModuleCat.instPreadditive instLinearRep ModuleCat.instLinear coinvariantsFunctor	—	coinvariantsFunctor_hom_ext ModuleCat.hom_ext LinearMap.ext map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass ModuleCat.Algebra.instSMulCommClassCarrier RingHomCompTriple.ids CategoryTheory.Linear.comp_smul
instLinearModuleCatObjFunctorCoinvariantsTensor 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Rep CommRing.toRing ModuleCat Action.instCategory ModuleCat.moduleCategory Action.instPreadditive ModuleCat.instPreadditive instLinearRep ModuleCat.instLinear CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor	—	CategoryTheory.MonoidalLinear.whiskerLeft_smul Action.instMonoidalPreadditive ModuleCat.instMonoidalPreadditive Action.instMonoidalLinear ModuleCat.instMonoidalLinear CategoryTheory.Functor.map_smul instLinearModuleCatCoinvariantsFunctor
instPreservesZeroMorphismsModuleCatCoinvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive coinvariantsFunctor	—	CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveModuleCatCoinvariantsFunctor
quotientToCoinvariantsFunctor_map_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group quotientToCoinvariants CategoryTheory.Functor.map Rep Action.instCategory quotientToCoinvariantsFunctor SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup coinvariantsFunctor CategoryTheory.Functor.obj Action Action.res Subgroup.subtype	—	—
quotientToCoinvariantsFunctor_obj_V 📖	mathematical	—	Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group CategoryTheory.Functor.obj Rep Action.instCategory quotientToCoinvariantsFunctor ModuleCat.of ModuleCat.carrier toCoinvariants ModuleCat.isAddCommGroup ModuleCat.isModule	—	—
toCoinvariantsMkQ_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid toCoinvariants Action.Hom.hom toCoinvariantsMkQ Subgroup SetLike.instMembership Subgroup.instSetLike ModuleCat.carrier Subgroup.toGroup ModuleCat.isAddCommGroup ModuleCat.isModule MonoidHom.comp LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ Subgroup.subtype	—	—

Representation

Definitions

Name	Category	Theorems
Coinvariants 📖	CompOp	41 math math: groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, Coinvariants.mk_inv_tmul, ofCoinvariantsTprodLeftRegular_mk_tmul_single, Rep.finsuppToCoinvariantsTensorFree_single, Rep.coinvariantsTensorFreeLEquiv_symm_apply, Coinvariants.mk_tmul_inv, Coinvariants.map_comp_mk, Coinvariants.lift_mk, coinvariantsFinsuppLEquiv_apply, groupHomology.d₁₀_comp_coinvariantsMk_apply, coinvariantsTprodLeftRegularLEquiv_apply, Coinvariants.mk_self_apply, Rep.coinvariantsFunctor_obj_carrier, Coinvariants.lift_comp_mk, Rep.coinvariantsTensorFreeLEquiv_apply, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, groupHomology.π_comp_H0Iso_hom_apply, finsuppToCoinvariants_single_mk, Coinvariants.map_mk, instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, Coinvariants.mk_eq_zero, Rep.coinvariantsMk_app_hom, Coinvariants.map_id, Coinvariants.mk_eq_iff, coinvariantsTprodLeftRegularLEquiv_symm_apply, groupHomology.map_id_comp_H0Iso_hom_apply, toCoinvariants_mk, Rep.coinvariantsTensorMk_apply, coinvariantsToFinsupp_mk_single, coinvariantsFinsuppLEquiv_symm_apply, groupHomology.inhomogeneousChains.d_eq, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, Coinvariants.map_comp, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, Rep.coinvariantsFunctor_map_hom, groupHomology.H0π_comp_H0Iso_hom_apply, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, Coinvariants.hom_ext_iff, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, Coinvariants.mk_surjective
coinvariantsFinsuppLEquiv 📖	CompOp	2 math math: coinvariantsFinsuppLEquiv_apply, coinvariantsFinsuppLEquiv_symm_apply
coinvariantsToFinsupp 📖	CompOp	2 math math: coinvariantsFinsuppLEquiv_apply, coinvariantsToFinsupp_mk_single
coinvariantsTprodLeftRegularLEquiv 📖	CompOp	3 math math: coinvariantsTprodLeftRegularLEquiv_apply, coinvariantsTprodLeftRegularLEquiv_symm_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply
finsuppToCoinvariants 📖	CompOp	2 math math: finsuppToCoinvariants_single_mk, coinvariantsFinsuppLEquiv_symm_apply
ofCoinvariantsTprodLeftRegular 📖	CompOp	2 math math: ofCoinvariantsTprodLeftRegular_mk_tmul_single, coinvariantsTprodLeftRegularLEquiv_apply
quotientToCoinvariants 📖	CompOp	—
toCoinvariants 📖	CompOp	2 math math: instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, toCoinvariants_mk
toCoinvariantsKer 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinvariantsFinsuppLEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Coinvariants Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.instAddCommGroup Finsupp.module finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Coinvariants.instAddCommGroup Finsupp.instAddCommMonoid Coinvariants.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv coinvariantsFinsuppLEquiv LinearMap LinearMap.instFunLike coinvariantsToFinsupp	—	RingHomInvPair.ids
coinvariantsFinsuppLEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp Coinvariants DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Coinvariants.instAddCommGroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module finsupp Finsupp.instAddCommMonoid Coinvariants.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm coinvariantsFinsuppLEquiv LinearMap LinearMap.instFunLike finsuppToCoinvariants	—	RingHomInvPair.ids
coinvariantsToFinsupp_mk_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Coinvariants Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.instAddCommGroup Finsupp.module finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Coinvariants.instAddCommGroup Finsupp.instAddCommMonoid Coinvariants.instModule LinearMap.instFunLike coinvariantsToFinsupp Finsupp.single	—	Finsupp.mapRange_single LinearMap.map_zero
coinvariantsTprodLeftRegularLEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Coinvariants TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup TensorProduct.instModule tprod leftRegular Coinvariants.instAddCommGroup Coinvariants.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv coinvariantsTprodLeftRegularLEquiv LinearMap LinearMap.instFunLike ofCoinvariantsTprodLeftRegular	—	RingHomInvPair.ids
coinvariantsTprodLeftRegularLEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Coinvariants TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup TensorProduct.instModule tprod leftRegular Coinvariants.instAddCommGroup Coinvariants.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm coinvariantsTprodLeftRegularLEquiv LinearMap LinearMap.instFunLike TensorProduct.tmul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.single InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids
finsuppToCoinvariants_single_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Coinvariants DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Coinvariants.instAddCommGroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module finsupp Finsupp.instAddCommMonoid Coinvariants.instModule LinearMap.instFunLike finsuppToCoinvariants Finsupp.single	—	Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants 📖	mathematical	—	IsTrivial Subgroup SetLike.instMembership Subgroup.instSetLike Coinvariants DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.comp LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Subgroup.subtype Coinvariants.instAddCommGroup Coinvariants.instModule toCoinvariants	—	Coinvariants.hom_ext LinearMap.ext RingHomCompTriple.ids Coinvariants.mk_eq_iff Coinvariants.mem_ker_of_eq
ofCoinvariantsTprodLeftRegular_mk_tmul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Coinvariants TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup TensorProduct.instModule tprod leftRegular Coinvariants.instAddCommGroup Coinvariants.instModule LinearMap.instFunLike ofCoinvariantsTprodLeftRegular TensorProduct.tmul Finsupp.single SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smulCommClass_self Finsupp.linearCombination_single
toCoinvariants_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Coinvariants Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.comp AddCommGroup.toAddCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Subgroup.subtype Coinvariants.instAddCommGroup Coinvariants.instModule LinearMap.instFunLike Representation MonoidHom.instFunLike toCoinvariants	—	—

Representation.Coinvariants

Definitions

Name	Category	Theorems
instAddCommGroup 📖	CompOp	42 math math: Rep.coindToInd_of_support_subset_orbit, mk_inv_tmul, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, Rep.finsuppToCoinvariantsTensorFree_single, Rep.coinvariantsTensorFreeLEquiv_symm_apply, mk_tmul_inv, map_comp_mk, lift_mk, Representation.coinvariantsFinsuppLEquiv_apply, Representation.coinvariantsTprodLeftRegularLEquiv_apply, mk_self_apply, lift_comp_mk, Rep.coinvariantsTensorFreeLEquiv_apply, Rep.indResAdjunction_counit_app_hom_hom, Rep.coindToInd_apply, Representation.finsuppToCoinvariants_single_mk, map_mk, Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, mk_eq_zero, Rep.coinvariantsMk_app_hom, map_id, mk_eq_iff, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, Representation.toCoinvariants_mk, Rep.coinvariantsTensorMk_apply, Rep.indMap_hom, Representation.coinvariantsToFinsupp_mk_single, Representation.ind_mk, Representation.coinvariantsFinsuppLEquiv_symm_apply, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, groupHomology.inhomogeneousChains.d_eq, Representation.ind_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, map_comp, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, Rep.coinvariantsFunctor_map_hom, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, Representation.IndV.hom_ext_iff, Rep.indResHomEquiv_symm_apply_hom, hom_ext_iff, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, mk_surjective
instModule 📖	CompOp	42 math math: Rep.coindToInd_of_support_subset_orbit, mk_inv_tmul, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, Rep.finsuppToCoinvariantsTensorFree_single, Rep.coinvariantsTensorFreeLEquiv_symm_apply, mk_tmul_inv, map_comp_mk, lift_mk, Representation.coinvariantsFinsuppLEquiv_apply, Representation.coinvariantsTprodLeftRegularLEquiv_apply, mk_self_apply, lift_comp_mk, Rep.coinvariantsTensorFreeLEquiv_apply, Rep.indResAdjunction_counit_app_hom_hom, Rep.coindToInd_apply, Representation.finsuppToCoinvariants_single_mk, map_mk, Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, mk_eq_zero, Rep.coinvariantsMk_app_hom, map_id, mk_eq_iff, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, Representation.toCoinvariants_mk, Rep.coinvariantsTensorMk_apply, Rep.indMap_hom, Representation.coinvariantsToFinsupp_mk_single, Representation.ind_mk, Representation.coinvariantsFinsuppLEquiv_symm_apply, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, groupHomology.inhomogeneousChains.d_eq, Representation.ind_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, map_comp, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, Rep.coinvariantsFunctor_map_hom, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, Representation.IndV.hom_ext_iff, Rep.indResHomEquiv_symm_apply_hom, hom_ext_iff, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, mk_surjective
ker 📖	CompOp	13 math math: groupHomology.coinfNatTrans_app, groupHomology.chains₁ToCoinvariantsKer_surjective, le_comap_ker, sub_mem_ker, Representation.FiniteCyclicGroup.coinvariantsKer_eq_range, groupHomology.range_d₁₀_eq_coinvariantsKer, Rep.coinvariantsShortComplex_f, mk_eq_zero, Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker, mk_eq_iff, mem_ker_of_eq, groupHomology.coinvariantsKerOfIsBoundary₀_coe, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
map 📖	CompOp	8 math math: map_comp_mk, map_mk, map_id, groupHomology.map_id_comp_H0Iso_hom_apply, Rep.indMap_hom, Representation.ind_apply, map_comp, Rep.coinvariantsFunctor_map_hom
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	LinearMap.comp Representation.Coinvariants CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—	RingHomCompTriple.ids Submodule.linearMap_qext
hom_ext_iff 📖	mathematical	—	LinearMap.comp Representation.Coinvariants CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomCompTriple.ids hom_ext
induction_on 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike	—	—	Submodule.Quotient.induction_on
le_comap_ker 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder ker Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Subgroup.subtype Submodule.comap DFunLike.coe Representation MonoidHom.instFunLike	—	Submodule.span_le map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass mem_ker_of_eq Subgroup.Normal.conj_mem map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Representation.inv_self_apply
lift_comp_mk 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	Representation.Coinvariants instAddCommGroup instModule lift	—	RingHomCompTriple.ids
lift_mk 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	Representation.Coinvariants instAddCommGroup instModule LinearMap.instFunLike lift	—	RingHomCompTriple.ids
map_comp 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	Representation.Coinvariants instAddCommGroup instModule map	—	RingHomCompTriple.ids hom_ext
map_comp_mk 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	Representation.Coinvariants instAddCommGroup instModule map	—	RingHomCompTriple.ids
map_id 📖	mathematical	—	map LinearMap.id CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Representation.Coinvariants instAddCommGroup instModule	—	hom_ext LinearMap.ext RingHomCompTriple.ids
map_mk 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	Representation.Coinvariants instAddCommGroup instModule LinearMap.instFunLike map	—	RingHomCompTriple.ids
mem_ker_of_eq 📖	mathematical	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	Submodule SetLike.instMembership Submodule.setLike ker	—	Submodule.subset_span
mk_eq_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike Submodule SetLike.instMembership Submodule.setLike ker SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Submodule.Quotient.eq
mk_eq_zero 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule SetLike.instMembership Submodule.setLike ker	—	Submodule.Quotient.mk_eq_zero
mk_inv_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct AddCommGroup.toAddCommMonoid Representation.Coinvariants DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup TensorProduct.instModule Representation.tprod instAddCommGroup instModule LinearMap.instFunLike TensorProduct.tmul Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mk_eq_iff mem_ker_of_eq Representation.inv_self_apply
mk_self_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	mk_eq_iff mem_ker_of_eq
mk_surjective 📖	mathematical	—	Representation.Coinvariants DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike	—	Submodule.Quotient.mk_surjective
mk_tmul_inv 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct AddCommGroup.toAddCommMonoid Representation.Coinvariants DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup TensorProduct.instModule Representation.tprod instAddCommGroup instModule LinearMap.instFunLike TensorProduct.tmul Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mk_eq_iff mem_ker_of_eq Representation.inv_self_apply
sub_mem_ker 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike ker SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	Submodule.subset_span Set.mem_range_self

---

← Back to Index