Documentation Verification Report

Preadditive

📁 Source: Mathlib/Algebra/Category/Grp/Preadditive.lean

Statistics

MetricCount
DefinitionshomAddEquiv, instAddCommGroupHom, instAddHom, instNegHom, instPreadditive, instSMulIntHom, instSMulNatHom, instSubHom, instZeroHom_1
9
TheoremshomAddEquiv_apply, homAddEquiv_symm_apply_hom, hom_add, hom_add_apply, hom_neg, hom_nsmul, hom_sub, hom_zero, hom_zsmul
9
Total18

AddCommGrpCat

Definitions

NameCategoryTheorems
homAddEquiv 📖CompOp
2 mathmath: homAddEquiv_symm_apply_hom, homAddEquiv_apply
instAddCommGroupHom 📖CompOp—
instAddHom 📖CompOp
6 mathmath: hom_add, homAddEquiv_symm_apply_hom, biprodIsoProd_inv_comp_desc, AlgebraicGeometry.Scheme.Modules.Hom.add_app, hom_add_apply, homAddEquiv_apply
instNegHom 📖CompOp
1 mathmath: hom_neg
instPreadditive 📖CompOp
80 mathmath: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, biproductIsoPi_inv_comp_π_apply, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁', CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, CochainComplex.HomComplex.leftHomologyData_K_coe, CochainComplex.HomComplex.leftHomologyData'_i, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, CategoryTheory.ShortComplex.abToCycles_apply_coe, CochainComplex.HomComplex.leftHomologyData_π_hom_apply, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂', CochainComplex.HomComplex.leftHomologyData_i_hom_apply, ModuleCat.smul_naturality, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc, uliftFunctor_additive, instHasFiniteBiproducts, CategoryTheory.ShortComplex.abLeftHomologyData_π, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁', CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃', CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles, biprodIsoProd_inv_comp_snd_apply, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, CategoryTheory.additive_yonedaObj', SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, CategoryTheory.ShortComplex.abLeftHomologyData_K_coe, CategoryTheory.Abelian.instAdditiveAddCommGrpCatExtFunctorObj, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, ModuleCat.smulNatTrans_apply_app, CategoryTheory.Abelian.Ext.covariantSequence_exact, CategoryTheory.additive_coyonedaObj', CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range, CategoryTheory.ShortComplex.abLeftHomologyData_f', kernelIsoKer_inv_comp_ι, CategoryTheory.Abelian.Ext.covariant_sequence_exact₂', CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod, ModuleCat.HasColimit.coconePointSMul_apply, CategoryTheory.ShortComplex.ab_exact_iff, CategoryTheory.ShortComplex.abLeftHomologyData_i, CategoryTheory.Abelian.instAdditiveOppositeFunctorAddCommGrpCatExtFunctor, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, ModuleCat.mkOfSMul_smul, biprodIsoProd_inv_comp_desc, biprodIsoProd_inv_comp_snd, biprodIsoProd_inv_comp_desc_apply, CochainComplex.HomComplex.leftHomologyData_H_coe, CochainComplex.HomComplex.leftHomologyData'_K_coe, biprodIsoProd_inv_comp_fst_apply, instPreservesHomologyFunctorAddCommGrpCatColim, biproductIsoPi_inv_comp_π, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc, CategoryTheory.ShortComplex.ab_zero_apply, ModuleCat.forget₂_addCommGrp_additive, biprodIsoProd_inv_comp_fst, CochainComplex.HomComplex_X, CochainComplex.HomComplex.leftHomologyData'_H_coe, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, kernelIsoKer_hom_comp_subtype, CochainComplex.HomComplex.leftHomologyData'_π, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃', CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ, CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished, CategoryTheory.ShortComplex.abLeftHomologyData_H_coe, PresheafOfModules.instAdditiveFunctorOppositeAbToPresheaf, CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂, CategoryTheory.Abelian.Ext.contravariantSequence_exact, CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, instHasBinaryBiproducts, CochainComplex.HomComplex_d_hom_apply, CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact
instSMulIntHom 📖CompOp
1 mathmath: hom_zsmul
instSMulNatHom 📖CompOp
1 mathmath: hom_nsmul
instSubHom 📖CompOp
2 mathmath: hom_sub, AlgebraicGeometry.Scheme.Modules.Hom.sub_app
instZeroHom_1 📖CompOp
8 mathmath: hom_zero, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ

Theorems

NameKindAssumesProvesValidatesDepends On
homAddEquiv_apply 📖mathematical—DFunLike.coe
AddEquiv
Quiver.Hom
AddCommGrpCat
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instCategory
AddMonoidHom
carrier
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
instAddHom
AddMonoidHom.add
AddCommGroup.toAddCommMonoid
EquivLike.toFunLike
AddEquiv.instEquivLike
homAddEquiv
CategoryTheory.ConcreteCategory.hom
CategoryTheory.ToHom
AddMonoidHom.instFunLike
instConcreteCategoryAddMonoidHomCarrier		——
homAddEquiv_symm_apply_hom 📖mathematical—Hom.hom
DFunLike.coe
AddEquiv
AddMonoidHom
carrier
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
Quiver.Hom
AddCommGrpCat
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instCategory
AddMonoidHom.add
AddCommGroup.toAddCommMonoid
instAddHom
EquivLike.toFunLike
AddEquiv.instEquivLike
AddEquiv.symm
homAddEquiv		——
hom_add 📖mathematical—Hom.hom
Quiver.Hom
AddCommGrpCat
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instCategory
instAddHom
AddMonoidHom
carrier
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
AddMonoidHom.add
AddCommGroup.toAddCommMonoid		——
hom_add_apply 📖mathematical—DFunLike.coe
carrier
CategoryTheory.ConcreteCategory.hom
AddCommGrpCat
instCategory
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
AddMonoidHom.instFunLike
instConcreteCategoryAddMonoidHomCarrier
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instAddHom
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
AddCommGroup.toAddCommMonoid		——
hom_neg 📖mathematical—Hom.hom
Quiver.Hom
AddCommGrpCat
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instCategory
instNegHom
AddMonoidHom
carrier
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
AddMonoidHom.instNeg		——
hom_nsmul 📖mathematical—Hom.hom
Quiver.Hom
AddCommGrpCat
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instCategory
instSMulNatHom
AddMonoidHom
carrier
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
AddMonoidHom.instNatSMul
AddCommGroup.toAddCommMonoid		——
hom_sub 📖mathematical—Hom.hom
Quiver.Hom
AddCommGrpCat
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instCategory
instSubHom
AddMonoidHom
carrier
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
AddMonoidHom.instSub		——
hom_zero 📖mathematical—Hom.hom
Quiver.Hom
AddCommGrpCat
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instCategory
instZeroHom_1
AddMonoidHom
carrier
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
instZeroAddMonoidHom		——
hom_zsmul 📖mathematical—Hom.hom
Quiver.Hom
AddCommGrpCat
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
instCategory
instSMulIntHom
AddMonoidHom
carrier
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
str
AddMonoidHom.instIntSMul		——

---

← Back to Index