mathlib3 documentation

algebraic_topology.alternating_face_map_complex

The alternating face map complex of a simplicial object in a preadditive category #

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

We construct the alternating face map complex, as a functor alternating_face_map_complex : simplicial_object C ⥤ chain_complex C ℕ for any preadditive category C. For any simplicial object X in C, this is the homological complex ... → X_2 → X_1 → X_0 where the differentials are alternating sums of faces.

The dual version alternating_coface_map_complex : cosimplicial_object C ⥤ cochain_complex C ℕ is also constructed.

We also construct the natural transformation inclusion_of_Moore_complex : normalized_Moore_complex A ⟶ alternating_face_map_complex A when A is an abelian category.

References #

Construction of the alternating face map complex #

@[simp]

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

X.obj (opposite.op (simplex_category.mk (n + 1))) ⟶ X.obj (opposite.op (simplex_category.mk n))

The differential on the alternating face map complex is the alternate sum of the face maps

Equations

algebraic_topology.alternating_face_map_complex.obj_d X n = finset.univ.sum (λ (i : fin (n + 2)), (-1) ^ ↑i • X.δ i)

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

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

The chain complex relation `d ≫ d` #

Construction of the alternating face map complex functor #

def algebraic_topology.alternating_face_map_complex.obj {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X : category_theory.simplicial_object C) :

chain_complex C ℕ

The alternating face map complex, on objects

Equations

algebraic_topology.alternating_face_map_complex.obj X = chain_complex.of (λ (n : ℕ), X.obj (opposite.op (simplex_category.mk n))) (algebraic_topology.alternating_face_map_complex.obj_d X) _

@[simp]

theorem algebraic_topology.alternating_face_map_complex.obj_X {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X : category_theory.simplicial_object C) (n : ℕ) :

(algebraic_topology.alternating_face_map_complex.obj X).X n = X.obj (opposite.op (simplex_category.mk n))

@[simp]

theorem algebraic_topology.alternating_face_map_complex.obj_d_eq {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X : category_theory.simplicial_object C) (n : ℕ) :

(algebraic_topology.alternating_face_map_complex.obj X).d (n + 1) n = finset.univ.sum (λ (i : fin (n + 2)), (-1) ^ ↑i • X.δ i)

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

algebraic_topology.alternating_face_map_complex.obj X ⟶ algebraic_topology.alternating_face_map_complex.obj Y

The alternating face map complex, on morphisms

Equations

algebraic_topology.alternating_face_map_complex.map f = chain_complex.of_hom (λ (n : ℕ), X.obj (opposite.op (simplex_category.mk n))) (algebraic_topology.alternating_face_map_complex.obj_d X) _ (λ (n : ℕ), Y.obj (opposite.op (simplex_category.mk n))) (algebraic_topology.alternating_face_map_complex.obj_d Y) _ (λ (n : ℕ), f.app (opposite.op (simplex_category.mk n))) _

@[simp]

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

(algebraic_topology.alternating_face_map_complex.map f).f n = f.app (opposite.op (simplex_category.mk n))

def algebraic_topology.alternating_face_map_complex (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] :

category_theory.simplicial_object C ⥤ chain_complex C ℕ

The alternating face map complex, as a functor

Equations

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

@[simp]

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

((algebraic_topology.alternating_face_map_complex C).obj X).X n = X.obj (opposite.op (simplex_category.mk n))

@[simp]

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

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

@[simp]

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

((algebraic_topology.alternating_face_map_complex C).map f).f n = f.app (opposite.op (simplex_category.mk n))

theorem algebraic_topology.map_alternating_face_map_complex {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {D : Type u_3} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.additive] :

algebraic_topology.alternating_face_map_complex C ⋙ F.map_homological_complex (complex_shape.down ℕ) = (category_theory.simplicial_object.whiskering C D).obj F ⋙ algebraic_topology.alternating_face_map_complex D

