map — Mathlib

English

The normalized Moore complex is a functor sending a morphism f: X → Y of simplicial objects to a morphism of chain complexes obj X → obj Y, defined levelwise by factoring through kernels as in objD and respecting composition via naturality of δ.

Русский

Нормализованный Moore-функтор отображает морфизм f: X → Y между симплициальными объектами в морфизмы между цепными комплексами, объектно по уровням через objD и совместим с композицией благодаря натурализму δ.

LaTeX

$$$\\mathrm{map}(f) : \\mathrm{obj}\,X \\to \\mathrm{obj}\,Y$$$

Lean4

/-- The normalized Moore complex functor, on morphisms.
-/
@[simps!]
def map (f : X ⟶ Y) : obj X ⟶ obj Y :=
  ChainComplex.ofHom _ _ _ _ _ _
    (fun n =>
      factorThru _ (arrow _ ≫ f.app (op ⦋n⦌))
        (by
          cases n <;> dsimp
          · apply top_factors
          · refine (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ ?_
            rw [Category.assoc, SimplicialObject.δ, ← f.naturality, ←
              factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)), Category.assoc]
            erw [kernelSubobject_arrow_comp_assoc]
            rw [zero_comp, comp_zero]))
    fun n => by cases n <;> dsimp [objD, objX] <;> cat_disch

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