Excision.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Excision for chart-small chains, open covers, and open embeddings.

def OAI.Kaplansky.puncturedChartIntersectionHomeomorph line 20
Source documentation
The punctured subspace and its ambient intersection have the same inherited topology, with the same underlying points.
```
def puncturedChartIntersectionHomeomorph (U : Set X) (x : X) (hx : x ∈ U) :
    ({⟨x, hx⟩}ᶜ : Set U) ≃ₜ ↥(U ∩ ({x}ᶜ : Set X)) := by
…
```
def OAI.Kaplansky.puncturedChartRelativeChainsIso line 37
def OAI.Kaplansky.chartRelativeChainInclusion line 48
def OAI.Kaplansky.chartSmallRelativeChainsIso line 59
Source documentation
Local relative chains are isomorphic to the small relative chains of the actual cover by the chart and the punctured ambient space.
```
def chartSmallRelativeChainsIso :
    relativeSingularChains (subspaceInclusion ({⟨x, hx⟩}ᶜ : Set U)) ≅
      smallRelativeChains U ({x}ᶜ : Set X) :=
…
```
Mentions: OAI.Kaplansky.relativeSingularChains, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.smallRelativeChains
theorem OAI.Kaplansky.chartSmallRelativeChainsIso_comparison line 64
theorem OAI.Kaplansky.chart_punctured_cover line 76
def OAI.Kaplansky.canonicalChartSmallRelativeIso line 88
theorem OAI.Kaplansky.canonicalChartRelativeInclusion_factor line 99
Source documentation
Exact factorization of the preserved projective-chart inclusion. The first factor is proved invertible. The second still needs subdivision.
```
theorem canonicalChartRelativeInclusion_factor (n : ℕ) :
    canonicalChartRelativeInclusion K n =
    (canonicalChartSmallRelativeIso K n).hom ≫
        HomologicalComplex.homologyMap
          (smallRelativeComparison (canonicalProductGraphChart K).source
            ({firstCoordinateProduct K}ᶜ : Set (ProjectiveProduct K))) n := by
…
```
Mentions: OAI.Kaplansky.canonicalChartRelativeInclusion, OAI.Kaplansky.canonicalChartSmallRelativeIso, OAI.Kaplansky.smallRelativeComparison, OAI.Kaplansky.canonicalProductGraphChart, OAI.Kaplansky.firstCoordinateProduct
theorem OAI.Kaplansky.canonicalChartRelativeInclusion_isIso_of_smallChains line 111
theorem OAI.Kaplansky.canonicalChart_punctured_open_cover line 120
def OAI.Kaplansky.openCoverSmallHomologyIso line 136
Source documentation
Comparison from the homology of small chains to full integral singular homology for a genuine two-set open cover.
```
def openCoverSmallHomologyIso (hU : IsOpen U) (hV : IsOpen V)
    (hUV : U ∪ V = Set.univ) (n : ℕ) :
    (smallSingularChains U V).homology n ≅ (integralSingularChains.obj (TopCat.of X)).homology n := by
…
```
Mentions: OAI.Kaplansky.smallSingularChains

theorem OAI.Kaplansky.openCover_relativeInclusion_isIso line 143

Source documentation

Singular relative excision for an actual two-set open cover.

theorem openCover_relativeInclusion_isIso (hU : IsOpen U) (hV : IsOpen V)
    (hUV : U ∪ V = Set.univ) (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) :=
…

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

def OAI.Kaplansky.openCoverMayerVietorisBoundaryIso line 155

Source documentation

Full singular Mayer–Vietoris boundary isomorphism for a cover by two contractible open subspaces, in degrees at least two.

