LoopDimensionShift.lean`

92 declarations, 0 contain sorry, 0 declared as axioms

Dimension-bounded cells for intelligent truncation

The cells of dimension at most n form a strict n-category. This supplies the representatives on which the intelligent-truncation congruence acts.

theorem OAI.Thomason.Construction.StrictOmegaCategory.lower_face_comp line 28
Source documentation
Lower boundaries of a composite are the corresponding boundaries of its first factor, by the source law and globularity.
```
theorem lower_face_comp (a : Bool) {k m : ℕ} (hkm : k < m) (x y : C)
    (h : C.target m x = C.source m y) :
    C.face a k (C.comp m x y h) = C.face a k x := by
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.lower_faces_equal line 34

theorem OAI.Thomason.Construction.StrictOmegaCategory.face_comp_le line 40

Source documentation

Boundaries at or below the composition level use the exterior factors.

theorem face_comp_le (a : Bool) {k m : ℕ} (hkm : k ≤ m) (x y : C)
    (h : C.target m x = C.source m y) :
    C.face a k (C.comp m x y h) = if a then C.face true k y else C.face false k x := by
…

theorem OAI.Thomason.Construction.StrictOmegaCategory.dimensionLE_face line 54
theorem OAI.Thomason.Construction.StrictOmegaCategory.comp_of_dimensionLE line 68
Source documentation
Composing above the dimension of both cells is composition of identities.
```
theorem comp_of_dimensionLE {n m : ℕ} (hnm : n ≤ m) {x y : C}
    (hx : C.DimensionLE n x) (h : C.target m x = C.source m y) : C.comp m x y h = y := by
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.dimensionLE_comp_all line 76
def OAI.Thomason.Construction.StrictOmegaCategory.bounded line 85
Source documentation
The actual subcategory of cells of dimension at most n.
```
def bounded (n : ℕ) : StrictOmegaCategory.{0} where
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.bounded_isTruncated line 103
def OAI.Thomason.Construction.StrictOmegaCategory.boundedInclusion line 106
def OAI.Thomason.Construction.HomotopyMaps.loopMap line 142
theorem OAI.Thomason.Construction.HomotopyMaps.loopMap_homotopic line 145
def OAI.Thomason.Construction.HomotopyMaps.groupMap line 150
def OAI.Thomason.Construction.HomotopyMaps.componentsMap line 154
theorem OAI.Thomason.Construction.HomotopyMaps.componentsMap_mk line 158
theorem OAI.Thomason.Construction.HomotopyMaps.componentsMap_id line 162
theorem OAI.Thomason.Construction.HomotopyMaps.componentsMap_comp line 167
theorem OAI.Thomason.Construction.HomotopyMaps.groupMap_id line 174
theorem OAI.Thomason.Construction.HomotopyMaps.groupMap_comp line 183
def OAI.Thomason.Construction.IsWeakHomotopyEquivalence line 197
Source documentation
The actual weak homotopy equivalences, using path components and all positive-dimensional homotopy groups of the source at all basepoints.
```
def IsWeakHomotopyEquivalence {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y]
    (f : C(X, Y)) : Prop :=
…
```
theorem OAI.Thomason.Construction.isWeakHomotopyEquivalence_iff line 203
Source documentation
The component and homotopy-group criterion is the common weak-homotopy test.
```
theorem isWeakHomotopyEquivalence_iff {X Y : Type u}
    [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :
    IsWeakHomotopyEquivalence f ↔ Thomason.WeakHomotopy.Equivalence f := Iff.rfl
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.WeakHomotopy.Equivalence
theorem OAI.Thomason.Construction.IsWeakHomotopyEquivalence.id line 212
theorem OAI.Thomason.Construction.IsWeakHomotopyEquivalence.comp line 218
def OAI.Thomason.Construction.topologicalWeakEquivalences line 230
def OAI.Thomason.Construction.realizationWeakEquivalences line 235
Source documentation
Kan–Quillen weak equivalences as weak homotopy equivalences of geometric realizations. No model structure is presupposed by this definition.
```
def realizationWeakEquivalences : MorphismProperty SSet.{u} :=
…
```
theorem OAI.Thomason.Construction.realizationWeakEquivalences_eq line 239
Source documentation
Both simplicial classes use the same weak-homotopy test on realization.
```
theorem realizationWeakEquivalences_eq :
    realizationWeakEquivalences.{u} = Thomason.simplicialWeakEquivalences := rfl
