MayerVietoris.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

Relative Mayer-Vietoris comparison, exactness, and gluing.

theorem OAI.Kaplansky.comp_zero_of_iso line 17
def OAI.Kaplansky.removedCoverSequenceMap line 29
Source documentation
The inclusion of the removed subspace, with its induced two-set cover.
```
def removedCoverSequenceMap :
    smallMayerVietorisSequence (Subtype.val ⁻¹' U : Set A) (Subtype.val ⁻¹' V : Set A) ⟶
      smallMayerVietorisSequence U V :=
…
```
Mentions: OAI.Kaplansky.smallMayerVietorisSequence
theorem OAI.Kaplansky.removedCoverSequenceMap_mono line 35
def OAI.Kaplansky.relativeCoverChainSequence line 40
Source documentation
The relative gluing sequence formed using the actual singular chains of A. Its right term compares directly with C(X)/C(A).
```
def relativeCoverChainSequence := quotientShortComplex (removedCoverSequenceMap U V A)
```
Mentions: OAI.Kaplansky.quotientShortComplex, OAI.Kaplansky.removedCoverSequenceMap
theorem OAI.Kaplansky.relativeCoverChainSequence_shortExact line 42
def OAI.Kaplansky.relativeCoverChainComparison line 48
def OAI.Kaplansky.relativeCoverQuotientSequence line 53
theorem OAI.Kaplansky.relativeCoverQuotientSequence_shortExact line 57
def OAI.Kaplansky.relativeCoverQuotientSequenceComparison line 65
theorem OAI.Kaplansky.relativeCoverChainComparison_quasiIso line 75
Source documentation
Subdivision on both X and A proves comparison with full relative singular chains. No openness of A is needed.
```
theorem relativeCoverChainComparison_quasiIso (hU : IsOpen U) (hV : IsOpen V)
    (hcover : U ∪ V = Set.univ) : QuasiIso (relativeCoverChainComparison U V A) := by
…
```
Mentions: OAI.Kaplansky.relativeCoverChainComparison
def OAI.Kaplansky.relativeOpenCoverHomologyIso line 87
def OAI.Kaplansky.intersectionSubtypeSwap line 103
Source documentation
The same intersection subspace, in the opposite order of its subtypes.
```
def intersectionSubtypeSwap (U A : Set X) :
    (Subtype.val ⁻¹' U : Set A) ≃ₜ (Subtype.val ⁻¹' A : Set U) where
…
```
def OAI.Kaplansky.removedRestrictionMap line 112
def OAI.Kaplansky.removedRestrictionChainsIso line 117
Source documentation
The relative chain group in a chart uses its actual removed subspace.
```
def removedRestrictionChainsIso (U A : Set X) :
    cokernel (integralSingularChains.map (removedRestrictionMap U A)) ≅
      relativeSingularChains (subspaceInclusion (Subtype.val ⁻¹' A : Set U)) :=
…
```
Mentions: OAI.Kaplansky.removedRestrictionMap, OAI.Kaplansky.relativeSingularChains, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.removedRestrictionChainsIso_projection line 128
def OAI.Kaplansky.relativeCoverLeftChainsIso line 134
def OAI.Kaplansky.relativeCoverMiddleChainsIso line 139
def OAI.Kaplansky.relativeCoverLeftHomologyIso line 146
def OAI.Kaplansky.relativeCoverMiddleHomologyIso line 151
def OAI.Kaplansky.restrictedPairChainMap line 164
Source documentation
Inclusion of restricted pairs (U,U∩A) into (V,V∩A).
```
def restrictedPairChainMap {U V : Set X} (h : U ⊆ V) (A : Set X) :=
…
```
def OAI.Kaplansky.restrictedPairToAmbientChainMap line 171
Source documentation
Inclusion of the actual chart pair into the whole pair.
```
def restrictedPairToAmbientChainMap (U A : Set X) :=
…
```
def OAI.Kaplansky.restrictedPairHomologyMap line 177
def OAI.Kaplansky.restrictedPairToAmbientHomologyMap line 182
theorem OAI.Kaplansky.restrictedPairChainMap_toAmbient line 187
theorem OAI.Kaplansky.restrictedPairHomologyMap_toAmbient line 194
theorem OAI.Kaplansky.relativeCoverMiddleChainsIso_projection line 201
theorem OAI.Kaplansky.relativeCoverLeftChainsIso_map line 218
Source documentation
Identification of the left gluing map, including its minus sign, with the two actual inclusions of intersection pairs.
```
theorem relativeCoverLeftChainsIso_map (U V A : Set X) :
    (relativeCoverLeftChainsIso U V A).hom ≫
      biprod.lift (restrictedPairChainMap (Set.inter_subset_left : U ∩ V ⊆ U) A)
        (-restrictedPairChainMap (Set.inter_subset_right : U ∩ V ⊆ V) A) =
    (relativeCoverChainSequence U V A).f ≫ (relativeCoverMiddleChainsIso U V A).hom := by
…
```
Mentions: OAI.Kaplansky.relativeCoverLeftChainsIso, OAI.Kaplansky.restrictedPairChainMap, OAI.Kaplansky.relativeCoverChainSequence, OAI.Kaplansky.relativeCoverMiddleChainsIso
theorem OAI.Kaplansky.relativeCoverMiddleChainsIso_map line 243
Source documentation
Identification of the right gluing map with the sum of the actual inclusions into (X,A), after the proved small-to-full chain comparison.
```
theorem relativeCoverMiddleChainsIso_map (U V A : Set X) :
    (relativeCoverMiddleChainsIso U V A).hom ≫
      biprod.desc (restrictedPairToAmbientChainMap U A) (restrictedPairToAmbientChainMap V A) =
    (relativeCoverChainSequence U V A).g ≫ relativeCoverChainComparison U V A := by
…
```
Mentions: OAI.Kaplansky.relativeCoverMiddleChainsIso, OAI.Kaplansky.restrictedPairToAmbientChainMap, OAI.Kaplansky.relativeCoverChainSequence, OAI.Kaplansky.relativeCoverChainComparison
theorem OAI.Kaplansky.relativeCoverLeftHomologyIso_map line 268
theorem OAI.Kaplansky.relativeCoverMiddleHomologyIso_map line 282
def OAI.Kaplansky.relativeMayerVietorisSumSequence line 297
Source documentation
The exact relative Mayer–Vietoris sequence at the direct sum, with the standard signed intersection map and actual pair inclusions.
```
def relativeMayerVietorisSumSequence (n : ℕ) : ShortComplex (ModuleCat.{0} ℤ) where
…
```
def OAI.Kaplansky.relativeMayerVietorisSumSequenceIso line 303
theorem OAI.Kaplansky.relativeMayerVietoris_exact_at_sum line 313
def OAI.Kaplansky.relativeMayerVietorisBoundary line 320
Source documentation
The connecting map on the actual full relative homology groups.
```
def relativeMayerVietorisBoundary (hU : IsOpen U) (hV : IsOpen V)
    (hcover : U ∪ V = Set.univ) (n : ℕ) :=
…
```
theorem OAI.Kaplansky.relativeMayerVietoris_sum_boundary line 326
theorem OAI.Kaplansky.relativeMayerVietoris_exact_at_relative line 338

