Theorems · Definition · algebraic topology

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.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Cited by

6 results in Mathlib

Foundations

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