Theorems · Definition · algebraic topology

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.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Cited by

5 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound