alternatingCofaceMapComplex — Mathlib

English

The morphism between alternating coface complexes induced by a morphism of cosimplicial objects is defined componentwise by f.app ⟦n⟧ and respects the differentials via naturality of f.

Русский

Морфизм между чередующими Coface-комплексами, индуцированный по морфизмy косимплициальных объектов, задан по компонентам f.app ⟦n⟧ и совместим с дифференциалами благодаря естественности f.

LaTeX

$$$\text{map } f = \mathrm{CochainComplex.ofHom}\ (n \mapsto f.app(⟦n⟧))\ (\text{with differential compatibility})$$$

Lean4

/-- The alternating coface map complex, as a functor -/
@[simps]
def alternatingCofaceMapComplex : CosimplicialObject C ⥤ CochainComplex C ℕ
    where
  obj := AlternatingCofaceMapComplex.obj
  map f := AlternatingCofaceMapComplex.map f

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