```
Mentions: OAI.Thomason.simplicialWeakEquivalences
instance OAI.Thomason.Construction.(instance at line 242) line 242
instance OAI.Thomason.Construction.(instance at line 245) line 245
instance OAI.Thomason.Construction.(instance at line 248) line 248
instance OAI.Thomason.Construction.(instance at line 250) line 250

theorem OAI.Thomason.Construction.realization_ex_twice_iff line 256

Source documentation

Extension twice preserves and reflects realization weak equivalences under the classical Kan–Quillen hypotheses.

theorem realization_ex_twice_iff
    [realizationWeakEquivalences.{u}.HasTwoOutOfThreeProperty]
    (hj : ∀ X, realizationWeakEquivalences.{u} (canonicalExtension.app X))
    {X Y : SSet.{u}} (f : X ⟶ Y) :
    realizationWeakEquivalences.{u} ((SSet.ex ⋙ SSet.ex).map f) ↔
      realizationWeakEquivalences.{u} f :=
…

def OAI.Thomason.Construction.HomotopyMaps.loopHomeomorphEquiv line 287
Source documentation
A homeomorphism gives an actual equivalence on based generalized loops.
```
noncomputable def loopHomeomorphEquiv (e : X ≃ₜ Y) (x : X) (N : Type*) :
    GenLoop N X x ≃ GenLoop N Y (e x) where
…
```
theorem OAI.Thomason.Construction.HomotopyMaps.loopHomeomorphEquiv_homotopic line 302
Source documentation
The loop equivalence preserves and reflects homotopy relative to the boundary.
```
theorem loopHomeomorphEquiv_homotopic (e : X ≃ₜ Y) (x : X) {N : Type*}
    (p q : GenLoop N X x) :
    GenLoop.Homotopic p q ↔
      GenLoop.Homotopic (loopHomeomorphEquiv e x N p) (loopHomeomorphEquiv e x N q) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.loopHomeomorphEquiv
theorem OAI.Thomason.Construction.HomotopyMaps.groupMap_homeomorph_bijective line 321
Source documentation
The induced map on actual homotopy groups is bijective.
```
theorem groupMap_homeomorph_bijective (e : X ≃ₜ Y) (n : ℕ) (x : X) :
    Function.Bijective (groupMap (e : C(X, Y)) n x) :=
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap
theorem OAI.Thomason.Construction.HomotopyMaps.componentsMap_homeomorph_bijective line 327
Source documentation
The induced map on path components is bijective as well.
```
theorem componentsMap_homeomorph_bijective (e : X ≃ₜ Y) :
    Function.Bijective (componentsMap (e : C(X, Y))) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.homeomorph_isWeakHomotopyEquivalence line 344
