Abelian

📁 Source: Mathlib/Algebra/Category/ModuleCat/Abelian.lean

Statistics

Metric	Count
Definitions abelian, normalEpi, normalMono	3
Theorems forget_reflectsLimits, forget_reflectsLimitsOfSize, forget₂_reflectsLimits, forget₂_reflectsLimitsOfSize, instHasLimitsOfSize	5
Total	8

ModuleCat

Definitions

Name	Category	Theorems
abelian 📖	CompOp	66 math math: CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom, CategoryTheory.projectiveDimension_eq_of_semiLinearEquiv, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply, injectiveDimension_eq_iSup_localizedModule_prime, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, groupCohomology.mapShortComplex₃_exact, hasInjectiveDimensionLE_iff_forall_maximalSpectrum, postcomp_extClass_surjective_of_projective_X₂, imageIsoRange_hom_subtype, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom, imageIsoRange_inv_image_ι_apply, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc, CategoryTheory.projectiveDimension_eq_of_linearEquiv, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_zero_iff, groupHomology.mapShortComplex₃_exact, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, localizedModule_hasProjectiveDimensionLE, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i, precomp_extClass_surjective_of_projective_X₂, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, instHasExtModuleCatOfSmall, imageIsoRange_hom_subtype_assoc, CategoryTheory.hasProjectiveDimensionLE_of_semiLinearEquiv, hasInjectiveDimensionLE_iff_forall_primeSpectrum, Rep.Tor_map, imageIsoRange_inv_image_ι, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, imageIsoRange_inv_image_ι_assoc, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc_apply, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, projectiveDimension_le_projectiveDimension_of_isLocalizedModule, groupCohomology.mapShortComplex₁_exact, hasProjectiveDimensionLE_iff_forall_primeSpectrum, groupHomology.pOpcycles_comp_opcyclesIso_hom, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, hasProjectiveDimensionLE_iff_forall_maximalSpectrum, groupHomology.mapShortComplex₁_exact, injectiveDimension_le_injectiveDimension_of_isLocalizedModule, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles, projectiveDimension_eq_iSup_localizedModule_maximal, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc, finite_ext, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, CategoryTheory.hasProjectiveDimensionLE_of_linearEquiv, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply, instIsGrothendieckAbelianModuleCat, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc, projectiveDimension_eq_iSup_localizedModule_prime, imageIsoRange_hom_subtype_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π, injectiveDimension_eq_iSup_localizedModule_maximal, Rep.Tor_obj, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply, localizedModule_hasInjectiveDimensionLE
normalEpi 📖	CompOp	—
normalMono 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_reflectsLimits 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimits ModuleCat moduleCategory CategoryTheory.types CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier	—	forget_reflectsLimitsOfSize
forget_reflectsLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfSize ModuleCat moduleCategory CategoryTheory.types CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier	—	CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms instReflectsIsomorphismsForgetLinearMapIdCarrier instHasLimitsOfSize forget_preservesLimitsOfSize univLE_of_max UnivLE.self
forget₂_reflectsLimits 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimits ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	forget₂_reflectsLimitsOfSize
forget₂_reflectsLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfSize ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier instHasLimitsOfSize forget₂AddCommGroup_preservesLimitsOfSize univLE_of_max UnivLE.self
instHasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize ModuleCat moduleCategory	—	hasLimitsOfSize univLE_of_max UnivLE.self

---

← Back to Index