mayerVietorisSquare' — Mathlib

English

A detailed version of injectivity of stalkToFiber, with explicit choice of refinements and maps.

Русский

Подробная версия инъективности stalkToFiber с явным выбором уточнений и отображений.

LaTeX

$$$ (\\text{stalkToFiber\\_injective}) \; (P,x)\\; (w) \\Rightarrow \\text{injective}. $$$

Lean4

/-- A square consisting of opens `X₂ ⊓ X₃`, `X₂`, `X₃` and `X₂ ⊔ X₃` is
a Mayer-Vietoris square. -/
@[simps! toSquare]
noncomputable def mayerVietorisSquare' (sq : Square (Opens T)) (h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃)
    (h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃) : (Opens.grothendieckTopology T).MayerVietorisSquare :=
  GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback (J := (Opens.grothendieckTopology T)) sq
    (Square.IsPullback.mk _
      (by
        refine PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_
        · intro s
          apply homOfLE
          rw [h₁, le_inf_iff]
          exact ⟨leOfHom s.fst, leOfHom s.snd⟩
        all_goals intros; apply Subsingleton.elim))
    (fun x hx ↦ by
      rw [h₄] at hx
      obtain (hx | hx) := hx
      · exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.left, hx⟩⟩
      · exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.right, hx⟩⟩)

Похожие утверждения