Equivalence.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Contractible-pair homology, equivalences, and relative map extensionality.

def OAI.Kaplansky.integralHomologyHomotopyIso line 16

Source documentation

An actual homotopy equivalence induces an integral homology isomorphism.

def integralHomologyHomotopyIso {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    (e : X ≃ₕ Y) (n : ℕ) :
    (integralSingularHomology n).obj (TopCat.of X) ≅
      (integralSingularHomology n).obj (TopCat.of Y) where
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.integralSingularHomology_isZero_contractible line 31
def OAI.Kaplansky.contractibleRelativeBoundaryIso line 45
Source documentation
In degrees at least two, relative homology in a contractible ambient space is the preceding homology of the subspace, via the actual boundary.
```
def contractibleRelativeBoundaryIso {A X : TopCat.{0}} (i : A ⟶ X) [Mono i]
    [ContractibleSpace X] (n : ℕ) (hn : n ≠ 0) :
    relativeSingularHomology i (n+1) ≅ (integralSingularHomology n).obj A :=
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.contractibleRelativeBoundaryIso_hom line 52
def OAI.Kaplansky.puncturedVectorBoundaryIso line 56
def OAI.Kaplansky.relativeChainsHomeomorphIso line 69
Source documentation
A genuine homeomorphism of pairs acts invertibly on relative singular chains.
```
def relativeChainsHomeomorphIso (e : X ≃ₜ Y) (U : Set X) (V : Set Y)
    (h : ∀ x, x ∈ U ↔ e x ∈ V) :
    relativeSingularChains (subspaceInclusion U) ≅
      relativeSingularChains (subspaceInclusion V) :=
…
```
Mentions: OAI.Kaplansky.relativeSingularChains, OAI.Kaplansky.subspaceInclusion
def OAI.Kaplansky.relativeHomologyHomeomorphIso line 82

theorem OAI.Kaplansky.relativeHomologyHomeomorphIso_hom line 89

Source documentation

The isomorphism is the same map as that induced by the actual map of pairs.

theorem relativeHomologyHomeomorphIso_hom (e : X ≃ₜ Y) (U : Set X) (V : Set Y)
    (h : ∀ x, x ∈ U ↔ e x ∈ V) (n : ℕ) :
    (relativeHomologyHomeomorphIso e U V h n).hom =
      relativeHomologyMap (subspaceInclusion U) (subspaceInclusion V)
        (subspaceMap U V ⟨e, e.continuous⟩ (fun x hx => (h x).mp hx))
        (TopCat.ofHom ⟨e, e.continuous⟩) (subspaceMap_square _ _ _ _) n := rfl

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

def OAI.Kaplansky.localHomologyHomeomorphIso line 96

theorem OAI.Kaplansky.relativeHomologyMap_congr_ambient line 109

Source documentation

Into an embedded subspace, the ambient map uniquely determines the map of relative chains and hence of relative homology.

theorem relativeHomologyMap_congr_ambient {A X B Y : TopCat.{0}}
    (i : A ⟶ X) (j : B ⟶ Y) [Mono j]
    (a b : A ⟶ B) (f g : X ⟶ Y)
    (h : i ≫ f = a ≫ j) (h' : i ≫ g = b ≫ j) (he : f = g) (n : ℕ) :
    relativeHomologyMap i j a f h n = relativeHomologyMap i j b g h' n := by
…

Mentions: OAI.Kaplansky.relativeHomologyMap

theorem OAI.Kaplansky.integralChains_homotopyEquiv_quasiIso line 125

Source documentation

Singular chains of an actual homotopy equivalence form a quasi-isomorphism.

theorem integralChains_homotopyEquiv_quasiIso {X Y : Type}
    [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₕ Y) :
    QuasiIso (integralSingularChains.map (TopCat.ofHom e.toFun)) := by
…

theorem OAI.Kaplansky.relativeHomologyMap_isIso_of_equivalences line 136

Source documentation

A map of genuine pairs whose ambient and subspace maps are homotopy equivalences induces an isomorphism on relative homology in every degree.

theorem relativeHomologyMap_isIso_of_equivalences
    {A X B Y : Type} [TopologicalSpace A] [TopologicalSpace X]
    [TopologicalSpace B] [TopologicalSpace Y]
    (i : TopCat.of A ⟶ TopCat.of X) (j : TopCat.of B ⟶ TopCat.of Y)
    [Mono i] [Mono j] (a : A ≃ₕ B) (f : X ≃ₕ Y)
    (h : i ≫ TopCat.ofHom f.toFun = TopCat.ofHom a.toFun ≫ j) (n : ℕ) :
    IsIso (relativeHomologyMap i j (TopCat.ofHom a.toFun) (TopCat.ofHom f.toFun) h n) := by
…

Mentions: OAI.Kaplansky.relativeHomologyMap