Documentation

Mathlib.Topology.Sheaves.MayerVietoris

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
source
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
    Instances For
      source
      @[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
      source
      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
        Instances For
          source
          @[simp]
          theorem Opens.mayerVietorisSquare_X₃ {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) :
          (mayerVietorisSquare U V).X₃ = V
          source
          @[simp]
          theorem Opens.coe_mayerVietorisSquare_X₄ {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) :
          ↑(mayerVietorisSquare U V).X₄ = ↑U ∪ ↑V
          source
          @[simp]
          theorem Opens.mayerVietorisSquare_X₂ {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) :
          (mayerVietorisSquare U V).X₂ = U
          source
          @[simp]
          theorem Opens.coe_mayerVietorisSquare_X₁ {T : Type u} [TopologicalSpace T] (U V : TopologicalSpace.Opens T) :
          ↑(mayerVietorisSquare U V).X₁ = ↑U ∩ ↑V