OpenUnion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of homology under open unions and finite covers.

theorem OAI.Kaplansky.openCoverHomology_isZero line 17

Source documentation

Actual open-cover Mayer–Vietoris vanishing, with all three adjacent groups explicit. No contractibility hypothesis is required.

theorem openCoverHomology_isZero (U V : Set X) (hU : IsOpen U) (hV : IsOpen V)
    (hUV : U ∪ V = Set.univ) (n : ℕ)
    (hu : IsZero ((integralSingularHomology (n+1)).obj (TopCat.of U)))
    (hv : IsZero ((integralSingularHomology (n+1)).obj (TopCat.of V)))
    (hi : IsZero ((integralSingularHomology n).obj (TopCat.of ↥(U ∩ V)))) :
    IsZero ((integralSingularHomology (n+1)).obj (TopCat.of X)) := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

def OAI.Kaplansky.subspaceSubsetHomeomorph line 29
Source documentation
Remove a redundant enclosing subtype without changing its topology.
```
def subspaceSubsetHomeomorph (U W : Set X) (h : U ⊆ W) :
    (Subtype.val ⁻¹' U : Set W) ≃ₜ U where
…
```

theorem OAI.Kaplansky.openUnionHomology_isZero line 39

Source documentation

Mayer–Vietoris for an open union viewed as a subspace of the ambient space.

theorem openUnionHomology_isZero (U V : Set X) (hU : IsOpen U) (hV : IsOpen V)
    (n : ℕ)
    (hu : IsZero ((integralSingularHomology (n+1)).obj (TopCat.of U)))
    (hv : IsZero ((integralSingularHomology (n+1)).obj (TopCat.of V)))
    (hi : IsZero ((integralSingularHomology n).obj (TopCat.of ↥(U ∩ V)))) :
    IsZero ((integralSingularHomology (n+1)).obj (TopCat.of ↥(U ∪ V))) := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.finiteOpenUnionHomology_isZero line 69

Source documentation

Finite open-cover homology vanishing from explicit bounds on every nonempty intersection. The degree shift is the number of intersected sets.

theorem finiteOpenUnionHomology_isZero (S : Finset ι) (U : ι → Set X)
    (hS : S.Nonempty) (hopen : ∀ i ∈ S, IsOpen (U i)) (n : ℕ) (hcard : S.card ≤ n+1)
    (hinter : ∀ T : Finset ι, T.Nonempty → T ⊆ S → ∀ q : ℕ, n < q + T.card →
      IsZero ((integralSingularHomology q).obj (TopCat.of (⋂ i ∈ T, U i)))) :
    IsZero ((integralSingularHomology n).obj (TopCat.of (⋃ i ∈ S, U i))) := by
…

Mentions: OAI.Kaplansky.integralSingularHomology