Documentation Verification Report

AreComplementary

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

Statistics

Metric	Count
Definitions `AreComplementary`, `equiv`, `indexOfBoundaryGE`, `indexOfBoundaryLE`, `desc`, `desc'`, `aux`, `equiv`, `fromSum`, `shortComplexTruncLEX₃ToTruncGE`	10
Theorems `exists₁`, `exists₂`, `fst`, `fst_inj`, `of_boundaryGE`, `of_boundaryLE`, `snd`, `snd_inj`, `desc'_inl`, `desc'_inr`, `aux_trans`, `desc_inl`, `desc_inr`, `disjoint`, `equiv_inl`, `equiv_inr`, `exists_i₁`, `exists_i₂`, `fromSum_bijective`, `hom_ext`, `hom_ext'`, `isStrictlySupportedOutside₁_iff`, `isStrictlySupportedOutside₂_iff`, `isSupportedOutside₁_iff`, `isSupportedOutside₂_iff`, `union`, `embeddingUpInt_areComplementary`, `g_shortComplexTruncLEX₃ToTruncGE`, `g_shortComplexTruncLEX₃ToTruncGE_assoc`, `instQuasiIsoShortComplexTruncLEX₃ToTruncGE`	30
Total	40

ComplexShape.Embedding

Definitions

Name	Category	Theorems
`AreComplementary` 📖	CompData	1 math math: `embeddingUpInt_areComplementary`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embeddingUpInt_areComplementary` 📖	mathematical	—	`AreComplementary` `ComplexShape.up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `ComplexShape.down` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `ComplexShape.embeddingUpIntLE` `ComplexShape.embeddingUpIntGE`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

ComplexShape.Embedding.AreComplementary

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	2 math math: `desc_inr`, `desc_inl`
`desc'` 📖	CompOp	2 math math: `desc'_inl`, `desc'_inr`
`equiv` 📖	CompOp	4 math math: `desc'_inl`, `equiv_inl`, `equiv_inr`, `desc'_inr`
`fromSum` 📖	CompOp	1 math math: `fromSum_bijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`desc'_inl` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`desc'` `DFunLike.coe` `Equiv` `ComplexShape.Embedding.f` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `desc.aux`	—	—
`desc'_inr` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`desc'` `DFunLike.coe` `Equiv` `ComplexShape.Embedding.f` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `desc.aux`	—	—
`desc_inl` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`desc` `ComplexShape.Embedding.f`	—	`Equiv.injective` `Equiv.apply_symm_apply` `desc'_inl` `desc.aux_trans`
`desc_inr` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`desc` `ComplexShape.Embedding.f`	—	`Equiv.injective` `Equiv.apply_symm_apply` `desc'_inr` `desc.aux_trans`
`disjoint` 📖	—	`ComplexShape.Embedding.AreComplementary`	—	—	—
`equiv_inl` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `ComplexShape.Embedding.f`	—	—
`equiv_inr` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `ComplexShape.Embedding.f`	—	—
`exists_i₁` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`ComplexShape.Embedding.f`	—	`union`
`exists_i₂` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`ComplexShape.Embedding.f`	—	`exists_i₁` `symm`
`fromSum_bijective` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`Function.Bijective` `fromSum`	—	`ComplexShape.Embedding.injective_f` `disjoint` `union`
`hom_ext` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`Quiver.Hom` `HomologicalComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.instZeroHom`	—	`hom_ext'` `isStrictlySupportedOutside₂_iff` `isStrictlySupportedOutside₁_iff`
`hom_ext'` 📖	mathematical	`ComplexShape.Embedding.AreComplementary` `HomologicalComplex.IsStrictlySupportedOutside`	`Quiver.Hom` `HomologicalComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.instZeroHom`	—	`HomologicalComplex.hom_ext` `union` `CategoryTheory.Limits.IsZero.eq_of_tgt` `HomologicalComplex.IsStrictlySupportedOutside.isZero` `CategoryTheory.Limits.IsZero.eq_of_src`
`isStrictlySupportedOutside₁_iff` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`HomologicalComplex.IsStrictlySupportedOutside` `HomologicalComplex.IsStrictlySupported`	—	`exists_i₁` `HomologicalComplex.IsStrictlySupportedOutside.isZero` `HomologicalComplex.isZero_X_of_isStrictlySupported` `disjoint`
`isStrictlySupportedOutside₂_iff` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`HomologicalComplex.IsStrictlySupportedOutside` `HomologicalComplex.IsStrictlySupported`	—	`isStrictlySupportedOutside₁_iff` `symm`
`isSupportedOutside₁_iff` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`HomologicalComplex.IsSupportedOutside` `HomologicalComplex.IsSupported`	—	`exists_i₁` `HomologicalComplex.IsSupportedOutside.exactAt` `HomologicalComplex.exactAt_of_isSupported` `disjoint`
`isSupportedOutside₂_iff` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`HomologicalComplex.IsSupportedOutside` `HomologicalComplex.IsSupported`	—	`isSupportedOutside₁_iff` `symm`
`union` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`ComplexShape.Embedding.f`	—	—

ComplexShape.Embedding.AreComplementary.Boundary

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—
`indexOfBoundaryGE` 📖	CompOp	1 math math: `of_boundaryGE`
`indexOfBoundaryLE` 📖	CompOp	1 math math: `of_boundaryLE`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists₁` 📖	mathematical	`ComplexShape.Embedding.AreComplementary` `ComplexShape.Embedding.BoundaryLE`	`ComplexShape.Embedding.AreComplementary.Boundary`	—	`ComplexShape.Embedding.AreComplementary.exists_i₂`
`exists₂` 📖	mathematical	`ComplexShape.Embedding.AreComplementary` `ComplexShape.Embedding.BoundaryGE`	`ComplexShape.Embedding.AreComplementary.Boundary`	—	`ComplexShape.Embedding.AreComplementary.exists_i₁`
`fst` 📖	mathematical	`ComplexShape.Embedding.AreComplementary` `ComplexShape.Embedding.AreComplementary.Boundary`	`ComplexShape.Embedding.BoundaryLE`	—	`ComplexShape.Embedding.boundaryLE` `ComplexShape.Embedding.AreComplementary.disjoint`
`fst_inj` 📖	—	`ComplexShape.Embedding.AreComplementary` `ComplexShape.Embedding.AreComplementary.Boundary`	—	—	`ComplexShape.Embedding.injective_f` `ComplexShape.prev_eq`
`of_boundaryGE` 📖	mathematical	`ComplexShape.Embedding.AreComplementary` `ComplexShape.Embedding.BoundaryGE`	`ComplexShape.Embedding.AreComplementary.Boundary` `indexOfBoundaryGE`	—	`exists₂`
`of_boundaryLE` 📖	mathematical	`ComplexShape.Embedding.AreComplementary` `ComplexShape.Embedding.BoundaryLE`	`ComplexShape.Embedding.AreComplementary.Boundary` `indexOfBoundaryLE`	—	`exists₁`
`snd` 📖	mathematical	`ComplexShape.Embedding.AreComplementary` `ComplexShape.Embedding.AreComplementary.Boundary`	`ComplexShape.Embedding.BoundaryGE`	—	`ComplexShape.Embedding.boundaryGE` `ComplexShape.Embedding.AreComplementary.disjoint` `ComplexShape.Embedding.AreComplementary.symm`
`snd_inj` 📖	—	`ComplexShape.Embedding.AreComplementary` `ComplexShape.Embedding.AreComplementary.Boundary`	—	—	`ComplexShape.Embedding.injective_f` `ComplexShape.next_eq`

ComplexShape.Embedding.AreComplementary.desc

Definitions

Name	Category	Theorems
`aux` 📖	CompOp	3 math math: `ComplexShape.Embedding.AreComplementary.desc'_inl`, `aux_trans`, `ComplexShape.Embedding.AreComplementary.desc'_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aux_trans` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `aux`	—	—

HomologicalComplex

Definitions

Name	Category	Theorems
`shortComplexTruncLEX₃ToTruncGE` 📖	CompOp	3 math math: `g_shortComplexTruncLEX₃ToTruncGE`, `instQuasiIsoShortComplexTruncLEX₃ToTruncGE`, `g_shortComplexTruncLEX₃ToTruncGE_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`g_shortComplexTruncLEX₃ToTruncGE` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex.X₂` `instHasZeroMorphisms` `shortComplexTruncLE` `CategoryTheory.ShortComplex.X₃` `truncGE` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.ShortComplex.g` `shortComplexTruncLEX₃ToTruncGE` `πTruncGE`	—	`CategoryTheory.Limits.cokernel.π_desc` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`g_shortComplexTruncLEX₃ToTruncGE_assoc` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex.X₂` `instHasZeroMorphisms` `shortComplexTruncLE` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g` `truncGE` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `CategoryTheory.Abelian.hasZeroObject` `shortComplexTruncLEX₃ToTruncGE` `πTruncGE`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `g_shortComplexTruncLEX₃ToTruncGE`
`instQuasiIsoShortComplexTruncLEX₃ToTruncGE` 📖	mathematical	`ComplexShape.Embedding.AreComplementary`	`QuasiIso` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.X₃` `HomologicalComplex` `instCategory` `instHasZeroMorphisms` `shortComplexTruncLE` `truncGE` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `CategoryTheory.Abelian.hasZeroObject` `shortComplexTruncLEX₃ToTruncGE` `truncGE.instHasHomology`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Abelian.hasZeroObject` `truncGE.instHasHomology` `ComplexShape.Embedding.AreComplementary.union` `IsSupportedOutside.exactAt` `ComplexShape.Embedding.AreComplementary.isSupportedOutside₁_iff` `instIsSupportedOfIsStrictlySupported` `instIsStrictlySupportedTruncGE` `shortComplexTruncLE_X₃_isSupportedOutside` `quasiIsoAt_iff_exactAt` `quasiIsoAt_shortComplexTruncLE_g` `ComplexShape.Embedding.AreComplementary.disjoint` `quasiIsoAt_iff_comp_left` `g_shortComplexTruncLEX₃ToTruncGE` `instQuasiIsoAtπTruncGEF`

---

← Back to Index