Product.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Product-pair homology, pair homotopies, and diagonal normalization.

def OAI.Kaplansky.contractibleProductProjection line 18
Source documentation
Projection from a product with an actually contractible base, keeping the projection itself as the forward map.
```
def contractibleProductProjection [ContractibleSpace B] (V : Type) [TopologicalSpace V] :
    B × V ≃ₕ V := by
…
```
theorem OAI.Kaplansky.contractibleProductProjection_apply line 24
def OAI.Kaplansky.productSubspaceHomeomorph line 29
Source documentation
The punctured trivial-bundle subspace really is the product of the base and the punctured model.
```
def productSubspaceHomeomorph (W : Set V) :
    ({z : B × V | z.2 ∈ W} : Set (B × V)) ≃ₜ B × W where
…
```
def OAI.Kaplansky.productPairProjection line 40
theorem OAI.Kaplansky.productPairProjection_isIso line 48
Source documentation
Genuine relative homology normalization for a trivial bundle over any contractible base, with no homology or orientation assumption.
```
theorem productPairProjection_isIso [ContractibleSpace B] (W : Set V) (n : ℕ) :
    IsIso (productPairProjection (B := B) W n) := by
…
```
Mentions: OAI.Kaplansky.productPairProjection
def OAI.Kaplansky.productPairProjectionIso line 55

theorem OAI.Kaplansky.relativeHomologyHomeomorphIso_trans_hom line 59

Source documentation

Composition of homeomorphisms agrees with composition on relative homology.

