Documentation Verification Report

IsSupported

📁 Source: Mathlib/Algebra/Homology/Embedding/IsSupported.lean

Statistics

Metric	Count
Definitions `IsSupported`, `IsStrictlySupported`, `IsStrictlySupportedOutside`, `IsSupported`, `IsSupportedOutside`	5
Theorems `isZero`, `isSupportedOutside`, `isZero`, `exactAt`, `exactAt`, `exactAt_of_isSupported`, `instIsStrictlySupportedOfNat`, `instIsStrictlySupportedOppositeOpOp`, `instIsSupportedOfIsStrictlySupported`, `isStrictlySupportedOutside_op_iff`, `isStrictlySupported_of_iso`, `isStrictlySupported_op_iff`, `isSupportedOutside_op_iff`, `isSupported_iff`, `isSupported_iff_of_quasiIso`, `isSupported_of_iso`, `isSupported_op_iff`, `isZero_X_of_isStrictlySupported`, `isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside`, `map_isStrictlySupported`	20
Total	25

FreeCommRing

Definitions

Name	Category	Theorems
`IsSupported` 📖	MathDef	6 math math: `isSupported_int`, `isSupported_of`, `exists_finset_support`, `isSupported_zero`, `exists_finite_support`, `isSupported_one`

HomologicalComplex

Definitions

