TopologicalDeformationTransport.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

Straightening a boundary homotopy with a specified square

The realized cylinder ends and side form a pushout. A homotopy of the boundary path to a constant path, fixed at both ends, extends across that pushout by the actual realization homotopy extension property.

def OAI.Thomason.Construction.RealizationHomotopyRectification.pathAt line 31
def OAI.Thomason.Construction.RealizationHomotopyRectification.constantPath line 34
theorem OAI.Thomason.Construction.RealizationHomotopyRectification.constantPath_pathAt line 37
theorem OAI.Thomason.Construction.RealizationHomotopyRectification.cylinder_comparison line 40
theorem OAI.Thomason.Construction.RealizationHomotopyRectification.cylinder_zero line 48
theorem OAI.Thomason.Construction.RealizationHomotopyRectification.cylinder_one line 59

theorem OAI.Thomason.Construction.RealizationHomotopyRectification.interval_boundary_hom_ext line 72

Source documentation

The two ends detect maps out of the actual realized interval boundary, with an arbitrary simplicial parameter and arbitrary topological target.

theorem interval_boundary_hom_ext {K : SSet.{0}} {X : TopCat.{0}}
    (f g : SSet.toTop.obj (K ⊗ (SSet.boundary 1 : SSet.{0})) ⟶ X)
    (h₀ : SSet.toTop.map (K ◁ SSet.boundary.ι (1 : Fin 2)) ≫ f =
      SSet.toTop.map (K ◁ SSet.boundary.ι (1 : Fin 2)) ≫ g)
    (h₁ : SSet.toTop.map (K ◁ SSet.boundary.ι (0 : Fin 2)) ≫ f =
      SSet.toTop.map (K ◁ SSet.boundary.ι (0 : Fin 2)) ≫ g) : f = g := by
…

theorem OAI.Thomason.Construction.RealizationHomotopyRectification.cylinder_postcomp line 85
theorem OAI.Thomason.Construction.RealizationHomotopyRectification.cylinder_boundary_congr line 89

theorem OAI.Thomason.Construction.RealizationHomotopyRectification.straighten_of_cylinder_deformation line 120

Source documentation

A path-valued deformation on the cylinder ends and side, initially equal to the given homotopy, straightens its side at the final time.

theorem straighten_of_cylinder_deformation
    {K : SSet.{0}} (A : K.Subcomplex) {X : TopCat.{0}}
    (f g : SSet.toTop.obj K ⟶ X) (H : f.hom.Homotopy g.hom)
    (q : SSet.toTop.obj (A.unionProd (SSet.boundary 1)).toSSet ⟶ continuousPathSpace X)
    (hq₀ : q ≫ pathAt X 0 = SSet.toTop.map (A.unionProd (SSet.boundary 1)).ι ≫
      cylinderRealizationMap H.toContinuousMap)
    (hqend : SSet.toTop.map (SSet.Subcomplex.unionProd.ι₁ A (SSet.boundary 1)) ≫ q =
      SSet.toTop.map (K ◁ (SSet.boundary 1).ι) ≫
        cylinderRealizationMap H.toContinuousMap ≫ constantPath X)
    (hqside : SSet.toTop.map (SSet.Subcomplex.unionProd.ι₂ A (SSet.boundary 1)) ≫
      q ≫ pathAt X 1 = SSet.toTop.map (fst A.toSSet Δ[1] ≫ A.ι) ≫ f) :
    Nonempty (f.hom.HomotopyRel g.hom (Set.range (SSet.toTop.map A.ι).hom)) := by
…

Mentions: OAI.Thomason.Construction.continuousPathSpace, OAI.Thomason.Construction.RealizationHomotopyRectification.pathAt, OAI.Thomason.Construction.cylinderRealizationMap, OAI.Thomason.Construction.RealizationHomotopyRectification.constantPath

def OAI.Thomason.Construction.RealizationHomotopyRectification.restriction line 228

Source documentation

Restriction of a continuous homotopy to a realized simplicial subobject.

def restriction {K : SSet.{0}} (A : K.Subcomplex) {X : TopCat.{0}}
    {f g : SSet.toTop.obj K ⟶ X} (H : f.hom.Homotopy g.hom) :
    C(unitInterval × SSet.toTop.obj A.toSSet, X) :=
…

