Mayer-Vietoris squares

Given two open subsets U and V of a topological space T, we construct the associated Mayer-Vietoris square:

U ⊓ V --->   U
  |          |
  v          v
  V   ---> U ⊔ V

noncomputable def Opens.mayerVietorisSquare' {T : Type u} [TopologicalSpace T] (sq : CategoryTheory.Square (TopologicalSpace.Opens T)) (h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃) (h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃) : (grothendieckTopology T).MayerVietorisSquare

A square consisting of opens X₂ ⊓ X₃, X₂, X₃ and X₂ ⊔ X₃ is a Mayer-Vietoris square.

Equations

• Opens.mayerVietorisSquare' sq h₄ h₁ = CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback sq ⋯ ⋯

@[simp]

theorem Opens.mayerVietorisSquare'_toSquare {T : Type u} [TopologicalSpace T] (sq : CategoryTheory.Square (TopologicalSpace.Opens T)) (h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃) (h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃) : (mayerVietorisSquare' sq h₄ h₁).toSquare = sq

noncomputable def Opens.mayerVietorisSquare {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) : (grothendieckTopology T).MayerVietorisSquare

The Mayer-Vietoris square attached to two open subsets of a topological space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Opens.mayerVietorisSquare_X₃ {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) : (mayerVietorisSquare U V).X₃ = V

@[simp]

theorem Opens.coe_mayerVietorisSquare_X₄ {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) : ↑(mayerVietorisSquare U V).X₄ = ↑U ∪ ↑V

@[simp]

theorem Opens.mayerVietorisSquare_X₂ {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) : (mayerVietorisSquare U V).X₂ = U

@[simp]

theorem Opens.coe_mayerVietorisSquare_X₁ {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) : ↑(mayerVietorisSquare U V).X₁ = ↑U ∩ ↑V