Commit 2023-05-26 11:51 23c0f40d

View on Github →

feat: port Topology.Sheaves.SheafCondition.PairwiseIntersections (#4384)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean

added def TopCat.Presheaf.IsSheafPairwiseIntersections

added def TopCat.Presheaf.IsSheafPreservesLimitPairwiseIntersections

added def TopCat.Presheaf.SheafCondition.pairwiseCoconeIso

added def TopCat.Presheaf.SheafCondition.pairwiseDiagramIso

added def TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover

added def TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverMap

added def TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj

added theorem TopCat.Presheaf.isSheafOpensLeCover_iff_isSheafPairwiseIntersections

added theorem TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections

added theorem TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections

added def TopCat.Sheaf.interUnionPullbackCone

added def TopCat.Sheaf.interUnionPullbackConeLift

added theorem TopCat.Sheaf.interUnionPullbackConeLift_left

added theorem TopCat.Sheaf.interUnionPullbackConeLift_right

added theorem TopCat.Sheaf.interUnionPullbackCone_fst

added theorem TopCat.Sheaf.interUnionPullbackCone_pt

added theorem TopCat.Sheaf.interUnionPullbackCone_snd

added def TopCat.Sheaf.isLimitPullbackCone

added def TopCat.Sheaf.isProductOfDisjoint

added def TopCat.Sheaf.objSupIsoProdEqLocus

added theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst

added theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd

added theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst

added theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd