Documentation Verification Report

MayerVietoris

📁 Source: Mathlib/CategoryTheory/Sites/SheafCohomology/MayerVietoris.lean

Statistics

Metric	Count
Definitions `fromBiprod`, `sequence`, `sequenceIso`, `toBiprod`, `δ`	5
Theorems `biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply`, `fromBiprod_biprodIsoProd_inv_apply`, `fromBiprod_δ`, `fromBiprod_δ_assoc`, `mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom`, `sequence_exact`, `toBiprod_apply`, `toBiprod_fromBiprod`, `toBiprod_fromBiprod_assoc`, `δ_toBiprod`, `δ_toBiprod_assoc`	11
Total	16

CategoryTheory.GrothendieckTopology.MayerVietorisSquare

Definitions

Name	Category	Theorems
`fromBiprod` 📖	CompOp	6 math math: `fromBiprod_δ_assoc`, `mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom`, `fromBiprod_biprodIsoProd_inv_apply`, `toBiprod_fromBiprod_assoc`, `toBiprod_fromBiprod`, `fromBiprod_δ`
`sequence` 📖	CompOp	1 math math: `sequence_exact`
`sequenceIso` 📖	CompOp	—
`toBiprod` 📖	CompOp	6 math math: `biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply`, `δ_toBiprod_assoc`, `δ_toBiprod`, `toBiprod_fromBiprod_assoc`, `toBiprod_fromBiprod`, `toBiprod_apply`
`δ` 📖	CompOp	4 math math: `fromBiprod_δ_assoc`, `δ_toBiprod_assoc`, `δ_toBiprod`, `fromBiprod_δ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`DFunLike.coe` `AddEquiv` `CategoryTheory.Abelian.Ext` `Opposite.unop` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `CategoryTheory.Functor.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.Functor.whiskeringRight` `AddCommGrpCat.free` `CategoryTheory.presheafToSheaf` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `Opposite.op` `CategoryTheory.Square.X₂` `toSquare` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `Prod.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Abelian.Ext.instAddCommGroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `CategoryTheory.Abelian.Ext.biprodAddEquiv` `AddCommGrpCat.instPreadditive` `CategoryTheory.Sheaf.H'` `AddCommGrpCat.instHasBinaryBiproducts` `AddCommGrpCat.of` `AddCommGrpCat.carrier` `Prod.instAddCommGroup` `AddCommGrpCat.str` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.Iso.hom` `AddCommGrpCat.biprodIsoProd` `CategoryTheory.Square.X₄` `toBiprod` `CategoryTheory.Abelian.Ext.comp` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.instPreadditiveSheaf` `shortComplex` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Abelian.Ext.mk₀` `CategoryTheory.ShortComplex.g` `zero_add` `Nat.instAddMonoid`	—	`AddEquiv.injective` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `AddCommGrpCat.instHasBinaryBiproducts` `zero_add` `toBiprod_apply` `CategoryTheory.Iso.inv_hom_id_apply` `AddEquiv.apply_symm_apply` `CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assoc` `CategoryTheory.Abelian.Ext.comp.congr_simp` `CategoryTheory.Limits.biprod.inl_desc` `CategoryTheory.Limits.biprod.inr_desc`
`fromBiprod_biprodIsoProd_inv_apply` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`DFunLike.coe` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `CategoryTheory.Sheaf.H'` `CategoryTheory.Square.X₂` `toSquare` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Square.X₁` `AddCommGrpCat.carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `fromBiprod` `AddCommGrpCat.of` `Prod.instAddCommGroup` `CategoryTheory.Iso.inv` `AddCommGrpCat.biprodIsoProd` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.cohomologyPresheaf` `Opposite.op` `SubNegMonoid.toSub` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Square.f₁₂` `CategoryTheory.Square.f₁₃`	—	`CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.ConcreteCategory.comp_apply` `AddCommGrpCat.biprodIsoProd_inv_comp_desc` `CategoryTheory.Preadditive.comp_neg` `sub_eq_add_neg`
`fromBiprod_δ` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `CategoryTheory.Sheaf.H'` `CategoryTheory.Square.X₂` `toSquare` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Square.X₁` `CategoryTheory.Square.X₄` `fromBiprod` `δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `AddCommGrpCat.instZeroHom_1`	—	`CategoryTheory.ComposableArrows.IsComplex.zero` `CategoryTheory.ComposableArrows.Exact.toIsComplex` `sequence_exact`
`fromBiprod_δ_assoc` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `CategoryTheory.Sheaf.H'` `CategoryTheory.Square.X₂` `toSquare` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Square.X₁` `fromBiprod` `CategoryTheory.Square.X₄` `δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `AddCommGrpCat.instZeroHom_1`	—	`CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fromBiprod_δ`
`mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`CategoryTheory.Abelian.Ext.comp` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Abelian.Ext.mk₀` `CategoryTheory.ShortComplex.f` `DFunLike.coe` `AddEquiv` `CategoryTheory.Abelian.Ext` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.presheafToSheaf` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Functor.comp` `CategoryTheory.types` `CategoryTheory.yoneda` `CategoryTheory.Square.X₂` `toSquare` `AddCommGrpCat.free` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.biprod` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `Prod.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Abelian.Ext.instAddCommGroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `CategoryTheory.Abelian.Ext.biprodAddEquiv` `CategoryTheory.Sheaf.H'` `AddCommGrpCat.instHasBinaryBiproducts` `AddCommGrpCat.of` `AddCommGrpCat.carrier` `Prod.instAddCommGroup` `AddCommGrpCat.str` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.Iso.hom` `AddCommGrpCat.biprodIsoProd` `zero_add` `Nat.instAddMonoid` `CategoryTheory.Square.X₁` `fromBiprod`	—	`CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Abelian.hasBinaryBiproducts` `zero_add` `AddEquiv.surjective` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Localization.HasSmallLocalizedHom.small` `CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor` `CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply` `CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply` `fromBiprod_biprodIsoProd_inv_apply` `CategoryTheory.Abelian.Ext.comp.congr_simp` `CategoryTheory.Iso.inv_hom_id_apply` `CategoryTheory.Abelian.Ext.comp_add` `CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assoc` `CategoryTheory.Limits.biprod.lift_fst` `CategoryTheory.Limits.biprod.lift_snd` `CategoryTheory.Abelian.Ext.mk₀_neg` `CategoryTheory.Abelian.Ext.neg_comp` `sub_eq_add_neg`
`sequence_exact` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`CategoryTheory.ComposableArrows.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `sequence`	—	`CategoryTheory.ComposableArrows.exact_of_iso` `shortComplex_shortExact` `CategoryTheory.Abelian.Ext.contravariantSequence_exact`
`toBiprod_apply` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`DFunLike.coe` `CategoryTheory.Sheaf.H'` `CategoryTheory.Square.X₄` `toSquare` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `AddCommGrpCat.carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `toBiprod` `AddCommGrpCat.of` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.cohomologyPresheaf` `Opposite.op` `Prod.instAddCommGroup` `CategoryTheory.Iso.inv` `AddCommGrpCat.biprodIsoProd` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Square.f₂₄` `CategoryTheory.Square.f₃₄`	—	`AddEquiv.injective` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply` `AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply` `CategoryTheory.Iso.hom_inv_id_apply` `CategoryTheory.ConcreteCategory.comp_apply` `CategoryTheory.Limits.biprod.lift_fst` `CategoryTheory.Iso.inv_hom_id_apply` `AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply` `CategoryTheory.Limits.biprod.lift_snd`
`toBiprod_fromBiprod` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Sheaf.H'` `CategoryTheory.Square.X₄` `toSquare` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Square.X₁` `toBiprod` `fromBiprod` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `AddCommGrpCat.instZeroHom_1`	—	`CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Limits.biprod.lift_desc` `CategoryTheory.Square.fac` `CategoryTheory.Preadditive.comp_neg`
`toBiprod_fromBiprod_assoc` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Sheaf.H'` `CategoryTheory.Square.X₄` `toSquare` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `toBiprod` `CategoryTheory.Square.X₁` `fromBiprod` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `AddCommGrpCat.instZeroHom_1`	—	`CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `toBiprod_fromBiprod`
`δ_toBiprod` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Sheaf.H'` `CategoryTheory.Square.X₁` `toSquare` `CategoryTheory.Square.X₄` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `δ` `toBiprod` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `AddCommGrpCat.instZeroHom_1`	—	`CategoryTheory.ComposableArrows.IsComplex.zero` `CategoryTheory.ComposableArrows.Exact.toIsComplex` `sequence_exact`
`δ_toBiprod_assoc` 📖	mathematical	`CategoryTheory.HasExt` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.sheafIsAbelian` `AddCommGrpCat.instAbelian`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Sheaf.H'` `CategoryTheory.Square.X₁` `toSquare` `CategoryTheory.Square.X₄` `δ` `CategoryTheory.Limits.biprod` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `toBiprod` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `AddCommGrpCat.instZeroHom_1`	—	`CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `AddCommGrpCat.instHasBinaryBiproducts` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_toBiprod`

---

← Back to Index