mathlib3 documentation

algebra.homology.augment

Augmentation and truncation of ℕ-indexed (co)chain complexes. #

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

source
@[simp]
theorem chain_complex.truncate_obj_X {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) (i : ℕ) :
(chain_complex.truncate.obj C).X i = C.X (i + 1)
source
@[simp]
theorem chain_complex.truncate_obj_d {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) (i j : ℕ) :
(chain_complex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
source
@[simp]
theorem chain_complex.truncate_map_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C D : chain_complex V ℕ) (f : C ⟶ D) (i : ℕ) :
(chain_complex.truncate.map f).f i = f.f (i + 1)
source
def chain_complex.truncate {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] :
chain_complex V ℕ ⥤ chain_complex V ℕ

The truncation of a ℕ-indexed chain complex, deleting the object at 0 and shifting everything else down.

Equations
source
noncomputable def chain_complex.truncate_to {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_object V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) :
chain_complex.truncate.obj C ⟶ (chain_complex.single₀ V).obj (C.X 0)

There is a canonical chain map from the truncation of a chain map C to the "single object" chain complex consisting of the truncated object C.X 0 in degree 0. The components of this chain map are C.d 1 0 in degree 0, and zero otherwise.

Equations
source
def chain_complex.augment {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) :
chain_complex V ℕ

We can "augment" a chain complex by inserting an arbitrary object in degree zero (shifting everything else up), along with a suitable differential.

Equations
  • C.augment f w = {X := λ (i : ℕ), chain_complex.augment._match_1 C i, d := λ (i j : ℕ), chain_complex.augment._match_2 C f i j, shape' := _, d_comp_d' := _}
  • chain_complex.augment._match_1 C (i + 1) = C.X i
  • chain_complex.augment._match_1 C 0 = X
  • chain_complex.augment._match_2 C f (n.succ + 1) (j + 1) = C.d n.succ j
  • chain_complex.augment._match_2 C f n.succ.succ 0 = 0
  • chain_complex.augment._match_2 C f (0 + 1) (j + 1) = C.d 0 j
  • chain_complex.augment._match_2 C f 1 0 = f
  • chain_complex.augment._match_2 C f 0 _x = 0
source
@[simp]
theorem chain_complex.augment_X_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) :
(C.augment f w).X 0 = X
source
@[simp]
theorem chain_complex.augment_X_succ {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) (i : ℕ) :
(C.augment f w).X (i + 1) = C.X i
source
@[simp]
theorem chain_complex.augment_d_one_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) :
(C.augment f w).d 1 0 = f
source
@[simp]
theorem chain_complex.augment_d_succ_succ {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) (i j : ℕ) :
(C.augment f w).d (i + 1) (j + 1) = C.d i j
source
def chain_complex.truncate_augment {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) :
chain_complex.truncate.obj (C.augment f w) ≅ C

Truncating an augmented chain complex is isomorphic (with components the identity) to the original complex.

Equations
source
@[simp]
theorem chain_complex.truncate_augment_hom_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) (i : ℕ) :
(C.truncate_augment f w).hom.f i = 𝟙 (C.X i)
source
@[simp]
theorem chain_complex.truncate_augment_inv_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) (i : ℕ) :
(C.truncate_augment f w).inv.f i = 𝟙 ((chain_complex.truncate.obj (C.augment f w)).X i)
source
@[simp]
theorem chain_complex.chain_complex_d_succ_succ_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) (i : ℕ) :
C.d (i + 2) 0 = 0
source
def chain_complex.augment_truncate {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) :
(chain_complex.truncate.obj C).augment (C.d 1 0) _ ≅ C

Augmenting a truncated complex with the original object and morphism is isomorphic (with components the identity) to the original complex.

Equations
source
@[simp]
theorem chain_complex.augment_truncate_hom_f_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) :
C.augment_truncate.hom.f 0 = 𝟙 (C.X 0)
source
@[simp]
theorem chain_complex.augment_truncate_hom_f_succ {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) (i : ℕ) :
C.augment_truncate.hom.f (i + 1) = 𝟙 (C.X (i + 1))
source
@[simp]
theorem chain_complex.augment_truncate_inv_f_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) :
C.augment_truncate.inv.f 0 = 𝟙 (C.X 0)
source
@[simp]
theorem chain_complex.augment_truncate_inv_f_succ {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : chain_complex V ℕ) (i : ℕ) :
C.augment_truncate.inv.f (i + 1) = 𝟙 (C.X (i + 1))
source
noncomputable def chain_complex.to_single₀_as_complex {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_zero_object V] (C : chain_complex V ℕ) (X : V) (f : C ⟶ (chain_complex.single₀ V).obj X) :
chain_complex V ℕ

A chain map from a chain complex to a single object chain complex in degree zero can be reinterpreted as a chain complex.

Ths is the inverse construction of truncate_to.

