FiniteCover.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Relative maps and vanishing and gluing over finite open covers.

theorem OAI.Kaplansky.relativeHomology_isZero_empty line 17
Source documentation
Relative homology of an empty ambient space is zero in every degree.
```
theorem relativeHomology_isZero_empty [IsEmpty X] (A : Set X) (n : ℕ) :
    IsZero (relativeSingularHomology (subspaceInclusion A) n) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.relativeOpenCover_sum_epi_zero line 33
Source documentation
The relative two-chart sum is surjective also in degree zero. There is no spurious degree-minus-one overlap hypothesis.
```
theorem relativeOpenCover_sum_epi_zero (U V A : Set X)
    (hU : IsOpen U) (hV : IsOpen V) (hcover : U ∪ V = Set.univ) :
    Epi (relativeMayerVietorisSumSequence U V A 0).g := by
…
```
Mentions: OAI.Kaplansky.relativeMayerVietorisSumSequence
theorem OAI.Kaplansky.relativeOpenCover_zero_isZero line 50

def OAI.Kaplansky.restrictedPairSubsetIso line 69

Source documentation

Nested restrictions give the same actual pair, with ambient subspace topology and the same removed set.

def restrictedPairSubsetIso (U W A : Set X) (h : U ⊆ W) (n : ℕ) :
    relativeSingularHomology (subspaceInclusion
      (Subtype.val ⁻¹' (Subtype.val ⁻¹' A : Set W) : Set (Subtype.val ⁻¹' U : Set W))) n ≅
    relativeSingularHomology (subspaceInclusion (Subtype.val ⁻¹' A : Set U)) n :=
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion

theorem OAI.Kaplansky.relativeOpenUnion_below_isZero line 78

Source documentation

Uniform vanishing below r is preserved by a two-set open union.

theorem relativeOpenUnion_below_isZero (U V A : Set X)
    (hU : IsOpen U) (hV : IsOpen V) (r : ℕ)
    (hu : ∀ n < r, IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set U)) n))
    (hv : ∀ n < r, IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set V)) n))
    (hi : ∀ n < r, IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∩ V))) n)) :
    ∀ n < r, IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∪ V))) n) := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion

theorem OAI.Kaplansky.finiteRelativeOpenUnion_below_isZero line 118

Source documentation

Uniform relative vanishing below r on all nonempty finite intersections implies the same bound on their union. The empty union and degree zero are included, and there is no loss depending on the number of charts.

theorem finiteRelativeOpenUnion_below_isZero (S : Finset ι) (U : ι → Set X)
    (A : Set X) (hopen : ∀ i ∈ S, IsOpen (U i)) (r : ℕ)
    (hinter : ∀ T : Finset ι, T.Nonempty → T ⊆ S → ∀ n < r,
      IsZero (relativeSingularHomology
        (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(⋂ i ∈ T, U i))) n)) :
    ∀ n < r, IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(⋃ i ∈ S, U i))) n) := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion

theorem OAI.Kaplansky.restrictedPairHomologyMap_comp line 191
theorem OAI.Kaplansky.restrictedPairSubsetIso_toAmbient line 203
Source documentation
Actual inclusion after eliminating a redundant enclosing subtype.
```
theorem restrictedPairSubsetIso_toAmbient (U W A : Set X) (h : U ⊆ W) (n : ℕ) :
    (restrictedPairSubsetIso U W A h n).hom ≫ restrictedPairHomologyMap h A n =
      restrictedPairToAmbientHomologyMap (Subtype.val ⁻¹' U : Set W) (Subtype.val ⁻¹' A) n := by
