Documentation

TauCeti.AlgebraicTopology.SimplicialSet.AnodyneExtensions.LeftRight.Basic

Left and right fibrations, left and right anodyne extensions #

A left horn is a horn Λ[n, i] ⊆ Δ[n] with i < n, i.e. one missing a face other than the last one, and a right horn is one with 0 < i. A morphism of simplicial sets is a left fibration (resp. a right fibration) when it has the right lifting property with respect to the left (resp. right) horn inclusions, and a left anodyne extension (resp. right anodyne extension) when it has the left lifting property with respect to all left (resp. right) fibrations.

Inner horns are both left and right horns, and left and right horns are horns of positive dimension, so every Kan fibration is a left and a right fibration, and both are inner fibrations; in particular, by Mathlib's SSet.quasicategory_of_innerFibration, the total space of a left or right fibration over a quasicategory is a quasicategory. Left and right fibrations are the covariant and contravariant models of space-valued functors on their base. For instance, the projections from the coslices and slices of a quasicategory to it are left and right fibrations, and they underlie the Yoneda embedding, the theory of final maps and straightening.

As for Mathlib's inner anodyne extensions, the small object argument identifies left (resp. right) anodyne extensions with the retracts of transfinite compositions of pushouts of coproducts of left (resp. right) horn inclusions. A regular pairing of a subcomplex in the sense of Moss whose type (II) simplices are never the last (resp. first) face of their partners gives a left (resp. right) anodyne extension (SSet.Subcomplex.Pairing.leftAnodyneExtensions, SSet.Subcomplex.Pairing.rightAnodyneExtensions).

Main definitions #

SSet.leftHornInclusions, SSet.rightHornInclusions: the left and right horn inclusions.
SSet.leftFibrations, SSet.rightFibrations, with the classes SSet.LeftFibration and SSet.RightFibration.
SSet.leftAnodyneExtensions, SSet.rightAnodyneExtensions.

References #

J. Lurie, Higher Topos Theory, Definition 2.0.0.3 and Section 2.1.2.
S. Moss, Another approach to the Kan-Quillen model structure, J. Homotopy Relat. Struct. 15 (2020).

inductive SSet.leftHornInclusions :

CategoryTheory.MorphismProperty SSet

The left horn inclusions Λ[n, i].ι : Λ[n, i] ⟶ Δ[n], for 0 < n and i < n.

intro {n : ℕ} (i : Fin (n + 2)) (hn : i < Fin.last (n + 1)) : leftHornInclusions (horn (n + 1) i).ι

Instances For

inductive SSet.rightHornInclusions :

CategoryTheory.MorphismProperty SSet

The right horn inclusions Λ[n, i].ι : Λ[n, i] ⟶ Δ[n], for 0 < i ≤ n.

intro {n : ℕ} (i : Fin (n + 2)) (h0 : 0 < i) : rightHornInclusions (horn (n + 1) i).ι

Instances For

theorem SSet.horn_ι_mem_leftHornInclusions {n : ℕ} {i : Fin (n + 1)} (hn : i < Fin.last n) :

leftHornInclusions (horn n i).ι

theorem SSet.horn_ι_mem_rightHornInclusions {n : ℕ} {i : Fin (n + 1)} (h0 : 0 < i) :

rightHornInclusions (horn n i).ι

theorem SSet.leftHornInclusions_eq_iSup :

