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₃) :
(Opens.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₃) :
    (Opens.mayerVietorisSquare' sq h₄ h₁).toSquare = sq
    source
    noncomputable def Opens.mayerVietorisSquare {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
    (Opens.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.
    Instances For
      source
      @[simp]
      theorem Opens.mayerVietorisSquare_X₃ {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
      (Opens.mayerVietorisSquare U V).X₃ = V
      source
      @[simp]
      theorem Opens.mayerVietorisSquare_f₁₃_down_down {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
      ⋯ = ⋯
      source
      @[simp]
      theorem Opens.mayerVietorisSquare_X₁_coe {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
      ↑(Opens.mayerVietorisSquare U V).X₁ = ↑U ∩ ↑V
      source
      @[simp]
      theorem Opens.mayerVietorisSquare_f₂₄_down_down {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
      ⋯ = ⋯
      source
      @[simp]
      theorem Opens.mayerVietorisSquare_f₃₄_down_down {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
      ⋯ = ⋯
      source
      @[simp]
      theorem Opens.mayerVietorisSquare_X₄_coe {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
      ↑(Opens.mayerVietorisSquare U V).X₄ = ↑U ∪ ↑V
      source
      @[simp]
      theorem Opens.mayerVietorisSquare_X₂ {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
      (Opens.mayerVietorisSquare U V).X₂ = U
      source
      @[simp]
      theorem Opens.mayerVietorisSquare_f₁₂_down_down {T : Type u} [TopologicalSpace T] (U : TopologicalSpace.Opens T) (V : TopologicalSpace.Opens T) :
      ⋯ = ⋯