Documentation Verification Report

ShortExact

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

Statistics

Metric	Count
Definitions `ShortExact`, `fIsKernel`, `gIsCokernel`, `splittingOfInjective`, `splittingOfProjective`	5
Theorems `shortExact`, `epi_g`, `exact`, `isIso_f_iff`, `isIso_g_iff`, `map`, `map_of_exact`, `mk'`, `mono_f`, `op`, `unop`, `shortExact`, `isIso₂_of_shortExact_of_isIso₁₃`, `isIso₂_of_shortExact_of_isIso₁₃'`, `shortExact_iff_of_iso`, `shortExact_iff_op`, `shortExact_iff_unop`, `shortExact_of_iso`	18
Total	23

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
`ShortExact` 📖	CompData	15 math math: `shortExact_iff_op`, `ModuleCat.shortExact_projectiveShortComplex`, `CategoryTheory.InjectivePresentation.shortExact_shortComplex`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact`, `LinearMap.shortExact_shortComplexKer`, `ShortExact.mk'`, `Exact.shortExact`, `shortExact_iff_of_iso`, `Splitting.shortExact`, `HomologicalComplex.shortComplexTruncLE_shortExact`, `CochainComplex.shortComplexTruncLE_shortExact`, `shortExact_iff_unop`, `IsSMulRegular.smulShortComplex_shortExact`, `HomologicalComplex.shortExact_iff_degreewise_shortExact`, `Rep.coinvariantsShortComplex_shortExact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso₂_of_shortExact_of_isIso₁₃` 📖	mathematical	`ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`CategoryTheory.IsIso` `X₂` `Hom.τ₂`	—	`ShortExact.mono_f` `ShortExact.epi_g` `mono_τ₂_of_exact_of_mono` `ShortExact.exact` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `epi_τ₂_of_exact_of_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.isIso_of_mono_of_epi`
`isIso₂_of_shortExact_of_isIso₁₃'` 📖	mathematical	`ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`CategoryTheory.IsIso` `X₂` `Hom.τ₂`	—	`isIso₂_of_shortExact_of_isIso₁₃`
`shortExact_iff_of_iso` 📖	mathematical	—	`ShortExact`	—	`shortExact_of_iso`
`shortExact_iff_op` 📖	mathematical	—	`ShortExact` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `op`	—	`ShortExact.op` `ShortExact.unop`
`shortExact_iff_unop` 📖	mathematical	—	`ShortExact` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `unop`	—	`shortExact_iff_op`
`shortExact_of_iso` 📖	—	`ShortExact`	—	—	`exact_of_iso` `ShortExact.exact` `ShortExact.mono_f` `Hom.comm₁₂` `CategoryTheory.mono_comp` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `instIsIsoτ₁` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.mono_of_mono` `ShortExact.epi_g` `Hom.comm₂₃` `CategoryTheory.epi_comp` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `instIsIsoτ₃` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.epi_of_epi`

CategoryTheory.ShortComplex.Exact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shortExact` 📖	mathematical	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.ShortComplex.LeftHomologyData.K` `CategoryTheory.ShortComplex.HomologyData.left` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.RightHomologyData.Q` `CategoryTheory.ShortComplex.HomologyData.right` `CategoryTheory.ShortComplex.LeftHomologyData.i` `CategoryTheory.ShortComplex.RightHomologyData.p` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero`	—	`CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero` `epi_f'` `mono_g'` `CategoryTheory.ShortComplex.LeftHomologyData.wi` `CategoryTheory.ShortComplex.LeftHomologyData.f'_i` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.ShortComplex.RightHomologyData.p_g'` `CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono` `CategoryTheory.instEpiId` `CategoryTheory.IsIso.id` `CategoryTheory.instMonoId` `CategoryTheory.ShortComplex.LeftHomologyData.instMonoI` `CategoryTheory.ShortComplex.RightHomologyData.instEpiP`

CategoryTheory.ShortComplex.ShortExact

Definitions

Name	Category	Theorems
`fIsKernel` 📖	CompOp	—
`gIsCokernel` 📖	CompOp	—
`splittingOfInjective` 📖	CompOp	—
`splittingOfProjective` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_g` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact`	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	—
`exact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact`	`CategoryTheory.ShortComplex.Exact`	—	—
`isIso_f_iff` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`CategoryTheory.IsIso` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f` `CategoryTheory.Limits.IsZero` `CategoryTheory.ShortComplex.X₃`	—	`CategoryTheory.ShortComplex.Exact.hasZeroObject` `exact` `mono_f` `epi_g` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.ShortComplex.zero_assoc` `CategoryTheory.Limits.zero_comp` `CategoryTheory.ShortComplex.exact_iff_epi` `CategoryTheory.Limits.IsZero.eq_of_tgt` `CategoryTheory.isIso_of_mono_of_epi`
`isIso_g_iff` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`CategoryTheory.IsIso` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g` `CategoryTheory.Limits.IsZero` `CategoryTheory.ShortComplex.X₁`	—	`CategoryTheory.ShortComplex.Exact.hasZeroObject` `exact` `mono_f` `epi_g` `CategoryTheory.cancel_mono` `CategoryTheory.Limits.zero_comp` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Category.assoc` `CategoryTheory.ShortComplex.zero` `CategoryTheory.Limits.comp_zero` `CategoryTheory.ShortComplex.exact_iff_mono` `CategoryTheory.Limits.IsZero.eq_of_src` `CategoryTheory.isIso_of_mono_of_epi`
`map` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact`	`CategoryTheory.ShortComplex.map`	—	`CategoryTheory.ShortComplex.Exact.map` `exact`
`map_of_exact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact`	`CategoryTheory.ShortComplex.map`	—	`mono_f` `epi_g` `map` `CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf` `CategoryTheory.Functor.preservesHomologyOfExact` `CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf` `CategoryTheory.Functor.map_mono` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Functor.map_epi` `CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape` `CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits`
`mk'` 📖	mathematical	`CategoryTheory.ShortComplex.Exact`	`CategoryTheory.ShortComplex.ShortExact`	—	—
`mono_f` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact`	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f`	—	—
`op` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact`	`Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `CategoryTheory.ShortComplex.op`	—	`CategoryTheory.ShortComplex.Exact.op` `exact` `epi_g` `CategoryTheory.op_mono_of_epi` `mono_f` `CategoryTheory.op_epi_of_mono`
`unop` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite`	`CategoryTheory.ShortComplex.unop`	—	`CategoryTheory.ShortComplex.Exact.unop` `exact` `epi_g` `CategoryTheory.unop_mono_of_epi` `mono_f` `CategoryTheory.unop_epi_of_mono`

CategoryTheory.ShortComplex.Splitting

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shortExact` 📖	mathematical	—	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`exact` `mono_f` `epi_g`

---

← Back to Index