SmallExcision.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

Small relative excision, Mayer-Vietoris, and naturality.

def OAI.Kaplansky.subspaceInclusionOfLE line 20
Source documentation
Inclusion between subspaces of the same ambient space.
```
def subspaceInclusionOfLE {U V : Set X} (h : U ⊆ V) :
    TopCat.of U ⟶ TopCat.of V :=
…
```
instance OAI.Kaplansky.(instance at line 25) line 25
theorem OAI.Kaplansky.subspaceInclusionOfLE_comp line 31
theorem OAI.Kaplansky.singularSubsetIso_naturality line 34
def OAI.Kaplansky.singularIntersectionIso line 40
theorem OAI.Kaplansky.singularIntersectionIso_left line 44
theorem OAI.Kaplansky.singularIntersectionIso_right line 51
def OAI.Kaplansky.singularIntoSmallLeft line 58
def OAI.Kaplansky.singularIntoSmallRight line 62
theorem OAI.Kaplansky.smallSingularSet_isPushout line 66
def OAI.Kaplansky.singularChainsIntoSmallLeft line 81
def OAI.Kaplansky.singularChainsIntoSmallRight line 85
theorem OAI.Kaplansky.singularChainsIntoSmallLeft_inclusion line 90
theorem OAI.Kaplansky.singularChainsIntoSmallRight_inclusion line 99
theorem OAI.Kaplansky.smallSingularChains_isPushout line 107
def OAI.Kaplansky.smallMayerVietorisSequence line 116
Source documentation
Mayer–Vietoris chain sequence for genuine subspaces, with the complex of small chains at the right. No open-cover comparison is assumed.
```
def smallMayerVietorisSequence (U V : Set X) :=
…
```
theorem OAI.Kaplansky.smallMayerVietorisSequence_shortExact line 119
def OAI.Kaplansky.smallMayerVietorisBoundary line 131
theorem OAI.Kaplansky.smallMayerVietoris_exact line 136
def OAI.Kaplansky.smallSingularChainsMap line 146
instance OAI.Kaplansky.(instance at line 151) line 151
theorem OAI.Kaplansky.smallSingularChainsMap_inclusion line 156
theorem OAI.Kaplansky.singularChainsIntoSmallLeft_map line 164
theorem OAI.Kaplansky.singularChainsIntoSmallRight_map line 172
def OAI.Kaplansky.smallMayerVietorisSequenceMap line 181
Source documentation
Naturality of the actual small-chain gluing sequence under inclusions of both members of the cover.
```
def smallMayerVietorisSequenceMap (hU : U₀ ⊆ U) (hV : V₀ ⊆ V) :
    smallMayerVietorisSequence U₀ V₀ ⟶ smallMayerVietorisSequence U V where
…
```
Mentions: OAI.Kaplansky.smallMayerVietorisSequence
def OAI.Kaplansky.smallRelativeMayerVietorisSequence line 198
Source documentation
Relative Mayer–Vietoris at chain level. The removed set is restricted to each chart and to their intersection; at the right it uses small chains in the removed subspace. Comparison with full chains is a separate theorem.
```
def smallRelativeMayerVietorisSequence (U V A : Set X) :=
…
```
theorem OAI.Kaplansky.smallRelativeMayerVietorisSequence_shortExact line 202
def OAI.Kaplansky.smallRelativeChains line 221
Source documentation
Small relative chains modulo the full chains of the second subspace.
```
def smallRelativeChains : ChainComplex (ModuleCat.{0} ℤ) ℕ :=
…
```
def OAI.Kaplansky.smallRelativeExcisionIso line 226
Source documentation
Actual chain-level excision into small relative chains. This needs no openness or covering hypothesis because the target only uses small simplices.
```
def smallRelativeExcisionIso :
    relativeSingularChains (subspaceInclusionOfLE (Set.inter_subset_left : U ∩ V ⊆ U)) ≅
      smallRelativeChains U V := by
…
```
Mentions: OAI.Kaplansky.relativeSingularChains, OAI.Kaplansky.subspaceInclusionOfLE, OAI.Kaplansky.smallRelativeChains
def OAI.Kaplansky.smallRelativeComparison line 235
Source documentation
Comparison with the full relative chains of (X,V).
```
def smallRelativeComparison : smallRelativeChains U V ⟶
    relativeSingularChains (subspaceInclusion V) :=
…
```
Mentions: OAI.Kaplansky.smallRelativeChains, OAI.Kaplansky.relativeSingularChains, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.smallRelativeExcision_comparison line 242
Source documentation
The composition of small excision and comparison is exactly the map induced by the inclusions of pairs (U,U∩V) → (X,V).
```
theorem smallRelativeExcision_comparison :
    (smallRelativeExcisionIso U V).hom ≫ smallRelativeComparison U V =
      relativeChainMap
        (subspaceInclusionOfLE (Set.inter_subset_left : U ∩ V ⊆ U))
        (subspaceInclusion V)
        (subspaceInclusionOfLE (Set.inter_subset_right : U ∩ V ⊆ V))
        (subspaceInclusion U) (by rfl) := by
…
```
Mentions: OAI.Kaplansky.smallRelativeExcisionIso, OAI.Kaplansky.smallRelativeComparison, OAI.Kaplansky.relativeChainMap, OAI.Kaplansky.subspaceInclusionOfLE, OAI.Kaplansky.subspaceInclusion
def OAI.Kaplansky.smallRelativeHomologyIso line 257
instance OAI.Kaplansky.(instance at line 263) line 263
def OAI.Kaplansky.smallRelativeSequence line 269
theorem OAI.Kaplansky.smallRelativeSequence_shortExact line 273
def OAI.Kaplansky.smallRelativeSequenceComparison line 278
theorem OAI.Kaplansky.smallRelativeComparison_quasiIso line 288
Source documentation
The purely homological step in singular excision. Its explicit premise is the small-chain theorem, which still requires subdivision for open covers.
```
theorem smallRelativeComparison_quasiIso
    (h : QuasiIso (smallSingularChainInclusion U V)) :
    QuasiIso (smallRelativeComparison U V) :=
…
```
Mentions: OAI.Kaplansky.smallSingularChainInclusion, OAI.Kaplansky.smallRelativeComparison