theorem algebraic_topology.karoubi_alternating_face_map_complex_d {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (P : category_theory.idempotents.karoubi (category_theory.simplicial_object C)) (n : ℕ) :

((algebraic_topology.alternating_face_map_complex.obj (category_theory.idempotents.karoubi_functor_category_embedding.obj P)).d (n + 1) n).f = P.p.app (opposite.op (simplex_category.mk (n + 1))) ≫ (algebraic_topology.alternating_face_map_complex.obj P.X).d (n + 1) n

noncomputable def algebraic_topology.alternating_face_map_complex.ε {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] :

category_theory.simplicial_object.augmented.drop ⋙ algebraic_topology.alternating_face_map_complex C ⟶ category_theory.simplicial_object.augmented.point ⋙ chain_complex.single₀ C

The natural transformation which gives the augmentation of the alternating face map complex attached to an augmented simplicial object.

Equations

algebraic_topology.alternating_face_map_complex.ε = {app := λ (X : category_theory.simplicial_object.augmented C), (((category_theory.simplicial_object.augmented.drop ⋙ algebraic_topology.alternating_face_map_complex C).obj X).to_single₀_equiv (category_theory.simplicial_object.augmented.point.obj X)).inv_fun ⟨X.hom.app (opposite.op (simplex_category.mk 0)), _⟩, naturality' := _}

Construction of the natural inclusion of the normalized Moore complex #

noncomputable def algebraic_topology.inclusion_of_Moore_complex_map {A : Type u_3} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) :

(algebraic_topology.normalized_Moore_complex A).obj X ⟶ (algebraic_topology.alternating_face_map_complex A).obj X

The inclusion map of the Moore complex in the alternating face map complex

Equations

algebraic_topology.inclusion_of_Moore_complex_map X = chain_complex.of_hom (λ (n : ℕ), ↑(algebraic_topology.normalized_Moore_complex.obj_X X n)) (λ (j : ℕ), algebraic_topology.normalized_Moore_complex.obj_d X j) _ (λ (n : ℕ), X.obj (opposite.op (simplex_category.mk n))) (λ (j : ℕ), algebraic_topology.alternating_face_map_complex.obj_d X j) _ (λ (n : ℕ), (algebraic_topology.normalized_Moore_complex.obj_X X n).arrow) _

Instances for algebraic_topology.inclusion_of_Moore_complex_map

algebraic_topology.dold_kan.algebraic_topology.inclusion_of_Moore_complex_map.category_theory.mono

@[simp]

theorem algebraic_topology.inclusion_of_Moore_complex_map_f {A : Type u_3} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) (n : ℕ) :

(algebraic_topology.inclusion_of_Moore_complex_map X).f n = (algebraic_topology.normalized_Moore_complex.obj_X X n).arrow

noncomputable def algebraic_topology.inclusion_of_Moore_complex (A : Type u_3) [category_theory.category A] [category_theory.abelian A] :

algebraic_topology.normalized_Moore_complex A ⟶ algebraic_topology.alternating_face_map_complex A

The inclusion map of the Moore complex in the alternating face map complex, as a natural transformation

Equations

algebraic_topology.inclusion_of_Moore_complex A = {app := algebraic_topology.inclusion_of_Moore_complex_map _inst_4, naturality' := _}

@[simp]

theorem algebraic_topology.inclusion_of_Moore_complex_app (A : Type u_3) [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) :

(algebraic_topology.inclusion_of_Moore_complex A).app X = algebraic_topology.inclusion_of_Moore_complex_map X

@[simp]

def algebraic_topology.alternating_coface_map_complex.obj_d {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X : category_theory.cosimplicial_object C) (n : ℕ) :

X.obj (simplex_category.mk n) ⟶ X.obj (simplex_category.mk (n + 1))

The differential on the alternating coface map complex is the alternate sum of the coface maps

Equations

algebraic_topology.alternating_coface_map_complex.obj_d X n = finset.univ.sum (λ (i : fin (n + 2)), (-1) ^ ↑i • X.δ i)

theorem algebraic_topology.alternating_coface_map_complex.d_eq_unop_d {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X : category_theory.cosimplicial_object C) (n : ℕ) :

algebraic_topology.alternating_coface_map_complex.obj_d X n = (algebraic_topology.alternating_face_map_complex.obj_d ((category_theory.cosimplicial_simplicial_equiv C).functor.obj (opposite.op X)) n).unop

theorem algebraic_topology.alternating_coface_map_complex.d_squared {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X : category_theory.cosimplicial_object C) (n : ℕ) :

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

def algebraic_topology.alternating_coface_map_complex.obj {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X : category_theory.cosimplicial_object C) :

cochain_complex C ℕ

The alternating coface map complex, on objects

Equations

algebraic_topology.alternating_coface_map_complex.obj X = cochain_complex.of (λ (n : ℕ), X.obj (simplex_category.mk n)) (algebraic_topology.alternating_coface_map_complex.obj_d X) _

@[simp]

def algebraic_topology.alternating_coface_map_complex.map {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {X Y : category_theory.cosimplicial_object C} (f : X ⟶ Y) :

algebraic_topology.alternating_coface_map_complex.obj X ⟶ algebraic_topology.alternating_coface_map_complex.obj Y

The alternating face map complex, on morphisms

Equations

algebraic_topology.alternating_coface_map_complex.map f = cochain_complex.of_hom (λ (n : ℕ), X.obj (simplex_category.mk n)) (algebraic_topology.alternating_coface_map_complex.obj_d X) _ (λ (n : ℕ), Y.obj (simplex_category.mk n)) (algebraic_topology.alternating_coface_map_complex.obj_d Y) _ (λ (n : ℕ), f.app (simplex_category.mk n)) _

@[simp]

theorem algebraic_topology.alternating_coface_map_complex_obj (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (X : category_theory.cosimplicial_object C) :

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

def algebraic_topology.alternating_coface_map_complex (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] :

category_theory.cosimplicial_object C ⥤ cochain_complex C ℕ

The alternating coface map complex, as a functor

Equations

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

@[simp]

theorem algebraic_topology.alternating_coface_map_complex_map (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (X Y : category_theory.cosimplicial_object C) (f : X ⟶ Y) :

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