unitHomEquiv — Mathlib

English

There is a natural equivalence between morphisms from the identity to K and the 0-simplices of K.

Русский

Существуют естественные эквивалентности между морфизмами от единицы к K и 0-симплексами K.

LaTeX

$$$ (\mathbb{1} \to K) \simeq K_{⟂0⟬} $$$

Lean4

/-- The bijection `(𝟙_ SSet ⟶ K) ≃ K _⦋0⦌`. -/
def unitHomEquiv (K : SSet.{u}) : (𝟙_ _ ⟶ K) ≃ K _⦋0⦌
    where
  toFun φ := φ.app _ PUnit.unit
  invFun
    x :=
    { app := fun Δ _ => K.map (SimplexCategory.const Δ.unop ⦋0⦌ 0).op x
      naturality := fun Δ Δ' f => by
        ext ⟨⟩
        dsimp
        rw [← FunctorToTypes.map_comp_apply]
        rfl }
  left_inv
    φ := by
    ext Δ ⟨⟩
    dsimp
    rw [← FunctorToTypes.naturality]
    rfl
  right_inv x := by simp

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