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.

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

SSet.innerAnodyneExtensions = SSet.innerFibrations.llp

Instances For

instance SSet.instIsMultiplicativeInnerAnodyneExtensions :

innerAnodyneExtensions.IsMultiplicative

instance SSet.instRespectsIsoInnerAnodyneExtensions :

innerAnodyneExtensions.RespectsIso

instance SSet.instIsStableUnderCobaseChangeInnerAnodyneExtensions :

innerAnodyneExtensions.IsStableUnderCobaseChange

instance SSet.instIsStableUnderRetractsInnerAnodyneExtensions :

innerAnodyneExtensions.IsStableUnderRetracts

instance SSet.instIsStableUnderTransfiniteCompositionInnerAnodyneExtensions :

innerAnodyneExtensions.IsStableUnderTransfiniteComposition

instance SSet.instIsStableUnderCoproductsInnerAnodyneExtensions :

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

theorem SSet.innerAnodyneExtensions.of_isIso {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

innerAnodyneExtensions f

theorem SSet.innerAnodyneExtensions_eq_llp_rlp :

innerAnodyneExtensions = innerHornInclusions.rlp.llp

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

innerAnodyneExtensions (horn n i).ι

theorem SSet.innerAnodyneExtensions_le :

innerAnodyneExtensions ≤ anodyneExtensions

instance SSet.instIsSmallInnerHornInclusions :

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

instance SSet.instIsCardinalForSmallObjectArgumentInnerHornInclusionsAleph0 :

innerHornInclusions.IsCardinalForSmallObjectArgument Cardinal.aleph0

instance SSet.instHasSmallObjectArgumentInnerHornInclusions :

innerHornInclusions.HasSmallObjectArgument

theorem SSet.innerAnodyneExtensions_eq_retracts_transfiniteCompositions :

innerAnodyneExtensions = (CategoryTheory.MorphismProperty.transfiniteCompositions.{u, u, u + 1} (CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts

theorem SSet.innerAnodyneExtensions_eq_retracts_transfiniteCompositionsOfShape :

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

def SSet.strongInnerAnodyneExtensions :

CategoryTheory.MorphismProperty SSet

In the category of simplicial sets, a strong inner anodyne extension is a morphism which belongs to the closure of inner horn inclusions by pushouts, coproducts, transfinite compositions (but not by retracts). We define this class here by saying that f : X ⟶ Y is a strong inner anodyne extension if f is a monomorphism and there exists a regular, inner pairing (in the sense of Moss) for the subcomplex Subcomplex.range f of Y.

Equations

SSet.strongInnerAnodyneExtensions f = (CategoryTheory.Mono f ∧ ∃ (P : (SSet.Subcomplex.range f).Pairing) (x : P.IsRegular), P.IsInner)

Instances For

theorem SSet.strongInnerAnodyneExtensions.mono {X Y : SSet} {f : X ⟶ Y} (hf : strongInnerAnodyneExtensions f) :

CategoryTheory.Mono f

theorem SSet.strongInnerAnodyneExtensions_le_strongAnodyneExtensions :

strongInnerAnodyneExtensions ≤ strongAnodyneExtensions

theorem SSet.Subcomplex.Pairing.strongInnerAnodyneExtensions {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [h₁ : P.IsRegular] [h₂ : P.IsInner] :

SSet.strongInnerAnodyneExtensions A.ι

theorem SSet.strongInnerAnodyneExtensions_ι_iff {X : SSet} (A : X.Subcomplex) :

strongInnerAnodyneExtensions A.ι ↔ ∃ (P : A.Pairing) (x : P.IsRegular), P.IsInner

theorem SSet.Subcomplex.Pairing.innerAnodyneExtensions {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] [P.IsInner] :

SSet.innerAnodyneExtensions A.ι

instance SSet.instRespectsIsoStrongInnerAnodyneExtensions :

strongInnerAnodyneExtensions.RespectsIso

theorem SSet.strongInnerAnodyneExtensions_le_innerAnodyneExtensions :

strongInnerAnodyneExtensions ≤ innerAnodyneExtensions