LeanPool.WhiteheadTheorem.Compressible.Defs #

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Compressible.Defs.

structure TopCat.LiftStructUpToRelHomotopy {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} (sq : CategoryTheory.CommSq f ι i F) :

Type u

A commutative square

A' -----f----→ A
|              |
ι              i
|              |
↓              ↓
X' -----F----→ X

in TopCat is said to have a lift, up to relative homotopy, if there exists a map l : X' ⟶ A and a homotopy H : I × X' ⟶ X from F to l ≫ i, such that ι ≫ l = f and ∀ t, ι ≫ H(t, ·) = f ≫ i.

(Note: If i is injective, then ι ≫ l = f is implied by ι ≫ H(1, ·) = f ≫ i, since H(1, ·) = l ≫ i.)

See TopCat.LiftStructUpToRelHomotopy.curriedMk for a more convenient constructor.

l : X' ⟶ A
The lift
fac_left : CategoryTheory.CategoryStruct.comp ι self.l = f
The upper left triangle commutes.
H : (Hom.hom F).HomotopicRel (Hom.hom (CategoryTheory.CategoryStruct.comp self.l i)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom ι))
The lower right triangle commutes up to relative homotopy.

Instances For

source

noncomputable def TopCat.LiftStructUpToRelHomotopy.curriedH {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} {sq : CategoryTheory.CommSq f ι i F} (l : LiftStructUpToRelHomotopy sq) :

X' ⟶ of C(↑unitInterval, ↑X)

curriedH

Equations

l.curriedH = TopCat.ofHom (ContinuousMap.argSwap (Nonempty.some ⋯).toContinuousMap).curry

Instances For

source

theorem TopCat.LiftStructUpToRelHomotopy.curriedH_apply_zero {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} {sq : CategoryTheory.CommSq f ι i F} (l : LiftStructUpToRelHomotopy sq) :

CategoryTheory.CategoryStruct.comp l.curriedH (PathSpace.eval₀ X) = F

source

theorem TopCat.LiftStructUpToRelHomotopy.curriedH_apply_zero' {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} {sq : CategoryTheory.CommSq f ι i F} (l : LiftStructUpToRelHomotopy sq) (x : ↑X') :

(ContinuousMap.argSwap (Hom.hom l.curriedH).uncurry).toFun (0, x) = (Hom.hom F) x

source

theorem TopCat.LiftStructUpToRelHomotopy.curriedH_apply_one {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} {sq : CategoryTheory.CommSq f ι i F} (l : LiftStructUpToRelHomotopy sq) :

CategoryTheory.CategoryStruct.comp l.curriedH (PathSpace.eval₁ X) = CategoryTheory.CategoryStruct.comp l.l i

source

theorem TopCat.LiftStructUpToRelHomotopy.curriedH_apply_one' {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} {sq : CategoryTheory.CommSq f ι i F} (l : LiftStructUpToRelHomotopy sq) (x : ↑X') :

(ContinuousMap.argSwap (Hom.hom l.curriedH).uncurry).toFun (1, x) = (Hom.hom (CategoryTheory.CategoryStruct.comp l.l i)) x

source

theorem TopCat.LiftStructUpToRelHomotopy.curriedH_prop {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} {sq : CategoryTheory.CommSq f ι i F} (l : LiftStructUpToRelHomotopy sq) (t : ↑unitInterval) :

CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp l.curriedH (PathSpace.evalAt X t)) = CategoryTheory.CategoryStruct.comp ι F

source

theorem TopCat.LiftStructUpToRelHomotopy.curriedH_prop' {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} {sq : CategoryTheory.CommSq f ι i F} (l : LiftStructUpToRelHomotopy sq) (t : ↑unitInterval) (x : ↑X') :

x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ι) → (ContinuousMap.argSwap (Hom.hom l.curriedH).uncurry) (t, x) = (Hom.hom F) x

source

def TopCat.LiftStructUpToRelHomotopy.curriedMk {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} {sq : CategoryTheory.CommSq f ι i F} (l : X' ⟶ A) (fac_left : CategoryTheory.CategoryStruct.comp ι l = f) (curriedH : X' ⟶ of C(↑unitInterval, ↑X)) (curriedH_apply_zero : CategoryTheory.CategoryStruct.comp curriedH (PathSpace.eval₀ X) = F) (curriedH_apply_one : CategoryTheory.CategoryStruct.comp curriedH (PathSpace.eval₁ X) = CategoryTheory.CategoryStruct.comp l i) (curriedH_prop : ∀ (t : ↑unitInterval), CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp curriedH (PathSpace.evalAt X t)) = CategoryTheory.CategoryStruct.comp ι F) :

LiftStructUpToRelHomotopy sq

curriedMk

Equations

TopCat.LiftStructUpToRelHomotopy.curriedMk l fac_left curriedH curriedH_apply_zero curriedH_apply_one curriedH_prop = { l := l, fac_left := fac_left, H := ⋯ }

Instances For

source

structure TopCat.HasLiftUpToRelHomotopy {A' A X' X : TopCat} {f : A' ⟶ A} {ι : A' ⟶ X'} {i : A ⟶ X} {F : X' ⟶ X} (sq : CategoryTheory.CommSq f ι i F) :

Prop

HasLiftUpToRelHomotopy

hasLift : Nonempty (LiftStructUpToRelHomotopy sq)

Instances For

source

structure TopCat.IsCompressible {A' A X' X : TopCat} (ι : A' ⟶ X') (i : A ⟶ X) :

Prop

A map i : A ⟶ X is called compressible with respect to ι : A' ⟶ X' if every commutative square

A' -----f----→ A
|              |
ι              i
|              |
↓              ↓
X' -----F----→ X

has a lift, up to relative homotopy.

sq_hasLift {F : X' ⟶ X} {f : A' ⟶ A} (sq : CategoryTheory.CommSq f ι i F) : HasLiftUpToRelHomotopy sq

Instances For