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	62 math math: CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, groupCohomology.mapShortComplex₃_exact, postcomp_extClass_surjective_of_projective_X₂, imageIsoRange_hom_subtype, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom, Rep.standardComplex.εToSingle₀_comp_eq, imageIsoRange_inv_image_ι_apply, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_zero_iff, Rep.barResolution_complex, groupHomology.mapShortComplex₃_exact, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i, precomp_extClass_surjective_of_projective_X₂, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, instHasExtModuleCatOfSmall, imageIsoRange_hom_subtype_assoc, 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₀, groupCohomology.mapShortComplex₁_exact, groupHomology.pOpcycles_comp_opcyclesIso_hom, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, inhomogeneousCochains.d_eq, Rep.FiniteCyclicGroup.resolution_complex, groupHomology.mapShortComplex₁_exact, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, Rep.standardComplex.instQuasiIsoNatεToSingle₀, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc, finite_ext, Rep.FiniteCyclicGroup.resolution_quasiIso, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply, instIsGrothendieckAbelianModuleCat, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, imageIsoRange_hom_subtype_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π, Rep.Tor_obj, Rep.FiniteCyclicGroup.resolution_π, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply, Rep.FiniteCyclicGroup.resolution.π_f, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
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