Functoriality

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

Statistics

Metric	Count
Definitions H1InfRes, cochainsFunctor, cochainsMap, cochainsMap₁, cochainsMap₂, cochainsMap₃, cocyclesMap, functor, infNatTrans, map, mapCocycles₁, mapCocycles₂, mapShortComplexH1, mapShortComplexH2, resNatTrans	15
Theorems H1InfRes_X₁, H1InfRes_X₂, H1InfRes_X₃, H1InfRes_exact, H1InfRes_f, H1InfRes_g, H1Map_id, H1π_comp_map, H1π_comp_map_apply, H1π_comp_map_assoc, H2π_comp_map, H2π_comp_map_apply, H2π_comp_map_assoc, cochainsFunctor_map, cochainsFunctor_obj, cochainsMap_comp, cochainsMap_comp_assoc, cochainsMap_f, cochainsMap_f_0_comp_cochainsIso₀, cochainsMap_f_0_comp_cochainsIso₀_apply, cochainsMap_f_0_comp_cochainsIso₀_assoc, cochainsMap_f_1_comp_cochainsIso₁, cochainsMap_f_1_comp_cochainsIso₁_apply, cochainsMap_f_1_comp_cochainsIso₁_assoc, cochainsMap_f_2_comp_cochainsIso₂, cochainsMap_f_2_comp_cochainsIso₂_apply, cochainsMap_f_2_comp_cochainsIso₂_assoc, cochainsMap_f_3_comp_cochainsIso₃, cochainsMap_f_3_comp_cochainsIso₃_apply, cochainsMap_f_3_comp_cochainsIso₃_assoc, cochainsMap_f_hom, cochainsMap_f_map_epi, cochainsMap_f_map_mono, cochainsMap_id, cochainsMap_id_comp, cochainsMap_id_comp_assoc, cochainsMap_id_f_hom_eq_compLeft, cochainsMap_id_f_map_epi, cochainsMap_id_f_map_mono, cochainsMap_zero, cocyclesMap_cocyclesIso₀_hom_f, cocyclesMap_cocyclesIso₀_hom_f_apply, cocyclesMap_cocyclesIso₀_hom_f_assoc, cocyclesMap_comp, cocyclesMap_comp_assoc, cocyclesMap_comp_isoCocycles₁_hom, cocyclesMap_comp_isoCocycles₁_hom_apply, cocyclesMap_comp_isoCocycles₁_hom_assoc, cocyclesMap_comp_isoCocycles₂_hom, cocyclesMap_comp_isoCocycles₂_hom_apply, cocyclesMap_comp_isoCocycles₂_hom_assoc, cocyclesMap_id, cocyclesMap_id_comp, cocyclesMap_id_comp_assoc, coe_mapCocycles₁, coe_mapCocycles₂, functor_map, functor_obj, infNatTrans_app, instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, instMonoModuleCatFH1InfRes, instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, instPreservesZeroMorphismsRepModuleCatFunctor, mapCocycles₁_comp_i, mapCocycles₁_comp_i_apply, mapCocycles₁_comp_i_assoc, mapCocycles₁_one, mapCocycles₂_comp_i, mapCocycles₂_comp_i_apply, mapCocycles₂_comp_i_assoc, mapShortComplexH1_comp, mapShortComplexH1_comp_assoc, mapShortComplexH1_id, mapShortComplexH1_id_comp, mapShortComplexH1_id_comp_assoc, mapShortComplexH1_zero, mapShortComplexH1_τ₁, mapShortComplexH1_τ₂, mapShortComplexH1_τ₃, mapShortComplexH2_comp, mapShortComplexH2_comp_assoc, mapShortComplexH2_id, mapShortComplexH2_id_comp, mapShortComplexH2_id_comp_assoc, mapShortComplexH2_zero, mapShortComplexH2_τ₁, mapShortComplexH2_τ₂, mapShortComplexH2_τ₃, map_H0Iso_hom_f, map_H0Iso_hom_f_apply, map_H0Iso_hom_f_assoc, map_comp, map_comp_assoc, map_id, map_id_comp, map_id_comp_H0Iso_hom, map_id_comp_H0Iso_hom_apply, map_id_comp_H0Iso_hom_assoc, map_id_comp_assoc, map₁_one, mono_map_0_of_mono, resNatTrans_app, π_map, π_map_apply, π_map_assoc	105
Total	120

groupCohomology

