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, toCoinvariantsMkQ	30
Theorems coinvariantsAdjunction_counit_app, coinvariantsAdjunction_homEquiv_apply_hom, coinvariantsAdjunction_homEquiv_symm_apply_hom, coinvariantsAdjunction_unit_app, 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, coinvariantsTensorFreeToFinsupp_mk_tmul_single, coinvariantsTensorMk_apply, coinvariantsTensor_hom_ext, coinvariantsTensor_hom_ext_iff, finsuppToCoinvariantsTensorFree_single, instAdditiveModuleCatCoinvariantsFunctor, instAdditiveModuleCatObjFunctorCoinvariantsTensor, instEpiModuleCatAppCoinvariantsMk, instIsLeftAdjointModuleCatCoinvariantsFunctor, instLinearModuleCatCoinvariantsFunctor, instLinearModuleCatObjFunctorCoinvariantsTensor, instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, quotientToCoinvariantsFunctor_map_hom_toLinearMap, quotientToCoinvariantsFunctor_obj_V, 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	57
Total	87

Rep

Definitions

Name	Category	Theorems
coinvariantsAdjunction 📖	CompOp	4 math math: coinvariantsAdjunction_counit_app, coinvariantsAdjunction_homEquiv_symm_apply_hom, coinvariantsAdjunction_unit_app, coinvariantsAdjunction_homEquiv_apply_hom
coinvariantsFunctor 📖	CompOp	35 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, instEpiModuleCatAppCoinvariantsMk, 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, groupHomology.d₁₀_comp_coinvariantsMk, instIsLeftAdjointModuleCatCoinvariantsFunctor, groupHomology.map_id_comp_H0Iso_hom_assoc, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, coinvariantsAdjunction_unit_app, 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, 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	22 math math: groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, groupHomology.π_comp_H0Iso_hom_assoc, instEpiModuleCatAppCoinvariantsMk, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupHomology.coinvariantsMk_comp_H0Iso_inv, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coinvariantsFunctor_hom_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, coinvariantsAdjunction_unit_app, 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, groupHomology.d₁₀_comp_coinvariantsMk_assoc, groupHomology.H0π_comp_H0Iso_hom_assoc, coinvariantsAdjunction_homEquiv_apply_hom, groupHomology.H0π_comp_H0Iso_hom_apply, 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	1 math math: 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	1 math math: finsuppToCoinvariantsTensorFree_single
quotientToCoinvariants 📖	CompOp	2 math math: groupHomology.H1CoresCoinf_X₃, groupHomology.H1CoresCoinf_g
quotientToCoinvariantsFunctor 📖	CompOp	3 math math: groupHomology.coinfNatTrans_app, quotientToCoinvariantsFunctor_map_hom_toLinearMap, quotientToCoinvariantsFunctor_obj_V
toCoinvariants 📖	CompOp	2 math math: quotientToCoinvariantsFunctor_map_hom_toLinearMap, coinvariantsShortComplex_X₃
toCoinvariantsKer 📖	CompOp	1 math math: coinvariantsShortComplex_X₁
toCoinvariantsMkQ 📖	CompOp	3 math math: groupHomology.coinfNatTrans_app, groupHomology.H1CoresCoinf_g, coinvariantsShortComplex_g

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinvariantsAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.comp Rep CommSemiring.toSemiring CommRing.toCommSemiring 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	—	Representation.IntertwiningMap.toLinearMap V CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.obj ModuleCat CommRing.toRing ModuleCat.moduleCategory Rep instCategory trivialFunctor AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct coinvariantsFunctor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv coinvariantsAdjunction ModuleCat.Hom.hom CategoryTheory.forget₂ Representation.IntertwiningMap Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app coinvariantsMk	—	—
coinvariantsAdjunction_homEquiv_symm_apply_hom 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj ModuleCat CommRing.toRing ModuleCat.moduleCategory trivialFunctor coinvariantsFunctor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv coinvariantsAdjunction desc Ring.toSemiring instIsTrivialObjModuleCatTrivialFunctor	—	coinvariantsFunctor_hom_ext instIsTrivialObjModuleCatTrivialFunctor ModuleCat.hom_ext LinearMap.ext
coinvariantsAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp ModuleCat CommRing.toRing ModuleCat.moduleCategory coinvariantsFunctor trivialFunctor CategoryTheory.Adjunction.unit coinvariantsAdjunction ofHom V ModuleCat.carrier CategoryTheory.Functor.obj hV1 ModuleCat.isAddCommGroup hV2 ModuleCat.isModule ρ Representation.trivial Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.Hom.hom CategoryTheory.forget₂ Representation.IntertwiningMap Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat coinvariantsMk	—	—
coinvariantsFunctor_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat coinvariantsFunctor CategoryTheory.NatTrans.app coinvariantsMk	—	—	CategoryTheory.cancel_epi instEpiModuleCatAppCoinvariantsMk
coinvariantsFunctor_hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat coinvariantsFunctor CategoryTheory.NatTrans.app coinvariantsMk	—	coinvariantsFunctor_hom_ext
coinvariantsFunctor_map_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of Representation.Coinvariants V CommSemiring.toSemiring CommRing.toCommSemiring hV1 hV2 ρ Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule CategoryTheory.Functor.map Rep instCategory ModuleCat ModuleCat.moduleCategory coinvariantsFunctor Representation.Coinvariants.map Representation.IntertwiningMap.toLinearMap AddCommGroup.toAddCommMonoid Hom.hom	—	—
coinvariantsFunctor_obj_carrier 📖	mathematical	—	ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory ModuleCat ModuleCat.moduleCategory coinvariantsFunctor Representation.Coinvariants V hV1 hV2 ρ	—	—
coinvariantsMk_app_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of V Ring.toSemiring hV1 hV2 Representation.Coinvariants CommSemiring.toSemiring CommRing.toCommSemiring ρ Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule CategoryTheory.NatTrans.app Rep instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat coinvariantsFunctor coinvariantsMk	—	—
coinvariantsShortComplex_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive coinvariantsShortComplex toCoinvariantsKer	—	—
coinvariantsShortComplex_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive coinvariantsShortComplex	—	—
coinvariantsShortComplex_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive coinvariantsShortComplex toCoinvariants	—	—
coinvariantsShortComplex_f 📖	mathematical	—	CategoryTheory.ShortComplex.f Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive coinvariantsShortComplex ofHom V Submodule AddCommGroup.toAddCommMonoid hV1 hV2 SetLike.instMembership Submodule.setLike Representation.Coinvariants.ker Subgroup Subgroup.instSetLike Subgroup.toGroup MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ Subgroup.subtype Submodule.addCommGroup CommRing.toRing Submodule.module Representation.toCoinvariantsKer Submodule.subtype	—	—
coinvariantsShortComplex_g 📖	mathematical	—	CategoryTheory.ShortComplex.g Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive coinvariantsShortComplex toCoinvariantsMkQ	—	—
coinvariantsShortComplex_shortExact 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive coinvariantsShortComplex	—	CategoryTheory.Functor.reflects_exact_of_faithful CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier 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 V DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instZero AddCommGroup.toAddCommMonoid hV1 Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid hV2 Finsupp.module Semiring.toModule TensorProduct.addCommGroup 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 instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory free LinearMap.instFunLike coinvariantsTensorFreeToFinsupp	—	—
coinvariantsTensorFreeToFinsupp_mk_tmul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants TensorProduct V DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instZero AddCommGroup.toAddCommMonoid hV1 Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid hV2 Finsupp.module Semiring.toModule TensorProduct.addCommGroup 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	—	RingHomInvPair.ids RingHomCompTriple.ids TensorProduct.finsuppRight_tmul_single 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 V ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj Rep instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor AddCommGroup.toAddCommMonoid hV1 ModuleCat.isAddCommGroup hV2 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 instMonoidalCategory ρ Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule TensorProduct.tmul	—	smulCommClass_self
coinvariantsTensor_hom_ext 📖	—	LinearMap.compr₂ CommRing.toCommSemiring CommSemiring.toSemiring V ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj Rep instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor AddCommGroup.toAddCommMonoid hV1 ModuleCat.isAddCommGroup hV2 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 V ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj Rep instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor AddCommGroup.toAddCommMonoid hV1 ModuleCat.isAddCommGroup hV2 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 V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid hV1 Representation.Coinvariants TensorProduct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instZero AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid hV2 Finsupp.module Semiring.toModule TensorProduct.addCommGroup 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 CommRing.toRing	—	RingHomInvPair.ids 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 CommSemiring.toSemiring CommRing.toCommSemiring ModuleCat CommRing.toRing instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive coinvariantsFunctor	—	coinvariantsFunctor_hom_ext ModuleCat.hom_ext LinearMap.ext RingHomCompTriple.ids CategoryTheory.Preadditive.comp_add
instAdditiveModuleCatObjFunctorCoinvariantsTensor 📖	mathematical	—	CategoryTheory.Functor.Additive Rep CommSemiring.toSemiring CommRing.toCommSemiring ModuleCat CommRing.toRing instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor	—	CategoryTheory.MonoidalPreadditive.whiskerLeft_add instMonoidalPreadditive CategoryTheory.Functor.map_add instAdditiveModuleCatCoinvariantsFunctor
instEpiModuleCatAppCoinvariantsMk 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat coinvariantsFunctor CategoryTheory.NatTrans.app coinvariantsMk	—	ModuleCat.epi_iff_surjective Representation.Coinvariants.mk_surjective
instIsLeftAdjointModuleCatCoinvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory coinvariantsFunctor	—	CategoryTheory.Adjunction.isLeftAdjoint
instLinearModuleCatCoinvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Rep ModuleCat CommRing.toRing instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive instLinear ModuleCat.instLinear coinvariantsFunctor	—	coinvariantsFunctor_hom_ext ModuleCat.hom_ext LinearMap.ext RingHomCompTriple.ids ModuleCat.Algebra.instSMulCommClassCarrier CategoryTheory.Linear.comp_smul
instLinearModuleCatObjFunctorCoinvariantsTensor 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Rep ModuleCat CommRing.toRing instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive instLinear ModuleCat.instLinear CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor	—	CategoryTheory.MonoidalLinear.whiskerLeft_smul instMonoidalPreadditive instMonoidalLinear CategoryTheory.Functor.map_smul instLinearModuleCatCoinvariantsFunctor
instPreservesZeroMorphismsModuleCatCoinvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive ModuleCat.instPreadditive coinvariantsFunctor	—	CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveModuleCatCoinvariantsFunctor
quotientToCoinvariantsFunctor_map_hom_toLinearMap 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid toCoinvariants QuotientGroup.Quotient.group AddCommGroup.toAddCommMonoid hV1 hV2 Representation.ofQuotient ρ Hom.hom of CategoryTheory.Functor.map Rep instCategory quotientToCoinvariantsFunctor Representation.Coinvariants.map SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Subgroup.subtype ofHom	—	—
quotientToCoinvariantsFunctor_obj_V 📖	mathematical	—	V HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group CategoryTheory.Functor.obj Rep instCategory quotientToCoinvariantsFunctor Representation.Coinvariants SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup hV1 hV2 MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid 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, 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, Rep.quotientToCoinvariantsFunctor_obj_V, 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	1 math math: Rep.coinvariantsShortComplex_f
toCoinvariantsMkQ 📖	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	43 math math: Rep.coindToInd_of_support_subset_orbit, mk_inv_tmul, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, Rep.coindToInd_indToCoind, Rep.finsuppToCoinvariantsTensorFree_single, mk_tmul_inv, map_comp_mk, lift_mk, Representation.coinvariantsFinsuppLEquiv_apply, Representation.coinvariantsTprodLeftRegularLEquiv_apply, mk_self_apply, lift_comp_mk, Rep.coinvariantsTensorFreeLEquiv_apply, Rep.coindToInd_apply, Representation.finsuppToCoinvariants_single_mk, map_mk, Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, mk_eq_zero, Rep.coinvariantsMk_app_hom, map_id, Rep.indCoindIso_hom_hom_toLinearMap, mk_eq_iff, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, Rep.indCoindIso_inv_hom_toLinearMap, Representation.toCoinvariants_mk, Rep.coinvariantsTensorMk_apply, Representation.coinvariantsToFinsupp_mk_single, Representation.ind_mk, Representation.coinvariantsFinsuppLEquiv_symm_apply, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.indToCoind_coindToInd, Rep.indResHomEquiv_symm_apply, 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, hom_ext_iff, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, mk_surjective
instModule 📖	CompOp	43 math math: Rep.coindToInd_of_support_subset_orbit, mk_inv_tmul, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, Rep.coindToInd_indToCoind, Rep.finsuppToCoinvariantsTensorFree_single, mk_tmul_inv, map_comp_mk, lift_mk, Representation.coinvariantsFinsuppLEquiv_apply, Representation.coinvariantsTprodLeftRegularLEquiv_apply, mk_self_apply, lift_comp_mk, Rep.coinvariantsTensorFreeLEquiv_apply, Rep.coindToInd_apply, Representation.finsuppToCoinvariants_single_mk, map_mk, Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, mk_eq_zero, Rep.coinvariantsMk_app_hom, map_id, Rep.indCoindIso_hom_hom_toLinearMap, mk_eq_iff, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, Rep.indCoindIso_inv_hom_toLinearMap, Representation.toCoinvariants_mk, Rep.coinvariantsTensorMk_apply, Representation.coinvariantsToFinsupp_mk_single, Representation.ind_mk, Representation.coinvariantsFinsuppLEquiv_symm_apply, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.indToCoind_coindToInd, Rep.indResHomEquiv_symm_apply, 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, hom_ext_iff, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, mk_surjective
ker 📖	CompOp	12 math math: 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.quotientToCoinvariantsFunctor_map_hom_toLinearMap, 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	LinearMap.comp Representation.Coinvariants CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids 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	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants AddCommGroup.toAddCommMonoid 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	LinearMap.comp Representation.Coinvariants CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids 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	LinearMap.comp Representation.Coinvariants CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids 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	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants AddCommGroup.toAddCommMonoid 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 CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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