leftHornInclusions = ⨆ (n : ℕ), CategoryTheory.MorphismProperty.ofHoms fun (p : { p : Fin (n + 2) // p < Fin.last (n + 1) }) => (horn (n + 1) ↑p).ι

theorem SSet.rightHornInclusions_eq_iSup :

rightHornInclusions = ⨆ (n : ℕ), CategoryTheory.MorphismProperty.ofHoms fun (p : { p : Fin (n + 2) // 0 < p }) => (horn (n + 1) ↑p).ι

theorem SSet.innerHornInclusions_le_leftHornInclusions :

innerHornInclusions ≤ leftHornInclusions

theorem SSet.innerHornInclusions_le_rightHornInclusions :

innerHornInclusions ≤ rightHornInclusions

theorem SSet.leftHornInclusions_le_J :

leftHornInclusions ≤ modelCategoryQuillen.J

theorem SSet.rightHornInclusions_le_J :

rightHornInclusions ≤ modelCategoryQuillen.J

def SSet.leftFibrations :

CategoryTheory.MorphismProperty SSet

The left fibrations are the morphisms which have the right lifting property with respect to the left horn inclusions Λ[n, i] ⟶ Δ[n], i < n.

Instances For

instance SSet.instIsMultiplicativeLeftFibrations :

leftFibrations.IsMultiplicative

instance SSet.instRespectsIsoLeftFibrations :

leftFibrations.RespectsIso

instance SSet.instIsStableUnderBaseChangeLeftFibrations :

leftFibrations.IsStableUnderBaseChange

instance SSet.instIsStableUnderRetractsLeftFibrations :

leftFibrations.IsStableUnderRetracts

def SSet.rightFibrations :

CategoryTheory.MorphismProperty SSet

The right fibrations are the morphisms which have the right lifting property with respect to the right horn inclusions Λ[n, i] ⟶ Δ[n], 0 < i.

Instances For

instance SSet.instIsMultiplicativeRightFibrations :

rightFibrations.IsMultiplicative

instance SSet.instRespectsIsoRightFibrations :

rightFibrations.RespectsIso

instance SSet.instIsStableUnderBaseChangeRightFibrations :

rightFibrations.IsStableUnderBaseChange

instance SSet.instIsStableUnderRetractsRightFibrations :

rightFibrations.IsStableUnderRetracts

theorem SSet.leftFibrations_eq_rlp :

leftFibrations = leftHornInclusions.rlp

theorem SSet.rightFibrations_eq_rlp :

rightFibrations = rightHornInclusions.rlp

class SSet.LeftFibration {X Y : SSet} (p : X ⟶ Y) :

A morphism p satisfies [LeftFibration p] if it belongs to leftFibrations.

mem : leftFibrations p

Instances

theorem SSet.leftFibration_iff {X Y : SSet} (p : X ⟶ Y) :

LeftFibration p ↔ leftFibrations p

class SSet.RightFibration {X Y : SSet} (p : X ⟶ Y) :

A morphism p satisfies [RightFibration p] if it belongs to rightFibrations.

mem : rightFibrations p

Instances

theorem SSet.rightFibration_iff {X Y : SSet} (p : X ⟶ Y) :

RightFibration p ↔ rightFibrations p

theorem SSet.mem_leftFibrations {X Y : SSet} (p : X ⟶ Y) [LeftFibration p] :

leftFibrations p

theorem SSet.mem_rightFibrations {X Y : SSet} (p : X ⟶ Y) [RightFibration p] :

rightFibrations p

theorem SSet.leftFibration_iff_hasLiftingProperty {X Y : SSet} (p : X ⟶ Y) :

LeftFibration p ↔ ∀ ⦃n : ℕ⦄, ∀ i < Fin.last n, CategoryTheory.HasLiftingProperty (horn n i).ι p

theorem SSet.rightFibration_iff_hasLiftingProperty {X Y : SSet} (p : X ⟶ Y) :

RightFibration p ↔ ∀ ⦃n : ℕ⦄ (i : Fin (n + 1)), 0 < i → CategoryTheory.HasLiftingProperty (horn n i).ι p

instance SSet.instLeftFibrationOfIsIso {X Y : SSet} (p : X ⟶ Y) [CategoryTheory.IsIso p] :

LeftFibration p

instance SSet.instRightFibrationOfIsIso {X Y : SSet} (p : X ⟶ Y) [CategoryTheory.IsIso p] :

RightFibration p

instance SSet.instLeftFibrationComp {X Y Z : SSet} (p : X ⟶ Y) (q : Y ⟶ Z) [LeftFibration p] [LeftFibration q] :

LeftFibration (CategoryTheory.CategoryStruct.comp p q)

instance SSet.instRightFibrationComp {X Y Z : SSet} (p : X ⟶ Y) (q : Y ⟶ Z) [RightFibration p] [RightFibration q] :

RightFibration (CategoryTheory.CategoryStruct.comp p q)

theorem SSet.LeftFibration.of_isPullback {X Y X' Y' : SSet} {p : X ⟶ Y} {p' : X' ⟶ Y'} {f : X' ⟶ X} {g : Y' ⟶ Y} (h : CategoryTheory.IsPullback f p' p g) [LeftFibration p] :

LeftFibration p'

Left fibrations are stable under base change.

theorem SSet.RightFibration.of_isPullback {X Y X' Y' : SSet} {p : X ⟶ Y} {p' : X' ⟶ Y'} {f : X' ⟶ X} {g : Y' ⟶ Y} (h : CategoryTheory.IsPullback f p' p g) [RightFibration p] :

RightFibration p'

Right fibrations are stable under base change.

instance SSet.instLeftFibrationOfFibration {X Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] :

LeftFibration p

Kan fibrations are left fibrations.

instance SSet.instRightFibrationOfFibration {X Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] :

RightFibration p

Kan fibrations are right fibrations.

instance SSet.instInnerFibrationOfLeftFibration {X Y : SSet} (p : X ⟶ Y) [LeftFibration p] :

InnerFibration p

Left fibrations are inner fibrations.

instance SSet.instInnerFibrationOfRightFibration {X Y : SSet} (p : X ⟶ Y) [RightFibration p] :

InnerFibration p

Right fibrations are inner fibrations.

def SSet.leftAnodyneExtensions :

CategoryTheory.MorphismProperty SSet

In the category of simplicial sets, a left anodyne extension is a morphism that has the left lifting property with respect to left fibrations.

Instances For

instance SSet.instIsMultiplicativeLeftAnodyneExtensions :

leftAnodyneExtensions.IsMultiplicative

instance SSet.instRespectsIsoLeftAnodyneExtensions :

leftAnodyneExtensions.RespectsIso

instance SSet.instIsStableUnderCobaseChangeLeftAnodyneExtensions :

leftAnodyneExtensions.IsStableUnderCobaseChange

instance SSet.instIsStableUnderRetractsLeftAnodyneExtensions :

leftAnodyneExtensions.IsStableUnderRetracts

instance SSet.instIsStableUnderTransfiniteCompositionLeftAnodyneExtensions :

leftAnodyneExtensions.IsStableUnderTransfiniteComposition

instance SSet.instIsStableUnderCoproductsLeftAnodyneExtensions :

CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u_1, u_2, u_2 + 1} leftAnodyneExtensions

def SSet.rightAnodyneExtensions :

CategoryTheory.MorphismProperty SSet

In the category of simplicial sets, a right anodyne extension is a morphism that has the left lifting property with respect to right fibrations.

Instances For

instance SSet.instIsMultiplicativeRightAnodyneExtensions :

rightAnodyneExtensions.IsMultiplicative

instance SSet.instRespectsIsoRightAnodyneExtensions :

rightAnodyneExtensions.RespectsIso

instance SSet.instIsStableUnderCobaseChangeRightAnodyneExtensions :

rightAnodyneExtensions.IsStableUnderCobaseChange

instance SSet.instIsStableUnderRetractsRightAnodyneExtensions :

rightAnodyneExtensions.IsStableUnderRetracts

instance SSet.instIsStableUnderTransfiniteCompositionRightAnodyneExtensions :

rightAnodyneExtensions.IsStableUnderTransfiniteComposition

instance SSet.instIsStableUnderCoproductsRightAnodyneExtensions :

CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u_1, u_2, u_2 + 1} rightAnodyneExtensions

theorem SSet.leftAnodyneExtensions_eq_llp :

leftAnodyneExtensions = leftFibrations.llp

theorem SSet.rightAnodyneExtensions_eq_llp :

rightAnodyneExtensions = rightFibrations.llp

theorem SSet.leftAnodyneExtensions_eq_llp_rlp :

leftAnodyneExtensions = leftHornInclusions.rlp.llp

theorem SSet.rightAnodyneExtensions_eq_llp_rlp :

rightAnodyneExtensions = rightHornInclusions.rlp.llp

theorem SSet.leftAnodyneExtensions.horn_ι {n : ℕ} {i : Fin (n + 1)} (hn : i < Fin.last n) :

leftAnodyneExtensions (horn n i).ι

theorem SSet.rightAnodyneExtensions.horn_ι {n : ℕ} {i : Fin (n + 1)} (h0 : 0 < i) :

rightAnodyneExtensions (horn n i).ι

theorem SSet.leftAnodyneExtensions.hasLiftingProperty {A B X Y : SSet} {i : A ⟶ B} (hi : leftAnodyneExtensions i) (p : X ⟶ Y) [LeftFibration p] :

CategoryTheory.HasLiftingProperty i p

theorem SSet.rightAnodyneExtensions.hasLiftingProperty {A B X Y : SSet} {i : A ⟶ B} (hi : rightAnodyneExtensions i) (p : X ⟶ Y) [RightFibration p] :

CategoryTheory.HasLiftingProperty i p

theorem SSet.innerAnodyneExtensions_le_leftAnodyneExtensions :

innerAnodyneExtensions ≤ leftAnodyneExtensions

theorem SSet.innerAnodyneExtensions_le_rightAnodyneExtensions :

innerAnodyneExtensions ≤ rightAnodyneExtensions

theorem SSet.leftAnodyneExtensions_le_anodyneExtensions :

leftAnodyneExtensions ≤ anodyneExtensions

theorem SSet.rightAnodyneExtensions_le_anodyneExtensions :

rightAnodyneExtensions ≤ anodyneExtensions

instance SSet.instIsSmallLeftHornInclusions :

CategoryTheory.MorphismProperty.IsSmall.{u, u, u + 1} leftHornInclusions

instance SSet.instIsSmallRightHornInclusions :

CategoryTheory.MorphismProperty.IsSmall.{u, u, u + 1} rightHornInclusions

instance SSet.instIsCardinalForSmallObjectArgumentLeftHornInclusionsAleph0 :

leftHornInclusions.IsCardinalForSmallObjectArgument Cardinal.aleph0

instance SSet.instIsCardinalForSmallObjectArgumentRightHornInclusionsAleph0 :

rightHornInclusions.IsCardinalForSmallObjectArgument Cardinal.aleph0

instance SSet.instHasSmallObjectArgumentLeftHornInclusions :

leftHornInclusions.HasSmallObjectArgument

instance SSet.instHasSmallObjectArgumentRightHornInclusions :

rightHornInclusions.HasSmallObjectArgument

theorem SSet.leftAnodyneExtensions_eq_retracts_transfiniteCompositionsOfShape :

leftAnodyneExtensions = ((CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} leftHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Left anodyne extensions are the retracts of transfinite compositions of pushouts of coproducts of left horn inclusions.

theorem SSet.rightAnodyneExtensions_eq_retracts_transfiniteCompositionsOfShape :

rightAnodyneExtensions = ((CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} rightHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Right anodyne extensions are the retracts of transfinite compositions of pushouts of coproducts of right horn inclusions.

theorem SSet.Subcomplex.Pairing.leftAnodyneExtensions {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] (hP : ∀ (x : ↑P.II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ Fin.last (d + 1)) :

SSet.leftAnodyneExtensions A.ι

The inclusion of a subcomplex admitting a regular pairing in which no type (II) simplex is the last face of the corresponding type (I) simplex is a left anodyne extension.

theorem SSet.Subcomplex.Pairing.rightAnodyneExtensions {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] (hP : ∀ (x : ↑P.II) {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ 0) :

SSet.rightAnodyneExtensions A.ι

The inclusion of a subcomplex admitting a regular pairing in which no type (II) simplex is the first face of the corresponding type (I) simplex is a right anodyne extension.