Theorems · Definition · category theory

CategoryTheory.nerve.edgeMk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {x y : C} → (x ⟶ y) → SSet.Edge (CategoryTheory.nerveEquiv.symm x) (CategoryTheory.nerveEquiv.symm y)

Constructor for edges in the nerve of a category. (See also homEquiv.)

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Cited by: 9 results in Mathlib
Foundations: Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

DFunLike.coestatement · cited by 62,936
CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
Equivstatement · cited by 8,337
Equiv.symmstatement · cited by 3,681
CategoryTheory.ComposableArrowsstatement · cited by 627
CategoryTheory.ComposableArrows.mk₁proof · cited by 350
CategoryTheory.nervestatement · cited by 68
SSet.Edgestatement · cited by 55
CategoryTheory.nerveEquivstatement · cited by 21
SSet.Edge.mkproof · cited by 4

Cited by10

Results whose statement or proof uses this declaration.

CategoryTheory.nerve.functorOfNerveMapproof · cited by 4
CategoryTheory.nerve.nonempty_compStruct_iffstatement and proof · cited by 1
CategoryTheory.nerve.edgeMk_surjectivestatement and proof · cited by 1
CategoryTheory.nerve.homEquiv_edgeMkstatement and proof · cited by 1
CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMapproof · cited by 0
CategoryTheory.nerve.edgeMk_edgestatement · cited by 0
CategoryTheory.nerve.edgeMk_idstatement · cited by 0
CategoryTheory.nerve.functorOfNerveMap_mapstatement · cited by 0
CategoryTheory.nerve.homEquiv_compproof · cited by 0
CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMapstatement · cited by 0