Documentation Verification Report

MayerVietorisSquare

📁 Source: Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

Statistics

Metric	Count
Definitions `MayerVietorisSquare`, `SheafCondition`, `glue`, `mk'`, `mk_of_isPullback`, `shortComplex`, `toPullbackObj`, `toSquare`	8
Theorems `bijective_toPullbackObj`, `ext`, `map_f₂₄_op_glue`, `map_f₃₄_op_glue`, `instEpiSheafAddCommGrpCatGShortComplex`, `instMonoSheafAddCommGrpCatFShortComplex`, `isPushout`, `isPushoutAddCommGrpFreeSheaf`, `mk'_toSquare`, `mk_of_isPullback_toSquare`, `mono_f₁₃`, `sheafCondition_iff_bijective_toPullbackObj`, `sheafCondition_iff_comp_coyoneda`, `sheafCondition_of_sheaf`, `shortComplex_X₁`, `shortComplex_X₂`, `shortComplex_X₃`, `shortComplex_exact`, `shortComplex_f`, `shortComplex_g`, `shortComplex_shortExact`, `isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff`	22
Total	30

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`MayerVietorisSquare` 📖	CompData	—

CategoryTheory.GrothendieckTopology.MayerVietorisSquare

Definitions

Name	Category	Theorems
`SheafCondition` 📖	MathDef	3 math math: `sheafCondition_of_sheaf`, `sheafCondition_iff_bijective_toPullbackObj`, `sheafCondition_iff_comp_coyoneda`
`mk'` 📖	CompOp	1 math math: `mk'_toSquare`
`mk_of_isPullback` 📖	CompOp	1 math math: `mk_of_isPullback_toSquare`
`shortComplex` 📖	CompOp	11 math math: `shortComplex_X₃`, `shortComplex_X₁`, `biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply`, `shortComplex_shortExact`, `mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom`, `instEpiSheafAddCommGrpCatGShortComplex`, `shortComplex_g`, `shortComplex_f`, `instMonoSheafAddCommGrpCatFShortComplex`, `shortComplex_X₂`, `shortComplex_exact`
`toPullbackObj` 📖	CompOp	2 math math: `sheafCondition_iff_bijective_toPullbackObj`, `SheafCondition.bijective_toPullbackObj`
`toSquare` 📖	CompOp	27 math math: `shortComplex_X₃`, `Opens.mayerVietorisSquare_X₃`, `shortComplex_X₁`, `biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply`, `isPushout`, `mono_f₁₃`, `fromBiprod_δ_assoc`, `mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom`, `mk'_toSquare`, `Opens.mayerVietorisSquare_X₂`, `Opens.coe_mayerVietorisSquare_X₁`, `δ_toBiprod_assoc`, `δ_toBiprod`, `sheafCondition_iff_bijective_toPullbackObj`, `mk_of_isPullback_toSquare`, `fromBiprod_biprodIsoProd_inv_apply`, `shortComplex_g`, `isPushoutAddCommGrpFreeSheaf`, `toBiprod_fromBiprod_assoc`, `shortComplex_f`, `Opens.mayerVietorisSquare'_toSquare`, `Opens.coe_mayerVietorisSquare_X₄`, `SheafCondition.bijective_toPullbackObj`, `toBiprod_fromBiprod`, `shortComplex_X₂`, `fromBiprod_δ`, `toBiprod_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEpiSheafAddCommGrpCatGShortComplex` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	`CategoryTheory.ShortComplex.zero` `CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `isPushoutAddCommGrpFreeSheaf`
`instMonoSheafAddCommGrpCatFShortComplex` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f`	—	`CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Limits.biprod.lift_snd` `CategoryTheory.Preadditive.instMonoNegHom` `CategoryTheory.Functor.map_mono` `CategoryTheory.Functor.instPreservesMonomorphisms` `CategoryTheory.Limits.HasZeroObject.instFunctor` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.presheafToSheaf_additive` `CategoryTheory.Functor.preservesHomologyOfExact` `CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf` `CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `CategoryTheory.instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf` `CategoryTheory.instMonoFunctorWhiskerRightOfPreservesMonomorphisms` `CategoryTheory.Limits.Types.instHasPullbacksType` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.yonedaFunctor_preservesLimits` `mono_f₁₃` `AddCommGrpCat.instPreservesMonomorphismsFree` `CategoryTheory.mono_of_mono`
`isPushout` 📖	mathematical	—	`CategoryTheory.Square.IsPushout` `CategoryTheory.Sheaf` `CategoryTheory.types` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Square.map` `toSquare` `CategoryTheory.Functor.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.presheafToSheaf`	—	—
`isPushoutAddCommGrpFreeSheaf` 📖	mathematical	—	`CategoryTheory.Square.IsPushout` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Square.map` `toSquare` `CategoryTheory.Functor.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `AddCommGrpCat.free` `CategoryTheory.presheafToSheaf`	—	`CategoryTheory.Square.IsPushout.of_iso` `CategoryTheory.Square.IsPushout.map` `isPushout` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Sheaf.instIsLeftAdjointComposeAndSheafify` `AddCommGrpCat.instIsLeftAdjointFree` `CategoryTheory.Sheaf.instPreservesSheafificationOfIsLeftAdjoint`
`mk'_toSquare` 📖	mathematical	`CategoryTheory.Square.IsPullback` `CategoryTheory.types` `CategoryTheory.Square.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Square.op` `CategoryTheory.Sheaf.val`	`toSquare` `mk'`	—	—
`mk_of_isPullback_toSquare` 📖	mathematical	`CategoryTheory.Square.IsPullback` `CategoryTheory.Sieve` `CategoryTheory.Square.X₄` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.ofTwoArrows` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Square.f₂₄` `CategoryTheory.Square.f₃₄`	`toSquare` `mk_of_isPullback`	—	—
`mono_f₁₃` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Square.X₁` `toSquare` `CategoryTheory.Square.X₃` `CategoryTheory.Square.f₁₃`	—	—
`sheafCondition_iff_bijective_toPullbackObj` 📖	mathematical	—	`SheafCondition` `CategoryTheory.types` `Function.Bijective` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Square.X₄` `toSquare` `CategoryTheory.Limits.Types.PullbackObj` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Square.X₁` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Square.f₁₂` `CategoryTheory.Square.f₁₃` `toPullbackObj`	—	—
`sheafCondition_iff_comp_coyoneda` 📖	mathematical	—	`SheafCondition` `CategoryTheory.types` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda`	—	`CategoryTheory.Square.isPullback_iff_map_coyoneda_isPullback`
`sheafCondition_of_sheaf` 📖	mathematical	—	`SheafCondition` `CategoryTheory.Sheaf.val`	—	`sheafCondition_iff_comp_coyoneda` `CategoryTheory.isSheaf_iff_isSheaf_of_type` `CategoryTheory.Sheaf.cond` `CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff` `CategoryTheory.Square.IsPullback.map` `CategoryTheory.Square.IsPushout.op` `isPushout` `CategoryTheory.yoneda_preservesLimit`
`shortComplex_X₁` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₁` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex` `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`	—	—
`shortComplex_X₂` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₂` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex` `CategoryTheory.Limits.biprod` `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₃`	—	—
`shortComplex_X₃` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex` `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`	—	—
`shortComplex_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex`	—	`CategoryTheory.ShortComplex.exact_of_g_is_cokernel` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `isPushoutAddCommGrpFreeSheaf` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`shortComplex_f` 📖	mathematical	—	`CategoryTheory.ShortComplex.f` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex` `CategoryTheory.Limits.biprod.lift` `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.Square.X₃` `CategoryTheory.Functor.map` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Square.f₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `NegZeroClass.toNeg` `CategoryTheory.Square.map` `CategoryTheory.Functor.whiskeringRight` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.Square.f₁₃`	—	`CategoryTheory.instHasWeakSheafifyOfHasSheafify`
`shortComplex_g` 📖	mathematical	—	`CategoryTheory.ShortComplex.g` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex` `CategoryTheory.Limits.biprod.desc` `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.Square.X₃` `CategoryTheory.Functor.map` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Square.f₂₄` `CategoryTheory.Square.f₃₄`	—	`CategoryTheory.instHasWeakSheafifyOfHasSheafify`
`shortComplex_shortExact` 📖	mathematical	—	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Sheaf` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.instPreadditiveSheaf` `AddCommGrpCat.instPreadditive` `shortComplex`	—	`shortComplex_exact` `instMonoSheafAddCommGrpCatFShortComplex` `instEpiSheafAddCommGrpCatGShortComplex`

CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition

Definitions

Name	Category	Theorems
`glue` 📖	CompOp	2 math math: `map_f₂₄_op_glue`, `map_f₃₄_op_glue`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_toPullbackObj` 📖	mathematical	`CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition` `CategoryTheory.types`	`Function.Bijective` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Square.X₄` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `CategoryTheory.Limits.Types.PullbackObj` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Square.X₁` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Square.f₁₂` `CategoryTheory.Square.f₁₃` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toPullbackObj`	—	`CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj`
`ext` 📖	—	`CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition` `CategoryTheory.types` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Square.X₄` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `CategoryTheory.Square.X₂` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Square.f₂₄` `CategoryTheory.Square.X₃` `CategoryTheory.Square.f₃₄`	—	—	`Function.Bijective.injective` `bijective_toPullbackObj`
`map_f₂₄_op_glue` 📖	mathematical	`CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition` `CategoryTheory.types` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Square.X₂` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `CategoryTheory.Square.X₁` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Square.f₁₂` `CategoryTheory.Square.X₃` `CategoryTheory.Square.f₁₃`	`CategoryTheory.Square.X₄` `CategoryTheory.Square.f₂₄` `glue`	—	`CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst`
`map_f₃₄_op_glue` 📖	mathematical	`CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition` `CategoryTheory.types` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Square.X₂` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `CategoryTheory.Square.X₁` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Square.f₁₂` `CategoryTheory.Square.X₃` `CategoryTheory.Square.f₁₃`	`CategoryTheory.Square.X₄` `CategoryTheory.Square.f₃₄` `glue`	—	`CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd`

CategoryTheory.Sheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff` 📖	mathematical	—	`CategoryTheory.Square.IsPullback` `CategoryTheory.types` `CategoryTheory.Square.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Square.op` `CategoryTheory.Functor.comp` `CategoryTheory.Sheaf` `instCategorySheaf` `CategoryTheory.Functor.op` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.presheafToSheaf` `CategoryTheory.Functor.obj` `val`	—	`CategoryTheory.Square.IsPullback.iff_of_equiv` `CategoryTheory.yonedaEquiv_naturality` `CategoryTheory.Adjunction.homEquiv_naturality_left`

---

← Back to Index