Homological complexes. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A homological_complex V c with a "shape" controlled by c : complex_shape ι
has chain groups X i (objects in V) indexed by i : ι,
and a differential d i j whenever c.rel i j.
We in fact ask for differentials d i j for all i j : ι,
but have a field shape' requiring that these are zero when not allowed by c.
This avoids a lot of dependent type theory hell!
The composite of any two differentials d i j ≫ d j k must be zero.
We provide chain_complex V α for
α-indexed chain complexes in which d i j ≠ 0 only if j + 1 = i,
and similarly cochain_complex V α, with i = j + 1.
There is a category structure, where morphisms are chain maps.
For C : homological_complex V c, we define C.X_next i, which is either C.X j for some
arbitrarily chosen j such that c.r i j, or C.X i if there is no such j.
Similarly we have C.X_prev j.
Defined in terms of these we have C.d_from i : C.X i ⟶ C.X_next i and
C.d_to j : C.X_prev j ⟶ C.X j, which are either defined as C.d i j, or zero, as needed.
structure
homological_complex
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι) :
Type (max u u_1 v)
- X : ι → V
- d : Π (i j : ι), self.X i ⟶ self.X j
- shape' : (∀ (i j : ι), ¬c.rel i j → self.d i j = 0) . "obviously"
- d_comp_d' : (∀ (i j k : ι), c.rel i j → c.rel j k → self.d i j ≫ self.d j k = 0) . "obviously"
A homological_complex V c with a "shape" controlled by c : complex_shape ι
has chain groups X i (objects in V) indexed by i : ι,
and a differential d i j whenever c.rel i j.
We in fact ask for differentials d i j for all i j : ι,
but have a field shape' requiring that these are zero when not allowed by c.
This avoids a lot of dependent type theory hell!
The composite of any two differentials d i j ≫ d j k must be zero.
Instances for homological_complex
- homological_complex.has_sizeof_inst
- homological_complex.category_theory.category
- homological_complex.category_theory.limits.has_zero_morphisms
- homological_complex.category_theory.limits.has_zero_object
- homological_complex.inhabited
- homological_complex.category_theory.preadditive
- category_theory.idempotents.homological_complex.category_theory.is_idempotent_complete
@[simp]
theorem
homological_complex.shape
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(self : homological_complex V c)
(i j : ι) :
@[simp]
theorem
homological_complex.d_comp_d
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
(i j k : ι) :
@[simp]
theorem
homological_complex.d_comp_d_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
(i j k : ι)
{X' : V}
(f' : C.X k ⟶ X') :
theorem
homological_complex.ext
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(h_X : C₁.X = C₂.X)
(h_d : ∀ (i j : ι), c.rel i j → C₁.d i j ≫ category_theory.eq_to_hom _ = category_theory.eq_to_hom _ ≫ C₂.d i j) :
C₁ = C₂
@[reducible]
def
chain_complex
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(α : Type u_1)
[add_right_cancel_semigroup α]
[has_one α] :
Type (max u u_1 v)
An α-indexed chain complex is a homological_complex
in which d i j ≠ 0 only if j + 1 = i.
@[reducible]
def
cochain_complex
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(α : Type u_1)
[add_right_cancel_semigroup α]
[has_one α] :
Type (max u u_1 v)
An α-indexed cochain complex is a homological_complex
in which d i j ≠ 0 only if i + 1 = j.
@[simp]
theorem
chain_complex.prev
(α : Type u_1)
[add_right_cancel_semigroup α]
[has_one α]
(i : α) :
(complex_shape.down α).prev i = i + 1
@[simp]
theorem
chain_complex.next
(α : Type u_1)
[add_group α]
[has_one α]
(i : α) :
(complex_shape.down α).next i = i - 1
@[simp]
@[simp]
theorem
cochain_complex.prev
(α : Type u_1)
[add_group α]
[has_one α]
(i : α) :
(complex_shape.up α).prev i = i - 1
@[simp]
theorem
cochain_complex.next
(α : Type u_1)
[add_right_cancel_semigroup α]
[has_one α]
(i : α) :
(complex_shape.up α).next i = i + 1
@[simp]
theorem
homological_complex.hom.ext
{ι : Type u_1}
{V : Type u}
{_inst_1 : category_theory.category V}
{_inst_2 : category_theory.limits.has_zero_morphisms V}
{c : complex_shape ι}
{A B : homological_complex V c}
(x y : A.hom B)
(h : x.f = y.f) :
x = y
theorem
homological_complex.hom.ext_iff
{ι : Type u_1}
{V : Type u}
{_inst_1 : category_theory.category V}
{_inst_2 : category_theory.limits.has_zero_morphisms V}
{c : complex_shape ι}
{A B : homological_complex V c}
(x y : A.hom B) :
@[ext]
structure
homological_complex.hom
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(A B : homological_complex V c) :
Type (max u_1 v)
- f : Π (i : ι), A.X i ⟶ B.X i
- comm' : (∀ (i j : ι), c.rel i j → self.f i ≫ B.d i j = A.d i j ≫ self.f j) . "obviously"
A morphism of homological complexes consists of maps between the chain groups, commuting with the differentials.
Instances for homological_complex.hom
- homological_complex.hom.has_sizeof_inst
- homological_complex.hom.inhabited
@[simp]
theorem
homological_complex.hom.comm_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{A B : homological_complex V c}
(f : A.hom B)
(i j : ι)
{X' : V}
(f' : B.X j ⟶ X') :
@[simp]
theorem
homological_complex.hom.comm
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{A B : homological_complex V c}
(f : A.hom B)
(i j : ι) :
@[protected, instance]
def
homological_complex.hom.inhabited
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(A B : homological_complex V c) :
def
homological_complex.id
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(A : homological_complex V c) :
A.hom A
Identity chain map.
def
homological_complex.comp
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(A B C : homological_complex V c)
(φ : A.hom B)
(ψ : B.hom C) :
A.hom C
Composition of chain maps.
@[protected, instance]
def
homological_complex.category_theory.category
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι} :
Equations
- homological_complex.category_theory.category = {to_category_struct := {to_quiver := {hom := homological_complex.hom c}, id := homological_complex.id c, comp := homological_complex.comp c}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
homological_complex.id_f
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
(i : ι) :
@[simp]
theorem
homological_complex.comp_f
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ C₃ : homological_complex V c}
(f : C₁ ⟶ C₂)
(g : C₂ ⟶ C₃)
(i : ι) :
@[simp]
theorem
homological_complex.eq_to_hom_f
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(h : C₁ = C₂)
(n : ι) :
theorem
homological_complex.hom_f_injective
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c} :
function.injective (λ (f : C₁.hom C₂), f.f)
@[protected, instance]
def
homological_complex.category_theory.limits.has_zero_morphisms
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι} :
Equations
- homological_complex.category_theory.limits.has_zero_morphisms = {has_zero := λ (C D : homological_complex V c), {zero := {f := λ (i : ι), 0, comm' := _}}, comp_zero' := _, zero_comp' := _}
@[simp]
theorem
homological_complex.zero_apply
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C D : homological_complex V c)
(i : ι) :
noncomputable
def
homological_complex.zero
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_zero_object V] :
The zero complex
theorem
homological_complex.is_zero_zero
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_zero_object V] :
@[protected, instance]
@[protected, instance]
noncomputable
def
homological_complex.inhabited
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_zero_object V] :
inhabited (homological_complex V c)
Equations
theorem
homological_complex.congr_hom
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C D : homological_complex V c}
{f g : C ⟶ D}
(w : f = g)
(i : ι) :
@[simp]
theorem
homological_complex.eval_map
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
(i : ι)
(C D : homological_complex V c)
(f : C ⟶ D) :
(homological_complex.eval V c i).map f = f.f i
@[simp]
theorem
homological_complex.eval_obj
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
(i : ι)
(C : homological_complex V c) :
(homological_complex.eval V c i).obj C = C.X i
def
homological_complex.eval
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
(i : ι) :
homological_complex V c ⥤ V
The functor picking out the i-th object of a complex.
Equations
- homological_complex.eval V c i = {obj := λ (C : homological_complex V c), C.X i, map := λ (C D : homological_complex V c) (f : C ⟶ D), f.f i, map_id' := _, map_comp' := _}
Instances for homological_complex.eval
@[simp]
theorem
homological_complex.forget_obj
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
(C : homological_complex V c)
(ᾰ : ι) :
(homological_complex.forget V c).obj C ᾰ = C.X ᾰ
@[simp]
theorem
homological_complex.forget_map
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
(_x _x_1 : homological_complex V c)
(f : _x ⟶ _x_1)
(i : ι) :
(homological_complex.forget V c).map f i = f.f i
def
homological_complex.forget
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι) :
The functor forgetting the differential in a complex, obtaining a graded object.
Equations
- homological_complex.forget V c = {obj := λ (C : homological_complex V c), C.X, map := λ (_x _x_1 : homological_complex V c) (f : _x ⟶ _x_1), f.f, map_id' := _, map_comp' := _}
def
homological_complex.forget_eval
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
(i : ι) :
Forgetting the differentials than picking out the i-th object is the same as
just picking out the i-th object.
Equations
@[simp]
theorem
homological_complex.forget_eval_inv_app
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
(i : ι)
(X : homological_complex V c) :
@[simp]
theorem
homological_complex.forget_eval_hom_app
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
(i : ι)
(X : homological_complex V c) :
@[simp]
theorem
homological_complex.d_comp_eq_to_hom
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j j' : ι}
(rij : c.rel i j)
(rij' : c.rel i j') :
C.d i j' ≫ category_theory.eq_to_hom _ = C.d i j
If C.d i j and C.d i j' are both allowed, then we must have j = j',
and so the differentials only differ by an eq_to_hom.
@[simp]
theorem
homological_complex.eq_to_hom_comp_d
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i i' j : ι}
(rij : c.rel i j)
(rij' : c.rel i' j) :
category_theory.eq_to_hom _ ≫ C.d i' j = C.d i j
If C.d i j and C.d i' j are both allowed, then we must have i = i',
and so the differentials only differ by an eq_to_hom.
theorem
homological_complex.kernel_eq_kernel
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_kernels V]
{i j j' : ι}
(r : c.rel i j)
(r' : c.rel i j') :
category_theory.limits.kernel_subobject (C.d i j) = category_theory.limits.kernel_subobject (C.d i j')
theorem
homological_complex.image_eq_image
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
{i i' j : ι}
(r : c.rel i j)
(r' : c.rel i' j) :
category_theory.limits.image_subobject (C.d i j) = category_theory.limits.image_subobject (C.d i' j)
@[reducible]
noncomputable
def
homological_complex.X_prev
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
(j : ι) :
V
Either C.X i, if there is some i with c.rel i j, or C.X j.
noncomputable
def
homological_complex.X_prev_iso
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j : ι}
(r : c.rel i j) :
If c.rel i j, then C.X_prev j is isomorphic to C.X i.
Equations
noncomputable
def
homological_complex.X_prev_iso_self
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{j : ι}
(h : ¬c.rel (c.prev j) j) :
If there is no i so c.rel i j, then C.X_prev j is isomorphic to C.X j.
Equations
@[reducible]
noncomputable
def
homological_complex.X_next
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
(i : ι) :
V
Either C.X j, if there is some j with c.rel i j, or C.X i.
noncomputable
def
homological_complex.X_next_iso
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j : ι}
(r : c.rel i j) :
If c.rel i j, then C.X_next i is isomorphic to C.X j.
Equations
noncomputable
def
homological_complex.X_next_iso_self
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i : ι}
(h : ¬c.rel i (c.next i)) :
If there is no j so c.rel i j, then C.X_next i is isomorphic to C.X i.
Equations
@[reducible]
noncomputable
def
homological_complex.d_to
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
(j : ι) :
The differential mapping into C.X j, or zero if there isn't one.
@[reducible]
noncomputable
def
homological_complex.d_from
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
(i : ι) :
The differential mapping out of C.X i, or zero if there isn't one.
theorem
homological_complex.d_to_eq
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j : ι}
(r : c.rel i j) :
@[simp]
theorem
homological_complex.d_to_eq_zero
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{j : ι}
(h : ¬c.rel (c.prev j) j) :
theorem
homological_complex.d_from_eq
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j : ι}
(r : c.rel i j) :
@[simp]
theorem
homological_complex.d_from_eq_zero
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i : ι}
(h : ¬c.rel i (c.next i)) :
@[simp]
theorem
homological_complex.X_prev_iso_comp_d_to
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j : ι}
(r : c.rel i j) :
@[simp]
theorem
homological_complex.X_prev_iso_comp_d_to_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j : ι}
(r : c.rel i j)
{X' : V}
(f' : C.X j ⟶ X') :
@[simp]
theorem
homological_complex.X_prev_iso_self_comp_d_to_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{j : ι}
(h : ¬c.rel (c.prev j) j)
{X' : V}
(f' : C.X j ⟶ X') :
@[simp]
theorem
homological_complex.X_prev_iso_self_comp_d_to
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{j : ι}
(h : ¬c.rel (c.prev j) j) :
(C.X_prev_iso_self h).inv ≫ C.d_to j = 0
@[simp]
theorem
homological_complex.d_from_comp_X_next_iso_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j : ι}
(r : c.rel i j)
{X' : V}
(f' : C.X j ⟶ X') :
@[simp]
theorem
homological_complex.d_from_comp_X_next_iso
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i j : ι}
(r : c.rel i j) :
@[simp]
theorem
homological_complex.d_from_comp_X_next_iso_self
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i : ι}
(h : ¬c.rel i (c.next i)) :
C.d_from i ≫ (C.X_next_iso_self h).hom = 0
@[simp]
theorem
homological_complex.d_from_comp_X_next_iso_self_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
{i : ι}
(h : ¬c.rel i (c.next i))
{X' : V}
(f' : C.X i ⟶ X') :
@[simp]
theorem
homological_complex.d_to_comp_d_from
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
(j : ι) :
theorem
homological_complex.kernel_from_eq_kernel
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_kernels V]
{i j : ι}
(r : c.rel i j) :
theorem
homological_complex.image_to_eq_image
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
{i j : ι}
(r : c.rel i j) :
def
homological_complex.hom.iso_app
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁ ≅ C₂)
(i : ι) :
The i-th component of an isomorphism of chain complexes.
Equations
- homological_complex.hom.iso_app f i = (homological_complex.eval V c i).map_iso f
@[simp]
theorem
homological_complex.hom.iso_app_inv
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁ ≅ C₂)
(i : ι) :
(homological_complex.hom.iso_app f i).inv = f.inv.f i
@[simp]
theorem
homological_complex.hom.iso_app_hom
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁ ≅ C₂)
(i : ι) :
(homological_complex.hom.iso_app f i).hom = f.hom.f i
@[simp]
theorem
homological_complex.hom.iso_of_components_hom_f
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : Π (i : ι), C₁.X i ≅ C₂.X i)
(hf : ∀ (i j : ι), c.rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom)
(i : ι) :
(homological_complex.hom.iso_of_components f hf).hom.f i = (f i).hom
@[simp]
theorem
homological_complex.hom.iso_of_components_inv_f
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : Π (i : ι), C₁.X i ≅ C₂.X i)
(hf : ∀ (i j : ι), c.rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom)
(i : ι) :
(homological_complex.hom.iso_of_components f hf).inv.f i = (f i).inv
def
homological_complex.hom.iso_of_components
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : Π (i : ι), C₁.X i ≅ C₂.X i)
(hf : ∀ (i j : ι), c.rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom) :
C₁ ≅ C₂
Construct an isomorphism of chain complexes from isomorphism of the objects which commute with the differentials.
Equations
- homological_complex.hom.iso_of_components f hf = {hom := {f := λ (i : ι), (f i).hom, comm' := hf}, inv := {f := λ (i : ι), (f i).inv, comm' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
homological_complex.hom.iso_of_components_app
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : Π (i : ι), C₁.X i ≅ C₂.X i)
(hf : ∀ (i j : ι), c.rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom)
(i : ι) :
theorem
homological_complex.hom.is_iso_of_components
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁ ⟶ C₂)
[∀ (n : ι), category_theory.is_iso (f.f n)] :
Lemmas relating chain maps and d_to/d_from.
@[reducible]
noncomputable
def
homological_complex.hom.prev
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(j : ι) :
f.prev j is f.f i if there is some r i j, and f.f j otherwise.
theorem
homological_complex.hom.prev_eq
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
{i j : ι}
(w : c.rel i j) :
f.prev j = (C₁.X_prev_iso w).hom ≫ f.f i ≫ (C₂.X_prev_iso w).inv
@[reducible]
noncomputable
def
homological_complex.hom.next
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(i : ι) :
f.next i is f.f j if there is some r i j, and f.f j otherwise.
theorem
homological_complex.hom.next_eq
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
{i j : ι}
(w : c.rel i j) :
f.next i = (C₁.X_next_iso w).hom ≫ f.f j ≫ (C₂.X_next_iso w).inv
@[simp]
theorem
homological_complex.hom.comm_from_apply
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(i : ι)
[I : category_theory.concrete_category V]
(x : ↥(C₁.X i)) :
@[simp]
theorem
homological_complex.hom.comm_from_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(i : ι)
{X' : V}
(f' : C₂.X_next i ⟶ X') :
@[simp]
theorem
homological_complex.hom.comm_from
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(i : ι) :
@[simp]
theorem
homological_complex.hom.comm_to_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(j : ι)
{X' : V}
(f' : C₂.X j ⟶ X') :
@[simp]
theorem
homological_complex.hom.comm_to
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(j : ι) :
@[simp]
theorem
homological_complex.hom.comm_to_apply
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(j : ι)
[I : category_theory.concrete_category V]
(x : ↥(C₁.X_prev j)) :
noncomputable
def
homological_complex.hom.sq_from
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(i : ι) :
category_theory.arrow.mk (C₁.d_from i) ⟶ category_theory.arrow.mk (C₂.d_from i)
A morphism of chain complexes induces a morphism of arrows of the differentials out of each object.
Equations
@[simp]
theorem
homological_complex.hom.sq_from_left
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(i : ι) :
@[simp]
theorem
homological_complex.hom.sq_from_right
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(i : ι) :
@[simp]
theorem
homological_complex.hom.sq_from_id
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C₁ : homological_complex V c)
(i : ι) :
homological_complex.hom.sq_from (𝟙 C₁) i = 𝟙 (category_theory.arrow.mk (C₁.d_from i))
@[simp]
theorem
homological_complex.hom.sq_from_comp
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ C₃ : homological_complex V c}
(f : C₁ ⟶ C₂)
(g : C₂ ⟶ C₃)
(i : ι) :
noncomputable
def
homological_complex.hom.sq_to
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(j : ι) :
category_theory.arrow.mk (C₁.d_to j) ⟶ category_theory.arrow.mk (C₂.d_to j)
A morphism of chain complexes induces a morphism of arrows of the differentials into each object.
Equations
@[simp]
theorem
homological_complex.hom.sq_to_left
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(j : ι) :
@[simp]
theorem
homological_complex.hom.sq_to_right
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
{C₁ C₂ : homological_complex V c}
(f : C₁.hom C₂)
(j : ι) :
def
chain_complex.of
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d : Π (n : α), X (n + 1) ⟶ X n)
(sq : ∀ (n : α), d (n + 1) ≫ d n = 0) :
chain_complex V α
Construct an α-indexed chain complex from a dependently-typed differential.
@[simp]
theorem
chain_complex.of_X
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d : Π (n : α), X (n + 1) ⟶ X n)
(sq : ∀ (n : α), d (n + 1) ≫ d n = 0)
(n : α) :
(chain_complex.of X d sq).X n = X n
@[simp]
theorem
chain_complex.of_d
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d : Π (n : α), X (n + 1) ⟶ X n)
(sq : ∀ (n : α), d (n + 1) ≫ d n = 0)
(j : α) :
(chain_complex.of X d sq).d (j + 1) j = d j
theorem
chain_complex.of_d_ne
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d : Π (n : α), X (n + 1) ⟶ X n)
(sq : ∀ (n : α), d (n + 1) ≫ d n = 0)
{i j : α}
(h : i ≠ j + 1) :
(chain_complex.of X d sq).d i j = 0
def
chain_complex.of_hom
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d_X : Π (n : α), X (n + 1) ⟶ X n)
(sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0)
(Y : α → V)
(d_Y : Π (n : α), Y (n + 1) ⟶ Y n)
(sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0)
(f : Π (i : α), X i ⟶ Y i)
(comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i) :
chain_complex.of X d_X sq_X ⟶ chain_complex.of Y d_Y sq_Y
A constructor for chain maps between α-indexed chain complexes built using chain_complex.of,
from a dependently typed collection of morphisms.
Equations
- chain_complex.of_hom X d_X sq_X Y d_Y sq_Y f comm = {f := f, comm' := _}
@[simp]
theorem
chain_complex.of_hom_f
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d_X : Π (n : α), X (n + 1) ⟶ X n)
(sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0)
(Y : α → V)
(d_Y : Π (n : α), Y (n + 1) ⟶ Y n)
(sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0)
(f : Π (i : α), X i ⟶ Y i)
(comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i)
(i : α) :
(chain_complex.of_hom X d_X sq_X Y d_Y sq_Y f comm).f i = f i
@[nolint]
structure
chain_complex.mk_struct
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
Type (max u v)
Auxiliary structure for setting up the recursion in mk.
This is purely an implementation detail: for some reason just using the dependent 6-tuple directly
results in mk_aux taking much longer (well over the -T100000 limit) to elaborate.
Instances for chain_complex.mk_struct
- chain_complex.mk_struct.has_sizeof_inst
def
chain_complex.mk_struct.flat
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(t : chain_complex.mk_struct V) :
Flatten to a tuple.
def
chain_complex.mk_aux
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : d₁ ≫ d₀ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), Σ' (X₃ : V) (d₂ : X₃ ⟶ t.snd.snd.fst), d₂ ≫ t.snd.snd.snd.snd.fst = 0)
(n : ℕ) :
Auxiliary definition for mk.
Equations
- chain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ (n + 1) = let p : chain_complex.mk_struct V := chain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ n in {X₀ := p.X₁, X₁ := p.X₂, X₂ := (succ p.flat).fst, d₀ := p.d₁, d₁ := (succ p.flat).snd.fst, s := _}
- chain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ 0 = {X₀ := X₀, X₁ := X₁, X₂ := X₂, d₀ := d₀, d₁ := d₁, s := s}
def
chain_complex.mk
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : d₁ ≫ d₀ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), Σ' (X₃ : V) (d₂ : X₃ ⟶ t.snd.snd.fst), d₂ ≫ t.snd.snd.snd.snd.fst = 0) :
A inductive constructor for ℕ-indexed chain complexes.
You provide explicitly the first two differentials, then a function which takes two differentials and the fact they compose to zero, and returns the next object, its differential, and the fact it composes appropiately to zero.
See also mk', which only sees the previous differential in the inductive step.
Equations
- chain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ = chain_complex.of (λ (n : ℕ), (chain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ n).X₀) (λ (n : ℕ), (chain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ n).d₀) _
@[simp]
theorem
chain_complex.mk_X_0
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : d₁ ≫ d₀ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), Σ' (X₃ : V) (d₂ : X₃ ⟶ t.snd.snd.fst), d₂ ≫ t.snd.snd.snd.snd.fst = 0) :
(chain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀
@[simp]
theorem
chain_complex.mk_X_1
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : d₁ ≫ d₀ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), Σ' (X₃ : V) (d₂ : X₃ ⟶ t.snd.snd.fst), d₂ ≫ t.snd.snd.snd.snd.fst = 0) :
(chain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁
@[simp]
theorem
chain_complex.mk_X_2
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : d₁ ≫ d₀ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), Σ' (X₃ : V) (d₂ : X₃ ⟶ t.snd.snd.fst), d₂ ≫ t.snd.snd.snd.snd.fst = 0) :
(chain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂
@[simp]
theorem
chain_complex.mk_d_1_0
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : d₁ ≫ d₀ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), Σ' (X₃ : V) (d₂ : X₃ ⟶ t.snd.snd.fst), d₂ ≫ t.snd.snd.snd.snd.fst = 0) :
(chain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀
@[simp]
theorem
chain_complex.mk_d_2_0
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : d₁ ≫ d₀ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), Σ' (X₃ : V) (d₂ : X₃ ⟶ t.snd.snd.fst), d₂ ≫ t.snd.snd.snd.snd.fst = 0) :
(chain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁
def
chain_complex.mk'
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ : V)
(d : X₁ ⟶ X₀)
(succ' : Π (t : Σ (X₀ X₁ : V), X₁ ⟶ X₀), Σ' (X₂ : V) (d : X₂ ⟶ t.snd.fst), d ≫ t.snd.snd = 0) :
A simpler inductive constructor for ℕ-indexed chain complexes.
You provide explicitly the first differential, then a function which takes a differential, and returns the next object, its differential, and the fact it composes appropriately to zero.
@[simp]
def
chain_complex.mk_hom_aux
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : chain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst)
(n : ℕ) :
An auxiliary construction for mk_hom.
Here we build by induction a family of commutative squares,
but don't require at the type level that these successive commutative squares actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map)
in mk_hom.
Equations
- P.mk_hom_aux Q zero one one_zero_comm succ (n + 1) = ⟨(P.mk_hom_aux Q zero one one_zero_comm succ n).snd.fst, ⟨(succ n (P.mk_hom_aux Q zero one one_zero_comm succ n)).fst, _⟩⟩
- P.mk_hom_aux Q zero one one_zero_comm succ 0 = ⟨zero, ⟨one, one_zero_comm⟩⟩
def
chain_complex.mk_hom
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : chain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst) :
P ⟶ Q
A constructor for chain maps between ℕ-indexed chain complexes,
working by induction on commutative squares.
You need to provide the components of the chain map in degrees 0 and 1, show that these form a commutative square, and then give a construction of each component, and the fact that it forms a commutative square with the previous component, using as an inductive hypothesis the data (and commutativity) of the previous two components.
@[simp]
theorem
chain_complex.mk_hom_f_0
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : chain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst) :
@[simp]
theorem
chain_complex.mk_hom_f_1
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : chain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst) :
@[simp]
theorem
chain_complex.mk_hom_f_succ_succ
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : chain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst)
(n : ℕ) :
def
cochain_complex.of
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d : Π (n : α), X n ⟶ X (n + 1))
(sq : ∀ (n : α), d n ≫ d (n + 1) = 0) :
cochain_complex V α
Construct an α-indexed cochain complex from a dependently-typed differential.
@[simp]
theorem
cochain_complex.of_X
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d : Π (n : α), X n ⟶ X (n + 1))
(sq : ∀ (n : α), d n ≫ d (n + 1) = 0)
(n : α) :
(cochain_complex.of X d sq).X n = X n
@[simp]
theorem
cochain_complex.of_d
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d : Π (n : α), X n ⟶ X (n + 1))
(sq : ∀ (n : α), d n ≫ d (n + 1) = 0)
(j : α) :
(cochain_complex.of X d sq).d j (j + 1) = d j
theorem
cochain_complex.of_d_ne
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d : Π (n : α), X n ⟶ X (n + 1))
(sq : ∀ (n : α), d n ≫ d (n + 1) = 0)
{i j : α}
(h : i + 1 ≠ j) :
(cochain_complex.of X d sq).d i j = 0
@[simp]
theorem
cochain_complex.of_hom_f
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d_X : Π (n : α), X n ⟶ X (n + 1))
(sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0)
(Y : α → V)
(d_Y : Π (n : α), Y n ⟶ Y (n + 1))
(sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0)
(f : Π (i : α), X i ⟶ Y i)
(comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1))
(i : α) :
(cochain_complex.of_hom X d_X sq_X Y d_Y sq_Y f comm).f i = f i
def
cochain_complex.of_hom
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{α : Type u_2}
[add_right_cancel_semigroup α]
[has_one α]
[decidable_eq α]
(X : α → V)
(d_X : Π (n : α), X n ⟶ X (n + 1))
(sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0)
(Y : α → V)
(d_Y : Π (n : α), Y n ⟶ Y (n + 1))
(sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0)
(f : Π (i : α), X i ⟶ Y i)
(comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)) :
cochain_complex.of X d_X sq_X ⟶ cochain_complex.of Y d_Y sq_Y
A constructor for chain maps between α-indexed cochain complexes built using cochain_complex.of,
from a dependently typed collection of morphisms.
Equations
- cochain_complex.of_hom X d_X sq_X Y d_Y sq_Y f comm = {f := f, comm' := _}
@[nolint]
structure
cochain_complex.mk_struct
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
Type (max u v)
Auxiliary structure for setting up the recursion in mk.
This is purely an implementation detail: for some reason just using the dependent 6-tuple directly
results in mk_aux taking much longer (well over the -T100000 limit) to elaborate.
Instances for cochain_complex.mk_struct
- cochain_complex.mk_struct.has_sizeof_inst
def
cochain_complex.mk_struct.flat
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(t : cochain_complex.mk_struct V) :
Flatten to a tuple.
def
cochain_complex.mk_aux
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : d₀ ≫ d₁ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0), Σ' (X₃ : V) (d₂ : t.snd.snd.fst ⟶ X₃), t.snd.snd.snd.snd.fst ≫ d₂ = 0)
(n : ℕ) :
Auxiliary definition for mk.
Equations
- cochain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ (n + 1) = let p : cochain_complex.mk_struct V := cochain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ n in {X₀ := p.X₁, X₁ := p.X₂, X₂ := (succ p.flat).fst, d₀ := p.d₁, d₁ := (succ p.flat).snd.fst, s := _}
- cochain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ 0 = {X₀ := X₀, X₁ := X₁, X₂ := X₂, d₀ := d₀, d₁ := d₁, s := s}
def
cochain_complex.mk
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : d₀ ≫ d₁ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0), Σ' (X₃ : V) (d₂ : t.snd.snd.fst ⟶ X₃), t.snd.snd.snd.snd.fst ≫ d₂ = 0) :
A inductive constructor for ℕ-indexed cochain complexes.
You provide explicitly the first two differentials, then a function which takes two differentials and the fact they compose to zero, and returns the next object, its differential, and the fact it composes appropiately to zero.
See also mk', which only sees the previous differential in the inductive step.
Equations
- cochain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ = cochain_complex.of (λ (n : ℕ), (cochain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ n).X₀) (λ (n : ℕ), (cochain_complex.mk_aux X₀ X₁ X₂ d₀ d₁ s succ n).d₀) _
@[simp]
theorem
cochain_complex.mk_X_0
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : d₀ ≫ d₁ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0), Σ' (X₃ : V) (d₂ : t.snd.snd.fst ⟶ X₃), t.snd.snd.snd.snd.fst ≫ d₂ = 0) :
(cochain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀
@[simp]
theorem
cochain_complex.mk_X_1
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : d₀ ≫ d₁ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0), Σ' (X₃ : V) (d₂ : t.snd.snd.fst ⟶ X₃), t.snd.snd.snd.snd.fst ≫ d₂ = 0) :
(cochain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁
@[simp]
theorem
cochain_complex.mk_X_2
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : d₀ ≫ d₁ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0), Σ' (X₃ : V) (d₂ : t.snd.snd.fst ⟶ X₃), t.snd.snd.snd.snd.fst ≫ d₂ = 0) :
(cochain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂
@[simp]
theorem
cochain_complex.mk_d_1_0
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : d₀ ≫ d₁ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0), Σ' (X₃ : V) (d₂ : t.snd.snd.fst ⟶ X₃), t.snd.snd.snd.snd.fst ≫ d₂ = 0) :
(cochain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀
@[simp]
theorem
cochain_complex.mk_d_2_0
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : d₀ ≫ d₁ = 0)
(succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0), Σ' (X₃ : V) (d₂ : t.snd.snd.fst ⟶ X₃), t.snd.snd.snd.snd.fst ≫ d₂ = 0) :
(cochain_complex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁
def
cochain_complex.mk'
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X₀ X₁ : V)
(d : X₀ ⟶ X₁)
(succ' : Π (t : Σ (X₀ X₁ : V), X₀ ⟶ X₁), Σ' (X₂ : V) (d : t.snd.fst ⟶ X₂), t.snd.snd ≫ d = 0) :
A simpler inductive constructor for ℕ-indexed cochain complexes.
You provide explicitly the first differential, then a function which takes a differential, and returns the next object, its differential, and the fact it composes appropriately to zero.
@[simp]
@[simp]
@[simp]
def
cochain_complex.mk_hom_aux
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : cochain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f'), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f'')
(n : ℕ) :
An auxiliary construction for mk_hom.
Here we build by induction a family of commutative squares,
but don't require at the type level that these successive commutative squares actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map)
in mk_hom.
Equations
- P.mk_hom_aux Q zero one one_zero_comm succ (n + 1) = ⟨(P.mk_hom_aux Q zero one one_zero_comm succ n).snd.fst, ⟨(succ n (P.mk_hom_aux Q zero one one_zero_comm succ n)).fst, _⟩⟩
- P.mk_hom_aux Q zero one one_zero_comm succ 0 = ⟨zero, ⟨one, one_zero_comm⟩⟩
def
cochain_complex.mk_hom
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : cochain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f'), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f'') :
P ⟶ Q
A constructor for chain maps between ℕ-indexed cochain complexes,
working by induction on commutative squares.
You need to provide the components of the chain map in degrees 0 and 1, show that these form a commutative square, and then give a construction of each component, and the fact that it forms a commutative square with the previous component, using as an inductive hypothesis the data (and commutativity) of the previous two components.
@[simp]
theorem
cochain_complex.mk_hom_f_0
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : cochain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f'), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f'') :
@[simp]
theorem
cochain_complex.mk_hom_f_1
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : cochain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f'), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f'') :
@[simp]
theorem
cochain_complex.mk_hom_f_succ_succ
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(P Q : cochain_complex V ℕ)
(zero : P.X 0 ⟶ Q.X 0)
(one : P.X 1 ⟶ Q.X 1)
(one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one)
(succ : Π (n : ℕ) (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f'), Σ' (f'' : P.X (n + 2) ⟶ Q.X (n + 2)), p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f'')
(n : ℕ) :