Source documentation
Every homeomorphism satisfies the actual component-and-homotopy-group definition.
```
theorem homeomorph_isWeakHomotopyEquivalence {X Y : Type u}
    [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) :
    IsWeakHomotopyEquivalence (e : C(X, Y)) :=
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence
theorem OAI.Thomason.Construction.topologicalWeakEquivalences_of_isIso line 351
Source documentation
Topological isomorphisms are weak before any model structure is supplied.
```
theorem topologicalWeakEquivalences_of_isIso {X Y : TopCat.{u}}
    (f : X ⟶ Y) [IsIso f] : topologicalWeakEquivalences f :=
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences
instance OAI.Thomason.Construction.(instance at line 355) line 355
instance OAI.Thomason.Construction.(instance at line 360) line 360
Source documentation
Geometric realization therefore respects isomorphic simplicial maps unconditionally.
```
instance : realizationWeakEquivalences.{u}.RespectsIso :=
…
```
def OAI.Thomason.Construction.HomotopyMaps.basedLoopMap line 387
Source documentation
Postcomposition with an explicitly preserved basepoint.
```
def basedLoopMap (f : C(X, Y)) {x : X} {y : Y} (e : f x = y)
    {N : Type*} (p : GenLoop N X x) : GenLoop N Y y :=
…
```
def OAI.Thomason.Construction.HomotopyMaps.basedGroupMap line 392
Source documentation
The corresponding map on the actual based homotopy quotient.
```
def basedGroupMap (f : C(X, Y)) {x : X} {y : Y} (e : f x = y) (n : ℕ) :
    HomotopyGroup.Pi n X x → HomotopyGroup.Pi n Y y :=
…
```
theorem OAI.Thomason.Construction.HomotopyMaps.basedGroupMap_rfl line 397
theorem OAI.Thomason.Construction.HomotopyMaps.basedGroupMap_bijective_iff line 401
Source documentation
Transporting the target basepoint does not change bijectivity.
```
theorem basedGroupMap_bijective_iff (f : C(X, Y)) {x : X} {y : Y}
    (e : f x = y) (n : ℕ) :
    Function.Bijective (basedGroupMap f e n) ↔ Function.Bijective (groupMap f n x) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.basedGroupMap, OAI.Thomason.Construction.HomotopyMaps.groupMap
abbrev OAI.Thomason.Construction.PointedHomotopyGroups.Pointed line 411
def OAI.Thomason.Construction.PointedHomotopyGroups.point line 413
theorem OAI.Thomason.Construction.PointedHomotopyGroups.map_point line 415
def OAI.Thomason.Construction.PointedHomotopyGroups.homotopyGroupFunctor line 419
Source documentation
The actual homotopy group quotient, functorially in based spaces.
```
def homotopyGroupFunctor (n : ℕ) : Pointed.{u} ⥤ Type u where
…
```
def OAI.Thomason.Construction.PointedHomotopyGroups.pointed line 442
Source documentation
A space with a chosen actual point.
```
def pointed (X : TopCat.{u}) (x : X) : Pointed.{u} :=
…
```
def OAI.Thomason.Construction.PointedHomotopyGroups.pointedMap line 446
Source documentation
A continuous map with an equality of the chosen basepoints.
```
def pointedMap {X Y : TopCat.{u}} (f : X ⟶ Y) {x : X} {y : Y} (e : f.hom x = y) :
    pointed X x ⟶ pointed Y y :=
…
```
Mentions: OAI.Thomason.Construction.PointedHomotopyGroups.pointed
theorem OAI.Thomason.Construction.PointedHomotopyGroups.map_bijective_iff line 455
Source documentation
The functor recovers exactly the map used to define weak equivalences.
```
theorem map_bijective_iff {X Y : TopCat.{u}} (f : X ⟶ Y) {x : X} {y : Y}
    (e : f.hom x = y) (n : ℕ) :
    Function.Bijective ((homotopyGroupFunctor n).map (pointedMap f e)) ↔
      Function.Bijective (HomotopyMaps.groupMap f.hom n x) :=
…
```
Mentions: OAI.Thomason.Construction.PointedHomotopyGroups.homotopyGroupFunctor, OAI.Thomason.Construction.PointedHomotopyGroups.pointedMap, OAI.Thomason.Construction.HomotopyMaps.groupMap
def OAI.Thomason.Construction.PointedHomotopyGroups.componentsFunctor line 462
Source documentation
Path components form a functor on unbased spaces.
```
noncomputable def componentsFunctor : TopCat.{u} ⥤ Type u where
…
```

theorem OAI.Thomason.Construction.HomotopyMaps.piOneEquiv_naturality line 495

Source documentation

The actual first-homotopy-group map agrees with the fundamental-group map.

theorem piOneEquiv_naturality (f : C(X, Y)) (x : X) (q : HomotopyGroup.Pi 1 X x) :
    HomotopyGroup.pi1EquivFundamentalGroup (groupMap f 1 x q) =
      FundamentalGroup.map f x (HomotopyGroup.pi1EquivFundamentalGroup q) := by
…

Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap

def OAI.Thomason.Construction.HomotopyMaps.piOneTransport line 502
Source documentation
Transport the actual cubical first homotopy group along a path.
```
noncomputable def piOneTransport {x y : X} (p : Path x y) :
    HomotopyGroup.Pi 1 X x ≃ HomotopyGroup.Pi 1 X y :=
