ModuleCat

📁 Source: Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean

Statistics

Metric	Count
Definitions moduleCatCyclesIso, moduleCatHomologyIso, moduleCatLeftHomologyData, moduleCatMk, moduleCatMkOfKerLERange, moduleCatOpcyclesIso, moduleCatToCycles, shortComplexKer, shortComplexOfCompEqZero	9
Theorems moduleCat_of_range_eq_ker, moduleCat_range_eq_ker, moduleCat_exact_iff_function_exact, moduleCat_injective_f, moduleCat_surjective_g, exact_iff_surjective_moduleCatToCycles, instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier, moduleCatCyclesIso_hom_i, moduleCatCyclesIso_hom_i_apply, moduleCatCyclesIso_hom_i_assoc, moduleCatCyclesIso_hom_i_assoc_apply, moduleCatCyclesIso_inv_iCycles, moduleCatCyclesIso_inv_iCycles_apply, moduleCatCyclesIso_inv_iCycles_assoc, moduleCatCyclesIso_inv_iCycles_assoc_apply, moduleCatCyclesIso_inv_π, moduleCatCyclesIso_inv_π_apply, moduleCatCyclesIso_inv_π_assoc, moduleCatCyclesIso_inv_π_assoc_apply, moduleCatLeftHomologyData_H, moduleCatLeftHomologyData_K, moduleCatLeftHomologyData_descH_hom, moduleCatLeftHomologyData_f'_hom, moduleCatLeftHomologyData_i_hom, moduleCatLeftHomologyData_liftK_hom, moduleCatLeftHomologyData_π_hom, moduleCatMkOfKerLERange_X₁, moduleCatMkOfKerLERange_X₂, moduleCatMkOfKerLERange_X₃, moduleCatMkOfKerLERange_f, moduleCatMkOfKerLERange_g, moduleCatMk_X₁_carrier, moduleCatMk_X₁_isAddCommGroup, moduleCatMk_X₁_isModule, moduleCatMk_X₂_carrier, moduleCatMk_X₂_isAddCommGroup, moduleCatMk_X₂_isModule, moduleCatMk_X₃_carrier, moduleCatMk_X₃_isAddCommGroup, moduleCatMk_X₃_isModule, moduleCatMk_f, moduleCatMk_g, moduleCat_exact_iff, moduleCat_exact_iff_ker_sub_range, moduleCat_exact_iff_range_eq_ker, moduleCat_pOpcycles_eq_iff, moduleCat_pOpcycles_eq_zero_iff, moduleCat_zero_apply, pOpcycles_comp_moduleCatOpcyclesIso_hom, pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, toCycles_moduleCatCyclesIso_hom, toCycles_moduleCatCyclesIso_hom_apply, toCycles_moduleCatCyclesIso_hom_assoc, toCycles_moduleCatCyclesIso_hom_assoc_apply, π_moduleCatCyclesIso_hom, π_moduleCatCyclesIso_hom_apply, π_moduleCatCyclesIso_hom_assoc, π_moduleCatCyclesIso_hom_assoc_apply, shortExact_shortComplexKer, shortComplex_exact, shortComplex_shortExact	62
Total	71

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
moduleCatCyclesIso 📖	CompOp	20 math math: π_moduleCatCyclesIso_hom, moduleCatCyclesIso_hom_i_apply, moduleCatCyclesIso_hom_i_assoc, moduleCatCyclesIso_inv_π_assoc_apply, moduleCatCyclesIso_hom_i, toCycles_moduleCatCyclesIso_hom, π_moduleCatCyclesIso_hom_assoc_apply, moduleCatCyclesIso_hom_i_assoc_apply, π_moduleCatCyclesIso_hom_apply, moduleCatCyclesIso_inv_iCycles, moduleCatCyclesIso_inv_π_assoc, π_moduleCatCyclesIso_hom_assoc, toCycles_moduleCatCyclesIso_hom_apply, moduleCatCyclesIso_inv_iCycles_assoc_apply, moduleCatCyclesIso_inv_π_apply, toCycles_moduleCatCyclesIso_hom_assoc_apply, toCycles_moduleCatCyclesIso_hom_assoc, moduleCatCyclesIso_inv_π, moduleCatCyclesIso_inv_iCycles_assoc, moduleCatCyclesIso_inv_iCycles_apply
moduleCatHomologyIso 📖	CompOp	8 math math: π_moduleCatCyclesIso_hom, moduleCatCyclesIso_inv_π_assoc_apply, π_moduleCatCyclesIso_hom_assoc_apply, π_moduleCatCyclesIso_hom_apply, moduleCatCyclesIso_inv_π_assoc, π_moduleCatCyclesIso_hom_assoc, moduleCatCyclesIso_inv_π_apply, moduleCatCyclesIso_inv_π
moduleCatLeftHomologyData 📖	CompOp	81 math math: groupHomology.π_comp_H2Iso_hom_assoc, π_moduleCatCyclesIso_hom, groupCohomology.toCocycles_comp_isoCocycles₁_hom, moduleCatCyclesIso_hom_i_apply, groupCohomology.π_comp_H1Iso_hom_assoc, groupCohomology.mapCocycles₂_comp_i, moduleCatLeftHomologyData_i_hom, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, groupHomology.π_comp_H1Iso_inv, groupHomology.isoCycles₁_inv_comp_iCycles_apply, groupCohomology.mapCocycles₂_comp_i_assoc, groupHomology.π_comp_H2Iso_inv_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom, groupHomology.mapCycles₁_comp_i, moduleCatCyclesIso_hom_i_assoc, groupHomology.mapCycles₂_comp_i, groupCohomology.π_comp_H1Iso_hom, moduleCatCyclesIso_inv_π_assoc_apply, moduleCatCyclesIso_hom_i, groupHomology.π_comp_H2Iso_hom, groupCohomology.isoCocycles₂_hom_comp_i, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, moduleCatLeftHomologyData_liftK_hom, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.isoCocycles₁_inv_comp_iCocycles, toCycles_moduleCatCyclesIso_hom, groupHomology.π_comp_H1Iso_hom_apply, groupHomology.toCycles_comp_isoCycles₂_hom, π_moduleCatCyclesIso_hom_assoc_apply, moduleCatLeftHomologyData_descH_hom, moduleCatCyclesIso_hom_i_assoc_apply, groupCohomology.mapCocycles₁_comp_i_assoc, groupCohomology.π_comp_H2Iso_hom_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, groupHomology.isoCycles₂_inv_comp_iCycles_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_hom_assoc, π_moduleCatCyclesIso_hom_apply, groupHomology.π_comp_H2Iso_inv, groupCohomology.isoCocycles₂_inv_comp_iCocycles, moduleCatCyclesIso_inv_iCycles, moduleCatLeftHomologyData_f'_hom, groupHomology.mapCycles₂_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i, moduleCatCyclesIso_inv_π_assoc, moduleCatLeftHomologyData_K, groupCohomology.π_comp_H2Iso_hom_apply, groupHomology.isoCycles₁_hom_comp_i_assoc, π_moduleCatCyclesIso_hom_assoc, groupCohomology.π_comp_H1Iso_hom_apply, toCycles_moduleCatCyclesIso_hom_apply, groupHomology.π_comp_H2Iso_hom_apply, moduleCatLeftHomologyData_π_hom, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.toCycles_comp_isoCycles₁_hom, groupHomology.isoCycles₂_hom_comp_i, groupHomology.π_comp_H1Iso_hom, moduleCatLeftHomologyData_H, moduleCatCyclesIso_inv_iCycles_assoc_apply, groupHomology.isoCycles₂_inv_comp_iCycles, moduleCatCyclesIso_inv_π_apply, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, groupHomology.π_comp_H1Iso_inv_apply, toCycles_moduleCatCyclesIso_hom_assoc_apply, groupHomology.isoCycles₁_hom_comp_i, toCycles_moduleCatCyclesIso_hom_assoc, moduleCatCyclesIso_inv_π, groupCohomology.isoCocycles₂_hom_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i_assoc, groupHomology.π_comp_H1Iso_inv_assoc, groupHomology.mapCycles₁_comp_i_assoc, moduleCatCyclesIso_inv_iCycles_assoc, moduleCatCyclesIso_inv_iCycles_apply, groupHomology.π_comp_H2Iso_inv_apply, groupCohomology.mapCocycles₁_comp_i, groupHomology.isoCycles₂_hom_comp_i_assoc, groupCohomology.π_comp_H2Iso_hom, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc
moduleCatMk 📖	CompOp	11 math math: moduleCatMk_X₁_carrier, moduleCatMk_X₁_isAddCommGroup, moduleCatMk_X₂_isModule, moduleCatMk_g, moduleCatMk_X₃_isAddCommGroup, moduleCatMk_X₃_carrier, moduleCatMk_X₁_isModule, moduleCatMk_f, moduleCatMk_X₃_isModule, moduleCatMk_X₂_carrier, moduleCatMk_X₂_isAddCommGroup
moduleCatMkOfKerLERange 📖	CompOp	6 math math: moduleCatMkOfKerLERange_g, moduleCatMkOfKerLERange_X₂, moduleCatMkOfKerLERange_X₃, moduleCatMkOfKerLERange_f, moduleCatMkOfKerLERange_X₁, Exact.moduleCat_of_range_eq_ker
moduleCatOpcyclesIso 📖	CompOp	3 math math: pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, pOpcycles_comp_moduleCatOpcyclesIso_hom, pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc
moduleCatToCycles 📖	CompOp	20 math math: groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.toCycles_comp_isoCycles₁_hom_apply, moduleCatCyclesIso_inv_π_assoc_apply, groupHomology.π_comp_H1Iso_hom_apply, π_moduleCatCyclesIso_hom_assoc_apply, exact_iff_surjective_moduleCatToCycles, groupHomology.toCycles_comp_isoCycles₂_hom_apply, π_moduleCatCyclesIso_hom_apply, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, moduleCatLeftHomologyData_f'_hom, groupCohomology.π_comp_H2Iso_hom_apply, groupCohomology.π_comp_H1Iso_hom_apply, toCycles_moduleCatCyclesIso_hom_apply, groupHomology.π_comp_H2Iso_hom_apply, moduleCatLeftHomologyData_π_hom, moduleCatLeftHomologyData_H, moduleCatCyclesIso_inv_π_apply, groupHomology.π_comp_H1Iso_inv_apply, toCycles_moduleCatCyclesIso_hom_assoc_apply, groupHomology.π_comp_H2Iso_inv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_iff_surjective_moduleCatToCycles 📖	mathematical	—	Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ModuleCat.carrier X₁ X₂ Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom g DFunLike.coe LinearMap Submodule.addCommMonoid Submodule.module LinearMap.instFunLike moduleCatToCycles	—	LeftHomologyData.exact_iff_epi_f' CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier 📖	mathematical	—	CategoryTheory.Functor.PreservesHomology ModuleCat Ab ModuleCat.moduleCategory AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddCommGrpCat.instPreadditive CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier ModuleCat.hasForgetToAddCommGroup CategoryTheory.Functor.preservesZeroMorphisms_of_additive ModuleCat.forget₂_addCommGrp_additive	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ModuleCat.forget₂_addCommGrp_additive ModuleCat.forget₂AddCommGroup_preservesLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier AddCommGrpCat.hasColimit
moduleCatCyclesIso_hom_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian LeftHomologyData.K moduleCatLeftHomologyData X₂ CategoryTheory.Iso.hom moduleCatCyclesIso LeftHomologyData.i iCycles	—	LeftHomologyData.cyclesIso_hom_comp_i hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
moduleCatCyclesIso_hom_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g LeftHomologyData.K moduleCatLeftHomologyData LinearMap.instFunLike Submodule.subtype cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of Submodule.addCommGroup Submodule.module CategoryTheory.Iso.hom moduleCatCyclesIso iCycles	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise moduleCatCyclesIso_hom_i
moduleCatCyclesIso_hom_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian LeftHomologyData.K moduleCatLeftHomologyData CategoryTheory.Iso.hom moduleCatCyclesIso X₂ LeftHomologyData.i iCycles	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' moduleCatCyclesIso_hom_i
moduleCatCyclesIso_hom_i_assoc_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier Submodule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g LeftHomologyData.K moduleCatLeftHomologyData Submodule.subtype cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian ModuleCat.of Submodule.addCommGroup Submodule.module CategoryTheory.Iso.hom moduleCatCyclesIso iCycles	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise moduleCatCyclesIso_hom_i_assoc
moduleCatCyclesIso_inv_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatLeftHomologyData cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian X₂ CategoryTheory.Iso.inv moduleCatCyclesIso iCycles LeftHomologyData.i	—	LeftHomologyData.cyclesIso_inv_comp_iCycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
moduleCatCyclesIso_inv_iCycles_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian X₂ AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier iCycles Submodule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g LeftHomologyData.K moduleCatLeftHomologyData ModuleCat.of Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv moduleCatCyclesIso Submodule.subtype	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise moduleCatCyclesIso_inv_iCycles
moduleCatCyclesIso_inv_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatLeftHomologyData cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian CategoryTheory.Iso.inv moduleCatCyclesIso X₂ iCycles LeftHomologyData.i	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' moduleCatCyclesIso_inv_iCycles
moduleCatCyclesIso_inv_iCycles_assoc_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian iCycles Submodule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g LeftHomologyData.K moduleCatLeftHomologyData ModuleCat.of Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv moduleCatCyclesIso Submodule.subtype	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise moduleCatCyclesIso_inv_iCycles_assoc
moduleCatCyclesIso_inv_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatLeftHomologyData cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian homology CategoryTheory.Iso.inv moduleCatCyclesIso homologyπ LeftHomologyData.H LeftHomologyData.π moduleCatHomologyIso	—	LeftHomologyData.π_comp_homologyIso_inv CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
moduleCatCyclesIso_inv_π_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian homology AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier homologyπ X₂ Submodule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g LeftHomologyData.K moduleCatLeftHomologyData ModuleCat.of Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv moduleCatCyclesIso HasQuotient.Quotient Submodule.addCommMonoid Submodule.hasQuotient LinearMap.range X₁ moduleCatToCycles LeftHomologyData.H Submodule.Quotient.addCommGroup Submodule.Quotient.module moduleCatHomologyIso Submodule.mkQ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian hasLeftHomology_of_hasHomology CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise moduleCatCyclesIso_inv_π
moduleCatCyclesIso_inv_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatLeftHomologyData cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian CategoryTheory.Iso.inv moduleCatCyclesIso homology homologyπ LeftHomologyData.H LeftHomologyData.π moduleCatHomologyIso	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' moduleCatCyclesIso_inv_π
moduleCatCyclesIso_inv_π_assoc_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier homology ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier cycles hasLeftHomology_of_hasHomology homologyπ X₂ Submodule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g LeftHomologyData.K moduleCatLeftHomologyData ModuleCat.of Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv moduleCatCyclesIso HasQuotient.Quotient Submodule.addCommMonoid Submodule.hasQuotient LinearMap.range X₁ moduleCatToCycles LeftHomologyData.H Submodule.Quotient.addCommGroup Submodule.Quotient.module moduleCatHomologyIso Submodule.mkQ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian hasLeftHomology_of_hasHomology CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise moduleCatCyclesIso_inv_π_assoc
moduleCatLeftHomologyData_H 📖	mathematical	—	LeftHomologyData.H ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatLeftHomologyData ModuleCat.of HasQuotient.Quotient ModuleCat.carrier X₂ Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range X₁ moduleCatToCycles Submodule.Quotient.addCommGroup Submodule.Quotient.module	—	—
moduleCatLeftHomologyData_K 📖	mathematical	—	LeftHomologyData.K ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatLeftHomologyData ModuleCat.of ModuleCat.carrier X₂ Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom g Submodule.addCommGroup Submodule.module	—	—
moduleCatLeftHomologyData_descH_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive LeftHomologyData.K moduleCatLeftHomologyData LeftHomologyData.f' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	ModuleCat.Hom.hom LeftHomologyData.H ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatLeftHomologyData LeftHomologyData.descH Submodule.liftQ ModuleCat.carrier LeftHomologyData.K ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.range X₁ Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LeftHomologyData.f' Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.ker LinearMap LinearMap.comp RingHomCompTriple.ids LinearMap.instZero LinearMap.range_le_ker_iff Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe LinearMap.instFunLike ModuleCat.hom_ext_iff	—	—
moduleCatLeftHomologyData_f'_hom 📖	mathematical	—	ModuleCat.Hom.hom X₁ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive LeftHomologyData.K moduleCatLeftHomologyData LeftHomologyData.f' moduleCatToCycles	—	—
moduleCatLeftHomologyData_i_hom 📖	mathematical	—	ModuleCat.Hom.hom ModuleCat.of ModuleCat.carrier X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ RingHom.id Semiring.toNonAssocSemiring g Submodule.addCommGroup Submodule.module LeftHomologyData.i moduleCatLeftHomologyData Submodule.subtype	—	—
moduleCatLeftHomologyData_liftK_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	ModuleCat.Hom.hom LeftHomologyData.K ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatLeftHomologyData LeftHomologyData.liftK LinearMap.codRestrict ModuleCat.carrier X₂ Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring LinearMap.ker X₃ g Submodule SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap LinearMap.instFunLike Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp ModuleCat.instZeroHom CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—
moduleCatLeftHomologyData_π_hom 📖	mathematical	—	ModuleCat.Hom.hom ModuleCat.of ModuleCat.carrier X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ RingHom.id Semiring.toNonAssocSemiring g Submodule.addCommGroup Submodule.module HasQuotient.Quotient Submodule.addCommMonoid Submodule.hasQuotient LinearMap.range X₁ moduleCatToCycles Submodule.Quotient.addCommGroup Submodule.Quotient.module LeftHomologyData.π moduleCatLeftHomologyData Submodule.mkQ	—	—
moduleCatMkOfKerLERange_X₁ 📖	mathematical	Submodule ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom LinearMap.ker	X₁ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMkOfKerLERange	—	RingHomSurjective.ids
moduleCatMkOfKerLERange_X₂ 📖	mathematical	Submodule ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom LinearMap.ker	X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMkOfKerLERange	—	RingHomSurjective.ids
moduleCatMkOfKerLERange_X₃ 📖	mathematical	Submodule ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom LinearMap.ker	X₃ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMkOfKerLERange	—	RingHomSurjective.ids
moduleCatMkOfKerLERange_f 📖	mathematical	Submodule ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom LinearMap.ker	f ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMkOfKerLERange	—	RingHomSurjective.ids
moduleCatMkOfKerLERange_g 📖	mathematical	Submodule ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom LinearMap.ker	g ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMkOfKerLERange	—	RingHomSurjective.ids
moduleCatMk_X₁_carrier 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.carrier X₁ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_X₁_isAddCommGroup 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.isAddCommGroup X₁ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_X₁_isModule 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.isModule X₁ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_X₂_carrier 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.carrier X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_X₂_isAddCommGroup 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.isAddCommGroup X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_X₂_isModule 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.isModule X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_X₃_carrier 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.carrier X₃ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_X₃_isAddCommGroup 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.isAddCommGroup X₃ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_X₃_isModule 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	ModuleCat.isModule X₃ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk	—	RingHomCompTriple.ids
moduleCatMk_f 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	f ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk ModuleCat.ofHom	—	RingHomCompTriple.ids
moduleCatMk_g 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap LinearMap.instZero	g ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive moduleCatMk ModuleCat.ofHom	—	RingHomCompTriple.ids
moduleCat_exact_iff 📖	mathematical	—	Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ModuleCat.carrier X₁ DFunLike.coe X₂ CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier f	—	exact_iff_of_hasForget ModuleCat.forget₂_addCommGrp_additive instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
moduleCat_exact_iff_ker_sub_range 📖	mathematical	—	Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive Submodule ModuleCat.carrier X₂ Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.ker X₃ RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom g LinearMap.range X₁ RingHomSurjective.ids f	—	RingHomSurjective.ids moduleCat_exact_iff
moduleCat_exact_iff_range_eq_ker 📖	mathematical	—	Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive LinearMap.range ModuleCat.carrier X₁ X₂ Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom f LinearMap.ker X₃ g	—	RingHomSurjective.ids moduleCat_exact_iff_ker_sub_range Submodule.ext moduleCat_zero_apply instReflLe
moduleCat_pOpcycles_eq_iff 📖	mathematical	—	DFunLike.coe X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive opcycles hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier pOpcycles Submodule SetLike.instMembership Submodule.setLike LinearMap.range X₁ RingHomSurjective.ids ModuleCat.Hom.hom f SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian RingHomSurjective.ids pOpcycles_comp_moduleCatOpcyclesIso_hom_apply ModuleCat.mono_iff_injective CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom Submodule.Quotient.eq
moduleCat_pOpcycles_eq_zero_iff 📖	mathematical	—	DFunLike.coe X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive opcycles hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier pOpcycles NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule SetLike.instMembership Submodule.setLike LinearMap.range X₁ RingHomSurjective.ids ModuleCat.Hom.hom f	—	hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian RingHomSurjective.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_zero moduleCat_pOpcycles_eq_iff
moduleCat_zero_apply 📖	mathematical	—	DFunLike.coe X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive X₃ ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier g X₁ f NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	zero_apply CategoryTheory.Functor.preservesZeroMorphisms_of_additive ModuleCat.forget₂_addCommGrp_additive
pOpcycles_comp_moduleCatOpcyclesIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive opcycles hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian ModuleCat.of HasQuotient.Quotient ModuleCat.carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Submodule.hasQuotient LinearMap.range X₁ RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom f Submodule.Quotient.addCommGroup Submodule.Quotient.module pOpcycles CategoryTheory.Iso.hom moduleCatOpcyclesIso ModuleCat.ofHom Submodule.mkQ	—	RingHomSurjective.ids hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian p_descOpcycles_assoc ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom
pOpcycles_comp_moduleCatOpcyclesIso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier opcycles ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HasQuotient.Quotient X₂ Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Submodule.hasQuotient LinearMap.range X₁ RingHomSurjective.ids ModuleCat.Hom.hom f ModuleCat.of Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom moduleCatOpcyclesIso pOpcycles	—	RingHomSurjective.ids hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise pOpcycles_comp_moduleCatOpcyclesIso_hom
pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive opcycles hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian pOpcycles ModuleCat.of HasQuotient.Quotient ModuleCat.carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Submodule.hasQuotient LinearMap.range X₁ RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom f Submodule.Quotient.addCommGroup Submodule.Quotient.module CategoryTheory.Iso.hom moduleCatOpcyclesIso ModuleCat.ofHom Submodule.mkQ	—	RingHomSurjective.ids hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_comp_moduleCatOpcyclesIso_hom
toCycles_moduleCatCyclesIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian LeftHomologyData.K moduleCatLeftHomologyData toCycles CategoryTheory.Iso.hom moduleCatCyclesIso LeftHomologyData.f'	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono LeftHomologyData.instMonoI CategoryTheory.Category.assoc moduleCatCyclesIso_hom_i toCycles_i LeftHomologyData.f'_i
toCycles_moduleCatCyclesIso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian X₂ Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g LeftHomologyData.K moduleCatLeftHomologyData LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of Submodule.addCommGroup Submodule.module CategoryTheory.Iso.hom moduleCatCyclesIso X₁ toCycles moduleCatToCycles	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toCycles_moduleCatCyclesIso_hom
toCycles_moduleCatCyclesIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian toCycles LeftHomologyData.K moduleCatLeftHomologyData CategoryTheory.Iso.hom moduleCatCyclesIso LeftHomologyData.f'	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_moduleCatCyclesIso_hom
toCycles_moduleCatCyclesIso_hom_assoc_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g LeftHomologyData.K moduleCatLeftHomologyData LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of Submodule.addCommGroup Submodule.module cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian CategoryTheory.Iso.hom moduleCatCyclesIso X₁ toCycles moduleCatToCycles	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toCycles_moduleCatCyclesIso_hom_assoc
π_moduleCatCyclesIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian homology LeftHomologyData.H moduleCatLeftHomologyData homologyπ CategoryTheory.Iso.hom moduleCatHomologyIso LeftHomologyData.K moduleCatCyclesIso LeftHomologyData.π	—	LeftHomologyData.homologyπ_comp_homologyIso_hom CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
π_moduleCatCyclesIso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier homology ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HasQuotient.Quotient X₂ Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range X₁ moduleCatToCycles LeftHomologyData.H moduleCatLeftHomologyData LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of Submodule.Quotient.addCommGroup Submodule.Quotient.module CategoryTheory.Iso.hom moduleCatHomologyIso cycles hasLeftHomology_of_hasHomology homologyπ LeftHomologyData.K Submodule.mkQ moduleCatCyclesIso	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_moduleCatCyclesIso_hom
π_moduleCatCyclesIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian homology homologyπ LeftHomologyData.H moduleCatLeftHomologyData CategoryTheory.Iso.hom moduleCatHomologyIso LeftHomologyData.K moduleCatCyclesIso LeftHomologyData.π	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_moduleCatCyclesIso_hom
π_moduleCatCyclesIso_hom_assoc_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient ModuleCat.carrier X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker X₃ ModuleCat.Hom.hom g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range X₁ moduleCatToCycles LeftHomologyData.H moduleCatLeftHomologyData LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of Submodule.Quotient.addCommGroup Submodule.Quotient.module homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian CategoryTheory.Iso.hom moduleCatHomologyIso cycles hasLeftHomology_of_hasHomology homologyπ LeftHomologyData.K Submodule.mkQ moduleCatCyclesIso	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_moduleCatCyclesIso_hom_assoc

