LeanPool.WhiteheadTheorem.HEP.Cofibration #
Imported Lean Pool material for LeanPool.WhiteheadTheorem.HEP.Cofibration.
def
HasHomotopyExtensionProperty
{A X : Type u}
[TopologicalSpace A]
[TopologicalSpace X]
(i : C(A, X))
(Y : Type u)
[TopologicalSpace Y]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map i : A ⟶ X is said to have
the "curried HomotopyExtensionProperty" with respect to Y,
if the commutative square
A ---h---> C(I, Y)
| |
i eval₀
| |
↓ ↓
X ---f---> Y
has a lift H : X → C(I, Y).
- hasLift : CategoryTheory.HasLiftingProperty i (TopCat.PathSpace.eval₀ Y)
Instances
instance
instHasLiftingPropertyTopCatEval₀OfHasCurriedHEP
{A X : TopCat}
(i : A ⟶ X)
(Y : TopCat)
[HasCurriedHEP i Y]
:
instance
HasCurriedHEP.of_iso
{A X : TopCat}
(i : A ⟶ X)
[CategoryTheory.IsIso i]
{Y : TopCat}
:
HasCurriedHEP i Y
instance
HasCurriedHEP.of_comp_left
{A X X' : TopCat}
(i : A ⟶ X)
(i' : X ⟶ X')
{Y : TopCat}
[HasCurriedHEP i Y]
[HasCurriedHEP i' Y]
:
instance
HasCurriedHEP.of_sigma_map
{J : Type u}
{A B : J → TopCat}
(f : (j : J) → A j ⟶ B j)
{Z : TopCat}
[∀ (j : J), HasCurriedHEP (f j) Z]
:
noncomputable def
Limits.Cocone.ofSequenceOfHasLiftingProperty.app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{Z Y : C}
{X : ℕ → C}
(i : (n : ℕ) → X n ⟶ X (n + 1))
[CategoryTheory.Limits.HasColimitsOfShape ℕ C]
(p : Z ⟶ Y)
[lp : ∀ (n : ℕ), CategoryTheory.HasLiftingProperty (i n) p]
(h : X 0 ⟶ Z)
(f : CategoryTheory.Limits.colimit (CategoryTheory.Functor.ofSequence i) ⟶ Y)
(bigSq : CategoryTheory.CommSq h (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.ofSequence i) 0) p f)
(n : ℕ)
:
{ app : X n ⟶ Z // CategoryTheory.CommSq app (i n) p
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.ofSequence i) (n + 1))
f) }
The cocone has a natural transformation from Functor.ofSequence i
to the constant functor at Z. Here we define the first component,
NatTrans.app, of this natural transformation.
(The second component NatTrans.naturality will be obtained by NatTrans.ofSequence.)
X n ------- app n -----> Z
| |
i n p
| |
v v
X (n+1) -----> X ---f---> Y
ι (n+1)
Each app gives rise to the next commutative square,
and is a lift for the previous square.
Equations
Instances For
noncomputable def
Limits.Cocone.ofSequenceOfHasLiftingProperty
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{Z Y : C}
{X : ℕ → C}
(i : (n : ℕ) → X n ⟶ X (n + 1))
[CategoryTheory.Limits.HasColimitsOfShape ℕ C]
(p : Z ⟶ Y)
[lp : ∀ (n : ℕ), CategoryTheory.HasLiftingProperty (i n) p]
(h : X 0 ⟶ Z)
(f : CategoryTheory.Limits.colimit (CategoryTheory.Functor.ofSequence i) ⟶ Y)
(bigSq : CategoryTheory.CommSq h (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.ofSequence i) 0) p f)
:
ofSequenceOfHasLiftingProperty
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.Cocone.postcompose
{J : Type u_1}
{C : Type u_2}
[Category.{u_3, u_1} J]
[Category.{u_4, u_2} C]
{F : Functor J C}
(cc : Cocone F)
{Y' : C}
(p : cc.pt ⟶ Y')
:
Cocone F
Postcompose a cocone cc with a morphism cc.pt ⟶ Y,
giving a cocone whose point is Y. (Does mathlib have this?)
Equations
- cc.postcompose p = { pt := Y', ι := { app := fun (j : J) => CategoryTheory.CategoryStruct.comp (cc.ι.app j) p, naturality := ⋯ } }
Instances For
instance
HasLiftingProperty.of_colimit_ofSequence_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{Z Y : C}
{X : ℕ → C}
(i : (n : ℕ) → X n ⟶ X (n + 1))
[CategoryTheory.Limits.HasColimitsOfShape ℕ C]
(p : Z ⟶ Y)
[lp : ∀ (n : ℕ), CategoryTheory.HasLiftingProperty (i n) p]
:
@[reducible, inline]
noncomputable abbrev
Functor.ofSequence.coconeDropFirst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : ℕ → C}
(i : (n : ℕ) → X n ⟶ X (n + 1))
(cc : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence i))
:
CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence fun (n : ℕ) => i (n + 1))
Equations
- Functor.ofSequence.coconeDropFirst i cc = { pt := cc.pt, ι := CategoryTheory.NatTrans.ofSequence (fun (n : ℕ) => cc.ι.app (n + 1)) ⋯ }
Instances For
@[reducible, inline]
noncomputable abbrev
Functor.ofSequence.coconeUndropFirst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : ℕ → C}
(i : (n : ℕ) → X n ⟶ X (n + 1))
(cc' : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.ofSequence fun (n : ℕ) => i (n + 1)))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
Functor.ofSequence.colimitCoconeUndropFirst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : ℕ → C}
(i : (n : ℕ) → X n ⟶ X (n + 1))
[CategoryTheory.Limits.HasColimitsOfShape ℕ C]
:
Undrop (recover) the first morphism of
Limits.colimit.cocone (Functor.ofSequence fun n ↦ i (n + 1))
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
HasLiftingProperty.of_colimit_ofSequence
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{Z Y : C}
{X : ℕ → C}
(i : (n : ℕ) → X n ⟶ X (n + 1))
[CategoryTheory.Limits.HasColimitsOfShape ℕ C]
(p : Z ⟶ Y)
[lp : ∀ (n : ℕ), CategoryTheory.HasLiftingProperty (i n) p]
(m : ℕ)
:
instance
HasCurriedHEP.of_colimit_ofSequence
{X : ℕ → TopCat}
(i : (n : ℕ) → X n ⟶ X (n + 1))
{Y : TopCat}
[∀ (n : ℕ), HasCurriedHEP (i n) Y]
(n : ℕ)
:
theorem
CategoryTheory.IsPushout.hasCurriedHEP
{A B X Y Z : TopCat}
{f : A ⟶ B}
{i : A ⟶ X}
{j : B ⟶ Y}
{F : X ⟶ Y}
(po : IsPushout f i j F)
[lhep : HasCurriedHEP i Z]
:
HasCurriedHEP j Z
If
A ---f---> B
| |
i j
| p.o. |
v v
X ---F---> Y
is a pushout square and the left side i has the homotopy extension property,
then the right side j has the homotopy extension property.
- hasCurriedHEP (Y : TopCat) : HasCurriedHEP i Y
Instances
instance
instHasCurriedHEPOfIsCofibration
{A X : TopCat}
(i : A ⟶ X)
[IsCofibration i]
(Y : TopCat)
:
HasCurriedHEP i Y
instance
IsCofibration.of_comp_left
{A X X' : TopCat}
(i : A ⟶ X)
(i' : X ⟶ X')
[IsCofibration i]
[IsCofibration i']
:
instance
IsCofibration.of_sigma_map
{J : Type u}
{A B : J → TopCat}
(f : (j : J) → A j ⟶ B j)
[∀ (j : J), IsCofibration (f j)]
:
instance
IsCofibration.of_colimit_ofSequence
{X : ℕ → TopCat}
(i : (n : ℕ) → X n ⟶ X (n + 1))
[∀ (n : ℕ), IsCofibration (i n)]
(n : ℕ)
:
theorem
CategoryTheory.IsPushout.isCofibration
{A B X Y : TopCat}
{f : A ⟶ B}
{i : A ⟶ X}
{j : B ⟶ Y}
{F : X ⟶ Y}
(po : IsPushout f i j F)
(cof : IsCofibration i)
:
curriedArgSwap
C(I, C(I, Y)) --------------------> C(I, C(I, Y))
| ≃ |
| |
(exp' I).map (PathSpace.eval₀ Y) PathSpace.eval₀ (TopCat.of C(I, Y))
| |
v v
C(I, Y) ========================= C(I, Y)
If A ⟶ X is a cofibration, then TopCat.of (A × I) ⟶ TopCat.of (X × I) is a cofibration.
A × I --------> C(I, Y)
| |
i × id (PathSpace.eval₀ Y)
| |
v v
X × I ----------> Y
A ---f----> C(I, C(I, Y)) ----curriedArgSwap---> C(I, C(I, Y))
| | |
i (exp' I).map (PathSpace.eval₀ Y) PathSpace.eval₀ (TopCat.of C(I, Y))
| | |
v v v
X ----g----> C(I, Y) =========================== C(I, Y)
theorem
HasLiftingProperty.of_comp_iso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A B B' X Y : C}
(i : A ⟶ B)
(p : X ⟶ Y)
(iso : B ≅ B')
(h : CategoryTheory.HasLiftingProperty i p)
:
instance
RelCWComplex.skInclSucc_isCofibration
(X : RelCWComplex)
(n : ℕ)
:
IsCofibration (X.skInclSucc n)