…
```

theorem OAI.Thomason.Construction.HomotopyMaps.fundamentalTransport_naturality line 509

Source documentation

Fundamental-group conjugation is natural in continuous maps.

theorem fundamentalTransport_naturality (f : C(X, Y)) {x y : X} (p : Path x y)
    (q : FundamentalGroup X x) :
    FundamentalGroup.map f y (FundamentalGroup.fundamentalGroupMulEquivOfPath p q) =
      FundamentalGroup.fundamentalGroupMulEquivOfPath (p.map f.continuous)
        (FundamentalGroup.map f x q) := by
…

theorem OAI.Thomason.Construction.HomotopyMaps.piOneTransport_naturality line 527
Source documentation
The first-homotopy-group square commutes with path basepoint transport.
```
theorem piOneTransport_naturality (f : C(X, Y)) {x y : X} (p : Path x y)
    (q : HomotopyGroup.Pi 1 X x) :
    groupMap f 1 y (piOneTransport p q) = piOneTransport (p.map f.continuous) (groupMap f 1 x q) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap, OAI.Thomason.Construction.HomotopyMaps.piOneTransport
theorem OAI.Thomason.Construction.HomotopyMaps.groupMap_one_bijective_iff line 538
Source documentation
Bijectivity on the actual first homotopy group is independent of a basepoint within its path component.
```
theorem groupMap_one_bijective_iff (f : C(X, Y)) {x y : X} (p : Path x y) :
    Function.Bijective (groupMap f 1 x) ↔ Function.Bijective (groupMap f 1 y) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap
theorem OAI.Thomason.Construction.HomotopyMaps.source_cancel_piOne line 549
Source documentation
The degree-one part of weak source cancellation holds at every target basepoint, using component surjectivity and natural path transport.
```
theorem source_cancel_piOne {Z : Type u} [TopologicalSpace Z]
    (f : C(X, Y)) (g : C(Y, Z)) (hf : IsWeakHomotopyEquivalence f)
    (hfg : IsWeakHomotopyEquivalence (g.comp f)) (y : Y) :
    Function.Bijective (groupMap g 1 y) := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.HomotopyMaps.groupMap
def OAI.Thomason.Construction.PathSpace.map line 585
Source documentation
Postcomposition is continuous on path spaces.
```
def map (f : C(X, Y)) {x y : X} : C(Path x y, Path (f x) (f y)) where
…
```
def OAI.Thomason.Construction.PathSpace.concatenate line 593
Source documentation
Concatenation is an actual continuous operation.
```
def concatenate {x y z : X} : C(Path x y × Path y z, Path x z) :=
…
```
def OAI.Thomason.Construction.PathSpace.reverse line 597
Source documentation
Reverse a path continuously.
```
def reverse {x y : X} : C(Path x y, Path y x) := ⟨Path.symm, Path.continuous_symm⟩
```
def OAI.Thomason.Construction.PathSpace.conjugate line 600
Source documentation
Conjugation by a fixed path, on unquotiented loop spaces.
```
def conjugate {x y : X} (p : Path x y) : C(Path x x, Path y y) where
…
```
theorem OAI.Thomason.Construction.PathSpace.conjugate_naturality line 605
Source documentation
The continuous conjugation operation is natural in the ambient space.
```
theorem conjugate_naturality (f : C(X, Y)) {x y : X} (p : Path x y) :
    (map f).comp (conjugate p) = (conjugate (p.map f.continuous)).comp (map f) := by
…
```
Mentions: OAI.Thomason.Construction.PathSpace.map, OAI.Thomason.Construction.PathSpace.conjugate

def OAI.Thomason.Construction.PathSpace.appendHomotopy line 614

Source documentation

The path-space version of concatenating a fixed homotopy with a variable path.

def appendHomotopy {x y z : X} {p q : Path x y} (H : p.Homotopy q) :
    (⟨fun r : Path y z => p.trans r, by fun_prop⟩ : C(Path y z, Path x z)).Homotopy
      ⟨fun r => q.trans r, by fun_prop⟩ where
…

def OAI.Thomason.Construction.PathSpace.prependHomotopy line 628

Source documentation

The path-space version of concatenating a variable path with a fixed homotopy.

def prependHomotopy {x y z : X} {p q : Path y z} (H : p.Homotopy q) :
    (⟨fun r : Path x y => r.trans p, by fun_prop⟩ : C(Path x y, Path x z)).Homotopy
      ⟨fun r => r.trans q, by fun_prop⟩ where
…

def OAI.Thomason.Construction.PathSpace.reparametrize line 662

Source documentation

Reparametrize every path by the same endpoint-preserving interval map.

def reparametrize (α : unitInterval → unitInterval) (hα : Continuous α)
    (h₀ : α 0 = 0) (h₁ : α 1 = 1) {x y : X} : C(Path x y, Path x y) where
