algebraic_topology.Moore_complex

Moore complex #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We construct the normalized Moore complex, as a functor simplicial_object C ⥤ chain_complex 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 normalized_Moore_complex and should usually only be accessed via that.

source

@[simp]

noncomputable def algebraic_topology.normalized_Moore_complex.obj_X {C : Type u_1} [category_theory.category C] [category_theory.abelian C] (X : category_theory.simplicial_object C) (n : ℕ) :

category_theory.subobject (X.obj (opposite.op (simplex_category.mk n)))

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

Equations

algebraic_topology.normalized_Moore_complex.obj_X X (n + 1) = finset.univ.inf (λ (k : fin (n + 1)), category_theory.limits.kernel_subobject (X.δ k.succ))
algebraic_topology.normalized_Moore_complex.obj_X X 0 = ⊤

source

@[simp]

noncomputable def algebraic_topology.normalized_Moore_complex.obj_d {C : Type u_1} [category_theory.category C] [category_theory.abelian C] (X : category_theory.simplicial_object C) (n : ℕ) :

↑(algebraic_topology.normalized_Moore_complex.obj_X X (n + 1)) ⟶ ↑(algebraic_topology.normalized_Moore_complex.obj_X X n)

The differentials in the normalized Moore complex.

Equations

algebraic_topology.normalized_Moore_complex.obj_d X (n + 1) = (algebraic_topology.normalized_Moore_complex.obj_X X (n + 1)).factor_thru ((algebraic_topology.normalized_Moore_complex.obj_X X (n + 1 + 1)).arrow ≫ X.δ 0) _
algebraic_topology.normalized_Moore_complex.obj_d X 0 = (algebraic_topology.normalized_Moore_complex.obj_X X (0 + 1)).arrow ≫ X.δ 0 ≫ category_theory.inv ⊤.arrow

source

theorem algebraic_topology.normalized_Moore_complex.d_squared {C : Type u_1} [category_theory.category C] [category_theory.abelian C] (X : category_theory.simplicial_object C) (n : ℕ) :

algebraic_topology.normalized_Moore_complex.obj_d X (n + 1) ≫ algebraic_topology.normalized_Moore_complex.obj_d X n = 0

source

noncomputable def algebraic_topology.normalized_Moore_complex.obj {C : Type u_1} [category_theory.category C] [category_theory.abelian C] (X : category_theory.simplicial_object C) :

chain_complex C ℕ

The normalized Moore complex functor, on objects.

Equations

algebraic_topology.normalized_Moore_complex.obj X = chain_complex.of (λ (n : ℕ), ↑(algebraic_topology.normalized_Moore_complex.obj_X X n)) (algebraic_topology.normalized_Moore_complex.obj_d X) _

source

@[simp]

theorem algebraic_topology.normalized_Moore_complex.obj_X_2 {C : Type u_1} [category_theory.category C] [category_theory.abelian C] (X : category_theory.simplicial_object C) (n : ℕ) :

(algebraic_topology.normalized_Moore_complex.obj X).X n = ↑(algebraic_topology.normalized_Moore_complex.obj_X X n)

source

@[simp]

theorem algebraic_topology.normalized_Moore_complex.obj_d_2 {C : Type u_1} [category_theory.category C] [category_theory.abelian C] (X : category_theory.simplicial_object C) (i j : ℕ) :

(algebraic_topology.normalized_Moore_complex.obj X).d i j = dite (i = j + 1) (λ (h : i = j + 1), category_theory.eq_to_hom _ ≫ algebraic_topology.normalized_Moore_complex.obj_d X j) (λ (h : ¬i = j + 1), 0)

source

noncomputable def algebraic_topology.normalized_Moore_complex.map {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : category_theory.simplicial_object C} (f : X ⟶ Y) :

algebraic_topology.normalized_Moore_complex.obj X ⟶ algebraic_topology.normalized_Moore_complex.obj Y

The normalized Moore complex functor, on morphisms.

Equations

source

@[simp]

theorem algebraic_topology.normalized_Moore_complex.map_f {C : Type u_1} [category_theory.category C] [category_theory.abelian C] {X Y : category_theory.simplicial_object C} (f : X ⟶ Y) (n : ℕ) :

(algebraic_topology.normalized_Moore_complex.map f).f n = (algebraic_topology.normalized_Moore_complex.obj_X Y n).factor_thru ((algebraic_topology.normalized_Moore_complex.obj_X X n).arrow ≫ f.app (opposite.op (simplex_category.mk n))) _

source

@[simp]

theorem algebraic_topology.normalized_Moore_complex_obj (C : Type u_1) [category_theory.category C] [category_theory.abelian C] (X : category_theory.simplicial_object C) :

(algebraic_topology.normalized_Moore_complex C).obj X = algebraic_topology.normalized_Moore_complex.obj X

source

@[simp]

theorem algebraic_topology.normalized_Moore_complex_map (C : Type u_1) [category_theory.category C] [category_theory.abelian C] (X Y : category_theory.simplicial_object C) (f : X ⟶ Y) :

(algebraic_topology.normalized_Moore_complex C).map f = algebraic_topology.normalized_Moore_complex.map f

source

noncomputable def algebraic_topology.normalized_Moore_complex (C : Type u_1) [category_theory.category C] [category_theory.abelian C] :

category_theory.simplicial_object C ⥤ chain_complex 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

algebraic_topology.normalized_Moore_complex C = {obj := algebraic_topology.normalized_Moore_complex.obj _inst_2, map := λ (X Y : category_theory.simplicial_object C) (f : X ⟶ Y), algebraic_topology.normalized_Moore_complex.map f, map_id' := _, map_comp' := _}

source

@[simp]

theorem algebraic_topology.normalized_Moore_complex_obj_d {C : Type u_1} [category_theory.category C] [category_theory.abelian C] (X : category_theory.simplicial_object C) (n : ℕ) :

((algebraic_topology.normalized_Moore_complex C).obj X).d (n + 1) n = algebraic_topology.normalized_Moore_complex.obj_d X n