Functoriality

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

Statistics

Metric	Count
Definitions H1CoresCoinf, H1CoresCoinfOfTrivial, chainsFunctor, chainsMap, chainsMap₁, chainsMap₂, chainsMap₃, coinfNatTrans, coresNatTrans, cyclesMap, functor, map, mapCycles₁, mapCycles₂, mapShortComplexH1, mapShortComplexH2	16
Theorems H0π_comp_map, H0π_comp_map_apply, H0π_comp_map_assoc, H1CoresCoinfOfTrivial_X₁, H1CoresCoinfOfTrivial_X₂, H1CoresCoinfOfTrivial_X₃, H1CoresCoinfOfTrivial_exact, H1CoresCoinfOfTrivial_f, H1CoresCoinfOfTrivial_g, H1CoresCoinfOfTrivial_g_epi, H1CoresCoinf_X₁, H1CoresCoinf_X₂, H1CoresCoinf_X₃, H1CoresCoinf_exact, H1CoresCoinf_f, H1CoresCoinf_g, H1π_comp_map, H1π_comp_map_apply, H1π_comp_map_assoc, H2π_comp_map, H2π_comp_map_apply, H2π_comp_map_assoc, chainsFunctor_map, chainsFunctor_obj, chainsMap_comp, chainsMap_f, chainsMap_f_0_comp_chainsIso₀, chainsMap_f_0_comp_chainsIso₀_apply, chainsMap_f_0_comp_chainsIso₀_assoc, chainsMap_f_1_comp_chainsIso₁, chainsMap_f_1_comp_chainsIso₁_apply, chainsMap_f_1_comp_chainsIso₁_assoc, chainsMap_f_2_comp_chainsIso₂, chainsMap_f_2_comp_chainsIso₂_apply, chainsMap_f_2_comp_chainsIso₂_assoc, chainsMap_f_3_comp_chainsIso₃, chainsMap_f_3_comp_chainsIso₃_apply, chainsMap_f_3_comp_chainsIso₃_assoc, chainsMap_f_hom, chainsMap_f_map_epi, chainsMap_f_map_mono, chainsMap_f_single, chainsMap_id, chainsMap_id_comp, chainsMap_id_f_hom_eq_mapRange, chainsMap_id_f_map_epi, chainsMap_id_f_map_mono, chainsMap_zero, coe_mapCycles₁, coe_mapCycles₂, coinfNatTrans_app, comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, coresNatTrans_app, cyclesIso₀_inv_comp_cyclesMap, cyclesIso₀_inv_comp_cyclesMap_apply, cyclesIso₀_inv_comp_cyclesMap_assoc, cyclesMap_comp, cyclesMap_comp_assoc, cyclesMap_comp_cyclesIso₀_hom, cyclesMap_comp_cyclesIso₀_hom_apply, cyclesMap_comp_cyclesIso₀_hom_assoc, cyclesMap_comp_isoCycles₁_hom, cyclesMap_comp_isoCycles₁_hom_apply, cyclesMap_comp_isoCycles₁_hom_assoc, cyclesMap_comp_isoCycles₂_hom, cyclesMap_comp_isoCycles₂_hom_apply, cyclesMap_comp_isoCycles₂_hom_assoc, cyclesMap_id, cyclesMap_id_comp, epi_map_0_of_epi, functor_map, functor_obj, instEpiModuleCatGH1CoresCoinf, instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, instPreservesZeroMorphismsRepModuleCatFunctor, lsingle_comp_chainsMap_f, lsingle_comp_chainsMap_f_assoc, mapCycles₁_comp, mapCycles₁_comp_apply, mapCycles₁_comp_assoc, mapCycles₁_comp_i, mapCycles₁_comp_i_apply, mapCycles₁_comp_i_assoc, mapCycles₁_hom, mapCycles₁_id_comp, mapCycles₁_id_comp_apply, mapCycles₁_id_comp_assoc, mapCycles₁_quotientGroupMk'_epi, mapCycles₂_comp, mapCycles₂_comp_apply, mapCycles₂_comp_assoc, mapCycles₂_comp_i, mapCycles₂_comp_i_apply, mapCycles₂_comp_i_assoc, mapCycles₂_hom, mapCycles₂_id_comp, mapCycles₂_id_comp_apply, mapCycles₂_id_comp_assoc, mapShortComplexH1_comp, mapShortComplexH1_id, mapShortComplexH1_id_comp, mapShortComplexH1_zero, mapShortComplexH1_τ₁, mapShortComplexH1_τ₂, mapShortComplexH1_τ₃, mapShortComplexH2_comp, mapShortComplexH2_id, mapShortComplexH2_id_comp, mapShortComplexH2_zero, mapShortComplexH2_τ₁, mapShortComplexH2_τ₂, mapShortComplexH2_τ₃, 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₁_one, map₁_quotientGroupMk'_epi, π_map, π_map_apply, π_map_assoc	124
Total	140

groupHomology

Definitions

