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 #

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.

source

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.obj (Opposite.op (SimplexCategory.mk n)))

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

Equations

AlgebraicTopology.NormalizedMooreComplex.objX X x = match x with | 0 => ⊤ | n.succ => Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)

Instances For

source

@[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 = ⊤

source

@[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.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)

source

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.obj (AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1)) ⟶ CategoryTheory.Subobject.underlying.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.

Instances For

source

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

source

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

source

@[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

source

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.

Instances For

source

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

source

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.

Instances For

source

@[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).map f = AlgebraicTopology.NormalizedMooreComplex.map f

source

@[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).obj X = AlgebraicTopology.NormalizedMooreComplex.obj X

source

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.

Instances For

source

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).obj X).d (n + 1) n = AlgebraicTopology.NormalizedMooreComplex.objD X n