Documentation Verification Report

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_hom_apply`	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_hom_f_hom_apply`, `homResolutionIso_inv_f_hom_apply_hom_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` `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` `groupCohomology` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `groupCohomologyπEven` `LinearMap.range` `RingHomSurjective.ids` `Rep.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Rep.instAddCommGroupCarrierVModuleCat`	—	`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` `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` `groupCohomology` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `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` `ModuleCat.carrier` `Action.V` `ModuleCat` `ModuleCat.moduleCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `Submodule.setLike` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.Hom.hom` `Action.Hom.hom` `Rep.norm` `Submodule.addCommGroup` `Submodule.module` `groupCohomology` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `groupCohomologyπOdd` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `LinearMap.range` `RingHomSurjective.ids` `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` `Rep.instAddCommGroupCarrierVModuleCat`	—	`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` `ModuleCat.carrier` `Action.V` `ModuleCat` `ModuleCat.moduleCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `Submodule.setLike` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.Hom.hom` `Action.Hom.hom` `Rep.norm` `Submodule.addCommGroup` `Submodule.module` `groupCohomology` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `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` `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`
`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` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Rep.leftRegular` `ModuleCat.carrier` `Action.V` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `Action.instPreadditive` `ModuleCat.instPreadditive` `ModuleCat.isAddCommGroup` `CategoryTheory.Linear.homModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instLinearRep` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.Hom.hom` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `ChainComplex.linearYonedaObj` `Action.instAbelian` `ModuleCat.abelian` `CategoryTheory.ProjectiveResolution.complex` `Action.instHasZeroMorphisms` `Rep.trivial` `Ring.toAddCommGroup` `Semiring.toModule` `resolution` `moduleCatCochainComplex` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `CochainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Abelian.hasZeroObject` `homResolutionIso` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommGroup` `Finsupp.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `CategoryTheory.ConcreteCategory.hom` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `ModuleCat.of` `Action.Hom.hom` `Finsupp.single` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Abelian.hasZeroObject`
`homResolutionIso_inv_f_hom_apply_hom_hom_apply` 📖	mathematical	`Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ModuleCat.carrier` `CommRing.toRing` `Action.V` `ModuleCat` `ModuleCat.moduleCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Finsupp.module` `Semiring.toModule` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.Hom.hom` `ModuleCat.of` `Finsupp.instAddCommGroup` `Ring.toAddCommGroup` `ModuleCat.isAddCommGroup` `Action.Hom.hom` `Rep.leftRegular` `Ring.toSemiring` `Quiver.Hom` `Rep` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Action.instCategory` `CategoryTheory.Preadditive.homGroup` `Action.instPreadditive` `ModuleCat.instPreadditive` `CategoryTheory.Linear.homModule` `instLinearRep` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `moduleCatCochainComplex` `ChainComplex.linearYonedaObj` `Action.instAbelian` `ModuleCat.abelian` `CategoryTheory.ProjectiveResolution.complex` `Action.instHasZeroMorphisms` `Rep.trivial` `resolution` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.inv` `CochainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Abelian.hasZeroObject` `homResolutionIso` `Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `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` `Rep.ρ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Abelian.hasZeroObject`

---

← Back to Index