English
There is a construction augmenting a cosimplicial object X by an object X0 and a morphism f : X0 → X[0], together with a coherence condition w ensuring compatibility of all maps with f.
Русский
Существует процесс дополнения косипликсиального объекта X объектом X0 и морфизмом f: X0 → X[0] с условием согласованности w между картинками карт X и f.
LaTeX
$$$\mathrm{augment}(X,X_0,f,w) : \mathrm{CosimplicialObject.Augmented}~C.$$$
Lean4
/-- Augment a cosimplicial object with an object. -/
@[simps]
def augment (X : CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.obj ⦋0⦌)
(w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂) : CosimplicialObject.Augmented C
where
left := X₀
right := X
hom :=
{ app := fun _ => f ≫ X.map (SimplexCategory.const _ _ 0)
naturality := by
intro i j g
dsimp
rw [Category.id_comp, Category.assoc, ← X.map_comp, w] }
-- Not `@[simp]` since `simp` can prove this.