theorem OAI.Kaplansky.relativeInclusion_isIso_of_smallChains line 298

Source documentation

The resulting isomorphism acts on the original relative singular map, not a proposition introduced to stand for excision.

theorem relativeInclusion_isIso_of_smallChains
    (h : QuasiIso (smallSingularChainInclusion U V)) (n : ℕ) :
    IsIso (relativeHomologyMap
      (subspaceInclusionOfLE (Set.inter_subset_left : U ∩ V ⊆ U))
      (subspaceInclusion V)
      (subspaceInclusionOfLE (Set.inter_subset_right : U ∩ V ⊆ V))
      (subspaceInclusion U) (by rfl) n) := by
…

Mentions: OAI.Kaplansky.smallSingularChainInclusion, OAI.Kaplansky.relativeHomologyMap, OAI.Kaplansky.subspaceInclusionOfLE, OAI.Kaplansky.subspaceInclusion

theorem OAI.Kaplansky.smallMayerVietoris_exact_at_intersection line 322
Source documentation
Exactness at the intersection term of the actual small-chain sequence.
```
theorem smallMayerVietoris_exact_at_intersection (n : ℕ) :
    (ShortComplex.mk _ _
      ((smallMayerVietorisSequence_shortExact U V).δ_comp (n+1) n rfl)).Exact :=
…
```
Mentions: OAI.Kaplansky.smallMayerVietorisSequence_shortExact
theorem OAI.Kaplansky.smallMayerVietoris_exact_at_sum line 328
Source documentation
Exactness at the homology of the sum of the two subspace complexes.
```
theorem smallMayerVietoris_exact_at_sum (n : ℕ) :
    ((smallMayerVietorisSequence U V).map
      (homologyFunctor (ModuleCat ℤ) (ComplexShape.down ℕ) n)).Exact :=
…
```
Mentions: OAI.Kaplansky.smallMayerVietorisSequence
theorem OAI.Kaplansky.homology_biprod_isZero line 333
theorem OAI.Kaplansky.smallMayerVietoris_sum_isZero line 344
def OAI.Kaplansky.smallMayerVietorisBoundaryIso line 354
Source documentation
For two contractible subspaces, the actual small-chain connecting map is an isomorphism in degrees at least two. Full singular homology still requires the small-to-full comparison theorem.
```
def smallMayerVietorisBoundaryIso [ContractibleSpace U] [ContractibleSpace V]
    (n : ℕ) (hn : n ≠ 0) :
    (smallSingularChains U V).homology (n+1) ≅
      (integralSingularHomology n).obj (TopCat.of ↥(U ∩ V)) :=
…
```
Mentions: OAI.Kaplansky.smallSingularChains, OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.smallMayerVietorisBoundaryIso_hom line 362
def OAI.Kaplansky.smallSingularChainsContinuousMap line 376
Source documentation
The induced map on small chains for a continuous map respecting covers. The construction uses the proved pushout of actual singular-chain complexes.
```
def smallSingularChainsContinuousMap : smallSingularChains U V ⟶ smallSingularChains U' V' :=
…
```
Mentions: OAI.Kaplansky.smallSingularChains
theorem OAI.Kaplansky.smallSingularChainsContinuousMap_left line 387
theorem OAI.Kaplansky.smallSingularChainsContinuousMap_right line 393
theorem OAI.Kaplansky.smallSingularChainsContinuousMap_inclusion line 399
theorem OAI.Kaplansky.smallSingularChainsContinuousMap_mono line 405
def OAI.Kaplansky.smallMayerVietorisContinuousMap line 415
Source documentation
Naturality includes the intersection term and the signs of the Mayer–Vietoris differential.
```
def smallMayerVietorisContinuousMap :
    smallMayerVietorisSequence U V ⟶ smallMayerVietorisSequence U' V' where
…
```
Mentions: OAI.Kaplansky.smallMayerVietorisSequence