Theorems · Definition · algebraic topology

SSet.Truncated.Edge.map

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

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

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Cited by: 17 results in Mathlib
Foundations: Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
Oppositestatement · cited by 8,081
CategoryTheory.NatTrans.appstatement and proof · cited by 7,406
CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
SimplexCategorystatement · cited by 2,204
TypeCat.Funstatement · cited by 1,307
SimplexCategory.lenstatement · cited by 542
SimplexCategory.Truncatedstatement · cited by 236
SSet.Truncatedstatement and proof · cited by 214
SSet.Truncated.Edgestatement and proof · cited by 81

Cited by22

Results whose statement or proof uses this declaration.

SSet.Edge.mapproof · cited by 7
SSet.OneTruncation₂.mapproof · cited by 4
CategoryTheory.nerve.functorOfNerveMapproof · cited by 4
SSet.Truncated.HomotopyCategory.descOfTruncationproof · cited by 3
SSet.Truncated.Edge.map_edgestatement and proof · cited by 2
SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMkstatement and proof · cited by 1
SSet.OneTruncation₂.map_mapstatement · cited by 1
SSet.Truncated.Edge.CompStruct.mapstatement · cited by 1
SSet.Truncated.Edge.map_idstatement · cited by 1
CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMapproof · cited by 0
SSet.Truncated.HomotopyCategory.descOfTruncation_compproof · cited by 0
SSet.Truncated.mapHomotopyCategory_homMkstatement · cited by 0