algebra.homology.additive

@[protected, instance]

def homological_complex.quiver.hom.has_zero {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} :

has_zero (C ⟶ D)

Equations

homological_complex.quiver.hom.has_zero = {zero := {f := λ (i : ι), 0, comm' := _}}

source

@[protected, instance]

def homological_complex.quiver.hom.has_add {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} :

has_add (C ⟶ D)

Equations

homological_complex.quiver.hom.has_add = {add := λ (f g : C ⟶ D), {f := λ (i : ι), f.f i + g.f i, comm' := _}}

source

@[protected, instance]

def homological_complex.quiver.hom.has_neg {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} :

has_neg (C ⟶ D)

Equations

homological_complex.quiver.hom.has_neg = {neg := λ (f : C ⟶ D), {f := λ (i : ι), -f.f i, comm' := _}}

source

@[protected, instance]

def homological_complex.quiver.hom.has_sub {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} :

has_sub (C ⟶ D)

Equations

homological_complex.quiver.hom.has_sub = {sub := λ (f g : C ⟶ D), {f := λ (i : ι), f.f i - g.f i, comm' := _}}

source

@[protected, instance]

def homological_complex.has_nat_scalar {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} :

has_smul ℕ (C ⟶ D)

Equations

homological_complex.has_nat_scalar = {smul := λ (n : ℕ) (f : C ⟶ D), {f := λ (i : ι), n • f.f i, comm' := _}}

source

@[protected, instance]

def homological_complex.has_int_scalar {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} :

has_smul ℤ (C ⟶ D)

Equations

homological_complex.has_int_scalar = {smul := λ (n : ℤ) (f : C ⟶ D), {f := λ (i : ι), n • f.f i, comm' := _}}

source

@[simp]

theorem homological_complex.zero_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (i : ι) :

0.f i = 0

source

@[simp]

theorem homological_complex.add_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f g : C ⟶ D) (i : ι) :

(f + g).f i = f.f i + g.f i

source

@[simp]

theorem homological_complex.neg_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : C ⟶ D) (i : ι) :

(-f).f i = -f.f i

source

@[simp]

theorem homological_complex.sub_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f g : C ⟶ D) (i : ι) :

(f - g).f i = f.f i - g.f i

source

@[simp]

theorem homological_complex.nsmul_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (n : ℕ) (f : C ⟶ D) (i : ι) :

(n • f).f i = n • f.f i

source

@[simp]

theorem homological_complex.zsmul_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (n : ℤ) (f : C ⟶ D) (i : ι) :

(n • f).f i = n • f.f i

source

@[protected, instance]

def homological_complex.quiver.hom.add_comm_group {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} :

add_comm_group (C ⟶ D)

Equations

homological_complex.quiver.hom.add_comm_group = function.injective.add_comm_group homological_complex.hom.f homological_complex.quiver.hom.add_comm_group._proof_1 homological_complex.quiver.hom.add_comm_group._proof_2 homological_complex.quiver.hom.add_comm_group._proof_3 homological_complex.quiver.hom.add_comm_group._proof_4 homological_complex.quiver.hom.add_comm_group._proof_5 homological_complex.quiver.hom.add_comm_group._proof_6 homological_complex.quiver.hom.add_comm_group._proof_7

source

@[protected, instance]

def homological_complex.category_theory.preadditive {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} :

category_theory.preadditive (homological_complex V c)

Equations

homological_complex.category_theory.preadditive = {hom_group := λ (P Q : homological_complex V c), homological_complex.quiver.hom.add_comm_group, add_comp' := _, comp_add' := _}

source

def homological_complex.hom.f_add_monoid_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C₁ C₂ : homological_complex V c} (i : ι) :

(C₁ ⟶ C₂) →+ (C₁.X i ⟶ C₂.X i)

The i-th component of a chain map, as an additive map from chain maps to morphisms.

Equations

homological_complex.hom.f_add_monoid_hom i = add_monoid_hom.mk' (λ (f : C₁ ⟶ C₂), f.f i) _

source

@[simp]

theorem homological_complex.hom.f_add_monoid_hom_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C₁ C₂ : homological_complex V c} (i : ι) (f : C₁ ⟶ C₂) :

⇑(homological_complex.hom.f_add_monoid_hom i) f = f.f i

source

@[protected, instance]

def homological_complex.eval_additive {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} (i : ι) :

(homological_complex.eval V c i).additive

source

@[protected, instance]

def homological_complex.cycles_additive {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} (i : ι) [category_theory.limits.has_equalizers V] :

(cycles_functor V c i).additive

source

@[protected, instance]

def homological_complex.boundaries_additive {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} (i : ι) [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] :

(boundaries_functor V c i).additive

source

@[protected, instance]

def homological_complex.homology_additive {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} (i : ι) [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] [category_theory.limits.has_equalizers V] [category_theory.limits.has_cokernels V] :

(homology_functor V c i).additive

source

@[simp]

theorem category_theory.functor.map_homological_complex_map_f {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V ⥤ W) [F.additive] (c : complex_shape ι) (C D : homological_complex V c) (f : C ⟶ D) (i : ι) :

((F.map_homological_complex c).map f).f i = F.map (f.f i)

source

def category_theory.functor.map_homological_complex {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V ⥤ W) [F.additive] (c : complex_shape ι) :

homological_complex V c ⥤ homological_complex W c

An additive functor induces a functor between homological complexes. This is sometimes called the "prolongation".

Equations

F.map_homological_complex c = {obj := λ (C : homological_complex V c), {X := λ (i : ι), F.obj (C.X i), d := λ (i j : ι), F.map (C.d i j), shape' := _, d_comp_d' := _}, map := λ (C D : homological_complex V c) (f : C ⟶ D), {f := λ (i : ι), F.map (f.f i), comm' := _}, map_id' := _, map_comp' := _}

Instances for category_theory.functor.map_homological_complex

source

@[simp]

theorem category_theory.functor.map_homological_complex_obj_X {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V ⥤ W) [F.additive] (c : complex_shape ι) (C : homological_complex V c) (i : ι) :

((F.map_homological_complex c).obj C).X i = F.obj (C.X i)

source

@[simp]

theorem category_theory.functor.map_homological_complex_obj_d {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V ⥤ W) [F.additive] (c : complex_shape ι) (C : homological_complex V c) (i j : ι) :

((F.map_homological_complex c).obj C).d i j = F.map (C.d i j)

source

@[simp]

theorem category_theory.functor.map_homological_complex_id_iso_hom_app_f {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) (X : homological_complex V c) (i : ι) :

((category_theory.functor.map_homological_complex_id_iso V c).hom.app X).f i = 𝟙 (X.X i)

source

@[simp]

theorem category_theory.functor.map_homological_complex_id_iso_inv_app_f {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) (X : homological_complex V c) (i : ι) :

((category_theory.functor.map_homological_complex_id_iso V c).inv.app X).f i = 𝟙 (X.X i)

source

def category_theory.functor.map_homological_complex_id_iso {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) :

(𝟭 V).map_homological_complex c ≅ 𝟭 (homological_complex V c)

The functor on homological complexes induced by the identity functor is isomorphic to the identity functor.

Equations

category_theory.functor.map_homological_complex_id_iso V c = category_theory.nat_iso.of_components (λ (K : homological_complex V c), homological_complex.hom.iso_of_components (λ (i : ι), category_theory.iso.refl ((((𝟭 V).map_homological_complex c).obj K).X i)) _) _

source

@[protected, instance]

def category_theory.functor.map_homogical_complex_additive {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V ⥤ W) [F.additive] (c : complex_shape ι) :

(F.map_homological_complex c).additive

source

@[protected, instance]

def category_theory.functor.map_homological_complex_reflects_iso {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V ⥤ W) [F.additive] [category_theory.reflects_isomorphisms F] (c : complex_shape ι) :

category_theory.reflects_isomorphisms (F.map_homological_complex c)

source

def category_theory.nat_trans.map_homological_complex {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {F G : V ⥤ W} [F.additive] [G.additive] (α : F ⟶ G) (c : complex_shape ι) :

F.map_homological_complex c ⟶ G.map_homological_complex c

A natural transformation between functors induces a natural transformation between those functors applied to homological complexes.

Equations

category_theory.nat_trans.map_homological_complex α c = {app := λ (C : homological_complex V c), {f := λ (i : ι), α.app (C.X i), comm' := _}, naturality' := _}

source

@[simp]

theorem category_theory.nat_trans.map_homological_complex_app_f {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {F G : V ⥤ W} [F.additive] [G.additive] (α : F ⟶ G) (c : complex_shape ι) (C : homological_complex V c) (i : ι) :

((category_theory.nat_trans.map_homological_complex α c).app C).f i = α.app (C.X i)

source

@[simp]

theorem category_theory.nat_trans.map_homological_complex_id {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (c : complex_shape ι) (F : V ⥤ W) [F.additive] :

category_theory.nat_trans.map_homological_complex (𝟙 F) c = 𝟙 (F.map_homological_complex c)

source

@[simp]

theorem category_theory.nat_trans.map_homological_complex_comp {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (c : complex_shape ι) {F G H : V ⥤ W} [F.additive] [G.additive] [H.additive] (α : F ⟶ G) (β : G ⟶ H) :

category_theory.nat_trans.map_homological_complex (α ≫ β) c = category_theory.nat_trans.map_homological_complex α c ≫ category_theory.nat_trans.map_homological_complex β c

source

@[simp]

theorem category_theory.nat_trans.map_homological_complex_naturality {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {c : complex_shape ι} {F G : V ⥤ W} [F.additive] [G.additive] (α : F ⟶ G) {C D : homological_complex V c} (f : C ⟶ D) :

(F.map_homological_complex c).map f ≫ (category_theory.nat_trans.map_homological_complex α c).app D = (category_theory.nat_trans.map_homological_complex α c).app C ≫ (G.map_homological_complex c).map f

source

@[simp]

theorem category_theory.nat_trans.map_homological_complex_naturality_assoc {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {c : complex_shape ι} {F G : V ⥤ W} [F.additive] [G.additive] (α : F ⟶ G) {C D : homological_complex V c} (f : C ⟶ D) {X' : homological_complex W c} (f' : (G.map_homological_complex c).obj D ⟶ X') :

(F.map_homological_complex c).map f ≫ (category_theory.nat_trans.map_homological_complex α c).app D ≫ f' = (category_theory.nat_trans.map_homological_complex α c).app C ≫ (G.map_homological_complex c).map f ≫ f'

source

def category_theory.nat_iso.map_homological_complex {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {F G : V ⥤ W} [F.additive] [G.additive] (α : F ≅ G) (c : complex_shape ι) :

F.map_homological_complex c ≅ G.map_homological_complex c

A natural isomorphism between functors induces a natural isomorphism between those functors applied to homological complexes.

Equations

category_theory.nat_iso.map_homological_complex α c = {hom := category_theory.nat_trans.map_homological_complex α.hom c, inv := category_theory.nat_trans.map_homological_complex α.inv c, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.nat_iso.map_homological_complex_inv {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {F G : V ⥤ W} [F.additive] [G.additive] (α : F ≅ G) (c : complex_shape ι) :

(category_theory.nat_iso.map_homological_complex α c).inv = category_theory.nat_trans.map_homological_complex α.inv c

source

@[simp]

theorem category_theory.nat_iso.map_homological_complex_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {F G : V ⥤ W} [F.additive] [G.additive] (α : F ≅ G) (c : complex_shape ι) :

(category_theory.nat_iso.map_homological_complex α c).hom = category_theory.nat_trans.map_homological_complex α.hom c

source

@[simp]

theorem category_theory.equivalence.map_homological_complex_unit_iso {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (e : V ≌ W) [e.functor.additive] (c : complex_shape ι) :

(e.map_homological_complex c).unit_iso = (category_theory.functor.map_homological_complex_id_iso V c).symm ≪≫ category_theory.nat_iso.map_homological_complex e.unit_iso c

source

@[simp]

theorem category_theory.equivalence.map_homological_complex_counit_iso {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (e : V ≌ W) [e.functor.additive] (c : complex_shape ι) :

(e.map_homological_complex c).counit_iso = category_theory.nat_iso.map_homological_complex e.counit_iso c ≪≫ category_theory.functor.map_homological_complex_id_iso W c

source

@[simp]

theorem category_theory.equivalence.map_homological_complex_functor {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (e : V ≌ W) [e.functor.additive] (c : complex_shape ι) :

(e.map_homological_complex c).functor = e.functor.map_homological_complex c

source

def category_theory.equivalence.map_homological_complex {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (e : V ≌ W) [e.functor.additive] (c : complex_shape ι) :

homological_complex V c ≌ homological_complex W c

An equivalence of categories induces an equivalences between the respective categories of homological complex.

Equations

source

@[simp]

theorem category_theory.equivalence.map_homological_complex_inverse {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (e : V ≌ W) [e.functor.additive] (c : complex_shape ι) :

(e.map_homological_complex c).inverse = e.inverse.map_homological_complex c

source

theorem chain_complex.map_chain_complex_of {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {α : Type u_4} [add_right_cancel_semigroup α] [has_one α] [decidable_eq α] (F : V ⥤ W) [F.additive] (X : α → V) (d : Π (n : α), X (n + 1) ⟶ X n) (sq : ∀ (n : α), d (n + 1) ≫ d n = 0) :

(F.map_homological_complex (complex_shape.down α)).obj (chain_complex.of X d sq) = chain_complex.of (λ (n : α), F.obj (X n)) (λ (n : α), F.map (d n)) _

source

noncomputable def homological_complex.single_map_homological_complex {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (c : complex_shape ι) (j : ι) :

homological_complex.single V c j ⋙ F.map_homological_complex c ≅ F ⋙ homological_complex.single W c j

Turning an object into a complex supported at j then applying a functor is the same as applying the functor then forming the complex.

Equations

homological_complex.single_map_homological_complex F c j = category_theory.nat_iso.of_components (λ (X : V), {hom := {f := λ (i : ι), dite (i = j) (λ (h : i = j), category_theory.eq_to_hom _) (λ (h : ¬i = j), 0), comm' := _}, inv := {f := λ (i : ι), dite (i = j) (λ (h : i = j), category_theory.eq_to_hom _) (λ (h : ¬i = j), 0), comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _

source

@[simp]

theorem homological_complex.single_map_homological_complex_hom_app_self {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (j : ι) (X : V) :

((homological_complex.single_map_homological_complex F c j).hom.app X).f j = category_theory.eq_to_hom _

source

@[simp]

theorem homological_complex.single_map_homological_complex_hom_app_ne {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] {i j : ι} (h : i ≠ j) (X : V) :

((homological_complex.single_map_homological_complex F c j).hom.app X).f i = 0

source

@[simp]

theorem homological_complex.single_map_homological_complex_inv_app_self {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (j : ι) (X : V) :

((homological_complex.single_map_homological_complex F c j).inv.app X).f j = category_theory.eq_to_hom _

source

@[simp]

theorem homological_complex.single_map_homological_complex_inv_app_ne {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] {i j : ι} (h : i ≠ j) (X : V) :

((homological_complex.single_map_homological_complex F c j).inv.app X).f i = 0

source

noncomputable def chain_complex.single₀_map_homological_complex {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] :

chain_complex.single₀ V ⋙ F.map_homological_complex (complex_shape.down ℕ) ≅ F ⋙ chain_complex.single₀ W

Turning an object into a chain complex supported at zero then applying a functor is the same as applying the functor then forming the complex.

Equations

chain_complex.single₀_map_homological_complex F = category_theory.nat_iso.of_components (λ (X : V), {hom := {f := λ (i : ℕ), chain_complex.single₀_map_homological_complex._match_1 F X i, comm' := _}, inv := {f := λ (i : ℕ), chain_complex.single₀_map_homological_complex._match_2 F X i, comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
chain_complex.single₀_map_homological_complex._match_1 F X (i + 1) = F.map_zero_object.hom
chain_complex.single₀_map_homological_complex._match_1 F X 0 = 𝟙 (((chain_complex.single₀ V ⋙ F.map_homological_complex (complex_shape.down ℕ)).obj X).X 0)
chain_complex.single₀_map_homological_complex._match_2 F X (i + 1) = F.map_zero_object.inv
chain_complex.single₀_map_homological_complex._match_2 F X 0 = 𝟙 (((F ⋙ chain_complex.single₀ W).obj X).X 0)

source

@[simp]

theorem chain_complex.single₀_map_homological_complex_hom_app_zero {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (X : V) :

((chain_complex.single₀_map_homological_complex F).hom.app X).f 0 = 𝟙 (((chain_complex.single₀ V ⋙ F.map_homological_complex (complex_shape.down ℕ)).obj X).X 0)

source

@[simp]

theorem chain_complex.single₀_map_homological_complex_hom_app_succ {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (X : V) (n : ℕ) :

((chain_complex.single₀_map_homological_complex F).hom.app X).f (n + 1) = 0

source

@[simp]

theorem chain_complex.single₀_map_homological_complex_inv_app_zero {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (X : V) :

((chain_complex.single₀_map_homological_complex F).inv.app X).f 0 = 𝟙 (((F ⋙ chain_complex.single₀ W).obj X).X 0)

source

@[simp]

theorem chain_complex.single₀_map_homological_complex_inv_app_succ {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (X : V) (n : ℕ) :

((chain_complex.single₀_map_homological_complex F).inv.app X).f (n + 1) = 0

source

noncomputable def cochain_complex.single₀_map_homological_complex {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] :

cochain_complex.single₀ V ⋙ F.map_homological_complex (complex_shape.up ℕ) ≅ F ⋙ cochain_complex.single₀ W

Turning an object into a cochain complex supported at zero then applying a functor is the same as applying the functor then forming the cochain complex.

Equations

cochain_complex.single₀_map_homological_complex F = category_theory.nat_iso.of_components (λ (X : V), {hom := {f := λ (i : ℕ), cochain_complex.single₀_map_homological_complex._match_1 F X i, comm' := _}, inv := {f := λ (i : ℕ), cochain_complex.single₀_map_homological_complex._match_2 F X i, comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
cochain_complex.single₀_map_homological_complex._match_1 F X (i + 1) = F.map_zero_object.hom
cochain_complex.single₀_map_homological_complex._match_1 F X 0 = 𝟙 (((cochain_complex.single₀ V ⋙ F.map_homological_complex (complex_shape.up ℕ)).obj X).X 0)
cochain_complex.single₀_map_homological_complex._match_2 F X (i + 1) = F.map_zero_object.inv
cochain_complex.single₀_map_homological_complex._match_2 F X 0 = 𝟙 (((F ⋙ cochain_complex.single₀ W).obj X).X 0)

source

@[simp]

theorem cochain_complex.single₀_map_homological_complex_hom_app_zero {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (X : V) :

((cochain_complex.single₀_map_homological_complex F).hom.app X).f 0 = 𝟙 (((cochain_complex.single₀ V ⋙ F.map_homological_complex (complex_shape.up ℕ)).obj X).X 0)

source

@[simp]

theorem cochain_complex.single₀_map_homological_complex_hom_app_succ {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (X : V) (n : ℕ) :

((cochain_complex.single₀_map_homological_complex F).hom.app X).f (n + 1) = 0

source

@[simp]

theorem cochain_complex.single₀_map_homological_complex_inv_app_zero {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (X : V) :

((cochain_complex.single₀_map_homological_complex F).inv.app X).f 0 = 𝟙 (((F ⋙ cochain_complex.single₀ W).obj X).X 0)

source

@[simp]

theorem cochain_complex.single₀_map_homological_complex_inv_app_succ {V : Type u} [category_theory.category V] [category_theory.preadditive V] [category_theory.limits.has_zero_object V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] [category_theory.limits.has_zero_object W] (F : V ⥤ W) [F.additive] (X : V) (n : ℕ) :

((cochain_complex.single₀_map_homological_complex F).inv.app X).f (n + 1) = 0

mathlib3 documentation

Homology is an additive functor #