def OAI.Thomason.Construction.RealizationHomotopyRectification.constantSide line 233
theorem OAI.Thomason.Construction.RealizationHomotopyRectification.straighten line 239
Source documentation
A square from the boundary path to the constant path, with its two ends fixed, straightens the full homotopy relative to that boundary.
```
theorem straighten {K : SSet.{0}} (A : K.Subcomplex) {X : TopCat.{0}}
    (f g : SSet.toTop.obj K ⟶ X) (H : f.hom.Homotopy g.hom)
    (D : (restriction A H).HomotopyRel (constantSide A f)
      {z | z.1 = 0 ∨ z.1 = 1}) :
    Nonempty (f.hom.HomotopyRel g.hom (Set.range (SSet.toTop.map A.ι).hom)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationHomotopyRectification.restriction, OAI.Thomason.Construction.RealizationHomotopyRectification.constantSide
def OAI.Thomason.Construction.RealizationHomotopyRectification.restrictionAlong line 330
def OAI.Thomason.Construction.RealizationHomotopyRectification.constantSideAlong line 335
theorem OAI.Thomason.Construction.RealizationHomotopyRectification.straighten_mono line 341
Source documentation
Passing through the actual range removes the literal-subcomplex restriction from boundary-square rectification.
```
theorem straighten_mono {A K : SSet.{0}} (i : A ⟶ K) [Mono i] {X : TopCat.{0}}
    (f g : SSet.toTop.obj K ⟶ X) (H : f.hom.Homotopy g.hom)
    (D : (restrictionAlong i H).HomotopyRel (constantSideAlong i f)
      {z | z.1 = 0 ∨ z.1 = 1}) :
    Nonempty (f.hom.HomotopyRel g.hom (Set.range (SSet.toTop.map i).hom)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationHomotopyRectification.restrictionAlong, OAI.Thomason.Construction.RealizationHomotopyRectification.constantSideAlong

def OAI.Thomason.Construction.simplexPointInterpolation line 413

Source documentation

Convex interpolation in the barycentric coordinates of a standard simplex.

def simplexPointInterpolation (n : ℕ) :
    C(unitInterval × (SSet.toTop.obj (Δ[n] : SSet.{0}) ×
      SSet.toTop.obj (Δ[n] : SSet.{0})), SSet.toTop.obj (Δ[n] : SSet.{0})) :=
…

theorem OAI.Thomason.Construction.simplexPointInterpolation_zero line 431
theorem OAI.Thomason.Construction.simplexPointInterpolation_one line 441
theorem OAI.Thomason.Construction.simplexPointInterpolation_diagonal line 451
def OAI.Thomason.Construction.simplexHomotopyFiberEquiv line 467
Source documentation
The projection of the genuine homotopy fibre over a geometric simplex is a homotopy equivalence, for any continuous map into that simplex.
```
def simplexHomotopyFiberEquiv {X : TopCat.{0}} (n : ℕ)
    (p : X ⟶ SSet.toTop.obj (Δ[n] : SSet.{0})) (b : SSet.toTop.obj (Δ[n] : SSet.{0})) :
    ContinuousMap.HomotopyEquiv (continuousHomotopyFiber p b) X :=
…
```
Mentions: OAI.Thomason.Construction.continuousHomotopyFiber
def OAI.Thomason.Construction.barycentricPathHomotopy line 492
Source documentation
Linear interpolation between two barycentric paths fixes their common endpoints. This is the path-level triangle compatibility used in realization.
```
def barycentricPathHomotopy {n : ℕ} {x y : StdSimplex ℝ (Fin (n+1))}
    (p q : Path x y) : p.Homotopy q where
…
```
def OAI.Thomason.Construction.barycentricEdge line 530
Source documentation
The image of the standard interval inside a barycentric simplex along any ordinal edge.
```
def barycentricEdge {n : ℕ} (f : Fin 2 →o Fin (n+1)) :
    Path (StdSimplex.single (f 0) : StdSimplex ℝ (Fin (n+1))) (StdSimplex.single (f 1)) where
…
```
def OAI.Thomason.Construction.continuousProductProjection line 554
def OAI.Thomason.Construction.continuousProductFiberEquiv line 559
Source documentation
Interpolation in the base makes each literal product fibre a homotopy-equivalent subspace of the entire product.
```
def continuousProductFiberEquiv (X B : TopCat.{0}) (b : B)
    (c : C(unitInterval × (B × B), B))
    (h₀ : ∀ x y, c (0,x,y) = x) (h₁ : ∀ x y, c (1,x,y) = y) :
    ContinuousMap.HomotopyEquiv
      (continuousFiber (continuousProductProjection X B) b) (TopCat.of (X × B)) where
…
```
Mentions: OAI.Thomason.Construction.continuousFiber, OAI.Thomason.Construction.continuousProductProjection
theorem OAI.Thomason.Construction.continuousProductSimplexFiberInclusion_weak line 585
Source documentation
In particular, the inclusion of any fibre over a realized simplex is an actual weak homotopy equivalence, without any Kan hypothesis.
```
theorem continuousProductSimplexFiberInclusion_weak (X : TopCat.{0}) (n : ℕ)
    (b : SSet.toTop.obj (Δ[n] : SSet.{0})) :
    topologicalWeakEquivalences (continuousFiberInclusion
      (continuousProductProjection X (SSet.toTop.obj (Δ[n] : SSet.{0}))) b) :=
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberInclusion, OAI.Thomason.Construction.continuousProductProjection
theorem OAI.Thomason.Construction.singularPathMap_fibration line 612
Source documentation
The natural internal-hom comparison transports the proved simplicial pushout-product theorem to the actual compact-open path space.
```
theorem singularPathMap_fibration {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)] :
    HomotopicalAlgebra.Fibration (TopCat.toSSet.map (continuousPathMap p)) := by