CategoryTheory.ShortComplex.Exact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moduleCat_of_range_eq_ker 📖	mathematical	LinearMap.range ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom LinearMap.ker	CategoryTheory.ShortComplex.Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.moduleCatMkOfKerLERange	—	RingHomSurjective.ids
moduleCat_range_eq_ker 📖	mathematical	CategoryTheory.ShortComplex.Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	LinearMap.range ModuleCat.carrier CategoryTheory.ShortComplex.X₁ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.X₂ Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom CategoryTheory.ShortComplex.f LinearMap.ker CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	RingHomSurjective.ids

CategoryTheory.ShortComplex.ShortExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moduleCat_exact_iff_function_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive Function.Exact ModuleCat.carrier CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.g NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	RingHomSurjective.ids CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker LinearMap.exact_iff
moduleCat_injective_f 📖	mathematical	CategoryTheory.ShortComplex.ShortExact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	ModuleCat.carrier CategoryTheory.ShortComplex.X₁ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.X₂ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.ShortComplex.f	—	injective_f ModuleCat.forget₂_addCommGrp_additive CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier ModuleCat.instHasZeroObject
moduleCat_surjective_g 📖	mathematical	CategoryTheory.ShortComplex.ShortExact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	ModuleCat.carrier CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.X₃ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.ShortComplex.g	—	surjective_g ModuleCat.forget₂_addCommGrp_additive CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier ModuleCat.instHasZeroObject

LinearMap

Definitions

Name	Category	Theorems
shortComplexKer 📖	CompOp	1 math math: shortExact_shortComplexKer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shortExact_shortComplexKer 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	CategoryTheory.ShortComplex.ShortExact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexKer	—	CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact Subtype.range_coe_subtype ModuleCat.mono_iff_injective Submodule.injective_subtype ModuleCat.epi_iff_surjective

ModuleCat

Definitions

Name	Category	Theorems
shortComplexOfCompEqZero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shortComplex_exact 📖	mathematical	Function.Exact carrier CategoryTheory.ShortComplex.X₁ ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.g NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CategoryTheory.ShortComplex.Exact ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	—	CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact
shortComplex_shortExact 📖	mathematical	Function.Exact carrier CategoryTheory.ShortComplex.X₁ ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.g NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CategoryTheory.ShortComplex.ShortExact ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	—	CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact mono_iff_injective epi_iff_surjective

---

← Back to Index