Name	Category	Theorems
`IsStrictlySupported` 📖	CompData	17 math math: `instIsStrictlySupportedOfNat`, `instIsStrictlySupportedTruncGE_1`, `map_isStrictlySupported`, `ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₁_iff`, `ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₂_iff`, `instIsStrictlySupportedStupidTrunc_1`, `isIso_ιTruncLE_iff`, `isStrictlySupported_op_iff`, `isIso_πTruncGE_iff`, `instIsStrictlySupportedTruncLE_1`, `instIsStrictlySupportedTruncGE`, `instIsStrictlySupportedExtend`, `isStrictlySupported_of_iso`, `isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside`, `instIsStrictlySupportedStupidTrunc`, `instIsStrictlySupportedTruncLE`, `instIsStrictlySupportedOppositeOpOp`
`IsStrictlySupportedOutside` 📖	CompData	5 math math: `isStrictlySupportedOutside_op_iff`, `isZero_stupidTrunc_iff`, `ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₁_iff`, `ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₂_iff`, `isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside`
`IsSupported` 📖	CompData	9 math math: `quasiIso_πTruncGE_iff_isSupported`, `isSupported_of_iso`, `isSupported_iff_of_quasiIso`, `instIsSupportedOfIsStrictlySupported`, `quasiIso_ιTruncLE_iff_isSupported`, `ComplexShape.Embedding.AreComplementary.isSupportedOutside₁_iff`, `isSupported_op_iff`, `ComplexShape.Embedding.AreComplementary.isSupportedOutside₂_iff`, `isSupported_iff`
`IsSupportedOutside` 📖	CompData	7 math math: `IsStrictlySupportedOutside.isSupportedOutside`, `isSupportedOutside_op_iff`, `acyclic_truncGE_iff_isSupportedOutside`, `ComplexShape.Embedding.AreComplementary.isSupportedOutside₁_iff`, `acyclic_truncLE_iff_isSupportedOutside`, `ComplexShape.Embedding.AreComplementary.isSupportedOutside₂_iff`, `shortComplexTruncLE_X₃_isSupportedOutside`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exactAt_of_isSupported` 📖	mathematical	—	`ExactAt`	—	`IsSupported.exactAt`
`instIsStrictlySupportedOfNat` 📖	mathematical	—	`IsStrictlySupported` `HomologicalComplex` `CategoryTheory.Limits.HasZeroObject.zero'` `instCategory` `instHasZeroObject`	—	`instHasZeroObject` `CategoryTheory.Functor.map_isZero` `instPreservesZeroMorphismsEval` `CategoryTheory.Limits.isZero_zero`
`instIsStrictlySupportedOppositeOpOp` 📖	mathematical	—	`IsStrictlySupported` `ComplexShape.symm` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `op` `ComplexShape.Embedding.op`	—	`isStrictlySupported_op_iff`
`instIsSupportedOfIsStrictlySupported` 📖	mathematical	—	`IsSupported`	—	`exactAt_iff` `CategoryTheory.ShortComplex.exact_of_isZero_X₂` `isZero_X_of_isStrictlySupported`
`isStrictlySupportedOutside_op_iff` 📖	mathematical	—	`IsStrictlySupportedOutside` `ComplexShape.symm` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `op` `ComplexShape.Embedding.op`	—	`CategoryTheory.Limits.IsZero.unop` `IsStrictlySupportedOutside.isZero` `CategoryTheory.Limits.IsZero.op`
`isStrictlySupported_of_iso` 📖	mathematical	—	`IsStrictlySupported`	—	`CategoryTheory.Limits.IsZero.of_iso` `isZero_X_of_isStrictlySupported`
`isStrictlySupported_op_iff` 📖	mathematical	—	`IsStrictlySupported` `ComplexShape.symm` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `op` `ComplexShape.Embedding.op`	—	`CategoryTheory.Limits.IsZero.unop` `isZero_X_of_isStrictlySupported` `CategoryTheory.Limits.IsZero.op`
`isSupportedOutside_op_iff` 📖	mathematical	—	`IsSupportedOutside` `ComplexShape.symm` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `op` `ComplexShape.Embedding.op`	—	`ExactAt.unop` `IsSupportedOutside.exactAt` `ExactAt.op`
`isSupported_iff` 📖	mathematical	—	`IsSupported` `ExactAt`	—	—
`isSupported_iff_of_quasiIso` 📖	mathematical	`HasHomology`	`IsSupported`	—	`exactAt_iff_of_quasiIsoAt` `QuasiIso.quasiIsoAt`
`isSupported_of_iso` 📖	mathematical	—	`IsSupported`	—	`ExactAt.of_iso` `exactAt_of_isSupported`
`isSupported_op_iff` 📖	mathematical	—	`IsSupported` `ComplexShape.symm` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.hasZeroMorphismsOpposite` `op` `ComplexShape.Embedding.op`	—	`ExactAt.unop` `exactAt_of_isSupported` `ExactAt.op`
`isZero_X_of_isStrictlySupported` 📖	mathematical	—	`CategoryTheory.Limits.IsZero` `X`	—	`IsStrictlySupported.isZero`
`isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside` 📖	mathematical	—	`CategoryTheory.Limits.IsZero` `HomologicalComplex` `instCategory` `IsStrictlySupported` `IsStrictlySupportedOutside`	—	`CategoryTheory.Functor.map_isZero` `instPreservesZeroMorphismsEval` `CategoryTheory.Limits.IsZero.iff_id_eq_zero` `hom_ext` `CategoryTheory.Limits.IsZero.eq_of_src` `IsStrictlySupportedOutside.isZero` `isZero_X_of_isStrictlySupported`
`map_isStrictlySupported` 📖	mathematical	—	`IsStrictlySupported` `CategoryTheory.Functor.obj` `HomologicalComplex` `instCategory` `CategoryTheory.Functor.mapHomologicalComplex`	—	`CategoryTheory.Limits.IsZero.iff_id_eq_zero` `CategoryTheory.Functor.map_id` `CategoryTheory.Limits.IsZero.eq_of_src` `isZero_X_of_isStrictlySupported` `CategoryTheory.Functor.map_zero`

HomologicalComplex.IsStrictlySupported

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isZero` 📖	mathematical	—	`CategoryTheory.Limits.IsZero` `HomologicalComplex.X`	—	—

HomologicalComplex.IsStrictlySupportedOutside

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSupportedOutside` 📖	mathematical	`HomologicalComplex.IsStrictlySupportedOutside`	`HomologicalComplex.IsSupportedOutside`	—	`CategoryTheory.ShortComplex.exact_of_isZero_X₂` `isZero`
`isZero` 📖	mathematical	`HomologicalComplex.IsStrictlySupportedOutside`	`CategoryTheory.Limits.IsZero` `HomologicalComplex.X` `ComplexShape.Embedding.f`	—	—

HomologicalComplex.IsSupported

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exactAt` 📖	mathematical	—	`HomologicalComplex.ExactAt`	—	—

HomologicalComplex.IsSupportedOutside

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exactAt` 📖	mathematical	`HomologicalComplex.IsSupportedOutside`	`HomologicalComplex.ExactAt` `ComplexShape.Embedding.f`	—	—

---

← Back to Index