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.

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.inf Finset.univ fun k => CategoryTheory.Limits.kernelSubobject (CategoryTheory.SimplicialObject.δ X (Fin.succ k))

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.

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 : ℕ) :

HomologicalComplex.X (AlgebraicTopology.NormalizedMooreComplex.obj 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 : ℕ) :

HomologicalComplex.d (AlgebraicTopology.NormalizedMooreComplex.obj X) i j = if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Subobject.underlying.obj (AlgebraicTopology.NormalizedMooreComplex.objX X i) = CategoryTheory.Subobject.underlying.obj (AlgebraicTopology.NormalizedMooreComplex.objX X (j + 1)))) (match j with | 0 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (Finset.inf Finset.univ fun k => 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 => CategoryTheory.Limits.kernelSubobject (CategoryTheory.SimplicialObject.δ X (Fin.succ k))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (Finset.inf Finset.univ fun k => CategoryTheory.Limits.kernelSubobject (CategoryTheory.SimplicialObject.δ X (Fin.succ k)))) (CategoryTheory.SimplicialObject.δ X 0)) (_ : CategoryTheory.Subobject.Factors (Finset.inf Finset.univ fun k => 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

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.

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 : ℕ) :

HomologicalComplex.Hom.f (AlgebraicTopology.NormalizedMooreComplex.map 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)))))

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.

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.

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 : ℕ) :

HomologicalComplex.d ((AlgebraicTopology.normalizedMooreComplex C).obj X) (n + 1) n = AlgebraicTopology.NormalizedMooreComplex.objD X n