Documentation Verification Report

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` `Rep.V` `CommSemiring.toSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Rep.hV1` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Rep.hV2` `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` `ModuleCat` `ModuleCat.moduleCategory` `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` `Rep.instCategory` `Rep.instPreadditive` `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` `Rep.instHasZeroObject` `Subgroup` `Subgroup.zpowers` `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` `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` `Rep.instHasZeroObject` `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` `Rep.V` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Representation.Coinvariants` `TensorProduct` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Rep.hV1` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Rep.hV2` `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` `ModuleCat` `ModuleCat.moduleCategory` `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` `Rep.instCategory` `Rep.instPreadditive` `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` `Rep.instHasZeroObject` `Subgroup` `Subgroup.zpowers` `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` `Rep.instHasZeroObject` `Subgroup.zpowers_inv`
`groupHomologyπ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` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Submodule` `AddCommGroup.toAddCommMonoid` `Rep.hV1` `Rep.hV2` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Representation.norm` `Rep.ρ` `Submodule.addCommGroup` `Submodule.module` `groupHomology` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `groupHomologyπEven` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `LinearMap.range` `RingHomSurjective.ids` `Representation.IntertwiningMap.toLinearMap` `Rep.Hom.hom` `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` `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` `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.norm` `Rep.ρ` `Submodule.addCommGroup` `Submodule.module` `groupHomology` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `groupHomologyπEven` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `LinearMap.range` `RingHomSurjective.ids` `Representation.IntertwiningMap.toLinearMap` `Rep.Hom.hom` `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`
`groupHomologyπ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` `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` `groupHomology` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `groupHomologyπOdd` `LinearMap.range` `RingHomSurjective.ids` `Representation.norm` `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` `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` `groupHomology` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `groupHomologyπOdd` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LinearMap.range` `RingHomSurjective.ids` `Representation.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`

---

← Back to Index