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

• https://stacks.math.columbia.edu/tag/0194
• https://ncatlab.org/nlab/show/Moore+complex

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

def AlgebraicTopology.NormalizedMooreComplex.objX {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : CategoryTheory.Subobject (X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)))

The normalized Moore complex in degree n, as a subobject of X n.

Equations

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

@[simp]

theorem AlgebraicTopology.NormalizedMooreComplex.objX_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) : AlgebraicTopology.NormalizedMooreComplex.objX X 0 = ⊤

@[simp]

theorem AlgebraicTopology.NormalizedMooreComplex.objX_add_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1) = Finset.inf Finset.univ fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (CategoryTheory.SimplicialObject.δ X (Fin.succ k))

def AlgebraicTopology.NormalizedMooreComplex.objD {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : CategoryTheory.Subobject.underlying.toPrefunctor.obj (AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1)) ⟶ CategoryTheory.Subobject.underlying.toPrefunctor.obj (AlgebraicTopology.NormalizedMooreComplex.objX X n)

The differentials in the normalized Moore complex.

Equations

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

theorem AlgebraicTopology.NormalizedMooreComplex.d_squared {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (AlgebraicTopology.NormalizedMooreComplex.objD X (n + 1)) (AlgebraicTopology.NormalizedMooreComplex.objD X n) = 0

@[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.toPrefunctor.obj (AlgebraicTopology.NormalizedMooreComplex.objX X n)

@[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 (_ : CategoryTheory.Subobject.underlying.toPrefunctor.obj (AlgebraicTopology.NormalizedMooreComplex.objX X i) = CategoryTheory.Subobject.underlying.toPrefunctor.obj (AlgebraicTopology.NormalizedMooreComplex.objX X (j + 1)))) (match j with | 0 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (Finset.inf Finset.univ fun (k : Fin (0 + 1)) => CategoryTheory.Limits.kernelSubobject (CategoryTheory.SimplicialObject.δ X (Fin.succ k)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X 0) (CategoryTheory.inv (CategoryTheory.Subobject.arrow ⊤))) | Nat.succ n => CategoryTheory.Subobject.factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (CategoryTheory.SimplicialObject.δ X (Fin.succ k))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) => CategoryTheory.Limits.kernelSubobject (CategoryTheory.SimplicialObject.δ X (Fin.succ k)))) (CategoryTheory.SimplicialObject.δ X 0)) (_ : CategoryTheory.Subobject.Factors (Finset.inf Finset.univ fun (k : Fin (Nat.add n 0 + 1)) => CategoryTheory.Limits.kernelSubobject (CategoryTheory.SimplicialObject.δ X (Fin.succ k))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1 + 1))) (CategoryTheory.SimplicialObject.δ X 0)))) else 0

def AlgebraicTopology.NormalizedMooreComplex.obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) : ChainComplex C ℕ

The normalized Moore complex functor, on objects.

Equations

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

@[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 = CategoryTheory.Subobject.factorThru (AlgebraicTopology.NormalizedMooreComplex.objX Y n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (AlgebraicTopology.NormalizedMooreComplex.objX X n)) (f.app (Opposite.op (SimplexCategory.mk n)))) (_ : CategoryTheory.Subobject.Factors (AlgebraicTopology.NormalizedMooreComplex.objX Y n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (AlgebraicTopology.NormalizedMooreComplex.objX X n)) (f.app (Opposite.op (SimplexCategory.mk n)))))

def AlgebraicTopology.NormalizedMooreComplex.map {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) : AlgebraicTopology.NormalizedMooreComplex.obj X ⟶ AlgebraicTopology.NormalizedMooreComplex.obj Y

The normalized Moore complex functor, on morphisms.

Equations

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

@[simp]

theorem AlgebraicTopology.normalizedMooreComplex_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y), (AlgebraicTopology.normalizedMooreComplex C).toPrefunctor.map f = AlgebraicTopology.NormalizedMooreComplex.map f

@[simp]

theorem AlgebraicTopology.normalizedMooreComplex_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) : (AlgebraicTopology.normalizedMooreComplex C).toPrefunctor.obj X = AlgebraicTopology.NormalizedMooreComplex.obj X

def AlgebraicTopology.normalizedMooreComplex (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (ChainComplex C ℕ)

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.

theorem AlgebraicTopology.normalizedMooreComplex_objD {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : ((AlgebraicTopology.normalizedMooreComplex C).toPrefunctor.obj X).d (n + 1) n = AlgebraicTopology.NormalizedMooreComplex.objD X n