Documentation Verification Report

ConcreteCategory

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

Statistics

Metric	Count
Definitions `cyclesMk`	1
Theorems `epi_iff_surjective`, `epi_iff_surjective'`, `mono_iff_injective`, `mono_iff_injective'`, `injective_f`, `surjective_g`, `δ_apply`, `δ_apply'`, `exact_iff_exact_map_forget₂`, `exact_iff_of_hasForget`, `i_cyclesMk`, `zero_apply`	12
Total	13

CategoryTheory.Preadditive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `AddCommGrpCat.carrier` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `AddCommGrpCat.epi_iff_surjective` `CategoryTheory.Functor.map_epi` `CategoryTheory.Functor.instPreservesEpimorphisms` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `CategoryTheory.forget₂_faithful`
`epi_iff_surjective'` 📖	mathematical	—	`CategoryTheory.Epi` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.RespectsIso.epimorphisms` `CategoryTheory.HasForget₂.forget_comp`
`mono_iff_injective` 📖	mathematical	—	`CategoryTheory.Mono` `AddCommGrpCat.carrier` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `AddCommGrpCat.mono_iff_injective` `CategoryTheory.Functor.map_mono` `CategoryTheory.Functor.instPreservesMonomorphisms` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.forget₂_faithful`
`mono_iff_injective'` 📖	mathematical	—	`CategoryTheory.Mono` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.RespectsIso.monomorphisms` `CategoryTheory.HasForget₂.forget_comp`

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
`cyclesMk` 📖	CompOp	1 math math: `i_cyclesMk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_iff_exact_map_forget₂` 📖	mathematical	—	`Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Ab` `AddCommGrpCat.instCategory` `AddCommGrpCat.instPreadditive` `map` `CategoryTheory.forget₂` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `exact_map_iff_of_faithful` `CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf` `CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf` `CategoryTheory.forget₂_faithful`
`exact_iff_of_hasForget` 📖	mathematical	—	`Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `DFunLike.coe` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `X₁` `X₂` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `f`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `exact_iff_exact_map_forget₂` `ab_exact_iff`
`i_cyclesMk` 📖	mathematical	`DFunLike.coe` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `X₃` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `g` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`cycles` `hasLeftHomology_of_hasHomology` `iCycles` `cyclesMk`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `hasLeftHomology_of_hasHomology` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `abCyclesIso_inv_apply_iCycles` `CategoryTheory.ConcreteCategory.comp_apply` `hasLeftHomology_of_preserves` `CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf` `mapCyclesIso_hom_iCycles`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `X₂` `X₃` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `g` `X₁` `f` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`CategoryTheory.ConcreteCategory.comp_apply` `CategoryTheory.Functor.map_comp` `zero` `CategoryTheory.Functor.map_zero`

CategoryTheory.ShortComplex.ShortExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_f` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`AddCommGrpCat.carrier` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₂` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.f`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Preadditive.mono_iff_injective` `mono_f`
`surjective_g` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`AddCommGrpCat.carrier` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.X₃` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.g`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Preadditive.epi_iff_surjective` `epi_g`

CategoryTheory.ShortComplex.SnakeInput

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`δ_apply` 📖	mathematical	`DFunLike.coe` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.ShortComplex.g` `L₀` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `CategoryTheory.ShortComplex.X₁` `L₂` `CategoryTheory.ShortComplex.f` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂`	`L₃` `δ` `CategoryTheory.ShortComplex.Hom.τ₁` `v₂₃`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Abelian.has_finite_products` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.HasForget₂.forget_comp` `CategoryTheory.Limits.comp_preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.congr_fun` `snd_δ` `CategoryTheory.Limits.Concrete.pullbackMk_fst` `CategoryTheory.Limits.Concrete.pullbackMk_snd` `CategoryTheory.ConcreteCategory.comp_apply` `CategoryTheory.congr_arg` `CategoryTheory.Preadditive.mono_iff_injective'` `mono_L₂_f` `φ₁_L₂_f`
`δ_apply'` 📖	mathematical	`DFunLike.coe` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.g` `L₀` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `CategoryTheory.ShortComplex.X₁` `L₂` `CategoryTheory.ShortComplex.f` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂`	`L₃` `δ` `CategoryTheory.ShortComplex.Hom.τ₁` `v₂₃`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.HasForget₂.forget_comp` `CategoryTheory.mono_iff_injective` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.Functor.instIsSplitMonoApp` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.ConcreteCategory.congr_hom` `CategoryTheory.NatTrans.naturality` `δ_apply`

---

← Back to Index