…

def OAI.Thomason.Construction.PathSpace.reparametrizeHomotopy line 671
Source documentation
Straight-line interpolation is continuous in both the path and its parameter.
```
def reparametrizeHomotopy (α : unitInterval → unitInterval) (hα : Continuous α)
    (h₀ : α 0 = 0) (h₁ : α 1 = 1) {x y : X} :
    (ContinuousMap.id (Path x y)).Homotopy (reparametrize α hα h₀ h₁) where
…
```
Mentions: OAI.Thomason.Construction.PathSpace.reparametrize
def OAI.Thomason.Construction.PathSpace.associatingParameter line 684
Source documentation
The fixed interval map relating the two associations of three paths.
```
def associatingParameter (t : unitInterval) : unitInterval :=
…
```
theorem OAI.Thomason.Construction.PathSpace.associatingParameter_continuous line 687
theorem OAI.Thomason.Construction.PathSpace.associatingParameter_zero line 690
theorem OAI.Thomason.Construction.PathSpace.associatingParameter_one line 693
def OAI.Thomason.Construction.PathSpace.leftAssociation line 696
def OAI.Thomason.Construction.PathSpace.rightAssociation line 700
def OAI.Thomason.Construction.PathSpace.associatingHomotopy line 705
Source documentation
Association is a continuous homotopy on the entire space of three paths.
```
def associatingHomotopy {a b c d : X} :
    (leftAssociation (a := a) (b := b) (c := c) (d := d)).Homotopy rightAssociation := by
…
```
Mentions: OAI.Thomason.Construction.PathSpace.leftAssociation, OAI.Thomason.Construction.PathSpace.rightAssociation
def OAI.Thomason.Construction.PathSpace.leftAppend line 735
Source documentation
Append a fixed path on the left.
```
def leftAppend {a b c : X} (p : Path a b) : C(Path b c, Path a c) :=
…
```
def OAI.Thomason.Construction.PathSpace.rightAppend line 739
Source documentation
Append a fixed path on the right.
```
def rightAppend {a b c : X} (p : Path b c) : C(Path a b, Path a c) :=
…
```
def OAI.Thomason.Construction.PathSpace.unitParameter line 742
def OAI.Thomason.Construction.PathSpace.rightUnitHomotopy line 746
Source documentation
The right unit law is a homotopy continuous in the entire path.
```
def rightUnitHomotopy (a b : X) :
    (rightAppend (a := a) (Path.refl b)).Homotopy (ContinuousMap.id (Path a b)) := by
…
```
Mentions: OAI.Thomason.Construction.PathSpace.rightAppend
def OAI.Thomason.Construction.PathSpace.leftUnitHomotopy line 762
Source documentation
The left unit law follows by reversing the continuous right unit homotopy.
```
def leftUnitHomotopy (a b : X) :
    (leftAppend (c := b) (Path.refl a)).Homotopy (ContinuousMap.id (Path a b)) := by
…
```
Mentions: OAI.Thomason.Construction.PathSpace.leftAppend
def OAI.Thomason.Construction.PathSpace.leftCancellation line 775
Source documentation
Cancelling a path and its reverse on the left, uniformly in the remaining path.
```
def leftCancellation {a b c : X} (p : Path a b) :
    ((leftAppend (c := c) p.symm).comp (leftAppend p)).Homotopy
…
```
Mentions: OAI.Thomason.Construction.PathSpace.leftAppend
def OAI.Thomason.Construction.PathSpace.rightCancellation line 784
Source documentation
Cancelling a path and its reverse on the right, uniformly in the preceding path.
```
def rightCancellation {a b c : X} (p : Path b c) :
    ((rightAppend (a := a) p.symm).comp (rightAppend p)).Homotopy
…
```
Mentions: OAI.Thomason.Construction.PathSpace.rightAppend
def OAI.Thomason.Construction.PathSpace.leftAppendEquiv line 816
Source documentation
Concatenating a fixed path on the left is a homotopy equivalence.
```
def leftAppendEquiv {a b : X} (p : Path a b) (c : X) :
    ContinuousMap.HomotopyEquiv (Path b c) (Path a c) where
…
```
def OAI.Thomason.Construction.PathSpace.rightAppendEquiv line 827
Source documentation
Concatenating a fixed path on the right is a homotopy equivalence.
```
def rightAppendEquiv (a : X) {b c : X} (p : Path b c) :
    ContinuousMap.HomotopyEquiv (Path a b) (Path a c) where
…
```
def OAI.Thomason.Construction.PathSpace.conjugateEquiv line 838
Source documentation
Conjugation gives an actual homotopy equivalence of loop spaces.
```
def conjugateEquiv {a b : X} (p : Path a b) :
    ContinuousMap.HomotopyEquiv (Path a a) (Path b b) :=
…
```
theorem OAI.Thomason.Construction.PathSpace.conjugateEquiv_toFun line 843
def OAI.Thomason.Construction.PathSpace.conjugateConstantPath line 848
Source documentation
The image of the constant loop under conjugation is joined to the constant loop. This path supplies the needed basepoint comparison.
```
def conjugateConstantPath {a b : X} (p : Path a b) :
    Path (conjugate p (Path.refl a)) (Path.refl b) where
…
```
Mentions: OAI.Thomason.Construction.PathSpace.conjugate
def OAI.Thomason.Construction.HomotopyMaps.curryLoop line 880
Source documentation
Curry the first coordinate of a based cube into a based path.
```
def curryLoop {x : X} {n : ℕ} (p : GenLoop (Fin (n+1)) X x) :
    GenLoop (Fin n) (Path x x) (Path.refl x) := by
…
```
def OAI.Thomason.Construction.HomotopyMaps.uncurryLoop line 894
Source documentation
Uncurry the first path coordinate into a based cube.
```
def uncurryLoop {x : X} {n : ℕ} (p : GenLoop (Fin n) (Path x x) (Path.refl x)) :
    GenLoop (Fin (n+1)) X x := by
…
```
theorem OAI.Thomason.Construction.HomotopyMaps.uncurry_curryLoop line 909
theorem OAI.Thomason.Construction.HomotopyMaps.curry_uncurryLoop line 916

