English
For an augmented simplicial object X augmented by X0 via f, the induced hom at level 0 equals f.
Русский
Для аугментированного симпликального объекта X, аугментированного через f, полученная в нулевом уровне морфизм равна f.
LaTeX
$$$$ (X.augment X_0 f w).hom.\\!\\app (op⟦0⟧) = f $$$$
Lean4
/-- Augment a simplicial object with an object. -/
@[simps]
def augment (X : SimplicialObject C) (X₀ : C) (f : X _⦋0⦌ ⟶ X₀)
(w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f) : SimplicialObject.Augmented C
where
left := X
right := X₀
hom :=
{ app := fun _ => X.map (SimplexCategory.const _ _ 0).op ≫ f
naturality := by
intro i j g
dsimp
rw [← g.op_unop]
simpa only [← X.map_comp, ← Category.assoc, Category.comp_id, ← op_comp] using w _ _ _ }
-- Not `@[simp]` since `simp` can prove this.
