Commit 2024-08-23 21:19 ca6a6fdc

View on Github →

feat(CategoryTheory/Sites): constructors for Mayer-Vietoris squares (#14867) In this PR, we give constructors for Mayer-Vietoris squares, which allows the construction of these squares in the case of topological spaces.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Grp/Adjunctions.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean

added theorem CategoryTheory.Square.IsPullback.flip

added theorem CategoryTheory.Square.IsPullback.mono_f₁₂

added theorem CategoryTheory.Square.IsPullback.mono_f₁₃

added theorem CategoryTheory.Square.IsPushout.epi_f₂₄

added theorem CategoryTheory.Square.IsPushout.epi_f₃₄

added theorem CategoryTheory.Square.IsPushout.flip

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.monomorphisms

added theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.epimorphisms

Modified Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

added theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf

added theorem CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/Square.lean

added def CategoryTheory.NatTrans.mapSquare

added def CategoryTheory.Square.mapFunctor

Created Mathlib/Topology/Sheaves/MayerVietoris.lean