The left lifting property is stable under transfinite composition #
Let C be a category, and p : X ⟶ Y be a morphism in C. In this file,
we show that a transfinite composition of morphisms that have the left
lifting property with respect to p also has the left lifting property with
respect to p, see HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot.
About the proof, given a colimit cocone c for a well-order-continuous
functor F : J ⥤ C from a well-ordered type J, we introduce a projective
system sqFunctor c p f g : Jᵒᵖ ⥤ Type _ which associates to any j : J
the structure SqStruct c p f g j which consists of those morphisms f'
which makes the diagram below commute. The data of such compatible f' for
all j shall give the expected lifting c.pt ⟶ X for the outer square.
f
F.obj ⊥ --> X
| Λ |
| f'╱ |
v ╱ |
F.obj j | p
| |
| |
v g v
c.pt ---> Y
This is constructed by transfinite induction on j:
- When
j = ⊥, this isf; - In order to pass from
jtoOrder.succ j, we use the assumption thatF.obj j ⟶ F.obj (Order.succ j)has the left lifting property with respect top; - When
jis a limit element, we use the "continuity" ofF.
TODO: Given P : MorphismProperty C, deduce that the class of morphisms
that have the left lifting property with respect to P is stable
by transfinite composition.
structure
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
(c : Limits.Cocone F)
{X Y : C}
(p : X ⟶ Y)
(f : F.obj ⊥ ⟶ X)
(g : c.pt ⟶ Y)
(j : J)
:
Type v
Given a cocone c for a functor F : J ⥤ C from a well-ordered type,
and maps p : X ⟶ Y, f : F.obj ⊥ ⟶ X, g : c.pt ⟶ Y, this structure
contains the data of a map F.obj j ⟶ X such that F.map (homOfLE bot_le) ≫ f' = f
and f' ≫ p = c.ι.app j ≫ g. (This implies that the outer square below
commutes, see SqStruct.w.)
f
F.obj ⊥ --> X
| Λ |
| f'╱ |
v ╱ |
F.obj j | p
| |
| |
v g v
c.pt ---> Y
- f' : F.obj j ⟶ X
a morphism
F.obj j ⟶ X - w₁ : CategoryStruct.comp (F.map (homOfLE ⋯)) self.f' = f
- w₂ : CategoryStruct.comp self.f' p = CategoryStruct.comp (c.ι.app j) g
Instances For
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.ext
{C : Type u}
{inst✝ : Category.{v, u} C}
{J : Type w}
{inst✝¹ : LinearOrder J}
{inst✝² : OrderBot J}
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
{j : J}
{x y : SqStruct c p f g j}
(f' : x.f' = y.f')
:
x = y
@[simp]
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂_assoc
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
{j : J}
(self : SqStruct c p f g j)
{Z : C}
(h : Y ⟶ Z)
:
CategoryStruct.comp self.f' (CategoryStruct.comp p h) = CategoryStruct.comp (c.ι.app j) (CategoryStruct.comp g h)
@[simp]
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁_assoc
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
{j : J}
(self : SqStruct c p f g j)
{Z : C}
(h : X ⟶ Z)
:
CategoryStruct.comp (F.map (homOfLE ⋯)) (CategoryStruct.comp self.f' h) = CategoryStruct.comp f h
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
{j : J}
(sq' : SqStruct c p f g j)
:
CategoryStruct.comp f p = CategoryStruct.comp (c.ι.app ⊥) g
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w_assoc
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
{j : J}
(sq' : SqStruct c p f g j)
{Z : C}
(h : Y ⟶ Z)
:
CategoryStruct.comp f (CategoryStruct.comp p h) = CategoryStruct.comp (c.ι.app ⊥) (CategoryStruct.comp g h)
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
{j : J}
(sq' : SqStruct c p f g j)
[SuccOrder J]
:
CommSq sq'.f' (F.map (homOfLE ⋯)) p (CategoryStruct.comp (c.ι.app (Order.succ j)) g)
Given sq' : SqStruct c p f g j, this is the commutative square
sq'.f'
F.obj j --------------------> X
| |
| |p
v g v
F.obj (succ j) ---> c.pt ---> Y
(Using the lifting property for this square is the key ingredient
in the proof that the left lifting property with respect to p
is stable under transfinite composition.)
def
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
{j : J}
(sq' : SqStruct c p f g j)
{j' : J}
(α : j' ⟶ j)
:
SqStruct c p f g j'
Auxiliary definition for sqFunctor.
Equations
- sq'.map α = { f' := CategoryTheory.CategoryStruct.comp (F.map α) sq'.f', w₁ := ⋯, w₂ := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map_f'
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
{j : J}
(sq' : SqStruct c p f g j)
{j' : J}
(α : j' ⟶ j)
:
(sq'.map α).f' = CategoryStruct.comp (F.map α) sq'.f'
def
CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
(c : Limits.Cocone F)
{X Y : C}
(p : X ⟶ Y)
(f : F.obj ⊥ ⟶ X)
(g : c.pt ⟶ Y)
:
The projective system j ↦ SqStruct c p f g j.unop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor_map
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
(c : Limits.Cocone F)
{X Y : C}
(p : X ⟶ Y)
(f : F.obj ⊥ ⟶ X)
(g : c.pt ⟶ Y)
{X✝ Y✝ : Jᵒᵖ}
(α : X✝ ⟶ Y✝)
(sq' : SqStruct c p f g (Opposite.unop X✝))
:
@[simp]
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor_obj
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
(c : Limits.Cocone F)
{X Y : C}
(p : X ⟶ Y)
(f : F.obj ⊥ ⟶ X)
(g : c.pt ⟶ Y)
(j : Jᵒᵖ)
:
(sqFunctor c p f g).obj j = SqStruct c p f g (Opposite.unop j)
noncomputable def
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
[F.IsWellOrderContinuous]
{j : J}
(hj : Order.IsSuccLimit j)
(s : ↑(⋯.functor.op.comp (sqFunctor c p f g)).sections)
:
F.obj j ⟶ X
Auxiliary definition for transfiniteComposition.wellOrderInductionData.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
[F.IsWellOrderContinuous]
{j : J}
(hj : Order.IsSuccLimit j)
(s : ↑(⋯.functor.op.comp (sqFunctor c p f g)).sections)
(i : J)
(hi : i < j)
:
CategoryStruct.comp (F.map (homOfLE ⋯)) (liftHom hj s) = (↑s (Opposite.op ⟨i, hi⟩)).f'
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
[F.IsWellOrderContinuous]
{j : J}
(hj : Order.IsSuccLimit j)
(s : ↑(⋯.functor.op.comp (sqFunctor c p f g)).sections)
(i : J)
(hi : i < j)
{Z : C}
(h : X ⟶ Z)
:
CategoryStruct.comp (F.map (homOfLE ⋯)) (CategoryStruct.comp (liftHom hj s) h) = CategoryStruct.comp (↑s (Opposite.op ⟨i, hi⟩)).f' h
noncomputable def
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
[F.IsWellOrderContinuous]
{j : J}
(hj : Order.IsSuccLimit j)
(s : ↑(⋯.functor.op.comp (sqFunctor c p f g)).sections)
:
(sqFunctor c p f g).obj (Opposite.op j)
Auxiliary definition for transfiniteComposition.wellOrderInductionData.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift_f'
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
[F.IsWellOrderContinuous]
{j : J}
(hj : Order.IsSuccLimit j)
(s : ↑(⋯.functor.op.comp (sqFunctor c p f g)).sections)
:
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
[F.IsWellOrderContinuous]
{j : J}
(hj : Order.IsSuccLimit j)
(s : ↑(⋯.functor.op.comp (sqFunctor c p f g)).sections)
{i : J}
(hij : i < j)
:
SqStruct.map (lift hj s) (homOfLE ⋯) = ↑s (Opposite.op ⟨i, hij⟩)
noncomputable def
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
(c : Limits.Cocone F)
{X Y : C}
{p : X ⟶ Y}
(f : F.obj ⊥ ⟶ X)
(g : c.pt ⟶ Y)
[F.IsWellOrderContinuous]
[SuccOrder J]
(hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p)
:
(sqFunctor c p f g).WellOrderInductionData
The projective system sqFunctor c p f g has a WellOrderInductionData structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLift
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
{X Y : C}
{p : X ⟶ Y}
{f : F.obj ⊥ ⟶ X}
{g : c.pt ⟶ Y}
[F.IsWellOrderContinuous]
[SuccOrder J]
[WellFoundedLT J]
(hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p)
(sq : CommSq f (c.ι.app ⊥) p g)
:
sq.HasLift
theorem
CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot
{C : Type u}
[Category.{v, u} C]
{J : Type w}
[LinearOrder J]
[OrderBot J]
{F : Functor J C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
{X Y : C}
{p : X ⟶ Y}
[F.IsWellOrderContinuous]
[SuccOrder J]
[WellFoundedLT J]
(hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p)
:
HasLiftingProperty (c.ι.app ⊥) p