Documentation

Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Inner fibrations #

Inner fibrations of simplicial sets are the morphisms in SSet which have the right lifting property with respect to all inner horn inclusions.

Basic consequences of inner fibrations with respect to the definition of quasi-categories are formalized.

source
inductive SSet.innerHornInclusions :
CategoryTheory.MorphismProperty SSet

The family of morphisms in SSet which consists of inner horn inclusions Λ[n, i].ι : Λ[n, i] ⟶ Δ[n] (for 0 < i < n).

Instances For
    source
    theorem SSet.horn_ι_mem_innerHornInclusions {n : ℕ} {i : Fin (n + 1)} (h0 : 0 < i) (hn : i < Fin.last n) :
    innerHornInclusions (horn n i).ι
    source
    theorem SSet.innerHornInclusions_eq_iSup :
    innerHornInclusions = ⨆ (n : ℕ), CategoryTheory.MorphismProperty.ofHoms fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) => (horn (n + 2) ↑p).ι
    source
    theorem SSet.innerHornInclusions_le_J :
    innerHornInclusions ≤ modelCategoryQuillen.J
    source
    theorem SSet.innerHornInclusions_le_monomorphisms :
    innerHornInclusions ≤ CategoryTheory.MorphismProperty.monomorphisms SSet
    source
    def SSet.innerFibrations :
    CategoryTheory.MorphismProperty SSet

    The inner fibrations are the morphisms which have the right lifting property with respect to inner horn inclusions.

    Equations
    Instances For
      source
      instance SSet.instIsMultiplicativeInnerFibrations :
      innerFibrations.IsMultiplicative
      source
      instance SSet.instRespectsIsoInnerFibrations :
      innerFibrations.RespectsIso
      source
      instance SSet.instIsStableUnderBaseChangeInnerFibrations :
      innerFibrations.IsStableUnderBaseChange
      source
      instance SSet.instIsStableUnderRetractsInnerFibrations :
      innerFibrations.IsStableUnderRetracts
      source
      class SSet.InnerFibration {X Y : SSet} (q : X ⟶ Y) :
      Prop

      A morphism q satisfies [InnerFibration q] if it belongs to innerFibrations.

      Instances
        source
        theorem SSet.innerFibration_iff {X Y : SSet} (q : X ⟶ Y) :
        InnerFibration q ↔ innerFibrations q
        source
        theorem SSet.mem_innerFibrations {X Y : SSet} (q : X ⟶ Y) [InnerFibration q] :
        innerFibrations q
        source
        theorem SSet.quasicategory_of_from_innerFibrations (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) (h : innerFibrations (t.from S)) :
        S.Quasicategory
        source
        theorem SSet.Quasicategory.from_innerFibrations (S : SSet) [S.Quasicategory] {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) :
        innerFibrations (t.from S)
        source
        theorem SSet.quasicategory_iff_from_innerFibration (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) :
        S.Quasicategory ↔ InnerFibration (t.from S)

        Kerodon Tag 01BB

        source
        theorem SSet.quasicategory_of_innerFibration_quasicategory {X Y : SSet} {q : X ⟶ Y} [Y.Quasicategory] [InnerFibration q] :
        X.Quasicategory

        Kerodon Tag 01BJ