Basic

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

Statistics

Metric	Count
Definitions groupCohomology, cocycles, cocyclesMk, iCocycles, inhomogeneousCochains, inhomogeneousCochainsIso, toCocycles, π, groupCohomologyIso, groupCohomologyIsoExt, d	11
Theorems iCocycles_mk, d_comp_d, d_def, ext, ext_iff, groupCohomology_induction_on, d_eq, d_hom_apply, isZero_groupCohomology_succ_of_subsingleton	9
Total	20

(root)

Definitions

Name	Category	Theorems
groupCohomology 📖	CompOp	46 math math: groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, groupCohomology.δ_apply, groupCohomology.H1π_comp_map_assoc, groupCohomology.π_comp_H0Iso_hom, groupCohomology.π_comp_H1Iso_hom_assoc, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.H2π_comp_map_apply, groupCohomology.π_map_assoc, groupCohomology.map_comp, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, groupCohomology.δ₁_apply, groupCohomology.map_H0Iso_hom_f, groupCohomology.π_comp_H1Iso_hom, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupCohomology.H1InfRes_X₂, groupCohomology.map₁_one, groupCohomology.map_id, groupCohomology.H2π_comp_map, groupCohomology.mono_map_0_of_mono, groupCohomology.π_comp_H0Iso_hom_apply, groupCohomology.H1InfRes_X₃, groupCohomology.functor_obj, groupCohomology.π_comp_H0Iso_hom_assoc, groupCohomology.π_map, groupCohomology.H2π_comp_map_assoc, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.map_id_comp_H0Iso_hom, isZero_groupCohomology_succ_of_subsingleton, groupCohomology.map_id_comp_assoc, groupCohomology.H1InfRes_X₁, groupCohomology.H1π_comp_map_apply, groupCohomology.π_comp_H2Iso_hom_assoc, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupCohomology.map_id_comp, groupCohomology.δ₀_apply, groupCohomology.H1Map_id, groupCohomology.π_comp_H2Iso_hom_apply, groupCohomology.π_comp_H1Iso_hom_apply, groupCohomology.π_map_apply, groupCohomology.H1π_comp_map, groupCohomology.map_H0Iso_hom_f_assoc, groupCohomology.map_id_comp_H0Iso_hom_assoc, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, groupCohomology.π_comp_H2Iso_hom, groupCohomology.map_comp_assoc
groupCohomologyIso 📖	CompOp	—
groupCohomologyIsoExt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
groupCohomology_induction_on 📖	—	DFunLike.coe groupCohomology.cocycles groupCohomology ModuleCat.carrier CommRing.toRing CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupCohomology.π	—	—	ModuleCat.epi_iff_surjective HomologicalComplex.instEpiHomologyπ
isZero_groupCohomology_succ_of_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero ModuleCat CommRing.toRing ModuleCat.moduleCategory groupCohomology	—	CategoryTheory.Limits.IsZero.of_iso Rep.instEnoughProjectives isZero_Ext_succ_of_projective Rep.trivial_projective_of_subsingleton

groupCohomology

Definitions