def openCoverMayerVietorisBoundaryIso [ContractibleSpace U] [ContractibleSpace V]
    (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
    (n : ℕ) (hn : n ≠ 0) :
    (integralSingularHomology (n+1)).obj (TopCat.of X) ≅
      (integralSingularHomology n).obj (TopCat.of ↥(U ∩ V)) :=
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.canonicalChartRelativeInclusion_isIso line 168
Source documentation
The preserved canonical projective-chart relative inclusion is now proved invertible, with no small-chain or excision premise.
```
theorem canonicalChartRelativeInclusion_isIso (n : ℕ) :
    IsIso (canonicalChartRelativeInclusion K n) := by
…
```
Mentions: OAI.Kaplansky.canonicalChartRelativeInclusion
def OAI.Kaplansky.canonicalChartExcisionIso line 175
Source documentation
Actual local singular homology equivalence for the canonical chart.
```
def canonicalChartExcisionIso (n : ℕ) :=
…
```
def OAI.Kaplansky.embeddingRelativeChainsIso line 186
Source documentation
The inverse-image pair of an embedding is the actual intersection pair in its image, including its inherited subspace topology.
```
def embeddingRelativeChainsIso (f : C(X,Y)) (hf : IsEmbedding f) (V : Set Y) :
    relativeSingularChains (subspaceInclusion (f ⁻¹' V)) ≅
      relativeSingularChains (subspaceInclusionOfLE
        (Set.inter_subset_left : Set.range f ∩ V ⊆ Set.range f)) :=
…
```
Mentions: OAI.Kaplansky.relativeSingularChains, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.subspaceInclusionOfLE

theorem OAI.Kaplansky.embeddingRelativeChainsIso_comparison line 202

Source documentation

Exact chain factorization through the image pair.

theorem embeddingRelativeChainsIso_comparison (f : C(X,Y)) (hf : IsEmbedding f)
    (V : Set Y) :
    (embeddingRelativeChainsIso f hf V).hom ≫ relativeChainMap
      (subspaceInclusionOfLE (Set.inter_subset_left : Set.range f ∩ V ⊆ Set.range f))
      (subspaceInclusion V)
      (subspaceInclusionOfLE (Set.inter_subset_right : Set.range f ∩ V ⊆ V))
      (subspaceInclusion (Set.range f)) (by rfl) =
    relativeChainMap (subspaceInclusion (f ⁻¹' V)) (subspaceInclusion V)
      (subspaceMap _ _ f (fun _ h => h)) (TopCat.ofHom f) (by rfl) := by
…

Mentions: OAI.Kaplansky.embeddingRelativeChainsIso, OAI.Kaplansky.relativeChainMap, OAI.Kaplansky.subspaceInclusionOfLE, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.subspaceMap

theorem OAI.Kaplansky.openEmbedding_relativeHomologyMap_isIso line 220

Source documentation

Excision for an actual open embedding, when its image and the removed open subspace cover the target. The map is the original map of pairs.

theorem openEmbedding_relativeHomologyMap_isIso (f : C(X,Y)) (hf : IsOpenEmbedding f)
    (V : Set Y) (hV : IsOpen V) (hcover : Set.range f ∪ V = Set.univ) (n : ℕ) :
    IsIso (relativeHomologyMap (subspaceInclusion (f ⁻¹' V)) (subspaceInclusion V)
      (subspaceMap _ _ f (fun _ h => h)) (TopCat.ofHom f) (by rfl) n) := by
…

Mentions: OAI.Kaplansky.relativeHomologyMap, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.subspaceMap

def OAI.Kaplansky.openChartLocalExcisionIso line 240
Source documentation
Excision at any point of an open chart, using the preserved chain-level comparison and the proved open-cover small-chain theorem.
```
def openChartLocalExcisionIso (U : Set X) (hU : IsOpen U) (x : X) (hx : x ∈ U) (n : ℕ) :
    relativeSingularHomology (subspaceInclusion ({⟨x,hx⟩}ᶜ : Set U)) n ≅
      relativeSingularHomology (subspaceInclusion ({x}ᶜ : Set X)) n := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion
theorem OAI.Kaplansky.openChartLocalExcisionIso_hom line 250
Source documentation
The excision isomorphism is precisely the actual inclusion of local chains.
```
theorem openChartLocalExcisionIso_hom (U : Set X) (hU : IsOpen U)
    (x : X) (hx : x ∈ U) (n : ℕ) :
    (openChartLocalExcisionIso U hU x hx n).hom =
      homologyMap (chartRelativeChainInclusion U x hx) n := by
…
```
Mentions: OAI.Kaplansky.openChartLocalExcisionIso, OAI.Kaplansky.chartRelativeChainInclusion

def OAI.Kaplansky.centeredChartHomeomorph line 258

Source documentation

Center an arbitrary full vector-space chart at the point under study.

def centeredChartHomeomorph {E : Type} [NormedAddCommGroup E]
    (U : Set X) (x : X) (hx : x ∈ U) (e : U ≃ₜ E) : U ≃ₜ E :=
…

theorem OAI.Kaplansky.centeredChartHomeomorph_center line 263

def OAI.Kaplansky.openChartCoordinateLocalHomologyIso line 269

Source documentation

Local homology in a full open vector-space chart, at an arbitrary point.

def openChartCoordinateLocalHomologyIso {E : Type} [NormedAddCommGroup E]
    (U : Set X) (hU : IsOpen U) (x : X) (hx : x ∈ U) (e : U ≃ₜ E) (n : ℕ) :
    relativeSingularHomology (subspaceInclusion ({x}ᶜ : Set X)) n ≅
      relativeSingularHomology (subspaceInclusion ({0}ᶜ : Set E)) n :=
…

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