…
```
Mentions: OAI.Thomason.Construction.continuousPathMap

def OAI.Thomason.Construction.subdividedFaceMap line 639

Source documentation

The actual inclusion of a subdivided face into the finite-chain nerve.

def subdividedFaceMap {n : ℕ} (S : Finset (Fin (n + 1))) :
    SSet.sd.obj (SSet.stdSimplex.face S : SSet.{0}) ⟶ SimplexCategory.sd.obj ⦋n⦌ :=
…

def OAI.Thomason.Construction.subdividedFace line 644
Source documentation
The full chain subcomplex supported on the original face vertices.
```
def subdividedFace {n : ℕ} (S : Finset (Fin (n + 1))) :
    (SimplexCategory.sd.obj ⦋n⦌).Subcomplex :=
…
```
def OAI.Thomason.Construction.faceOrdinalMap line 648
instance OAI.Thomason.Construction.faceOrdinalMap_mono line 652
theorem OAI.Thomason.Construction.faceIso_inclusion line 658
theorem OAI.Thomason.Construction.subdividedFaceMap_fac line 665
theorem OAI.Thomason.Construction.faceOrdinalMap_range line 674
theorem OAI.Thomason.Construction.subdividedFaceMap_mono line 690
Source documentation
Subdivision preserves every face inclusion, including arbitrary codimension.
```
theorem subdividedFaceMap_mono {n : ℕ} (S : Finset (Fin (n+1))) :
    Mono (subdividedFaceMap S) := by
…
```
Mentions: OAI.Thomason.Construction.subdividedFaceMap
theorem OAI.Thomason.Construction.subdividedFaceMap_range line 721
Source documentation
Exact range: every chain is supported on the original face and every such chain simplex lifts, in every simplicial dimension.
```
theorem subdividedFaceMap_range {n : ℕ} (S : Finset (Fin (n+1))) :
    SSet.Subcomplex.range (subdividedFaceMap S) = subdividedFace S := by
…
```
Mentions: OAI.Thomason.Construction.subdividedFaceMap, OAI.Thomason.Construction.subdividedFace
theorem OAI.Thomason.Construction.subdividedFace_inter line 758
theorem OAI.Thomason.Construction.subdividedFace_empty line 769
def OAI.Thomason.Construction.TopologicalDeformation.coproductRetraction line 800
theorem OAI.Thomason.Construction.TopologicalDeformation.coproductRetraction_fac line 804
theorem OAI.Thomason.Construction.TopologicalDeformation.coproductRetraction_left line 808
def OAI.Thomason.Construction.TopologicalDeformation.coproductTrack line 816
Source documentation
Assemble the tracks using preservation of coproducts by the interval cylinder.
```
def coproductTrack : TopologicalInterval.cylinder.obj (∐ B) ⟶ ∐ B :=
…
```
theorem OAI.Thomason.Construction.TopologicalDeformation.coproductTrack_fac line 822
theorem OAI.Thomason.Construction.TopologicalDeformation.coproductTrack_zero line 827
theorem OAI.Thomason.Construction.TopologicalDeformation.coproductTrack_one line 836
theorem OAI.Thomason.Construction.TopologicalDeformation.coproductTrack_stationary line 843
def OAI.Thomason.Construction.TopologicalDeformation.coproductData line 859
Source documentation
A whole coproduct of relative deformations remains a relative deformation.
```
def coproductData : Data (CategoryTheory.Limits.Sigma.map i) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
def OAI.Thomason.Construction.TopologicalDeformation.Data.retractMap line 893
Source documentation
The retraction obtained by traversing the given arrow retract.
```
def Data.retractMap (e : Data g) (r : RetractArrow f g) : B ⟶ A :=
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.Data.retractMap_left line 897
def OAI.Thomason.Construction.TopologicalDeformation.Data.ofRetract line 905
Source documentation
An arrow retract of a stationary deformation inclusion is again one.
```
def Data.ofRetract (e : Data g) (r : RetractArrow f g) : Data f where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
def OAI.Thomason.Construction.TopologicalDeformation.Data.conjugate line 959
Source documentation
Change coordinates in both the retract and its ambient space.
```
def Data.conjugate (d : Data i) (a : A ≅ A') (b : B ≅ B') :
    Data (a.inv ≫ i ≫ b.hom) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
def OAI.Thomason.Construction.TopologicalDeformation.Data.ofIso line 1000
Source documentation
The same data transported across a commuting square of isomorphisms.
```
def Data.ofIso (d : Data i) {i' : A' ⟶ B'} (a : A ≅ A') (b : B ≅ B')
    (w : i ≫ b.hom = a.hom ≫ i') : Data i' := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data