Name	Category	Theorems
cocycles 📖	CompOp	58 math math: toCocycles_comp_isoCocycles₁_hom, isoCocycles₁_hom_comp_i_apply, π_comp_H0IsoOfIsTrivial_hom_assoc, δ_apply, cocyclesMap_id_comp_assoc, toCocycles_comp_isoCocycles₂_hom_apply, cocyclesIso₀_hom_comp_f, π_comp_H0Iso_hom, π_comp_H1Iso_hom_assoc, cocyclesMap_comp_isoCocycles₂_hom_apply, cocyclesMap_cocyclesIso₀_hom_f_apply, cocyclesIso₀_inv_comp_iCocycles, π_map_assoc, toCocycles_comp_isoCocycles₂_hom, π_comp_H0IsoOfIsTrivial_hom, π_comp_H1Iso_hom, cocyclesMap_comp_isoCocycles₁_hom_assoc, isoCocycles₂_hom_comp_i, π_comp_H0Iso_hom_apply, isoCocycles₁_inv_comp_iCocycles_apply, cocyclesMap_comp_isoCocycles₁_hom, cocyclesIso₀_inv_comp_iCocycles_assoc, cocyclesMap_comp, π_comp_H0Iso_hom_assoc, π_map, π_comp_H0IsoOfIsTrivial_hom_apply, toCocycles_comp_isoCocycles₁_hom_assoc, isoCocycles₂_inv_comp_iCocycles_apply, cocyclesMap_cocyclesIso₀_hom_f_assoc, isoCocycles₁_inv_comp_iCocycles, cocyclesMap_comp_isoCocycles₂_hom, cocyclesIso₀_hom_comp_f_assoc, cocyclesMap_comp_isoCocycles₁_hom_apply, cocyclesMk₁_eq, cocyclesMap_cocyclesIso₀_hom_f, π_comp_H2Iso_hom_assoc, toCocycles_comp_isoCocycles₂_hom_assoc, cocyclesMap_comp_assoc, cocyclesMap_comp_isoCocycles₂_hom_assoc, isoCocycles₂_inv_comp_iCocycles, cocyclesMk₂_eq, toCocycles_comp_isoCocycles₁_hom_apply, isoCocycles₁_hom_comp_i, π_comp_H2Iso_hom_apply, π_comp_H1Iso_hom_apply, cocyclesMap_id, cocyclesIso₀_hom_comp_f_apply, iCocycles_mk, π_map_apply, cocyclesMap_id_comp, isoCocycles₁_inv_comp_iCocycles_assoc, isoCocycles₂_hom_comp_i_apply, cocyclesIso₀_inv_comp_iCocycles_apply, cocyclesMk₀_eq, isoCocycles₂_hom_comp_i_assoc, isoCocycles₁_hom_comp_i_assoc, π_comp_H2Iso_hom, isoCocycles₂_inv_comp_iCocycles_assoc
cocyclesMk 📖	CompOp	5 math math: δ_apply, cocyclesMk₁_eq, cocyclesMk₂_eq, iCocycles_mk, cocyclesMk₀_eq
iCocycles 📖	CompOp	23 math math: isoCocycles₁_hom_comp_i_apply, π_comp_H0IsoOfIsTrivial_hom_assoc, cocyclesIso₀_hom_comp_f, cocyclesMap_cocyclesIso₀_hom_f_apply, cocyclesIso₀_inv_comp_iCocycles, π_comp_H0IsoOfIsTrivial_hom, isoCocycles₂_hom_comp_i, isoCocycles₁_inv_comp_iCocycles_apply, cocyclesIso₀_inv_comp_iCocycles_assoc, π_comp_H0IsoOfIsTrivial_hom_apply, isoCocycles₂_inv_comp_iCocycles_apply, isoCocycles₁_inv_comp_iCocycles, cocyclesIso₀_hom_comp_f_assoc, isoCocycles₂_inv_comp_iCocycles, isoCocycles₁_hom_comp_i, cocyclesIso₀_hom_comp_f_apply, iCocycles_mk, isoCocycles₁_inv_comp_iCocycles_assoc, isoCocycles₂_hom_comp_i_apply, cocyclesIso₀_inv_comp_iCocycles_apply, isoCocycles₂_hom_comp_i_assoc, isoCocycles₁_hom_comp_i_assoc, isoCocycles₂_inv_comp_iCocycles_assoc
inhomogeneousCochains 📖	CompOp	69 math math: toCocycles_comp_isoCocycles₁_hom, inhomogeneousCochains.d_def, π_comp_H0IsoOfIsTrivial_hom_assoc, cocyclesIso₀_hom_comp_f, eq_d₀₁_comp_inv, eq_d₁₂_comp_inv, cochainsMap_f_3_comp_cochainsIso₃_assoc, cochainsMap_f_2_comp_cochainsIso₂, cochainsMap_comp, comp_d₁₂_eq, dArrowIso₀₁_inv_right, eq_d₂₃_comp_inv_assoc, eq_d₂₃_comp_inv_apply, eq_d₁₂_comp_inv_apply, cochainsMap_f_1_comp_cochainsIso₁_apply, cochainsMap_f_3_comp_cochainsIso₃_apply, cocyclesIso₀_inv_comp_iCocycles, dArrowIso₀₁_hom_right, toCocycles_comp_isoCocycles₂_hom, cochainsMap_f_1_comp_cochainsIso₁_assoc, comp_d₂₃_eq, π_comp_H0IsoOfIsTrivial_hom, cochainsMap_f_map_epi, comp_d₀₁_eq, cochainsMap_zero, dArrowIso₀₁_inv_left, cochainsMap_id_comp, cochainsMap_comp_assoc, isoCocycles₂_hom_comp_i, dArrowIso₀₁_hom_left, eq_d₀₁_comp_inv_apply, cocyclesIso₀_inv_comp_iCocycles_assoc, cochainsMap_id_f_map_mono, toCocycles_comp_isoCocycles₁_hom_assoc, isoCocycles₁_inv_comp_iCocycles, cochainsMap_f_0_comp_cochainsIso₀_apply, cochainsMap_f_2_comp_cochainsIso₂_apply, cocyclesIso₀_hom_comp_f_assoc, cochainsMap_f, cocyclesMk₁_eq, toCocycles_comp_isoCocycles₂_hom_assoc, eq_d₂₃_comp_inv, cochainsMap_f_map_mono, isoShortComplexH1_hom, isoCocycles₂_inv_comp_iCocycles, cocyclesMk₂_eq, cochainsMap_id_f_map_epi, isoCocycles₁_hom_comp_i, cochainsMap_f_0_comp_cochainsIso₀, cochainsMap_f_3_comp_cochainsIso₃, cochainsMap_f_hom, isoShortComplexH2_hom, iCocycles_mk, isoCocycles₁_inv_comp_iCocycles_assoc, cochainsMap_f_2_comp_cochainsIso₂_assoc, cocyclesMk₀_eq, isoShortComplexH1_inv, cochainsMap_id_f_hom_eq_compLeft, cochainsMap_f_1_comp_cochainsIso₁, cochainsMap_id_comp_assoc, cochainsMap_f_0_comp_cochainsIso₀_assoc, eq_d₁₂_comp_inv_assoc, isoShortComplexH2_inv, isoCocycles₂_hom_comp_i_assoc, eq_d₀₁_comp_inv_assoc, isoCocycles₁_hom_comp_i_assoc, cochainsFunctor_obj, isoCocycles₂_inv_comp_iCocycles_assoc, cochainsMap_id
inhomogeneousCochainsIso 📖	CompOp	—
toCocycles 📖	CompOp	6 math math: toCocycles_comp_isoCocycles₁_hom, toCocycles_comp_isoCocycles₂_hom_apply, toCocycles_comp_isoCocycles₂_hom, toCocycles_comp_isoCocycles₁_hom_assoc, toCocycles_comp_isoCocycles₂_hom_assoc, toCocycles_comp_isoCocycles₁_hom_apply
π 📖	CompOp	15 math math: π_comp_H0IsoOfIsTrivial_hom_assoc, δ_apply, π_comp_H0Iso_hom, π_comp_H1Iso_hom_assoc, π_map_assoc, π_comp_H0IsoOfIsTrivial_hom, π_comp_H1Iso_hom, π_comp_H0Iso_hom_apply, π_comp_H0Iso_hom_assoc, π_map, π_comp_H2Iso_hom_assoc, π_comp_H2Iso_hom_apply, π_comp_H1Iso_hom_apply, π_map_apply, π_comp_H2Iso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iCocycles_mk 📖	mathematical	DFunLike.coe ModuleCat.of CommRing.toRing Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier inhomogeneousCochains.d Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	cocycles HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles cocyclesMk	—	HomologicalComplex.i_cyclesMk ModuleCat.forget₂_addCommGrp_additive CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits ModuleCat.forget₂AddCommGroup_preservesLimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.next DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass CochainComplex.of_d