Name	Category	Theorems
H1CoresCoinf 📖	CompOp	7 math math: H1CoresCoinf_exact, H1CoresCoinf_X₃, H1CoresCoinf_X₁, H1CoresCoinf_g, H1CoresCoinf_X₂, instEpiModuleCatGH1CoresCoinf, H1CoresCoinf_f
H1CoresCoinfOfTrivial 📖	CompOp	7 math math: H1CoresCoinfOfTrivial_X₁, H1CoresCoinfOfTrivial_X₂, H1CoresCoinfOfTrivial_exact, H1CoresCoinfOfTrivial_f, H1CoresCoinfOfTrivial_g, H1CoresCoinfOfTrivial_g_epi, H1CoresCoinfOfTrivial_X₃
chainsFunctor 📖	CompOp	4 math math: map_chainsFunctor_shortExact, chainsFunctor_obj, chainsFunctor_map, instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor
chainsMap 📖	CompOp	27 math math: chainsMap_f_3_comp_chainsIso₃_apply, chainsMap_id, chainsMap_id_f_map_mono, chainsMap_f_3_comp_chainsIso₃, chainsMap_f_single, chainsMap_f_map_epi, chainsMap_id_f_map_epi, chainsMap_id_comp, chainsMap_id_f_hom_eq_mapRange, chainsMap_f_map_mono, chainsMap_f_1_comp_chainsIso₁_assoc, lsingle_comp_chainsMap_f, chainsMap_comp, chainsMap_f_3_comp_chainsIso₃_assoc, chainsMap_f_0_comp_chainsIso₀_assoc, chainsMap_f_1_comp_chainsIso₁, chainsMap_f_2_comp_chainsIso₂, chainsFunctor_map, chainsMap_f_hom, chainsMap_zero, chainsMap_f_2_comp_chainsIso₂_assoc, chainsMap_f_0_comp_chainsIso₀_apply, lsingle_comp_chainsMap_f_assoc, chainsMap_f_1_comp_chainsIso₁_apply, chainsMap_f_0_comp_chainsIso₀, chainsMap_f, chainsMap_f_2_comp_chainsIso₂_apply
chainsMap₁ 📖	CompOp	8 math math: mapShortComplexH1_τ₂, mapCycles₁_comp_i, chainsMap_f_1_comp_chainsIso₁_assoc, chainsMap_f_1_comp_chainsIso₁, mapCycles₁_hom, coe_mapCycles₁, mapShortComplexH2_τ₃, mapCycles₁_comp_i_assoc
chainsMap₂ 📖	CompOp	8 math math: mapCycles₂_comp_i, coe_mapCycles₂, mapShortComplexH2_τ₂, mapShortComplexH1_τ₁, mapCycles₂_hom, chainsMap_f_2_comp_chainsIso₂, mapCycles₂_comp_i_assoc, chainsMap_f_2_comp_chainsIso₂_assoc
chainsMap₃ 📖	CompOp	3 math math: mapShortComplexH2_τ₁, chainsMap_f_3_comp_chainsIso₃, chainsMap_f_3_comp_chainsIso₃_assoc
coinfNatTrans 📖	CompOp	1 math math: coinfNatTrans_app
coresNatTrans 📖	CompOp	1 math math: coresNatTrans_app
cyclesMap 📖	CompOp	19 math math: cyclesMap_id_comp, cyclesMap_comp_isoCycles₂_hom, cyclesMap_comp_assoc, cyclesMap_comp_cyclesIso₀_hom_apply, cyclesIso₀_inv_comp_cyclesMap_apply, cyclesMap_comp_isoCycles₂_hom_assoc, cyclesMap_comp_isoCycles₂_hom_apply, cyclesMap_comp_cyclesIso₀_hom, cyclesMap_comp_isoCycles₁_hom_apply, π_map_assoc, cyclesIso₀_inv_comp_cyclesMap_assoc, cyclesIso₀_inv_comp_cyclesMap, π_map_apply, cyclesMap_comp_isoCycles₁_hom_assoc, cyclesMap_comp, cyclesMap_comp_cyclesIso₀_hom_assoc, cyclesMap_id, π_map, cyclesMap_comp_isoCycles₁_hom
functor 📖	CompOp	5 math math: coinfNatTrans_app, coresNatTrans_app, instPreservesZeroMorphismsRepModuleCatFunctor, functor_obj, functor_map
map 📖	CompOp	29 math math: map₁_quotientGroupMk'_epi, coinfNatTrans_app, map₁_one, H0π_comp_map, map_id, coresNatTrans_app, map_comp, map_id_comp, map_comp_assoc, H1CoresCoinf_g, H1π_comp_map_apply, H0π_comp_map_assoc, H2π_comp_map_assoc, map_id_comp_H0Iso_hom_assoc, π_map_assoc, H2π_comp_map, H1π_comp_map_assoc, H1π_comp_map, map_id_comp_H0Iso_hom_apply, H1CoresCoinfOfTrivial_f, functor_map, H2π_comp_map_apply, H1CoresCoinfOfTrivial_g, map_id_comp_H0Iso_hom, π_map_apply, epi_map_0_of_epi, H1CoresCoinf_f, π_map, H0π_comp_map_apply
mapCycles₁ 📖	CompOp	18 math math: mapCycles₁_comp_apply, mapCycles₁_comp_assoc, mapCycles₁_id_comp_assoc, mapCycles₁_comp, mapCycles₁_comp_i, mapCycles₁_id_comp_apply, mapCycles₁_comp_i_apply, H1π_comp_map_apply, mapCycles₁_id_comp, cyclesMap_comp_isoCycles₁_hom_apply, H1π_comp_map_assoc, H1π_comp_map, mapCycles₁_hom, cyclesMap_comp_isoCycles₁_hom_assoc, coe_mapCycles₁, mapCycles₁_quotientGroupMk'_epi, mapCycles₁_comp_i_assoc, cyclesMap_comp_isoCycles₁_hom
mapCycles₂ 📖	CompOp	17 math math: mapCycles₂_comp_assoc, cyclesMap_comp_isoCycles₂_hom, mapCycles₂_id_comp, mapCycles₂_comp_i, mapCycles₂_comp, coe_mapCycles₂, H2π_comp_map_assoc, mapCycles₂_comp_apply, cyclesMap_comp_isoCycles₂_hom_assoc, mapCycles₂_id_comp_assoc, cyclesMap_comp_isoCycles₂_hom_apply, mapCycles₂_hom, H2π_comp_map, mapCycles₂_comp_i_assoc, mapCycles₂_id_comp_apply, H2π_comp_map_apply, mapCycles₂_comp_i_apply
mapShortComplexH1 📖	CompOp	8 math math: mapShortComplexH1_zero, comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, mapShortComplexH1_τ₂, mapShortComplexH1_id_comp, mapShortComplexH1_comp, mapShortComplexH1_τ₁, mapShortComplexH1_id, mapShortComplexH1_τ₃
mapShortComplexH2 📖	CompOp	7 math math: mapShortComplexH2_τ₁, mapShortComplexH2_id, mapShortComplexH2_zero, mapShortComplexH2_comp, mapShortComplexH2_τ₂, mapShortComplexH2_id_comp, mapShortComplexH2_τ₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
H0π_comp_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0 groupHomology H0π map CategoryTheory.Functor.obj Action Action.instCategory Action.res Action.Hom.hom	—	CategoryTheory.Category.assoc HomologicalComplex.homologyπ_naturality cyclesIso₀_inv_comp_cyclesMap_assoc
H0π_comp_map_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier H0 groupHomology AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier map Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0π Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise H0π_comp_map
H0π_comp_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0 H0π groupHomology map CategoryTheory.Functor.obj Action Action.instCategory Action.res Action.Hom.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' H0π_comp_map
H1CoresCoinfOfTrivial_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinfOfTrivial H1 Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup CategoryTheory.Functor.obj Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.res Subgroup.subtype	—	—
H1CoresCoinfOfTrivial_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinfOfTrivial H1	—	—
H1CoresCoinfOfTrivial_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinfOfTrivial H1 HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.ofQuotient	—	—
H1CoresCoinfOfTrivial_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinfOfTrivial	—	RingHomSurjective.ids CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range H1_induction_on H1π_eq_zero_iff H1π_comp_map_apply CategoryTheory.ShortComplex.Hom.comm₁₂ RingHomCompTriple.ids Finsupp.mapRange.linearMap_id CategoryTheory.Category.comp_id Finsupp.mapDomain_id Finsupp.mapDomain_comp Finsupp.sum_sub_index Finsupp.single_sub coe_mapCycles₁ sub_self LeftCancelSemigroup.toIsLeftCancelMul mul_inv_cancel_left Finsupp.sum_add Finsupp.sum_sub Finsupp.sum_single add_sub_cancel Finset.mem_union Finsupp.support_add Finset.mem_biUnion Finsupp.support_sum Finsupp.support_single_subset Set.injOn_of_injective Subtype.val_injective Submodule.add_mem Submodule.sub_mem d₂₁_apply_mem_cycles₁ mem_cycles₁_iff Set.BijOn.injOn Set.mapsTo_preimage Finsupp.sum_comapDomain H1π_eq_iff Function.Injective.injOn Finsupp.mapDomain_comapDomain map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.restrict.congr_simp add_sub_assoc sub_add_sub_cancel' QuotientGroup.mk'_surjective
H1CoresCoinfOfTrivial_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinfOfTrivial 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 Rep CategoryTheory.Category.toCategoryStruct	—	—
H1CoresCoinfOfTrivial_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinfOfTrivial map HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.ofQuotient QuotientGroup.mk' CategoryTheory.Iso.inv Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Functor.obj Action.res Rep.resOfQuotientIso	—	—
H1CoresCoinfOfTrivial_g_epi 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinfOfTrivial CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	map₁_quotientGroupMk'_epi
H1CoresCoinf_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinf H1 Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup CategoryTheory.Functor.obj Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.res Subgroup.subtype	—	—
H1CoresCoinf_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinf H1	—	—
H1CoresCoinf_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinf H1 HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.quotientToCoinvariants	—	—
H1CoresCoinf_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinf	—	RingHomSurjective.ids CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range H1_induction_on H1π_eq_zero_iff H1π_comp_map_apply Rep.instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants H1CoresCoinfOfTrivial_exact mapCycles₁_comp_apply H1π_eq_iff map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.mapRange_surjective Representation.Coinvariants.mk_surjective Representation.Coinvariants.mk_eq_iff CategoryTheory.ShortComplex.Hom.comm₁₂ Finsupp.ext_iff Finsupp.mapRange_apply LinearMap.map_zero Finsupp.mapRange.linearMap_apply map_add SemilinearMapClass.toAddHomClass RingHomCompTriple.ids Finsupp.lmapDomain_id CategoryTheory.Category.id_comp Mathlib.Tactic.TermCongr.cHole.congr_simp Finsupp.mapRange.linearMap_id CategoryTheory.Category.comp_id LinearMap.restrict.congr_simp Function.leftInverse_invFun Subtype.val_injective Finsupp.ext CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian eq_top_iff comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff sub_add_eq_add_sub add_sub_cancel Finsupp.mapDomain_add mem_cycles₁_iff Submodule.add_mem d₂₁_apply_mem_cycles₁ eq_sub_iff_add_eq'
H1CoresCoinf_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinf 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 Rep CategoryTheory.Category.toCategoryStruct	—	—
H1CoresCoinf_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinf map HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.quotientToCoinvariants QuotientGroup.mk' Rep.toCoinvariantsMkQ	—	—
H1π_comp_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H1 groupHomology H1π map mapCycles₁	—	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 groupHomology AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier map Finsupp Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Finsupp.module SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module ModuleCat.of H1π mapCycles₁	—	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 Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H1 H1π groupHomology map mapCycles₁	—	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 Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H2 groupHomology H2π map mapCycles₂	—	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 groupHomology AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier map Finsupp Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Finsupp.module SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module ModuleCat.of H2π mapCycles₂	—	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 Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H2 H2π groupHomology map mapCycles₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' H2π_comp_map
chainsFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd chainsFunctor chainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass	—	AddRightCancelSemigroup.toIsRightCancelAdd
chainsFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd chainsFunctor inhomogeneousChains	—	AddRightCancelSemigroup.toIsRightCancelAdd
chainsMap_comp 📖	mathematical	—	chainsMap MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousChains	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousChains.ext ModuleCat.hom_ext LinearMap.ext RingHomCompTriple.ids Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero CategoryTheory.Category.assoc
chainsMap_f 📖	mathematical	—	HomologicalComplex.Hom.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains chainsMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ModuleCat.isAddCommGroup ModuleCat.ofHom Finsupp.lmapDomain CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Finsupp.mapRange.linearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	AddRightCancelSemigroup.toIsRightCancelAdd
chainsMap_f_0_comp_chainsIso₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid HomologicalComplex.Hom.f chainsMap CategoryTheory.Iso.hom chainsIso₀ CategoryTheory.Functor.obj Action Action.instCategory Action.res Action.Hom.hom	—	inhomogeneousChains.ext AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.hom_ext LinearMap.ext RingHomCompTriple.ids Fin.isEmpty' Unique.eq_default CategoryTheory.Category.assoc Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero Finsupp.single_eq_same
chainsMap_f_0_comp_chainsIso₀_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup ModuleCat.isAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom chainsIso₀ HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains chainsMap Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise chainsMap_f_0_comp_chainsIso₀
chainsMap_f_0_comp_chainsIso₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Iso.hom chainsIso₀ Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' chainsMap_f_0_comp_chainsIso₀
chainsMap_f_1_comp_chainsIso₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.Hom.f chainsMap CategoryTheory.Iso.hom chainsIso₁ chainsMap₁	—	inhomogeneousChains.ext AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.hom_ext LinearMap.ext Finsupp.ext RingHomCompTriple.ids CategoryTheory.Category.assoc Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero Finsupp.equivMapDomain_single
chainsMap_f_1_comp_chainsIso₁_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom chainsIso₁ HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains chainsMap Finsupp.mapRange AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ModuleCat.Hom.hom Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.map_zero Finsupp.mapDomain MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.map_zero CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise chainsMap_f_1_comp_chainsIso₁
chainsMap_f_1_comp_chainsIso₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom chainsIso₁ chainsMap₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' chainsMap_f_1_comp_chainsIso₁
chainsMap_f_2_comp_chainsIso₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.Hom.f chainsMap CategoryTheory.Iso.hom chainsIso₂ chainsMap₂	—	inhomogeneousChains.ext AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.hom_ext LinearMap.ext Finsupp.ext RingHomCompTriple.ids CategoryTheory.Category.assoc Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero Finsupp.equivMapDomain_single
chainsMap_f_2_comp_chainsIso₂_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom chainsIso₂ HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains chainsMap Finsupp.mapRange AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ModuleCat.Hom.hom Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.map_zero Finsupp.mapDomain MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.map_zero CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise chainsMap_f_2_comp_chainsIso₂
chainsMap_f_2_comp_chainsIso₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom chainsIso₂ chainsMap₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' chainsMap_f_2_comp_chainsIso₂
chainsMap_f_3_comp_chainsIso₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.Hom.f chainsMap CategoryTheory.Iso.hom chainsIso₃ chainsMap₃	—	inhomogeneousChains.ext AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.hom_ext LinearMap.ext Finsupp.ext RingHomCompTriple.ids CategoryTheory.Category.assoc Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero Finsupp.equivMapDomain_single
chainsMap_f_3_comp_chainsIso₃_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom chainsIso₃ HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains chainsMap Finsupp.mapRange AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ModuleCat.Hom.hom Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res LinearMap.map_zero Finsupp.mapDomain MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.map_zero CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise chainsMap_f_3_comp_chainsIso₃
chainsMap_f_3_comp_chainsIso₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom chainsIso₃ chainsMap₃	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' chainsMap_f_3_comp_chainsIso₃
chainsMap_f_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains chainsMap LinearMap.comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ModuleCat.isAddCommGroup Finsupp.instAddCommMonoid RingHom.id Semiring.toNonAssocSemiring Finsupp.mapRange.linearMap Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res Finsupp.lmapDomain CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd
chainsMap_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.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap	—	AddRightCancelSemigroup.toIsRightCancelAdd map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.mapRange_surjective Rep.epi_iff_surjective Finsupp.mapDomain_surjective Function.Surjective.comp_left
chainsMap_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.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap	—	AddRightCancelSemigroup.toIsRightCancelAdd map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.mapRange_injective Rep.mono_iff_injective Finsupp.mapDomain_injective Function.Injective.comp_left
chainsMap_f_single 📖	mathematical	—	DFunLike.coe HomologicalComplex.X ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier HomologicalComplex.Hom.f chainsMap Finsupp.single Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat CategoryTheory.Functor.obj Action Action.instCategory Action.res MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Action.Hom.hom	—	AddRightCancelSemigroup.toIsRightCancelAdd Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero
chainsMap_id 📖	mathematical	—	chainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousChains	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.hom_ext Finsupp.lhom_ext' RingHomCompTriple.ids ModuleCat.hom_ext_iff lsingle_comp_chainsMap_f
chainsMap_id_comp 📖	mathematical	—	chainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousChains	—	chainsMap_comp
chainsMap_id_f_hom_eq_mapRange 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing HomologicalComplex.X ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.mapRange.linearMap ModuleCat.carrier Action.V Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring Action.Hom.hom	—	Finsupp.lhom_ext AddRightCancelSemigroup.toIsRightCancelAdd RingHomCompTriple.ids CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero
chainsMap_id_f_map_epi 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	chainsMap_f_map_epi
chainsMap_id_f_map_mono 📖	mathematical	—	CategoryTheory.Mono ModuleCat CommRing.toRing ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	chainsMap_f_map_mono
chainsMap_zero 📖	mathematical	—	chainsMap Quiver.Hom Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res Action.instZeroHom CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ChainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousChains HomologicalComplex.instZeroHom_1	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd inhomogeneousChains.ext ModuleCat.hom_ext LinearMap.ext Finsupp.mapDomain_single LinearMap.map_zero Finsupp.mapRange_single LinearMap.zero_apply Finsupp.single_zero CategoryTheory.Limits.comp_zero
coe_mapCycles₁ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ DFunLike.coe ModuleCat.of Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier mapCycles₁ chainsMap₁	—	—
coe_mapCycles₂ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ DFunLike.coe ModuleCat.of Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier mapCycles₂ chainsMap₂	—	—
coinfNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory functor CategoryTheory.Functor.comp HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.quotientToCoinvariantsFunctor coinfNatTrans map CategoryTheory.Functor.obj QuotientGroup.mk' Rep.mkQ Representation.Coinvariants.ker SetLike.instMembership Subgroup.instSetLike ModuleCat.carrier Action.V Subgroup.toGroup ModuleCat.isAddCommGroup ModuleCat.isModule MonoidHom.comp LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ Subgroup.subtype	—	—
comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top 📖	mathematical	—	Submodule.comap ModuleCat.carrier CommRing.toRing CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.X₁ Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.instHasZeroMorphisms Rep.coinvariantsShortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.Hom.τ₂ mapShortComplexH1 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.pOpcycles LinearMap.range Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup CategoryTheory.Functor.obj Action Action.res Subgroup.subtype RingHomSurjective.ids CategoryTheory.CategoryStruct.id Top.top Submodule Submodule.instTop	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian RingHomSurjective.ids eq_top_iff map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.mapRange_surjective chains₁ToCoinvariantsKer_surjective CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff sub_add_eq_add_sub Finsupp.sum_sub mul_assoc map_sub map_finsuppSum mul_inv_cancel_left Finsupp.sum_single_index Finsupp.single_zero add_zero sub_self Finsupp.sum_add sub_sub_sub_cancel_right Finsupp.mapRange.congr_simp map_inv MonoidHom.instMonoidHomClass MulAut.inv_apply LinearMap.map_zero Finsupp.mapRange_single MulAut.conjNormal_symm_apply Finsupp.mapRange_id Finsupp.sum_mapRange_index Finsupp.single_sum Finsupp.single_sub sub_sub_sub_eq add_comm
coresNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Action ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Functor.comp Action.res functor coresNatTrans map CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id Rep CategoryTheory.Category.toCategoryStruct	—	—
cyclesIso₀_inv_comp_cyclesMap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid cycles CategoryTheory.Iso.inv cyclesIso₀ cyclesMap CategoryTheory.Functor.obj Action Action.instCategory Action.res Action.Hom.hom	—	CategoryTheory.CommSq.w CategoryTheory.CommSq.vert_inv cyclesMap_comp_cyclesIso₀_hom
cyclesIso₀_inv_comp_cyclesMap_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier cyclesMap Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Iso.inv cyclesIso₀ Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cyclesIso₀_inv_comp_cyclesMap
cyclesIso₀_inv_comp_cyclesMap_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid cycles CategoryTheory.Iso.inv cyclesIso₀ cyclesMap CategoryTheory.Functor.obj Action Action.instCategory Action.res Action.Hom.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIso₀_inv_comp_cyclesMap
cyclesMap_comp 📖	mathematical	—	cyclesMap MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map cycles	—	—
cyclesMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles cyclesMap MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Rep Action.instCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_comp
cyclesMap_comp_cyclesIso₀_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid cyclesMap CategoryTheory.Iso.hom cyclesIso₀ CategoryTheory.Functor.obj Action Action.instCategory Action.res Action.Hom.hom	—	HomologicalComplex.cyclesMap_i_assoc chainsMap_f_0_comp_chainsIso₀ CategoryTheory.Category.assoc
cyclesMap_comp_cyclesIso₀_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom cyclesIso₀ cyclesMap Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cyclesMap_comp_cyclesIso₀_hom
cyclesMap_comp_cyclesIso₀_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles cyclesMap Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Iso.hom cyclesIso₀ Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_comp_cyclesIso₀_hom
cyclesMap_comp_isoCycles₁_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module cyclesMap CategoryTheory.Iso.hom isoCycles₁ mapCycles₁	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI CategoryTheory.Category.assoc isoCycles₁_hom_comp_i HomologicalComplex.cyclesMap_i_assoc chainsMap_f_1_comp_chainsIso₁ AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.cyclesMap'_i isoCycles₁_hom_comp_i_assoc
cyclesMap_comp_isoCycles₁_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles Finsupp Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ ModuleCat.isAddCommGroup Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCycles₁ cyclesMap mapCycles₁	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cyclesMap_comp_isoCycles₁_hom
cyclesMap_comp_isoCycles₁_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles cyclesMap ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.Iso.hom isoCycles₁ mapCycles₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_comp_isoCycles₁_hom
cyclesMap_comp_isoCycles₂_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module cyclesMap CategoryTheory.Iso.hom isoCycles₂ mapCycles₂	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI CategoryTheory.Category.assoc isoCycles₂_hom_comp_i HomologicalComplex.cyclesMap_i_assoc chainsMap_f_2_comp_chainsIso₂ AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.cyclesMap'_i isoCycles₂_hom_comp_i_assoc
cyclesMap_comp_isoCycles₂_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles Finsupp Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ ModuleCat.isAddCommGroup Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCycles₂ cyclesMap mapCycles₂	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cyclesMap_comp_isoCycles₂_hom
cyclesMap_comp_isoCycles₂_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles cyclesMap ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.Iso.hom isoCycles₂ mapCycles₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_comp_isoCycles₂_hom
cyclesMap_id 📖	mathematical	—	cyclesMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory cycles	—	AddRightCancelSemigroup.toIsRightCancelAdd chainsMap_id HomologicalComplex.cyclesMap_id
cyclesMap_id_comp 📖	mathematical	—	cyclesMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res cycles	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian AddRightCancelSemigroup.toIsRightCancelAdd chainsMap_id_comp HomologicalComplex.cyclesMap_comp
epi_map_0_of_epi 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory groupHomology map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	H0π_comp_map_assoc Rep.instEpiModuleCatHom instEpiModuleCatH0π CategoryTheory.cancel_epi
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 groupHomology	—	—
instEpiModuleCatGH1CoresCoinf 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive H1CoresCoinf CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	ModuleCat.epi_iff_surjective H1_induction_on Rep.instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants mapCycles₁_quotientGroupMk'_epi map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.mapRange_surjective Representation.Coinvariants.mk_surjective CategoryTheory.ShortComplex.Hom.comm₂₃ RingHomCompTriple.ids Finsupp.lmapDomain_id CategoryTheory.Category.id_comp LinearMap.map_coe_ker chains₁ToCoinvariantsKer_surjective map_sub H1π_comp_map_apply H1π_eq_iff LinearMap.map_zero map_add SemilinearMapClass.toAddHomClass QuotientGroup.eq_one_iff Subtype.prop Finsupp.mapRange.linearMap_id CategoryTheory.Category.comp_id LinearMap.restrict.congr_simp sub_sub_cancel_left AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass Submodule.finsuppSum_mem single_one_mem_boundaries₁
instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Action.instHasZeroMorphisms HomologicalComplex.instHasZeroMorphisms chainsFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd chainsMap_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 chainsMap_zero HomologicalComplex.homologyMap_zero
lsingle_comp_chainsMap_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains ModuleCat.ofHom Finsupp.lsingle HomologicalComplex.Hom.f chainsMap CategoryTheory.Functor.obj Action Action.instCategory Action.res ModuleCat.isAddCommGroup Action.Hom.hom DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero
lsingle_comp_chainsMap_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring ModuleCat.ofHom Finsupp.lsingle HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains HomologicalComplex.Hom.f chainsMap CategoryTheory.Functor.obj Action Action.instCategory Action.res Action.Hom.hom ModuleCat.isAddCommGroup DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lsingle_comp_chainsMap_f
mapCycles₁_comp 📖	mathematical	—	mapCycles₁ MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map ModuleCat.of Finsupp ModuleCat.carrier Action.V NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module	—	CategoryTheory.ShortComplex.cyclesMap'_comp mapShortComplexH1_comp
mapCycles₁_comp_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of mapCycles₁ MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise mapCycles₁_comp
mapCycles₁_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module mapCycles₁ MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass Rep Action.instCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCycles₁_comp
mapCycles₁_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 mapCycles₁ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.LeftHomologyData.K Ring.toSemiring chainsMap₁	—	CategoryTheory.ShortComplex.cyclesMap'_i
mapCycles₁_comp_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 Submodule.addCommGroup Finsupp.instAddCommGroup 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 mapCycles₁ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.mapRange.linearMap Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res Finsupp.lmapDomain MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise mapCycles₁_comp_i
mapCycles₁_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module mapCycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData chainsMap₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCycles₁_comp_i
mapCycles₁_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module mapCycles₁ LinearMap.restrict Ring.toSemiring ModuleCat.isAddCommGroup chainsMap₁	—	—
mapCycles₁_id_comp 📖	mathematical	—	mapCycles₁ MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res ModuleCat.of Finsupp ModuleCat.carrier Action.V NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module	—	mapCycles₁_comp
mapCycles₁_id_comp_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of mapCycles₁ MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action Action.res	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise mapCycles₁_id_comp
mapCycles₁_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module mapCycles₁ MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Rep Action.instCategory CategoryTheory.Functor.obj Action Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCycles₁_id_comp
mapCycles₁_quotientGroupMk'_epi 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.ofQuotient mapCycles₁ QuotientGroup.mk' CategoryTheory.Iso.inv Action Action.instCategory CategoryTheory.Functor.obj Action.res Rep.resOfQuotientIso	—	ModuleCat.epi_iff_surjective mem_cycles₁_iff Finsupp.sum_congr QuotientGroup.induction_on Representation.apply_eq_of_coe_eq Finsupp.mapRange.linearMap_id CategoryTheory.Category.comp_id LinearMap.restrict.congr_simp Finsupp.mapDomain_id QuotientGroup.mk_surjective
mapCycles₂_comp 📖	mathematical	—	mapCycles₂ MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map ModuleCat.of Finsupp ModuleCat.carrier Action.V NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module	—	CategoryTheory.ShortComplex.cyclesMap'_comp mapShortComplexH2_comp
mapCycles₂_comp_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of mapCycles₂ MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise mapCycles₂_comp
mapCycles₂_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module mapCycles₂ MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass Rep Action.instCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCycles₂_comp
mapCycles₂_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 mapCycles₂ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.LeftHomologyData.K Ring.toSemiring chainsMap₂	—	CategoryTheory.ShortComplex.cyclesMap'_i
mapCycles₂_comp_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 Submodule.addCommGroup Finsupp.instAddCommGroup 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 mapCycles₂ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.mapRange.linearMap Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory Action.res Finsupp.lmapDomain MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise mapCycles₂_comp_i
mapCycles₂_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module mapCycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData chainsMap₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCycles₂_comp_i
mapCycles₂_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module mapCycles₂ LinearMap.restrict Ring.toSemiring ModuleCat.isAddCommGroup chainsMap₂	—	—
mapCycles₂_id_comp 📖	mathematical	—	mapCycles₂ MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res ModuleCat.of Finsupp ModuleCat.carrier Action.V NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module	—	mapCycles₂_comp
mapCycles₂_id_comp_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of mapCycles₂ MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action Action.res	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise mapCycles₂_id_comp
mapCycles₂_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module mapCycles₂ MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Rep Action.instCategory CategoryTheory.Functor.obj Action Action.res	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCycles₂_id_comp
mapShortComplexH1_comp 📖	mathematical	—	mapShortComplexH1 MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH1	—	CategoryTheory.ShortComplex.hom_ext ModuleCat.hom_ext d₂₁_comp_d₁₀ Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids Finsupp.ext Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero LinearMap.comp.congr_simp CategoryTheory.Category.assoc
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	—	CategoryTheory.ShortComplex.hom_ext d₂₁_comp_d₁₀ ModuleCat.hom_ext LinearMap.ext Finsupp.lmapDomain_id Finsupp.mapRange.linearMap_id CategoryTheory.Category.comp_id
mapShortComplexH1_id_comp 📖	mathematical	—	mapShortComplexH1 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH1	—	mapShortComplexH1_comp
mapShortComplexH1_zero 📖	mathematical	—	mapShortComplexH1 Quiver.Hom Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res Action.instZeroHom CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory shortComplexH1 CategoryTheory.ShortComplex.instZeroHom	—	CategoryTheory.ShortComplex.hom_ext ModuleCat.hom_ext d₂₁_comp_d₁₀ Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids Finsupp.ext Finsupp.mapDomain_single LinearMap.map_zero Finsupp.mapRange_single Finsupp.single_zero
mapShortComplexH1_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 mapShortComplexH1 chainsMap₂	—	—
mapShortComplexH1_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 mapShortComplexH1 chainsMap₁	—	—
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	—	—
mapShortComplexH2_comp 📖	mathematical	—	mapShortComplexH2 MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH2	—	CategoryTheory.ShortComplex.hom_ext ModuleCat.hom_ext d₃₂_comp_d₂₁ Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids Finsupp.ext Finsupp.mapDomain_single Finsupp.mapRange_single LinearMap.map_zero LinearMap.comp.congr_simp CategoryTheory.Category.assoc
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	—	CategoryTheory.ShortComplex.hom_ext ModuleCat.hom_ext d₃₂_comp_d₂₁ Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids Finsupp.ext LinearMap.comp.congr_simp Finsupp.lmapDomain_id Finsupp.mapRange.linearMap_id CategoryTheory.Category.comp_id
mapShortComplexH2_id_comp 📖	mathematical	—	mapShortComplexH2 MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory shortComplexH2	—	mapShortComplexH2_comp
mapShortComplexH2_zero 📖	mathematical	—	mapShortComplexH2 Quiver.Hom Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res Action.instZeroHom CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory shortComplexH2 CategoryTheory.ShortComplex.instZeroHom	—	CategoryTheory.ShortComplex.hom_ext ModuleCat.hom_ext d₃₂_comp_d₂₁ Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids Finsupp.ext Finsupp.mapDomain_single LinearMap.map_zero Finsupp.mapRange_single Finsupp.single_zero
mapShortComplexH2_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 mapShortComplexH2 chainsMap₃	—	—
mapShortComplexH2_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 mapShortComplexH2 chainsMap₂	—	—
mapShortComplexH2_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 mapShortComplexH2 chainsMap₁	—	—
map_comp 📖	mathematical	—	map MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res CategoryTheory.Functor.map groupHomology	—	—
map_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory groupHomology map MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Rep Action.instCategory CategoryTheory.Functor.obj Action 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 groupHomology	—	AddRightCancelSemigroup.toIsRightCancelAdd chainsMap_id HomologicalComplex.homologyMap_id
map_id_comp 📖	mathematical	—	map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res groupHomology	—	map.eq_1 AddRightCancelSemigroup.toIsRightCancelAdd chainsMap_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 groupHomology CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Rep.coinvariantsFunctor map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Iso.hom H0 H0Iso CategoryTheory.Functor.map	—	CategoryTheory.cancel_epi instEpiModuleCatH0π ModuleCat.hom_ext LinearMap.ext RingHomCompTriple.ids H0π_comp_map_assoc H0π_comp_H0Iso_hom H0π_comp_H0Iso_hom_assoc
map_id_comp_H0Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupHomology Representation.Coinvariants Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Rep.ρ AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj Rep Action.instCategory Rep.coinvariantsFunctor LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom H0 H0Iso map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Representation.Coinvariants.map ModuleCat.Hom.hom Action.Hom.hom	—	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 groupHomology map MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory Rep.coinvariantsFunctor CategoryTheory.Iso.hom H0 H0Iso CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_id_comp_H0Iso_hom
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 groupHomology ModuleCat.instZeroHom	—	CategoryTheory.cancel_epi instEpiModuleCatH1π H1π_comp_map CategoryTheory.Limits.comp_zero ModuleCat.hom_ext LinearMap.ext RingHomCompTriple.ids ModuleCat.hom_comp H1π_eq_zero_iff map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.map_zero Finsupp.mapRange_single Submodule.finsuppSum_mem single_one_mem_boundaries₁
map₁_quotientGroupMk'_epi 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory groupHomology HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Rep.ofQuotient map QuotientGroup.mk' CategoryTheory.Iso.inv Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Functor.obj Action.res Rep.resOfQuotientIso	—	CategoryTheory.epi_of_epi H1π_comp_map CategoryTheory.epi_comp mapCycles₁_quotientGroupMk'_epi instEpiModuleCatH1π
π_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology π map cyclesMap	—	HomologicalComplex.homologyπ_naturality
π_map_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupHomology AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier map cycles π cyclesMap	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_map
π_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology π map cyclesMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_map

---

← Back to Index