δ₁_mk₂_eq — Mathlib

English

In a category C, for any objects X0, X1, X2 and arrows f: X0 → X1, g: X1 → X2, the first face map applied to the 2-simplex consisting of f and g equals the 1-simplex given by the composite f ∘ g.

Русский

В категории C для любых объектов X0, X1, X2 и стрелок f: X0 → X1, g: X1 → X2, первый лицевой морфизм применённый к 2-границе mk₂(f,g) равен 1-границе mk₁(ƒ ∘ g).

LaTeX

$$$\delta_1\big(\mathrm{mk}_2(f,g)\big) = \mathrm{mk}_1(f \circ g).$$$

Lean4

theorem δ₁_mk₂_eq : (nerve C).δ 1 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ (f ≫ g) :=
  ComposableArrows.ext₁ rfl rfl (by simp; rfl)

Похожие утверждения