Theorems · Definition · algebraic topology

SSet.Edge.map

{X Y : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    SSet.Edge x₀ x₁ →
      (f : X ⟶ Y) →
        SSet.Edge ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₀)
          ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₁)

The image of an edge by a morphism of simplicial sets.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Cited by

7 results in Mathlib

Foundations

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