def OAI.Thomason.Construction.HomotopyMaps.curryLoopHomotopy line 925

Source documentation

A cubical homotopy curries continuously and remains fixed on the boundary.

def curryLoopHomotopy {x : X} {n : ℕ} {p q : GenLoop (Fin (n+1)) X x}
    (H : p.val.HomotopyRel q.val (Cube.boundary (Fin (n+1)))) :
    (curryLoop p).val.HomotopyRel (curryLoop q).val (Cube.boundary (Fin n)) := by
…

Mentions: OAI.Thomason.Construction.HomotopyMaps.curryLoop

def OAI.Thomason.Construction.HomotopyMaps.uncurryLoopHomotopy line 946

Source documentation

Conversely a path-space cubical homotopy uncurries relative to the full boundary.

def uncurryLoopHomotopy {x : X} {n : ℕ}
    {p q : GenLoop (Fin n) (Path x x) (Path.refl x)}
    (H : p.val.HomotopyRel q.val (Cube.boundary (Fin n))) :
    (uncurryLoop p).val.HomotopyRel (uncurryLoop q).val (Cube.boundary (Fin (n+1))) := by
…

Mentions: OAI.Thomason.Construction.HomotopyMaps.uncurryLoop

def OAI.Thomason.Construction.HomotopyMaps.loopDimensionShift line 968
Source documentation
Dimension shift on the actual homotopy-group quotients.
```
def loopDimensionShift (n : ℕ) (x : X) :
    HomotopyGroup.Pi (n+1) X x ≃ HomotopyGroup.Pi n (Path x x) (Path.refl x) where
…
```
theorem OAI.Thomason.Construction.HomotopyMaps.loopDimensionShift_naturality line 980
Source documentation
Dimension shift commutes with the actual induced maps.
```
theorem loopDimensionShift_naturality (f : C(X, Y)) (n : ℕ) (x : X)
    (p : HomotopyGroup.Pi (n+1) X x) :
    loopDimensionShift n (f x) (groupMap f (n+1) x p) =
      basedGroupMap (PathSpace.map f) (show PathSpace.map f (Path.refl x) = Path.refl (f x) from rfl) n (loopDimensionShift n x p) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.loopDimensionShift, OAI.Thomason.Construction.HomotopyMaps.groupMap, OAI.Thomason.Construction.HomotopyMaps.basedGroupMap, OAI.Thomason.Construction.PathSpace.map