Documentation

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Inner anodyne extensions #

Much of this file is mirrored from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic.

Inner anodyne extensions form a property of morphisms in the category of simplicial sets. It contains inner horn inclusions and it is closed under coproducts, pushouts, transfinite compositions and retracts. Equivalently, using the small object argument, inner anodyne extensions can be defined (and are defined here) as the class of morphisms that satisfy the left lifting property with respect to the class of inner fibrations.

source
def SSet.innerAnodyneExtensions :
CategoryTheory.MorphismProperty SSet

In the category of simplicial sets, an inner anodyne extension is a morphism that has the left lifting property with respect to inner fibrations, where an inner fibration is a morphism that has the right lifting property with respect to inner horn inclusions.

Equations
Instances For
    source
    instance SSet.instIsMultiplicativeInnerAnodyneExtensions :
    innerAnodyneExtensions.IsMultiplicative
    source
    instance SSet.instRespectsIsoInnerAnodyneExtensions :
    innerAnodyneExtensions.RespectsIso
    source
    instance SSet.instIsStableUnderCobaseChangeInnerAnodyneExtensions :
    innerAnodyneExtensions.IsStableUnderCobaseChange
    source
    instance SSet.instIsStableUnderRetractsInnerAnodyneExtensions :
    innerAnodyneExtensions.IsStableUnderRetracts
    source
    instance SSet.instIsStableUnderTransfiniteCompositionInnerAnodyneExtensions :
    innerAnodyneExtensions.IsStableUnderTransfiniteComposition
    source
    instance SSet.instIsStableUnderCoproductsInnerAnodyneExtensions :
    CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u_1, u_2, u_2 + 1} innerAnodyneExtensions
    source
    theorem SSet.innerAnodyneExtensions.of_isIso {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
    innerAnodyneExtensions f
    source
    theorem SSet.innerAnodyneExtensions_eq_llp_rlp :
    innerAnodyneExtensions = innerHornInclusions.rlp.llp
    source
    theorem SSet.innerAnodyneExtensions.horn_ι {n : ℕ} {i : Fin (n + 1)} (h0 : 0 < i) (hn : i < Fin.last n) :
    innerAnodyneExtensions (horn n i).ι
    source
    theorem SSet.innerAnodyneExtensions_le :
    innerAnodyneExtensions ≤ anodyneExtensions
    source
    instance SSet.instIsSmallInnerHornInclusions :
    CategoryTheory.MorphismProperty.IsSmall.{u, u, u + 1} innerHornInclusions
    source
    instance SSet.instIsCardinalForSmallObjectArgumentInnerHornInclusionsAleph0 :
    innerHornInclusions.IsCardinalForSmallObjectArgument Cardinal.aleph0
    source
    instance SSet.instHasSmallObjectArgumentInnerHornInclusions :
    innerHornInclusions.HasSmallObjectArgument
    source
    theorem SSet.innerAnodyneExtensions_eq_retracts_transfiniteCompositions :
    innerAnodyneExtensions = (CategoryTheory.MorphismProperty.transfiniteCompositions.{u, u, u + 1} (CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts
    source
    theorem SSet.innerAnodyneExtensions_eq_retracts_transfiniteCompositionsOfShape :
    innerAnodyneExtensions = ((CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts