Documentation

Mathlib.AlgebraicTopology.MooreComplex

Moore complex #

We construct the normalized Moore complex, as a functor SimplicialObject C ⥤ ChainComplex C ℕ, for any abelian category C.

The n-th object is intersection of the kernels of X.δ i : X.obj n ⟶ X.obj (n-1), for i = 1, ..., n.

The differentials are induced from X.δ 0, which maps each of these intersections of kernels to the next.

This functor is one direction of the Dold-Kan equivalence, which we're still working towards.

References #

The definitions in this namespace are all auxiliary definitions for NormalizedMooreComplex and should usually only be accessed via that.

The differentials in the normalized Moore complex.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem AlgebraicTopology.NormalizedMooreComplex.obj_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ) :
    (AlgebraicTopology.NormalizedMooreComplex.obj X).X n = CategoryTheory.Subobject.underlying.obj (match n with | 0 => | n.succ => Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X k.succ))
    @[simp]
    theorem AlgebraicTopology.NormalizedMooreComplex.obj_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (i : ) (j : ) :
    (AlgebraicTopology.NormalizedMooreComplex.obj X).d i j = if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ) (match j with | 0 => CategoryTheory.CategoryStruct.comp (Finset.univ.inf fun (k : Fin (0 + 1)) => CategoryTheory.Limits.kernelSubobject (X k.succ)).arrow (CategoryTheory.CategoryStruct.comp (X 0) (CategoryTheory.inv .arrow)) | n.succ => (Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X k.succ)).factorThru (CategoryTheory.CategoryStruct.comp (Finset.univ.inf fun (k : Fin (n + 1 + 1)) => CategoryTheory.Limits.kernelSubobject (X k.succ)).arrow (X 0)) ) else 0

    The normalized Moore complex functor, on objects.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem AlgebraicTopology.NormalizedMooreComplex.map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X Y) (n : ) :
      (AlgebraicTopology.NormalizedMooreComplex.map f).f n = (match n with | 0 => | n.succ => Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (Y k.succ)).factorThru (CategoryTheory.CategoryStruct.comp (match n with | 0 => | n.succ => Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X k.succ)).arrow (f.app (Opposite.op (SimplexCategory.mk n))))

      The normalized Moore complex functor, on morphisms.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The (normalized) Moore complex of a simplicial object X in an abelian category C.

        The n-th object is intersection of the kernels of X.δ i : X.obj n ⟶ X.obj (n-1), for i = 1, ..., n.

        The differentials are induced from X.δ 0, which maps each of these intersections of kernels to the next.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For