theorem OAI.Kaplansky.relativeOpenCover_left_image_zero_iff line 357

Source documentation

The exact reason a class in one chart can die in the whole pair: it comes from an overlap class whose image in the other chart is zero.

theorem relativeOpenCover_left_image_zero_iff (n : ℕ)
    (z : relativeSingularHomology (subspaceInclusion (Subtype.val ⁻¹' A : Set U)) n) :
    restrictedPairToAmbientHomologyMap U A n z = 0 ↔
      ∃ w : relativeSingularHomology
          (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∩ V))) n,
        restrictedPairHomologyMap (Set.inter_subset_left : U ∩ V ⊆ U) A n w = z ∧
        restrictedPairHomologyMap (Set.inter_subset_right : U ∩ V ⊆ V) A n w = 0 := by
…

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

theorem OAI.Kaplansky.relativeOpenCover_left_mono line 394
theorem OAI.Kaplansky.relativeOpenCover_sum_epi line 409
Source documentation
Below the overlap degree, the two actual chart maps jointly generate the full relative homology group.
```
theorem relativeOpenCover_sum_epi (n : ℕ)
    (hi : IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∩ V))) n)) :
    Epi (relativeMayerVietorisSumSequence U V A (n+1)).g := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.relativeMayerVietorisSumSequence

def OAI.Kaplansky.relativeOpenCoverGlue line 418

Source documentation

Compatible local linear normalizations glue to a genuine global normalization when the preceding overlap group vanishes.

def relativeOpenCoverGlue (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 (Set.inter_subset_left : U ∩ V ⊆ U) A (n+1) ≫ u =
      restrictedPairHomologyMap (Set.inter_subset_right : U ∩ V ⊆ V) A (n+1) ≫ v) :
    relativeSingularHomology (subspaceInclusion A) (n+1) ⟶ Z := by
…

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

theorem OAI.Kaplansky.relativeOpenCoverGlue_restrictions line 434
theorem OAI.Kaplansky.relativeMayerVietoris_boundary_sum line 470
theorem OAI.Kaplansky.relativeMayerVietoris_exact_at_intersection line 481

theorem OAI.Kaplansky.relativeOpenCover_isZero line 494

Source documentation

Vanishing criterion in full relative singular homology, suitable for inductively joining bundle charts.

theorem relativeOpenCover_isZero (n : ℕ)
    (hu : IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set U)) (n+1)))
    (hv : IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set V)) (n+1)))
    (hi : IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∩ V))) n)) :
    IsZero (relativeSingularHomology (subspaceInclusion A) (n+1)) := by
…

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

theorem OAI.Kaplansky.relativeOpenCover_hom_ext line 512

Source documentation

Agreement on the two charts determines a global normalization uniquely when the preceding overlap group vanishes.

theorem relativeOpenCover_hom_ext (n : ℕ)
    (hi : IsZero (relativeSingularHomology
      (subspaceInclusion (Subtype.val ⁻¹' A : Set ↥(U ∩ V))) n))
    {Z : ModuleCat.{0} ℤ}
    (f g : relativeSingularHomology (subspaceInclusion A) (n+1) ⟶ Z)
    (hu : restrictedPairToAmbientHomologyMap U A (n+1) ≫ f =
      restrictedPairToAmbientHomologyMap U A (n+1) ≫ g)
    (hv : restrictedPairToAmbientHomologyMap V A (n+1) ≫ f =
      restrictedPairToAmbientHomologyMap V A (n+1) ≫ g) : f = g := by
…

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