groupCohomology.inhomogeneousCochains

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_comp_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule inhomogeneousCochains.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id HomologicalComplex.d_comp_d
d_def 📖	mathematical	—	HomologicalComplex.d ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne groupCohomology.inhomogeneousCochains inhomogeneousCochains.d DivInvMonoid.toMonoid Group.toDivInvMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.of_d
ext 📖	—	—	—	—	AddRightCancelSemigroup.toIsRightCancelAdd
ext_iff 📖	—	—	—	—	AddRightCancelSemigroup.toIsRightCancelAdd ext

inhomogeneousCochains

Definitions

Name	Category	Theorems
d 📖	CompOp	4 math math: groupCohomology.inhomogeneousCochains.d_def, groupCohomology.inhomogeneousCochains.d_comp_d, d_hom_apply, d_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_eq 📖	mathematical	—	d DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver Action.instCategory Rep.free CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep CategoryTheory.Iso.inv LinearEquiv.toModuleIso Rep.freeLiftLEquiv HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ChainComplex.linearYonedaObj Action.instAbelian ModuleCat.abelian Rep.barComplex HomologicalComplex.d CategoryTheory.Iso.hom	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext RingHomCompTriple.ids Rep.barComplex.d_def Rep.barComplex.d_single map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.uncurry_single map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Finset.sum_congr LinearMap.semilinearMapClass Finsupp.linearCombination_single one_smul map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
d_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of d AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ Finset.sum Finset.univ Fin.fintype SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Monoid.toNatPow NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Fin.contractNth MulOne.toMul	—	—

---

← Back to Index