ModuleCat

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

Statistics

Metric	Count
Definitions moduleCatCyclesIso, moduleCatHomologyIso, moduleCatLeftHomologyData, moduleCatMk, moduleCatMkOfKerLERange, moduleCatOpcyclesIso, moduleCatToCycles, shortComplexKer	8
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	60
Total	68

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	60 math math: groupHomology.π_comp_H2Iso_hom_assoc, π_moduleCatCyclesIso_hom, groupCohomology.toCocycles_comp_isoCocycles₁_hom, groupCohomology.π_comp_H1Iso_hom_assoc, groupCohomology.mapCocycles₂_comp_i, moduleCatLeftHomologyData_i_hom, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, groupHomology.π_comp_H1Iso_inv, 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_hom_i, groupHomology.π_comp_H2Iso_hom, groupCohomology.isoCocycles₂_hom_comp_i, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, moduleCatLeftHomologyData_liftK_hom, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₁_inv_comp_iCocycles, toCycles_moduleCatCyclesIso_hom, groupHomology.toCycles_comp_isoCycles₂_hom, groupCohomology.mapCocycles₁_comp_i_assoc, groupCohomology.π_comp_H2Iso_hom_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_hom_assoc, 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, groupHomology.isoCycles₁_hom_comp_i_assoc, π_moduleCatCyclesIso_hom_assoc, moduleCatLeftHomologyData_π_hom, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.toCycles_comp_isoCycles₁_hom, groupHomology.isoCycles₂_hom_comp_i, groupHomology.π_comp_H1Iso_hom, moduleCatLeftHomologyData_H, groupHomology.isoCycles₂_inv_comp_iCycles, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, 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, 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	—	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 ModuleCat.Hom.hom g DFunLike.coe LinearMap cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian Submodule.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of 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 cycles hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian Submodule.addCommGroup Submodule.module ModuleCat.of 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 Submodule.addCommGroup Submodule.module ModuleCat.of CategoryTheory.Iso.inv moduleCatCyclesIso	—	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 Submodule.addCommGroup Submodule.module ModuleCat.of CategoryTheory.Iso.inv moduleCatCyclesIso	—	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 Submodule.addCommGroup Submodule.module ModuleCat.of CategoryTheory.Iso.inv moduleCatCyclesIso HasQuotient.Quotient Submodule.addCommMonoid Submodule.hasQuotient LinearMap.range X₁ moduleCatToCycles Submodule.Quotient.addCommGroup Submodule.Quotient.module moduleCatHomologyIso	—	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 Submodule.addCommGroup Submodule.module ModuleCat.of CategoryTheory.Iso.inv moduleCatCyclesIso HasQuotient.Quotient Submodule.addCommMonoid Submodule.hasQuotient LinearMap.range X₁ moduleCatToCycles Submodule.Quotient.addCommGroup Submodule.Quotient.module moduleCatHomologyIso	—	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 LeftHomologyData.descH Submodule.liftQ ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.range Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.ker LinearMap LinearMap.comp RingHomCompTriple.ids LinearMap.instZero LinearMap.range_le_ker_iff 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 moduleCatLeftHomologyData LeftHomologyData.liftK LinearMap.codRestrict ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring LinearMap.ker Submodule SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap LinearMap.instFunLike 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 DFunLike.coe X₁ X₂ ModuleCat.carrier 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
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 Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of 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 Submodule.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of 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 Submodule.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of 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 Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom moduleCatHomologyIso cycles hasLeftHomology_of_hasHomology homologyπ 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 Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian CategoryTheory.Iso.hom moduleCatHomologyIso cycles hasLeftHomology_of_hasHomology homologyπ 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₁ 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₁ 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₂ 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

---

← Back to Index