FiniteCyclic

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

Statistics

Metric	Count
Definitions groupCohomologyIsoEven, groupCohomologyIsoOdd, groupCohomologyIso₀, groupCohomologyπEven, groupCohomologyπOdd, homResolutionIso	6
Theorems groupCohomologyπEven_eq_iff, groupCohomologyπEven_eq_zero_iff, groupCohomologyπOdd_eq_iff, groupCohomologyπOdd_eq_zero_iff, homResolutionIso_hom_f_hom_apply, homResolutionIso_inv_f_hom_apply_hom_toFun	6
Total	12

Rep.FiniteCyclicGroup

Definitions

Name	Category	Theorems
groupCohomologyIsoEven 📖	CompOp	—
groupCohomologyIsoOdd 📖	CompOp	—
groupCohomologyIso₀ 📖	CompOp	—
groupCohomologyπEven 📖	CompOp	2 math math: groupCohomologyπEven_eq_zero_iff, groupCohomologyπEven_eq_iff
groupCohomologyπOdd 📖	CompOp	2 math math: groupCohomologyπOdd_eq_iff, groupCohomologyπOdd_eq_zero_iff
homResolutionIso 📖	CompOp	2 math math: homResolutionIso_inv_f_hom_apply_hom_toFun, homResolutionIso_hom_f_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
groupCohomologyπEven_eq_iff 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Even	DFunLike.coe ModuleCat.of CommRing.toRing Rep.V CommSemiring.toSemiring CommRing.toCommSemiring CommMonoid.toMonoid CommGroup.toCommMonoid Submodule AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Representation.IntertwiningMap.toLinearMap Rep.ρ Rep.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Rep.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id Submodule.addCommGroup Submodule.module groupCohomology ModuleCat.carrier CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupCohomologyπEven LinearMap.range RingHomSurjective.ids Rep.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	RingHomSurjective.ids sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass groupCohomologyπEven_eq_zero_iff
groupCohomologyπEven_eq_zero_iff 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Even	DFunLike.coe ModuleCat.of CommRing.toRing Rep.V CommSemiring.toSemiring CommRing.toCommSemiring CommMonoid.toMonoid CommGroup.toCommMonoid Submodule AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Representation.IntertwiningMap.toLinearMap Rep.ρ Rep.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Rep.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id Submodule.addCommGroup Submodule.module groupCohomology ModuleCat.carrier CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupCohomologyπEven NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LinearMap.range RingHomSurjective.ids Rep.norm	—	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
groupCohomologyπOdd_eq_iff 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Odd Nat.instSemiring	DFunLike.coe ModuleCat.of CommRing.toRing Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Submodule AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Representation.IntertwiningMap.toLinearMap Rep.ρ Rep.Hom.hom Rep.norm Submodule.addCommGroup Submodule.module groupCohomology ModuleCat.carrier CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupCohomologyπOdd CommMonoid.toMonoid CommGroup.toCommMonoid LinearMap.range RingHomSurjective.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	RingHomSurjective.ids sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass groupCohomologyπOdd_eq_zero_iff Submodule.addSubgroupClass AddSubgroupClass.coe_sub
groupCohomologyπOdd_eq_zero_iff 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Odd Nat.instSemiring	DFunLike.coe ModuleCat.of CommRing.toRing Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Submodule AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Representation.IntertwiningMap.toLinearMap Rep.ρ Rep.Hom.hom Rep.norm Submodule.addCommGroup Submodule.module groupCohomology ModuleCat.carrier CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupCohomologyπOdd NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CommMonoid.toMonoid CommGroup.toCommMonoid LinearMap.range RingHomSurjective.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.instSubHom 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
homResolutionIso_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 Quiver.Hom Rep DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.leftRegular Rep.V CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupHom Rep.hV1 Rep.instModuleHom Rep.hV2 LinearMap.instFunLike ModuleCat.Hom.hom HomologicalComplex.X ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne ChainComplex.linearYonedaObj Rep.instAbelian CategoryTheory.ProjectiveResolution.complex Rep.instPreadditive Rep.trivial Ring.toAddCommGroup Semiring.toModule resolution Rep.instLinear moduleCatCochainComplex HomologicalComplex.Hom.f CategoryTheory.Iso.hom CochainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd Rep.instHasZeroObject homResolutionIso Representation.IntertwiningMap Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Representation.leftRegular Rep.ρ Representation.IntertwiningMap.instFunLike Equiv Representation.ofMulAction Monoid.toMulAction EquivLike.toFunLike Equiv.instEquivLike Rep.homEquiv Finsupp.single MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	AddRightCancelSemigroup.toIsRightCancelAdd Rep.instHasZeroObject
homResolutionIso_inv_f_hom_apply_hom_toFun 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	DFunLike.coe Representation.IntertwiningMap Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Rep.leftRegular CommRing.toRing AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.Hom.hom Ring.toSemiring LinearMap RingHom.id Semiring.toNonAssocSemiring Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.instAddCommGroupHom Rep.instModuleHom LinearMap.instFunLike ModuleCat.Hom.hom HomologicalComplex.X ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne moduleCatCochainComplex ChainComplex.linearYonedaObj Rep.instAbelian CategoryTheory.ProjectiveResolution.complex Rep.instPreadditive Rep.trivial Ring.toAddCommGroup Semiring.toModule resolution Rep.instLinear HomologicalComplex.Hom.f CategoryTheory.Iso.inv CochainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd Rep.instHasZeroObject homResolutionIso Finsupp.sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	AddRightCancelSemigroup.toIsRightCancelAdd Rep.instHasZeroObject

---

← Back to Index