FiniteCyclic

📁 Source: Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.lean

Statistics

Metric	Count
Definitions coinvariantsTensorResolutionIso, groupHomologyIsoEven, groupHomologyIsoOdd, groupHomologyIso₀, groupHomologyπEven, groupHomologyπOdd	6
Theorems coinvariantsTensorResolutionIso_hom_f_hom_apply, coinvariantsTensorResolutionIso_inv_f_hom_apply, groupHomologyπEven_eq_iff, groupHomologyπEven_eq_zero_iff, groupHomologyπOdd_eq_iff, groupHomologyπOdd_eq_zero_iff	6
Total	12

Rep.FiniteCyclicGroup

Definitions

Name	Category	Theorems
coinvariantsTensorResolutionIso 📖	CompOp	2 math math: coinvariantsTensorResolutionIso_inv_f_hom_apply, coinvariantsTensorResolutionIso_hom_f_hom_apply
groupHomologyIsoEven 📖	CompOp	—
groupHomologyIsoOdd 📖	CompOp	—
groupHomologyIso₀ 📖	CompOp	—
groupHomologyπEven 📖	CompOp	2 math math: groupHomologyπEven_eq_iff, groupHomologyπEven_eq_zero_iff
groupHomologyπOdd 📖	CompOp	2 math math: groupHomologyπOdd_eq_zero_iff, groupHomologyπOdd_eq_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinvariantsTensorResolutionIso_hom_f_hom_apply 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants TensorProduct CommRing.toCommSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ModuleCat.isModule Finsupp.module Semiring.toModule TensorProduct.addCommGroup TensorProduct.instModule Representation.tprod Rep.ρ Representation.leftRegular Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule LinearMap.instFunLike ModuleCat.Hom.hom HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.coinvariantsTensorObj CategoryTheory.ProjectiveResolution.complex Rep Action.instCategory Action.instHasZeroMorphisms Rep.trivial Ring.toAddCommGroup resolution InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid moduleCatChainComplex HomologicalComplex.Hom.f CategoryTheory.Iso.hom ChainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject Action.instAbelian ModuleCat.abelian Group.toDivisionMonoid Subgroup.zpowers_inv coinvariantsTensorResolutionIso AddMonoidHom HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup Submodule.toAddSubgroup Representation.Coinvariants.ker AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike QuotientAddGroup.lift LinearMap.toAddMonoidHom LinearMap.comp TensorProduct.addCommMonoid TensorProduct.lift Finsupp.linearCombination LinearMap.addCommMonoid LinearMap.module Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearEquiv.toLinearMap TensorProduct.comm	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject Subgroup.zpowers_inv
coinvariantsTensorResolutionIso_inv_f_hom_apply 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Representation.Coinvariants TensorProduct CommRing.toCommSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ModuleCat.isModule Finsupp.module Semiring.toModule TensorProduct.addCommGroup TensorProduct.instModule Representation.tprod Rep.ρ Representation.leftRegular Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule LinearMap.instFunLike ModuleCat.Hom.hom HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne moduleCatChainComplex HomologicalComplex.coinvariantsTensorObj CategoryTheory.ProjectiveResolution.complex Rep Action.instCategory Action.instHasZeroMorphisms Rep.trivial Ring.toAddCommGroup resolution InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid HomologicalComplex.Hom.f CategoryTheory.Iso.inv ChainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject Action.instAbelian ModuleCat.abelian Group.toDivisionMonoid Subgroup.zpowers_inv coinvariantsTensorResolutionIso LinearMap.inverse LinearEquiv.toLinearMap Representation.coinvariantsTprodLeftRegularLEquiv LinearEquiv EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm LinearEquiv.left_inv LinearEquiv.right_inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject Subgroup.zpowers_inv
groupHomologyπEven_eq_iff 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Even	DFunLike.coe ModuleCat.of CommRing.toRing ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Representation.norm Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module groupHomology CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupHomologyπEven CommMonoid.toMonoid CommGroup.toCommMonoid LinearMap.range RingHomSurjective.ids ModuleCat.Hom.hom Action.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory Action.instSubHom ModuleCat.instPreadditive Rep.applyAsHom CategoryTheory.CategoryStruct.id SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	RingHomSurjective.ids sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass groupHomologyπEven_eq_zero_iff Submodule.addSubgroupClass AddSubgroupClass.coe_sub
groupHomologyπEven_eq_zero_iff 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Even	DFunLike.coe ModuleCat.of CommRing.toRing ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Representation.norm Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module groupHomology CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupHomologyπEven NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CommMonoid.toMonoid CommGroup.toCommMonoid LinearMap.range RingHomSurjective.ids ModuleCat.Hom.hom Action.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory Action.instSubHom ModuleCat.instPreadditive Rep.applyAsHom CategoryTheory.CategoryStruct.id	—	RingHomSurjective.ids CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.moduleCat_zero_apply RingHomCompTriple.ids CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc map_eq_zero_iff ModuleCat.mono_iff_injective AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv LinearMap.range_codRestrict
groupHomologyπOdd_eq_iff 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Odd Nat.instSemiring	DFunLike.coe ModuleCat.of CommRing.toRing ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory CommMonoid.toMonoid CommGroup.toCommMonoid Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom Action.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instSubHom ModuleCat.instPreadditive Rep.applyAsHom CategoryTheory.CategoryStruct.id Submodule.addCommGroup Submodule.module groupHomology CategoryTheory.ConcreteCategory.hom LinearMap LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupHomologyπOdd CommSemiring.toSemiring CommRing.toCommSemiring Rep.instAddCommGroupCarrierVModuleCat LinearMap.range RingHomSurjective.ids Representation.norm Rep.ρ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	RingHomSurjective.ids sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass groupHomologyπOdd_eq_zero_iff Submodule.addSubgroupClass AddSubgroupClass.coe_sub
groupHomologyπOdd_eq_zero_iff 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Odd Nat.instSemiring	DFunLike.coe ModuleCat.of CommRing.toRing ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory CommMonoid.toMonoid CommGroup.toCommMonoid Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom Action.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instSubHom ModuleCat.instPreadditive Rep.applyAsHom CategoryTheory.CategoryStruct.id Submodule.addCommGroup Submodule.module groupHomology CategoryTheory.ConcreteCategory.hom LinearMap LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupHomologyπOdd NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CommSemiring.toSemiring CommRing.toCommSemiring Rep.instAddCommGroupCarrierVModuleCat LinearMap.range RingHomSurjective.ids Representation.norm Rep.ρ	—	RingHomSurjective.ids CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.moduleCat_zero_apply RingHomCompTriple.ids CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc map_eq_zero_iff ModuleCat.mono_iff_injective AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv LinearMap.range_codRestrict

---

← Back to Index