…
```
Mentions: OAI.Kaplansky.restrictedPairSubsetIso, OAI.Kaplansky.restrictedPairHomologyMap, OAI.Kaplansky.restrictedPairToAmbientHomologyMap

theorem OAI.Kaplansky.relativeOpenUnion_hom_ext line 215

Source documentation

Maps out of a restricted open union are determined on its two actual subsets when the preceding relative overlap group vanishes.

theorem relativeOpenUnion_hom_ext (U V A : Set X) (hU : IsOpen U) (hV : IsOpen V)
    (n : ℕ) (hi : IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∩ V))) n))
    {Z : ModuleCat.{0} ℤ}
    (f g : relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∪ V))) (n+1) ⟶ Z)
    (hu : restrictedPairHomologyMap (Set.subset_union_left : U ⊆ U ∪ V) A (n+1) ≫ f =
      restrictedPairHomologyMap (Set.subset_union_left : U ⊆ U ∪ V) A (n+1) ≫ g)
    (hv : restrictedPairHomologyMap (Set.subset_union_right : V ⊆ U ∪ V) A (n+1) ≫ f =
      restrictedPairHomologyMap (Set.subset_union_right : V ⊆ U ∪ V) A (n+1) ≫ g) : f = g := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.restrictedPairHomologyMap

theorem OAI.Kaplansky.finiteRelativeOpenUnion_hom_ext line 247

Source documentation

The actual chart inclusions jointly detect maps out of a finite open union in degree n+1 if every intersection vanishes in degrees at most n.

theorem finiteRelativeOpenUnion_hom_ext (S : Finset ι) (U : ι → Set X)
    (A : Set X) (hopen : ∀ i ∈ S, IsOpen (U i)) (n : ℕ)
    (hinter : ∀ T : Finset ι, T.Nonempty → T ⊆ S → ∀ q < n+1,
      IsZero (relativeSingularHomology
        (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(⋂ i ∈ T, U i))) q))
    {Z : ModuleCat.{0} ℤ}
    (f g : relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(⋃ i ∈ S, U i))) (n+1) ⟶ Z)
    (hfg : ∀ i (_ : i ∈ S) (h : U i ⊆ ⋃ j ∈ S, U j),
      restrictedPairHomologyMap h A (n+1) ≫ f =
      restrictedPairHomologyMap h A (n+1) ≫ g) : f = g := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.restrictedPairHomologyMap

theorem OAI.Kaplansky.restrictedPairSubsetIso_map line 315

theorem OAI.Kaplansky.relativeOpenUnion_exists_glue line 332

Source documentation

Compatible linear maps on two open subspaces glue to a map on their union when the preceding overlap homology is zero.

theorem relativeOpenUnion_exists_glue (U V A : Set X)
    (hU : IsOpen U) (hV : IsOpen V) (n : ℕ)
    (hi : IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∩ V))) n))
    {Z : ModuleCat.{0} ℤ}
    (u : relativeSingularHomology (subspaceInclusion (Subtype.val ⁻¹' A : Set U)) (n+1) ⟶ Z)
    (v : relativeSingularHomology (subspaceInclusion (Subtype.val ⁻¹' A : Set V)) (n+1) ⟶ Z)
    (hcompat : restrictedPairHomologyMap (inter_subset_left : U ∩ V ⊆ U) A (n+1) ≫ u =
      restrictedPairHomologyMap (inter_subset_right : U ∩ V ⊆ V) A (n+1) ≫ v) :
    ∃ f : relativeSingularHomology
        (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∪ V))) (n+1) ⟶ Z,
      restrictedPairHomologyMap (subset_union_left : U ⊆ U ∪ V) A (n+1) ≫ f = u ∧
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.restrictedPairHomologyMap

theorem OAI.Kaplansky.restrictedPairToAmbient_univ_isIso line 388
Source documentation
Restricting a pair to the whole ambient set changes no homology.
```
theorem restrictedPairToAmbient_univ_isIso (A : Set X) (n : ℕ) :
    IsIso (restrictedPairToAmbientHomologyMap Set.univ A n) := by
…
```
Mentions: OAI.Kaplansky.restrictedPairToAmbientHomologyMap

theorem OAI.Kaplansky.finiteRelativeOpenCover_hom_ext line 400

Source documentation

Finite chart detection for the whole actual pair.

theorem finiteRelativeOpenCover_hom_ext (S : Finset ι) (U : ι → Set X)
    (A : Set X) (hopen : ∀ i ∈ S, IsOpen (U i))
    (hcover : (⋃ i ∈ S, U i) = Set.univ) (n : ℕ)
    (hinter : ∀ T : Finset ι, T.Nonempty → T ⊆ S → ∀ q < n+1,
      IsZero (relativeSingularHomology
        (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(⋂ i ∈ T, U i))) q))
    {Z : ModuleCat.{0} ℤ}
    (f g : relativeSingularHomology (subspaceInclusion A) (n+1) ⟶ Z)
    (hfg : ∀ i ∈ S, restrictedPairToAmbientHomologyMap (U i) A (n+1) ≫ f =
      restrictedPairToAmbientHomologyMap (U i) A (n+1) ≫ g) : f = g := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.restrictedPairToAmbientHomologyMap

theorem OAI.Kaplansky.finiteRelativeOpenUnion_exists_glue line 428

Source documentation

Pairwise compatible normalizations on a finite open cover glue in the first possibly nonzero relative degree. All inclusions are the actual restricted-pair maps; no extension of a homomorphism is postulated.

theorem finiteRelativeOpenUnion_exists_glue (S : Finset J) (U : J → Set X)
    (A : Set X) (hopen : ∀ i ∈ S, IsOpen (U i)) (n : ℕ)
    (hinter : ∀ T : Finset J, T.Nonempty → T ⊆ S → ∀ q < n+1,
      IsZero (relativeSingularHomology
        (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(⋂ i ∈ T, U i))) q))
    {Z : ModuleCat.{0} ℤ}
    (u : ∀ i, relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set (U i))) (n+1) ⟶ Z)
    (hc : ∀ i ∈ S, ∀ j ∈ S,
      restrictedPairHomologyMap (inter_subset_left : U i ∩ U j ⊆ U i) A (n+1) ≫ u i =
      restrictedPairHomologyMap (inter_subset_right : U i ∩ U j ⊆ U j) A (n+1) ≫ u j) :
    ∃ f : relativeSingularHomology
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.restrictedPairHomologyMap

theorem OAI.Kaplansky.finiteRelativeOpenCover_exists_glue line 508

Source documentation

A finite open cover now gives a genuine map on the whole pair.

theorem finiteRelativeOpenCover_exists_glue (S : Finset J) (U : J → Set X)
    (A : Set X) (hopen : ∀ i ∈ S, IsOpen (U i))
    (hcover : (⋃ i ∈ S, U i) = univ) (n : ℕ)
    (hinter : ∀ T : Finset J, T.Nonempty → T ⊆ S → ∀ q < n+1,
      IsZero (relativeSingularHomology
        (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(⋂ i ∈ T, U i))) q))
    {Z : ModuleCat.{0} ℤ}
    (u : ∀ i, relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set (U i))) (n+1) ⟶ Z)
    (hc : ∀ i ∈ S, ∀ j ∈ S,
      restrictedPairHomologyMap (inter_subset_left : U i ∩ U j ⊆ U i) A (n+1) ≫ u i =
      restrictedPairHomologyMap (inter_subset_right : U i ∩ U j ⊆ U j) A (n+1) ≫ u j) :
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.restrictedPairHomologyMap