theorem relativeHomologyHomeomorphIso_trans_hom
    {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    (e : X ≃ₜ Y) (f : Y ≃ₜ Z) (U : Set X) (V : Set Y) (W : Set Z)
    (he : ∀ x, x ∈ U ↔ e x ∈ V) (hf : ∀ y, y ∈ V ↔ f y ∈ W) (n : ℕ) :
    (relativeHomologyHomeomorphIso (e.trans f) U W
      (fun x => (he x).trans (hf (e x))) n).hom =
      (relativeHomologyHomeomorphIso e U V he n).hom ≫
        (relativeHomologyHomeomorphIso f V W hf n).hom := by
…

Mentions: OAI.Kaplansky.relativeHomologyHomeomorphIso

theorem OAI.Kaplansky.productPairNormalization_restrict line 73

Source documentation

Restricting product coordinates commutes with projection to relative fiber homology.

theorem productPairNormalization_restrict
    {X Y A B V : Type} [TopologicalSpace X] [TopologicalSpace Y]
    [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace V] [Zero V]
    (U : Set X) (W : Set Y) (i : C(X,Y)) (hi : Set.MapsTo i U W)
    (e : X ≃ₜ A × V) (f : Y ≃ₜ B × V)
    (he : ∀ x, x ∈ U ↔ (e x).2 ≠ 0) (hf : ∀ y, y ∈ W ↔ (f y).2 ≠ 0)
    (hcoords : ∀ x, (f (i x)).2 = (e x).2) (n : ℕ) :
    relativeHomologyMap (subspaceInclusion U) (subspaceInclusion W)
        (subspaceMap U W i hi) (TopCat.ofHom i) (subspaceMap_square U W i hi) n ≫
      ((relativeHomologyHomeomorphIso f W {z | z.2 ≠ 0} hf n).hom ≫
        productPairProjection (B := B) ({0}ᶜ : Set V) n) =
…

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

def OAI.Kaplansky.productPairFiberMap line 102
Source documentation
Inclusion of one genuine fiber of a product pair.
```
def productPairFiberMap (b : B) (W : Set V) (n : ℕ) :=
…
```
theorem OAI.Kaplansky.productPairFiberMap_projection line 109
Source documentation
The fiber inclusion is split injective over ANY base containing that point.
```
theorem productPairFiberMap_projection (b : B) (W : Set V) (n : ℕ) :
    productPairFiberMap b W n ≫ productPairProjection W n = 𝟙 _ := by
…
```
Mentions: OAI.Kaplansky.productPairFiberMap, OAI.Kaplansky.productPairProjection
theorem OAI.Kaplansky.productPairFiberMap_mono line 116
theorem OAI.Kaplansky.productPairFiberMap_eq_inv line 124
Source documentation
Over a contractible base the actual inclusion is the inverse normalization.
```
theorem productPairFiberMap_eq_inv [ContractibleSpace B] (b : B) (W : Set V) (n : ℕ) :
    productPairFiberMap b W n = (productPairProjectionIso (B := B) W n).inv := by
…
```
Mentions: OAI.Kaplansky.productPairFiberMap, OAI.Kaplansky.productPairProjectionIso
theorem OAI.Kaplansky.productPairFiberMap_eq line 131

theorem OAI.Kaplansky.relativeHomologyMap_homotopy line 145

Source documentation

A homotopy that carries the removed subspace into the removed subspace at EVERY time gives equal maps on relative singular homology. The proof uses the actual cylinder projection and its two equal inverse inclusions.

theorem relativeHomologyMap_homotopy (U : Set X) (V : Set Y)
    {f g : C(X,Y)} (hf : Set.MapsTo f U V) (hg : Set.MapsTo g U V)
    (H : Homotopy f g) (hH : ∀ t : I, ∀ x ∈ U, H (t,x) ∈ V) (n : ℕ) :
    relativeHomologyMap (subspaceInclusion U) (subspaceInclusion V)
      (subspaceMap U V f hf) (TopCat.ofHom f) (by rfl) n =
    relativeHomologyMap (subspaceInclusion U) (subspaceInclusion V)
      (subspaceMap U V g hg) (TopCat.ofHom g) (by rfl) n := by
…

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

theorem OAI.Kaplansky.productPairFiberMap_eq_of_joined line 172

Source documentation

Fiber inclusions agree along any actual path in the base.

theorem productPairFiberMap_eq_of_joined {B V : Type} [TopologicalSpace B]
    [TopologicalSpace V] {b c : B} (hbc : Joined b c) (W : Set V) (n : ℕ) :
    productPairFiberMap b W n = productPairFiberMap c W n := by
…

Mentions: OAI.Kaplansky.productPairFiberMap

def OAI.Kaplansky.complexDiagonalMap line 196
Source documentation
Complex diagonal coordinate change with every multiplier invertible.
```
def complexDiagonalMap (a : ι → ℂˣ) : C((ι → ℂ),(ι → ℂ)) :=
…
```
theorem OAI.Kaplansky.complexDiagonalMap_nonzero line 199
def OAI.Kaplansky.complexDiagonalHomotopy line 209
Source documentation
A path through complex units supplies a genuine nonzero-preserving homotopy to the identity; no determinant-to-degree assertion is assumed.
```
def complexDiagonalHomotopy (a : ι → ℂˣ) :
    Homotopy (complexDiagonalMap a) (ContinuousMap.id (ι → ℂ)) := by
…
```
Mentions: OAI.Kaplansky.complexDiagonalMap
theorem OAI.Kaplansky.complexDiagonalHomotopy_nonzero line 221
def OAI.Kaplansky.complexDiagonalRelativeMap line 226
theorem OAI.Kaplansky.complexDiagonalRelativeMap_eq_id line 234
Source documentation
Every invertible complex diagonal change acts as the identity on actual integral local relative homology, in every degree.
```
theorem complexDiagonalRelativeMap_eq_id (a : ι → ℂˣ) (n : ℕ) :
    complexDiagonalRelativeMap a n = 𝟙 _ := by
…
```
Mentions: OAI.Kaplansky.complexDiagonalRelativeMap

def OAI.Kaplansky.productPairCoordinateMap line 251

Source documentation

A map from a product pair to its fiber pair.

def productPairCoordinateMap (f : C(B × (ι → ℂ),(ι → ℂ)))
    (hf : ∀ z, z.2 ≠ 0 → f z ≠ 0) (n : ℕ) :=
…

theorem OAI.Kaplansky.productPairCoordinateMap_eq_projection line 260
Source documentation
Over an actually contractible base, checking one fiber suffices. An invertible complex diagonal change there preserves the full normalization. The map away from that fiber may vary arbitrarily and need not be linear.
```
theorem productPairCoordinateMap_eq_projection [ContractibleSpace B]
    (f : C(B × (ι → ℂ),(ι → ℂ))) (hf : ∀ z, z.2 ≠ 0 → f z ≠ 0)
    (b : B) (a : ι → ℂˣ) (he : ∀ v, f (b,v) = complexDiagonalMap a v) (n : ℕ) :
    productPairCoordinateMap f hf n =
      productPairProjection (B := B) ({0}ᶜ : Set (ι → ℂ)) n := by
…
```
Mentions: OAI.Kaplansky.complexDiagonalMap, OAI.Kaplansky.productPairCoordinateMap, OAI.Kaplansky.productPairProjection
def OAI.Kaplansky.complexLineCoordinateUnit line 280
Source documentation
The unit comparing two genuine complex coordinates on a line.
```
def complexLineCoordinateUnit {L : Type} [AddCommGroup L] [Module ℂ L]
    (e f : L ≃ₗ[ℂ] ℂ) : ℂˣ :=
…
```
theorem OAI.Kaplansky.complexLineCoordinate_change line 288