Anodyne extensions

Anodyne extensions form a property of morphisms in the category of simplicial sets. It contains horn inclusions and it is closed under coproducts, pushouts, transfinite compositions and retracts. Equivalently, using the small object argument, 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 fibrations (for the Quillen model category structure: fibrations are morphisms that have the right lifting property with respect to horn inclusions). When the Quillen model category structure is fully upstreamed (TODO @joelriou), it can be shown that a morphism f is an anodyne extension iff f is a cofibration that is also a weak equivalence.

We also introduce the class of strong anodyne extensions that could be defined as a closure similarly as anodyne extensions, but without taking the closure under retracts. Sean Moss has given a combinatorial description of these strong anodyne extensions: the inclusion A.ι : A ⟶ X of a subcomplex A of a simplicial set X is a strong anodyne extension iff there exists a regular pairing for A. In this file, we define strong anodyne extensions in terms of such regular pairings, and using the main result of the file Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean we show that a strong anodyne extension is an anodyne extension.

TODO

• introduce inner variants of these definitions
• show that strong anodyne extensions are indeed stable under coproducts, transfinite compositions and pushouts (the proof should reduce to the construction of pairings)
• study the interaction between anodyne extension and binary products: the critical case consists in showing that inclusions Λ[m, i] ⊗ Δ[n] ∪ Δ[m] ⊗ ∂Δ[n] ⟶ Δ[m] ⊗ Δ[n] are strong anodyne extensions (@joelriou)
• show that anodyne extensions are stable under the subdivision functor (@joelriou)

References

• P. Gabriel, M. Zisman, Calculus of fractions and homotopy theory, IV.2
• Sean Moss, Another approach to the Kan-Quillen model structure

def SSet.anodyneExtensions : CategoryTheory.MorphismProperty SSet

In the category of simplicial sets, an anodyne extension is a morphism that has the left lifting property with respect to fibrations, where a fibration is a morphism that has the right lifting property with respect to horn inclusions. We do not introduce a typeclass for anodyne extensions because when the Quillen model structure is fully upstreamed (TODO @joelriou), the assumption anodyneExtensions f can be spelled as [Cofibration f] [WeakEquivalence f].

Equations

• SSet.anodyneExtensions = (HomotopicalAlgebra.fibrations SSet).llp

instance SSet.instIsMultiplicativeAnodyneExtensions : anodyneExtensions.IsMultiplicative

instance SSet.instRespectsIsoAnodyneExtensions : anodyneExtensions.RespectsIso

instance SSet.instIsStableUnderCobaseChangeAnodyneExtensions : anodyneExtensions.IsStableUnderCobaseChange

instance SSet.instIsStableUnderRetractsAnodyneExtensions : anodyneExtensions.IsStableUnderRetracts

instance SSet.instIsStableUnderTransfiniteCompositionAnodyneExtensions : anodyneExtensions.IsStableUnderTransfiniteComposition

instance SSet.instIsStableUnderCoproductsAnodyneExtensions : CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u_1, u_2, u_2 + 1} anodyneExtensions

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

theorem SSet.anodyneExtensions_eq_llp_rlp : anodyneExtensions = modelCategoryQuillen.J.rlp.llp

theorem SSet.anodyneExtensions.horn_ι {n : ℕ} [NeZero n] (i : Fin (n + 1)) : anodyneExtensions (horn n i).ι

instance SSet.instIsSmallOfHomsFinHAddNatOfNatιHorn (n : ℕ) : CategoryTheory.MorphismProperty.IsSmall.{u, u, u + 1} (CategoryTheory.MorphismProperty.ofHoms fun (i : Fin (n + 2)) => (horn (n + 1) i).ι)

instance SSet.instIsSmallJ : CategoryTheory.MorphismProperty.IsSmall.{u, u, u + 1} modelCategoryQuillen.J

instance SSet.instIsCardinalForSmallObjectArgumentJAleph0 : modelCategoryQuillen.J.IsCardinalForSmallObjectArgument Cardinal.aleph0

instance SSet.instHasSmallObjectArgumentJ : modelCategoryQuillen.J.HasSmallObjectArgument

theorem SSet.anodyneExtensions_eq_retracts_transfiniteCompositions : anodyneExtensions = (CategoryTheory.MorphismProperty.transfiniteCompositions.{u, u, u + 1} (CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts

theorem SSet.anodyneExtensions_eq_retracts_transfiniteCompositionsOfShape : anodyneExtensions = ((CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts

def SSet.strongAnodyneExtensions : CategoryTheory.MorphismProperty SSet

In the category of simplicial sets, a strong anodyne extension is a morphism which belongs to the closure of 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 anodyne extension if f is a monomorphism and there exists a regular pairing (in the sense of Moss) for the subcomplex Subcomplex.range f of Y.

Equations

• SSet.strongAnodyneExtensions f = (CategoryTheory.Mono f ∧ ∃ (P : (SSet.Subcomplex.range f).Pairing), P.IsRegular)

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

theorem SSet.strongAnodyneExtensions_ι_iff {X : SSet} (A : X.Subcomplex) : strongAnodyneExtensions A.ι ↔ ∃ (P : A.Pairing), P.IsRegular

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

theorem SSet.strongAnodyneExtensions_le_anodyneExtensions : strongAnodyneExtensions ≤ anodyneExtensions