Definitions

Name	Category	Theorems
H1InfRes 📖	CompOp	7 math math: instMonoModuleCatFH1InfRes, H1InfRes_X₂, H1InfRes_X₃, H1InfRes_X₁, H1InfRes_g, H1InfRes_exact, H1InfRes_f
cochainsFunctor 📖	CompOp	5 math math: instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, map_cochainsFunctor_shortExact, cochainsFunctor_map, cochainsFunctor_obj
cochainsMap 📖	CompOp	26 math math: cochainsMap_f_3_comp_cochainsIso₃_assoc, cochainsMap_f_2_comp_cochainsIso₂, cochainsMap_comp, cochainsMap_f_1_comp_cochainsIso₁_apply, cochainsMap_f_3_comp_cochainsIso₃_apply, cochainsMap_f_1_comp_cochainsIso₁_assoc, cochainsMap_f_map_epi, cochainsMap_zero, cochainsMap_id_comp, cochainsMap_comp_assoc, cochainsMap_id_f_map_mono, cochainsMap_f_0_comp_cochainsIso₀_apply, cochainsMap_f_2_comp_cochainsIso₂_apply, cochainsMap_f, cochainsMap_f_map_mono, cochainsMap_id_f_map_epi, cochainsMap_f_0_comp_cochainsIso₀, cochainsMap_f_3_comp_cochainsIso₃, cochainsMap_f_hom, cochainsMap_f_2_comp_cochainsIso₂_assoc, cochainsFunctor_map, cochainsMap_id_f_hom_eq_compLeft, cochainsMap_f_1_comp_cochainsIso₁, cochainsMap_id_comp_assoc, cochainsMap_f_0_comp_cochainsIso₀_assoc, cochainsMap_id
cochainsMap₁ 📖	CompOp	7 math math: mapShortComplexH1_τ₂, coe_mapCocycles₁, cochainsMap_f_1_comp_cochainsIso₁_assoc, mapShortComplexH2_τ₁, mapCocycles₁_comp_i_assoc, cochainsMap_f_1_comp_cochainsIso₁, mapCocycles₁_comp_i
cochainsMap₂ 📖	CompOp	7 math math: mapCocycles₂_comp_i, mapShortComplexH1_τ₃, cochainsMap_f_2_comp_cochainsIso₂, mapCocycles₂_comp_i_assoc, mapShortComplexH2_τ₂, cochainsMap_f_2_comp_cochainsIso₂_assoc, coe_mapCocycles₂
cochainsMap₃ 📖	CompOp	3 math math: cochainsMap_f_3_comp_cochainsIso₃_assoc, cochainsMap_f_3_comp_cochainsIso₃, mapShortComplexH2_τ₃
cocyclesMap 📖	CompOp	17 math math: cocyclesMap_id_comp_assoc, cocyclesMap_comp_isoCocycles₂_hom_apply, cocyclesMap_cocyclesIso₀_hom_f_apply, π_map_assoc, cocyclesMap_comp_isoCocycles₁_hom_assoc, cocyclesMap_comp_isoCocycles₁_hom, cocyclesMap_comp, π_map, cocyclesMap_cocyclesIso₀_hom_f_assoc, cocyclesMap_comp_isoCocycles₂_hom, cocyclesMap_comp_isoCocycles₁_hom_apply, cocyclesMap_cocyclesIso₀_hom_f, cocyclesMap_comp_assoc, cocyclesMap_comp_isoCocycles₂_hom_assoc, cocyclesMap_id, π_map_apply, cocyclesMap_id_comp
functor 📖	CompOp	5 math math: infNatTrans_app, functor_obj, resNatTrans_app, instPreservesZeroMorphismsRepModuleCatFunctor, functor_map
infNatTrans 📖	CompOp	1 math math: infNatTrans_app
map 📖	CompOp	28 math math: H1π_comp_map_assoc, map_H0Iso_hom_f_apply, H2π_comp_map_apply, π_map_assoc, map_comp, infNatTrans_app, map_H0Iso_hom_f, map₁_one, map_id, H2π_comp_map, mono_map_0_of_mono, resNatTrans_app, π_map, H2π_comp_map_assoc, map_id_comp_H0Iso_hom_apply, map_id_comp_H0Iso_hom, map_id_comp_assoc, H1π_comp_map_apply, H1InfRes_g, map_id_comp, H1Map_id, π_map_apply, H1π_comp_map, map_H0Iso_hom_f_assoc, H1InfRes_f, map_id_comp_H0Iso_hom_assoc, functor_map, map_comp_assoc
mapCocycles₁ 📖	CompOp	11 math math: H1π_comp_map_assoc, coe_mapCocycles₁, cocyclesMap_comp_isoCocycles₁_hom_assoc, cocyclesMap_comp_isoCocycles₁_hom, mapCocycles₁_one, cocyclesMap_comp_isoCocycles₁_hom_apply, mapCocycles₁_comp_i_assoc, H1π_comp_map_apply, mapCocycles₁_comp_i_apply, H1π_comp_map, mapCocycles₁_comp_i
mapCocycles₂ 📖	CompOp	10 math math: mapCocycles₂_comp_i, mapCocycles₂_comp_i_apply, cocyclesMap_comp_isoCocycles₂_hom_apply, mapCocycles₂_comp_i_assoc, H2π_comp_map_apply, H2π_comp_map, H2π_comp_map_assoc, cocyclesMap_comp_isoCocycles₂_hom, cocyclesMap_comp_isoCocycles₂_hom_assoc, coe_mapCocycles₂
mapShortComplexH1 📖	CompOp	9 math math: mapShortComplexH1_τ₂, mapShortComplexH1_τ₃, mapShortComplexH1_id, mapShortComplexH1_id_comp, mapShortComplexH1_comp, mapShortComplexH1_id_comp_assoc, mapShortComplexH1_zero, mapShortComplexH1_comp_assoc, mapShortComplexH1_τ₁
mapShortComplexH2 📖	CompOp	9 math math: mapShortComplexH2_comp_assoc, mapShortComplexH2_comp, mapShortComplexH2_zero, mapShortComplexH2_τ₁, mapShortComplexH2_id_comp_assoc, mapShortComplexH2_τ₂, mapShortComplexH2_id_comp, mapShortComplexH2_id, mapShortComplexH2_τ₃
resNatTrans 📖	CompOp	1 math math: resNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
H1InfRes_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1InfRes groupCohomology HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.quotientToInvariants	—	—
H1InfRes_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1InfRes groupCohomology	—	—
H1InfRes_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1InfRes groupCohomology Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup CategoryTheory.Functor.obj Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.res Subgroup.subtype	—	—
H1InfRes_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1InfRes	—	RingHomSurjective.ids CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range H1_induction_on H1π_eq_zero_iff H1π_comp_map_apply mem_cocycles₁_iff map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass sub_eq_of_eq_add add_eq_of_eq_sub mul_assoc mul_inv_cancel_left map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Representation.self_inv_apply Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.zero_termg eq_sub_of_add_eq' Subgroup.Normal.conj_mem' QuotientGroup.leftRel_apply cocycles₁_map_inv QuotientGroup.induction_on sub_add_eq_add_sub add_assoc Quotient.liftOn'.congr_simp Representation.le_comap_invariants add_sub_cancel H1π_eq_iff coe_mapCocycles₁ sub_sub_cancel
H1InfRes_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1InfRes map HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.quotientToInvariants QuotientGroup.mk' Rep.subtype DivInvMonoid.toMonoid Group.toDivInvMonoid Representation.invariants SetLike.instMembership Subgroup.instSetLike ModuleCat.carrier Action.V CommRing.toCommSemiring Subgroup.toGroup AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule MonoidHom.comp LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ Subgroup.subtype	—	—
H1InfRes_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1InfRes map Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup CategoryTheory.Functor.obj Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.res Subgroup.subtype CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
H1Map_id 📖	mathematical	—	map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory groupCohomology	—	map_id
H1π_comp_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 groupCohomology H1π map mapCocycles₁	—	CategoryTheory.Category.assoc HomologicalComplex.homologyπ_naturality CategoryTheory.Iso.hom_inv_id_assoc
H1π_comp_map_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier H1 groupCohomology AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier map Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module ModuleCat.of H1π mapCocycles₁	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise H1π_comp_map
H1π_comp_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 H1π groupCohomology map mapCocycles₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' H1π_comp_map
H2π_comp_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module H2 groupCohomology H2π map mapCocycles₂	—	CategoryTheory.Category.assoc HomologicalComplex.homologyπ_naturality CategoryTheory.Iso.hom_inv_id_assoc
H2π_comp_map_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier H2 groupCohomology AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier map Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module ModuleCat.of H2π mapCocycles₂	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise H2π_comp_map
H2π_comp_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module H2 H2π groupCohomology map mapCocycles₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' H2π_comp_map
cochainsFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd cochainsFunctor cochainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainsFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd cochainsFunctor inhomogeneousCochains	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainsMap_comp 📖	mathematical	—	cochainsMap MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousCochains	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainsMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousCochains cochainsMap MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cochainsMap_comp
cochainsMap_f 📖	mathematical	—	HomologicalComplex.Hom.f 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 inhomogeneousCochains cochainsMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule ModuleCat.isAddCommGroup ModuleCat.ofHom LinearMap.funLeft CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike LinearMap.compLeft ModuleCat.Hom.hom Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainsMap_f_0_comp_cochainsIso₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid HomologicalComplex.Hom.f cochainsMap CategoryTheory.Iso.hom cochainsIso₀ Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext Fin.isEmpty' Unique.eq_default
cochainsMap_f_0_comp_cochainsIso₀_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Pi.addCommGroup Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isAddCommGroup Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom cochainsIso₀ HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cochainsMap Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cochainsMap_f_0_comp_cochainsIso₀
cochainsMap_f_0_comp_cochainsIso₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 HomologicalComplex.Hom.f cochainsMap Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Iso.hom cochainsIso₀ Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cochainsMap_f_0_comp_cochainsIso₀
cochainsMap_f_1_comp_cochainsIso₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.Hom.f cochainsMap CategoryTheory.Iso.hom cochainsIso₁ cochainsMap₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainsMap_f_1_comp_cochainsIso₁_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom cochainsIso₁ HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cochainsMap CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.compLeft ModuleCat.Hom.hom Action.Hom.hom LinearMap.funLeft CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cochainsMap_f_1_comp_cochainsIso₁
cochainsMap_f_1_comp_cochainsIso₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 HomologicalComplex.Hom.f cochainsMap ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom cochainsIso₁ cochainsMap₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cochainsMap_f_1_comp_cochainsIso₁
cochainsMap_f_2_comp_cochainsIso₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.Hom.f cochainsMap CategoryTheory.Iso.hom cochainsIso₂ cochainsMap₂	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext Fintype.complete
cochainsMap_f_2_comp_cochainsIso₂_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom cochainsIso₂ HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cochainsMap CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.compLeft ModuleCat.Hom.hom Action.Hom.hom LinearMap.funLeft CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cochainsMap_f_2_comp_cochainsIso₂
cochainsMap_f_2_comp_cochainsIso₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 HomologicalComplex.Hom.f cochainsMap ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom cochainsIso₂ cochainsMap₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cochainsMap_f_2_comp_cochainsIso₂
cochainsMap_f_3_comp_cochainsIso₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.Hom.f cochainsMap CategoryTheory.Iso.hom cochainsIso₃ cochainsMap₃	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext Fintype.complete
cochainsMap_f_3_comp_cochainsIso₃_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom cochainsIso₃ HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cochainsMap CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.compLeft ModuleCat.Hom.hom Action.Hom.hom LinearMap.funLeft CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cochainsMap_f_3_comp_cochainsIso₃
cochainsMap_f_3_comp_cochainsIso₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 HomologicalComplex.Hom.f cochainsMap ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom cochainsIso₃ cochainsMap₃	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cochainsMap_f_3_comp_cochainsIso₃
cochainsMap_f_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cochainsMap LinearMap.comp Pi.addCommMonoid ModuleCat.isAddCommGroup RingHom.id Semiring.toNonAssocSemiring LinearMap.compLeft Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.funLeft CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainsMap_f_map_epi 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory 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 HomologicalComplex.Hom.f cochainsMap	—	AddRightCancelSemigroup.toIsRightCancelAdd Function.Surjective.comp_left Rep.epi_iff_surjective LinearMap.funLeft_surjective_of_injective Function.Injective.comp_left
cochainsMap_f_map_mono 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	CategoryTheory.Mono ModuleCat CommRing.toRing ModuleCat.moduleCategory 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 HomologicalComplex.Hom.f cochainsMap	—	AddRightCancelSemigroup.toIsRightCancelAdd Function.Injective.comp_left Rep.mono_iff_injective LinearMap.funLeft_injective_of_surjective Function.Surjective.comp_left
cochainsMap_id 📖	mathematical	—	cochainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousCochains	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainsMap_id_comp 📖	mathematical	—	cochainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousCochains	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainsMap_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousCochains cochainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cochainsMap_id_comp
cochainsMap_id_f_hom_eq_compLeft 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing HomologicalComplex.X ModuleCat 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 inhomogeneousCochains HomologicalComplex.Hom.f cochainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap.compLeft ModuleCat.carrier Action.V Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Action.Hom.hom	—	LinearMap.ext AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousCochains.ext
cochainsMap_id_f_map_epi 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory 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 HomologicalComplex.Hom.f cochainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	cochainsMap_f_map_epi
cochainsMap_id_f_map_mono 📖	mathematical	—	CategoryTheory.Mono ModuleCat CommRing.toRing ModuleCat.moduleCategory 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 HomologicalComplex.Hom.f cochainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	cochainsMap_f_map_mono
cochainsMap_zero 📖	mathematical	—	cochainsMap Quiver.Hom Action ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res Action.instZeroHom CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousCochains HomologicalComplex.instZeroHom_1	—	AddRightCancelSemigroup.toIsRightCancelAdd
cocyclesMap_cocyclesIso₀_hom_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 cocyclesMap ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.Iso.hom cocyclesIso₀ CategoryTheory.ShortComplex.f Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	cocyclesIso₀_hom_comp_f HomologicalComplex.cyclesMap_i_assoc cochainsMap_f_0_comp_cochainsIso₀ cocyclesIso₀_hom_comp_f_assoc
cocyclesMap_cocyclesIso₀_hom_f_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 AddCommGroup.toAddCommMonoid Pi.addCommGroup Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isAddCommGroup Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom cochainsIso₀ cocycles iCocycles cocyclesMap Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	cocyclesIso₀_hom_comp_f_apply CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cocyclesMap_cocyclesIso₀_hom_f
cocyclesMap_cocyclesIso₀_hom_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles cocyclesMap ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.Iso.hom cocyclesIso₀ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 CategoryTheory.ShortComplex.f Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cocyclesMap_cocyclesIso₀_hom_f
cocyclesMap_comp 📖	mathematical	—	cocyclesMap MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map cocycles	—	—
cocyclesMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles cocyclesMap MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cocyclesMap_comp
cocyclesMap_comp_isoCocycles₁_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module cocyclesMap CategoryTheory.Iso.hom isoCocycles₁ mapCocycles₁	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI CategoryTheory.Category.assoc isoCocycles₁_hom_comp_i HomologicalComplex.cyclesMap_i_assoc cochainsMap_f_1_comp_cochainsIso₁ AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.cyclesMap'_i isoCocycles₁_hom_comp_i_assoc
cocyclesMap_comp_isoCocycles₁_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cocycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ ModuleCat.isAddCommGroup Submodule.addCommGroup Pi.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCocycles₁ cocyclesMap mapCocycles₁	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cocyclesMap_comp_isoCocycles₁_hom
cocyclesMap_comp_isoCocycles₁_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles cocyclesMap ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.Iso.hom isoCocycles₁ mapCocycles₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cocyclesMap_comp_isoCocycles₁_hom
cocyclesMap_comp_isoCocycles₂_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module cocyclesMap CategoryTheory.Iso.hom isoCocycles₂ mapCocycles₂	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI CategoryTheory.Category.assoc isoCocycles₂_hom_comp_i HomologicalComplex.cyclesMap_i_assoc cochainsMap_f_2_comp_cochainsIso₂ AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.cyclesMap'_i isoCocycles₂_hom_comp_i_assoc
cocyclesMap_comp_isoCocycles₂_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cocycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ ModuleCat.isAddCommGroup Submodule.addCommGroup Pi.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCocycles₂ cocyclesMap mapCocycles₂	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cocyclesMap_comp_isoCocycles₂_hom
cocyclesMap_comp_isoCocycles₂_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles cocyclesMap ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.Iso.hom isoCocycles₂ mapCocycles₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cocyclesMap_comp_isoCocycles₂_hom
cocyclesMap_id 📖	mathematical	—	cocyclesMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory cocycles	—	HomologicalComplex.cyclesMap_id
cocyclesMap_id_comp 📖	mathematical	—	cocyclesMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res cocycles	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian AddRightCancelSemigroup.toIsRightCancelAdd cochainsMap_id_comp HomologicalComplex.cyclesMap_comp
cocyclesMap_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles cocyclesMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cocyclesMap_id_comp
coe_mapCocycles₁ 📖	mathematical	—	DFunLike.coe ModuleCat.carrier CommRing.toRing ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier mapCocycles₁ cochainsMap₁	—	—
coe_mapCocycles₂ 📖	mathematical	—	DFunLike.coe ModuleCat.carrier CommRing.toRing ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier mapCocycles₂ cochainsMap₂	—	—
functor_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory functor map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory functor groupCohomology	—	—
infNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.comp HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.quotientToInvariantsFunctor functor infNatTrans map CategoryTheory.Functor.obj QuotientGroup.mk' Rep.subtype Representation.invariants SetLike.instMembership Subgroup.instSetLike ModuleCat.carrier Action.V CommRing.toCommSemiring Subgroup.toGroup AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule MonoidHom.comp LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ Subgroup.subtype	—	—
instAdditiveRepCochainComplexModuleCatNatCochainsFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CochainComplex ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne Action.instCategory HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Action.instPreadditive HomologicalComplex.instPreadditive cochainsFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd
instMonoModuleCatFH1InfRes 📖	mathematical	—	CategoryTheory.Mono ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1InfRes CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	ModuleCat.mono_iff_injective injective_iff_map_eq_zero DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass H1_induction_on H1π_eq_zero_iff H1π_comp_map_apply coe_mapCocycles₁ QuotientGroup.eq_one_iff cocycles₁_map_one QuotientGroup.induction_on
instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Action.instHasZeroMorphisms HomologicalComplex.instHasZeroMorphisms cochainsFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd cochainsMap_zero
instPreservesZeroMorphismsRepModuleCatFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive functor	—	AddRightCancelSemigroup.toIsRightCancelAdd cochainsMap_zero HomologicalComplex.homologyMap_zero
mapCocycles₁_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 mapCocycles₁ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.LeftHomologyData.K Ring.toSemiring cochainsMap₁	—	CategoryTheory.ShortComplex.cyclesMap'_i
mapCocycles₁_comp_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 Submodule.addCommGroup Pi.addCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of mapCocycles₁ CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.compLeft Action.Hom.hom LinearMap.funLeft MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise mapCocycles₁_comp_i
mapCocycles₁_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module mapCocycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData cochainsMap₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCocycles₁_comp_i
mapCocycles₁_one 📖	mathematical	—	mapCocycles₁ MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instOneMonoidHom Quiver.Hom ModuleCat CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module ModuleCat.instZeroHom	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI CategoryTheory.ShortComplex.cyclesMap'_i ModuleCat.hom_ext LinearMap.ext cocycles₁_map_one map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass CategoryTheory.Limits.zero_comp d₀₁_comp_d₁₂ Pi.zero_apply
mapCocycles₂_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 mapCocycles₂ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.LeftHomologyData.K Ring.toSemiring cochainsMap₂	—	CategoryTheory.ShortComplex.cyclesMap'_i
mapCocycles₂_comp_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 Submodule.addCommGroup Pi.addCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of mapCocycles₂ CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.compLeft Action.Hom.hom LinearMap.funLeft MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise mapCocycles₂_comp_i
mapCocycles₂_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module mapCocycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData cochainsMap₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCocycles₂_comp_i
mapShortComplexH1_comp 📖	mathematical	—	mapShortComplexH1 MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH1	—	—
mapShortComplexH1_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory shortComplexH1 mapShortComplexH1 MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapShortComplexH1_comp
mapShortComplexH1_id 📖	mathematical	—	mapShortComplexH1 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH1	—	—
mapShortComplexH1_id_comp 📖	mathematical	—	mapShortComplexH1 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH1	—	—
mapShortComplexH1_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory shortComplexH1 mapShortComplexH1 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapShortComplexH1_id_comp
mapShortComplexH1_zero 📖	mathematical	—	mapShortComplexH1 Quiver.Hom Action ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res Action.instZeroHom CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory shortComplexH1 CategoryTheory.ShortComplex.instZeroHom	—	—
mapShortComplexH1_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 mapShortComplexH1 Action.Hom.hom DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	—
mapShortComplexH1_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 mapShortComplexH1 cochainsMap₁	—	—
mapShortComplexH1_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 mapShortComplexH1 cochainsMap₂	—	—
mapShortComplexH2_comp 📖	mathematical	—	mapShortComplexH2 MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH2	—	—
mapShortComplexH2_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory shortComplexH2 mapShortComplexH2 MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapShortComplexH2_comp
mapShortComplexH2_id 📖	mathematical	—	mapShortComplexH2 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH2	—	—
mapShortComplexH2_id_comp 📖	mathematical	—	mapShortComplexH2 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH2	—	—
mapShortComplexH2_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory shortComplexH2 mapShortComplexH2 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapShortComplexH2_id_comp
mapShortComplexH2_zero 📖	mathematical	—	mapShortComplexH2 Quiver.Hom Action ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res Action.instZeroHom CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory shortComplexH2 CategoryTheory.ShortComplex.instZeroHom	—	—
mapShortComplexH2_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 mapShortComplexH2 cochainsMap₁	—	—
mapShortComplexH2_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 mapShortComplexH2 cochainsMap₂	—	—
mapShortComplexH2_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 mapShortComplexH2 cochainsMap₃	—	—
map_H0Iso_hom_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory groupCohomology CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 map ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.Iso.hom H0 H0Iso CategoryTheory.ShortComplex.f Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	CategoryTheory.cancel_epi HomologicalComplex.instEpiHomologyπ HomologicalComplex.homologyπ_naturality_assoc AddRightCancelSemigroup.toIsRightCancelAdd π_comp_H0Iso_hom_assoc cocyclesIso₀_hom_comp_f HomologicalComplex.cyclesMap_i_assoc cochainsMap_f_0_comp_cochainsIso₀ cocyclesIso₀_hom_comp_f_assoc
map_H0Iso_hom_f_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.ShortComplex.f groupCohomology CategoryTheory.Iso.hom H0 H0Iso map Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise map_H0Iso_hom_f
map_H0Iso_hom_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory groupCohomology map ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.Iso.hom H0 H0Iso CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 CategoryTheory.ShortComplex.f Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_H0Iso_hom_f
map_comp 📖	mathematical	—	map MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map groupCohomology	—	—
map_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory groupCohomology map MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory groupCohomology	—	HomologicalComplex.homologyMap_id
map_id_comp 📖	mathematical	—	map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res groupCohomology	—	map.eq_1 AddRightCancelSemigroup.toIsRightCancelAdd cochainsMap_id_comp CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.homologyMap_comp
map_id_comp_H0Iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory groupCohomology ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Iso.hom H0 H0Iso CategoryTheory.Functor.obj Rep Action.instCategory Rep.invariantsFunctor CategoryTheory.Functor.map	—	CategoryTheory.cancel_mono instMonoModuleCatFShortComplexH0 CategoryTheory.Category.assoc map_H0Iso_hom_f
map_id_comp_H0Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupCohomology Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ ModuleCat.isAddCommGroup Submodule.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom H0 H0Iso map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass LinearMap.codRestrict Submodule.addCommMonoid LinearMap.comp ModuleCat.Hom.hom Action.Hom.hom Submodule.subtype	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise map_id_comp_H0Iso_hom
map_id_comp_H0Iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory groupCohomology map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of ModuleCat.carrier Action.V Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.Iso.hom H0 H0Iso CategoryTheory.Functor.map Rep Action.instCategory Rep.invariantsFunctor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_id_comp_H0Iso_hom
map_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory groupCohomology map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Action Action.instCategory CategoryTheory.Functor.obj Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_id_comp
map₁_one 📖	mathematical	—	map MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instOneMonoidHom Quiver.Hom ModuleCat CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory groupCohomology ModuleCat.instZeroHom	—	CategoryTheory.cancel_epi instEpiModuleCatH1π H1π_comp_map mapCocycles₁_one CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
mono_map_0_of_mono 📖	mathematical	—	CategoryTheory.Mono ModuleCat CommRing.toRing ModuleCat.moduleCategory groupCohomology map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint Rep.instIsRightAdjointModuleCatInvariantsFunctor CategoryTheory.cancel_mono CategoryTheory.Category.assoc map_id_comp_H0Iso_hom
resNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory functor CategoryTheory.Functor.comp Action Action.res resNatTrans map CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
π_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology π map cocyclesMap	—	HomologicalComplex.homologyπ_naturality
π_map_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupCohomology AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier map cocycles π cocyclesMap	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_map
π_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology π map cocyclesMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_map

---

← Back to Index