Equations
source
@[simp]
theorem cochain_complex.truncate_obj_d {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) (i j : ℕ) :
(cochain_complex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
source
def cochain_complex.truncate {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] :
cochain_complex V ℕ ⥤ cochain_complex V ℕ

The truncation of a ℕ-indexed cochain complex, deleting the object at 0 and shifting everything else down.

Equations
source
@[simp]
theorem cochain_complex.truncate_map_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C D : cochain_complex V ℕ) (f : C ⟶ D) (i : ℕ) :
(cochain_complex.truncate.map f).f i = f.f (i + 1)
source
@[simp]
theorem cochain_complex.truncate_obj_X {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) (i : ℕ) :
(cochain_complex.truncate.obj C).X i = C.X (i + 1)
source
noncomputable def cochain_complex.to_truncate {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_object V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) :
(cochain_complex.single₀ V).obj (C.X 0) ⟶ cochain_complex.truncate.obj C

There is a canonical chain map from the truncation of a cochain complex C to the "single object" cochain complex consisting of the truncated object C.X 0 in degree 0. The components of this chain map are C.d 0 1 in degree 0, and zero otherwise.

Equations
source
def cochain_complex.augment {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
cochain_complex V ℕ

We can "augment" a cochain complex by inserting an arbitrary object in degree zero (shifting everything else up), along with a suitable differential.

Equations
  • C.augment f w = {X := λ (i : ℕ), cochain_complex.augment._match_1 C i, d := λ (i j : ℕ), cochain_complex.augment._match_2 C f i j, shape' := _, d_comp_d' := _}
  • cochain_complex.augment._match_1 C (i + 1) = C.X i
  • cochain_complex.augment._match_1 C 0 = X
  • cochain_complex.augment._match_2 C f (i + 1) (j + 1) = C.d i j
  • cochain_complex.augment._match_2 C f n.succ 0 = 0
  • cochain_complex.augment._match_2 C f 0 n.succ.succ = 0
  • cochain_complex.augment._match_2 C f 0 1 = f
  • cochain_complex.augment._match_2 C f 0 0 = 0
source
@[simp]
theorem cochain_complex.augment_X_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
(C.augment f w).X 0 = X
source
@[simp]
theorem cochain_complex.augment_X_succ {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i : ℕ) :
(C.augment f w).X (i + 1) = C.X i
source
@[simp]
theorem cochain_complex.augment_d_zero_one {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
(C.augment f w).d 0 1 = f
source
@[simp]
theorem cochain_complex.augment_d_succ_succ {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i j : ℕ) :
(C.augment f w).d (i + 1) (j + 1) = C.d i j
source
def cochain_complex.truncate_augment {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
cochain_complex.truncate.obj (C.augment f w) ≅ C

Truncating an augmented cochain complex is isomorphic (with components the identity) to the original complex.

Equations
source
@[simp]
theorem cochain_complex.truncate_augment_hom_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i : ℕ) :
(C.truncate_augment f w).hom.f i = 𝟙 (C.X i)
source
@[simp]
theorem cochain_complex.truncate_augment_inv_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i : ℕ) :
(C.truncate_augment f w).inv.f i = 𝟙 ((cochain_complex.truncate.obj (C.augment f w)).X i)
source
@[simp]
theorem cochain_complex.cochain_complex_d_succ_succ_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) (i : ℕ) :
C.d 0 (i + 2) = 0
source
def cochain_complex.augment_truncate {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) :
(cochain_complex.truncate.obj C).augment (C.d 0 1) _ ≅ C

Augmenting a truncated complex with the original object and morphism is isomorphic (with components the identity) to the original complex.

Equations
source
@[simp]
theorem cochain_complex.augment_truncate_hom_f_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) :
C.augment_truncate.hom.f 0 = 𝟙 (C.X 0)
source
@[simp]
theorem cochain_complex.augment_truncate_hom_f_succ {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) (i : ℕ) :
C.augment_truncate.hom.f (i + 1) = 𝟙 (C.X (i + 1))
source
@[simp]
theorem cochain_complex.augment_truncate_inv_f_zero {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) :
C.augment_truncate.inv.f 0 = 𝟙 (C.X 0)
source
@[simp]
theorem cochain_complex.augment_truncate_inv_f_succ {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (C : cochain_complex V ℕ) (i : ℕ) :
C.augment_truncate.inv.f (i + 1) = 𝟙 (C.X (i + 1))
source
noncomputable def cochain_complex.from_single₀_as_complex {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_zero_object V] (C : cochain_complex V ℕ) (X : V) (f : (cochain_complex.single₀ V).obj X ⟶ C) :
cochain_complex V ℕ

A chain map from a single object cochain complex in degree zero to a cochain complex can be reinterpreted as a cochain complex.

Ths is the inverse construction of to_truncate.

Equations