The cochain complex of homomorphisms between cochain complexes
If F and G are cochain complexes (indexed by ℤ) in a preadditive category,
there is a cochain complex of abelian groups whose 0-cocycles identify to
morphisms F ⟶ G. Informally, in degree n, this complex shall consist of
cochains of degree n from F to G, i.e. arbitrary families for morphisms
F.X p ⟶ G.X (p + n). This complex shall be denoted HomComplex F G.
In order to avoid type theoretic issues, a cochain of degree n : ℤ
(i.e. a term of type of Cochain F G n) shall be defined here
as the data of a morphism F.X p ⟶ G.X q for all triplets
⟨p, q, hpq⟩ where p and q are integers and hpq : p + n = q.
If α : Cochain F G n, we shall define α.v p q hpq : F.X p ⟶ G.X q.
We follow the signs conventions appearing in the introduction of [Brian Conrad's book Grothendieck duality and base change][conrad2000].
References #
- [Brian Conrad, Grothendieck duality and base change][conrad2000]
A term of type HomComplex.Triplet n consists of two integers p and q
such that p + n = q. (This type is introduced so that the instance
AddCommGroup (Cochain F G n) defined below can be found automatically.)
Instances For
theorem
CochainComplex.HomComplex.Triplet.hpq
{n : ℤ}
(self : CochainComplex.HomComplex.Triplet n)
:
the condition on the two integers
def
CochainComplex.HomComplex.Cochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
:
Type (max 0 v)
A cochain of degree n : ℤ between to cochain complexes F and G consists
of a family of morphisms F.X p ⟶ G.X q whenever p + n = q, i.e. for all
triplets in HomComplex.Triplet n.
Equations
- CochainComplex.HomComplex.Cochain F G n = ((T : CochainComplex.HomComplex.Triplet n) → F.X T.p ⟶ G.X T.q)
Instances For
instance
CochainComplex.HomComplex.instAddCommGroupCochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
:
Equations
- CochainComplex.HomComplex.instAddCommGroupCochain F G n = id inferInstance
instance
CochainComplex.HomComplex.instModuleCochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
:
Module R (CochainComplex.HomComplex.Cochain F G n)
Equations
- CochainComplex.HomComplex.instModuleCochain F G n = id inferInstance
def
CochainComplex.HomComplex.Cochain.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(v : (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q))
:
A practical constructor for cochains.
Equations
- CochainComplex.HomComplex.Cochain.mk v { p := p, q := q, hpq := hpq } = v p q hpq
Instances For
def
CochainComplex.HomComplex.Cochain.v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(γ : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
F.X p ⟶ G.X q
The value of a cochain on a triplet ⟨p, q, hpq⟩.
Equations
- γ.v p q hpq = γ { p := p, q := q, hpq := hpq }
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cochain.mk_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(v : (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q))
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
(CochainComplex.HomComplex.Cochain.mk v).v p q hpq = v p q hpq
theorem
CochainComplex.HomComplex.Cochain.congr_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
{z₁ : CochainComplex.HomComplex.Cochain F G n}
{z₂ : CochainComplex.HomComplex.Cochain F G n}
(h : z₁ = z₂)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
z₁.v p q hpq = z₂.v p q hpq
theorem
CochainComplex.HomComplex.Cochain.ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
{z₁ : CochainComplex.HomComplex.Cochain F G n}
{z₂ : CochainComplex.HomComplex.Cochain F G n}
:
theorem
CochainComplex.HomComplex.Cochain.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n)
(z₂ : CochainComplex.HomComplex.Cochain F G n)
(h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq)
:
z₁ = z₂
theorem
CochainComplex.HomComplex.Cochain.ext₀_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{z₁ : CochainComplex.HomComplex.Cochain F G 0}
{z₂ : CochainComplex.HomComplex.Cochain F G 0}
:
theorem
CochainComplex.HomComplex.Cochain.ext₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G 0)
(z₂ : CochainComplex.HomComplex.Cochain F G 0)
(h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯)
:
z₁ = z₂
@[simp]
theorem
CochainComplex.HomComplex.Cochain.zero_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
CochainComplex.HomComplex.Cochain.v 0 p q hpq = 0
@[simp]
theorem
CochainComplex.HomComplex.Cochain.add_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n)
(z₂ : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.sub_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n)
(z₂ : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.neg_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.smul_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(k : R)
(z : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.units_smul_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(k : Rˣ)
(z : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
def
CochainComplex.HomComplex.Cochain.ofHoms
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(ψ : (p : ℤ) → F.X p ⟶ G.X p)
:
A cochain of degree 0 from F to G can be constructed from a family
of morphisms F.X p ⟶ G.X p for all p : ℤ.
Equations
- CochainComplex.HomComplex.Cochain.ofHoms ψ = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + 0 = q) => CategoryTheory.CategoryStruct.comp (ψ p) (CategoryTheory.eqToHom ⋯)
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHoms_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(ψ : (p : ℤ) → F.X p ⟶ G.X p)
(p : ℤ)
:
(CochainComplex.HomComplex.Cochain.ofHoms ψ).v p p ⋯ = ψ p
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHoms_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
:
(CochainComplex.HomComplex.Cochain.ofHoms fun (p : ℤ) => 0) = 0
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(ψ : (p : ℤ) → F.X p ⟶ G.X p)
(p : ℤ)
(q : ℤ)
(q' : ℤ)
(hpq : p + 0 = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) (G.d q q') = CategoryTheory.CategoryStruct.comp (ψ p) (G.d p q')
@[simp]
theorem
CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(ψ : (p : ℤ) → F.X p ⟶ G.X p)
(p' : ℤ)
(p : ℤ)
(q : ℤ)
(hpq : p + 0 = q)
:
CategoryTheory.CategoryStruct.comp (F.d p' p) ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) = CategoryTheory.CategoryStruct.comp (F.d p' q) (ψ q)
def
CochainComplex.HomComplex.Cochain.ofHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
:
The 0-cochain attached to a morphism of cochain complexes.
Equations
- CochainComplex.HomComplex.Cochain.ofHom φ = CochainComplex.HomComplex.Cochain.ofHoms fun (p : ℤ) => φ.f p
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHom_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHom_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
(p : ℤ)
:
(CochainComplex.HomComplex.Cochain.ofHom φ).v p p ⋯ = φ.f p
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHom_v_comp_d
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
(p : ℤ)
(q : ℤ)
(q' : ℤ)
(hpq : p + 0 = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) (G.d q q') = CategoryTheory.CategoryStruct.comp (φ.f p) (G.d p q')
@[simp]
theorem
CochainComplex.HomComplex.Cochain.d_comp_ofHom_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
(p' : ℤ)
(p : ℤ)
(q : ℤ)
(hpq : p + 0 = q)
:
CategoryTheory.CategoryStruct.comp (F.d p' p) ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) = CategoryTheory.CategoryStruct.comp (F.d p' q) (φ.f q)
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHom_add
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ₁ : F ⟶ G)
(φ₂ : F ⟶ G)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHom_sub
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ₁ : F ⟶ G)
(φ₂ : F ⟶ G)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHom_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
:
def
CochainComplex.HomComplex.Cochain.ofHomotopy
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{φ₁ : F ⟶ G}
{φ₂ : F ⟶ G}
(ho : Homotopy φ₁ φ₂)
:
CochainComplex.HomComplex.Cochain F G (-1)
The cochain of degree -1 given by an homotopy between two morphism of complexes.
Equations
- CochainComplex.HomComplex.Cochain.ofHomotopy ho = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (x : p + -1 = q) => ho.hom p q
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{φ₁ : F ⟶ G}
{φ₂ : F ⟶ G}
(h : φ₁ = φ₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHomotopy_refl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
:
theorem
CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(γ : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(q' : ℤ)
(hpq : p + n = q)
(hq' : q = q')
{Z : C}
(h : G.X q' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (γ.v p q hpq)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').hom h) = CategoryTheory.CategoryStruct.comp (γ.v p q' ⋯) h
theorem
CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(γ : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(q' : ℤ)
(hpq : p + n = q)
(hq' : q = q')
:
CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯
theorem
CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(γ : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(q' : ℤ)
(hpq : p + n = q)
(hq' : q' = q)
{Z : C}
(h : G.X q' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (γ.v p q hpq)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').inv h) = CategoryTheory.CategoryStruct.comp (γ.v p q' ⋯) h
theorem
CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(γ : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(q' : ℤ)
(hpq : p + n = q)
(hq' : q' = q)
:
CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯
def
CochainComplex.HomComplex.Cochain.comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
The composition of cochains.
Equations
- z₁.comp z₂ h = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + n₁₂ = q) => CategoryTheory.CategoryStruct.comp (z₁.v p (p + n₁) ⋯) (z₂.v (p + n₁) q ⋯)
Instances For
If z₁ is a cochain of degree n₁ and z₂ is a cochain of degree n₂, and that
we have a relation h : n₁ + n₂ = n₁₂, then z₁.comp z₂ h is a cochain of degree n₁₂.
The following lemma comp_v computes the value of this composition z₁.comp z₂ h
on a triplet ⟨p₁, p₃, _⟩ (with p₁ + n₁₂ = p₃). In order to use this lemma,
we need to provide an intermediate integer p₂ such that p₁ + n₁ = p₂.
It is advisable to use a p₂ that has good definitional properties
(i.e. p₁ + n₁ is not always the best choice.)
When z₁ or z₂ is a 0-cochain, there is a better choice of p₂, and this leads
to the two simplification lemmas comp_zero_cochain_v and zero_cochain_comp_v.
theorem
CochainComplex.HomComplex.Cochain.comp_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
(p₁ : ℤ)
(p₂ : ℤ)
(p₃ : ℤ)
(h₁ : p₁ + n₁ = p₂)
(h₂ : p₂ + n₂ = p₃)
:
(z₁.comp z₂ h).v p₁ p₃ ⋯ = CategoryTheory.CategoryStruct.comp (z₁.v p₁ p₂ h₁) (z₂.v p₂ p₃ h₂)
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_zero_cochain_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n)
(z₂ : CochainComplex.HomComplex.Cochain G K 0)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
(z₁.comp z₂ ⋯).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p q hpq) (z₂.v q q ⋯)
@[simp]
theorem
CochainComplex.HomComplex.Cochain.zero_cochain_comp_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G 0)
(z₂ : CochainComplex.HomComplex.Cochain G K n)
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
(z₁.comp z₂ ⋯).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p p ⋯) (z₂.v p q hpq)
theorem
CochainComplex.HomComplex.Cochain.comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₃ : ℤ}
{n₁₂ : ℤ}
{n₂₃ : ℤ}
{n₁₂₃ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(z₃ : CochainComplex.HomComplex.Cochain K L n₃)
(h₁₂ : n₁ + n₂ = n₁₂)
(h₂₃ : n₂ + n₃ = n₂₃)
(h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃)
:
(z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ h₂₃) ⋯
The associativity of the composition of cochains.
The formulation of the associativity of the composition of cochains given by the
lemma comp_assoc often requires a careful selection of degrees with good definitional
properties. In a few cases, like when one of the three cochains is a 0-cochain,
there are better choices, which provides the following simplification lemmas.
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n₂ : ℤ}
{n₃ : ℤ}
{n₂₃ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G 0)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(z₃ : CochainComplex.HomComplex.Cochain K L n₃)
(h₂₃ : n₂ + n₃ = n₂₃)
:
(z₁.comp z₂ ⋯).comp z₃ h₂₃ = z₁.comp (z₂.comp z₃ h₂₃) ⋯
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n₁ : ℤ}
{n₃ : ℤ}
{n₁₃ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K 0)
(z₃ : CochainComplex.HomComplex.Cochain K L n₃)
(h₁₃ : n₁ + n₃ = n₁₃)
:
(z₁.comp z₂ ⋯).comp z₃ h₁₃ = z₁.comp (z₂.comp z₃ ⋯) h₁₃
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_assoc_of_third_is_zero_cochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(z₃ : CochainComplex.HomComplex.Cochain K L 0)
(h₁₂ : n₁ + n₂ = n₁₂)
:
(z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) h₁₂
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_assoc_of_second_degree_eq_neg_third_degree
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K (-n₂))
(z₃ : CochainComplex.HomComplex.Cochain K L n₂)
(h₁₂ : n₁ + -n₂ = n₁₂)
:
(z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) ⋯
@[simp]
theorem
CochainComplex.HomComplex.Cochain.zero_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
CochainComplex.HomComplex.Cochain.comp 0 z₂ h = 0
@[simp]
theorem
CochainComplex.HomComplex.Cochain.add_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₁' : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.sub_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₁' : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.neg_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.smul_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(k : R)
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.units_smul_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(k : Rˣ)
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.id_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z₂ : CochainComplex.HomComplex.Cochain F G n)
:
(CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)).comp z₂ ⋯ = z₂
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(h : n₁ + n₂ = n₁₂)
:
z₁.comp 0 h = 0
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_add
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(z₂' : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_sub
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(z₂' : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_smul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(k : R)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_units_smul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(k : Rˣ)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.comp_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n)
:
z₁.comp (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id G)) ⋯ = z₁
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHoms_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
(φ : (p : ℤ) → F.X p ⟶ G.X p)
(ψ : (p : ℤ) → G.X p ⟶ K.X p)
:
(CochainComplex.HomComplex.Cochain.ofHoms φ).comp (CochainComplex.HomComplex.Cochain.ofHoms ψ) ⋯ = CochainComplex.HomComplex.Cochain.ofHoms fun (p : ℤ) => CategoryTheory.CategoryStruct.comp (φ p) (ψ p)
@[simp]
theorem
CochainComplex.HomComplex.Cochain.ofHom_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
(f : F ⟶ G)
(g : G ⟶ K)
:
def
CochainComplex.HomComplex.Cochain.diff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(K : CochainComplex C ℤ)
:
The differential on a cochain complex, as a cochain of degree 1.
Equations
- CochainComplex.HomComplex.Cochain.diff K = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (x : p + 1 = q) => K.d p q
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cochain.diff_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(K : CochainComplex C ℤ)
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
:
(CochainComplex.HomComplex.Cochain.diff K).v p q hpq = K.d p q
def
CochainComplex.HomComplex.δ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(z : CochainComplex.HomComplex.Cochain F G n)
:
The differential on the complex of morphisms between cochain complexes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similarly as for the composition of cochains, if z : Cochain F G n,
we usually need to carefully select intermediate indices with
good definitional properties in order to obtain a suitable expansion of the
morphisms which constitute δ n m z : Cochain F G m (when n + 1 = m, otherwise
it shall be zero). The basic equational lemma is δ_v below.
theorem
CochainComplex.HomComplex.δ_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(hnm : n + 1 = m)
(z : CochainComplex.HomComplex.Cochain F G n)
(p : ℤ)
(q : ℤ)
(hpq : p + m = q)
(q₁ : ℤ)
(q₂ : ℤ)
(hq₁ : q₁ = q - 1)
(hq₂ : p + 1 = q₂)
:
(CochainComplex.HomComplex.δ n m z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p q₁ ⋯) (G.d q₁ q) + m.negOnePow • CategoryTheory.CategoryStruct.comp (F.d p q₂) (z.v q₂ q ⋯)
theorem
CochainComplex.HomComplex.δ_shape
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(hnm : ¬n + 1 = m)
(z : CochainComplex.HomComplex.Cochain F G n)
:
CochainComplex.HomComplex.δ n m z = 0
@[simp]
theorem
CochainComplex.HomComplex.δ_hom_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(R : Type u_1)
[Ring R]
[CategoryTheory.Linear R C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
(m : ℤ)
(z : CochainComplex.HomComplex.Cochain F G n)
:
(CochainComplex.HomComplex.δ_hom R F G n m) z = CochainComplex.HomComplex.δ n m z
def
CochainComplex.HomComplex.δ_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(R : Type u_1)
[Ring R]
[CategoryTheory.Linear R C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
(m : ℤ)
:
The differential on the complex of morphisms between cochain complexes, as a linear map.
Equations
- CochainComplex.HomComplex.δ_hom R F G n m = { toFun := CochainComplex.HomComplex.δ n m, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
CochainComplex.HomComplex.δ_add
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(z₁ : CochainComplex.HomComplex.Cochain F G n)
(z₂ : CochainComplex.HomComplex.Cochain F G n)
:
CochainComplex.HomComplex.δ n m (z₁ + z₂) = CochainComplex.HomComplex.δ n m z₁ + CochainComplex.HomComplex.δ n m z₂
@[simp]
theorem
CochainComplex.HomComplex.δ_sub
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(z₁ : CochainComplex.HomComplex.Cochain F G n)
(z₂ : CochainComplex.HomComplex.Cochain F G n)
:
CochainComplex.HomComplex.δ n m (z₁ - z₂) = CochainComplex.HomComplex.δ n m z₁ - CochainComplex.HomComplex.δ n m z₂
@[simp]
theorem
CochainComplex.HomComplex.δ_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
:
CochainComplex.HomComplex.δ n m 0 = 0
@[simp]
theorem
CochainComplex.HomComplex.δ_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(z : CochainComplex.HomComplex.Cochain F G n)
:
CochainComplex.HomComplex.δ n m (-z) = -CochainComplex.HomComplex.δ n m z
@[simp]
theorem
CochainComplex.HomComplex.δ_smul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(k : R)
(z : CochainComplex.HomComplex.Cochain F G n)
:
CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z
@[simp]
theorem
CochainComplex.HomComplex.δ_units_smul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(k : Rˣ)
(z : CochainComplex.HomComplex.Cochain F G n)
:
CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z
theorem
CochainComplex.HomComplex.δ_δ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n₀ : ℤ)
(n₁ : ℤ)
(n₂ : ℤ)
(z : CochainComplex.HomComplex.Cochain F G n₀)
:
CochainComplex.HomComplex.δ n₁ n₂ (CochainComplex.HomComplex.δ n₀ n₁ z) = 0
theorem
CochainComplex.HomComplex.δ_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
(m₁ : ℤ)
(m₂ : ℤ)
(m₁₂ : ℤ)
(h₁₂ : n₁₂ + 1 = m₁₂)
(h₁ : n₁ + 1 = m₁)
(h₂ : n₂ + 1 = m₂)
:
CochainComplex.HomComplex.δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ ⋯
theorem
CochainComplex.HomComplex.δ_zero_cochain_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G 0)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(m₂ : ℤ)
(h₂ : n₂ + 1 = m₂)
:
CochainComplex.HomComplex.δ n₂ m₂ (z₁.comp z₂ ⋯) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ 0 1 z₁).comp z₂ ⋯
theorem
CochainComplex.HomComplex.δ_comp_zero_cochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n₁ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K 0)
(m₁ : ℤ)
(h₁ : n₁ + 1 = m₁)
:
CochainComplex.HomComplex.δ n₁ m₁ (z₁.comp z₂ ⋯) = z₁.comp (CochainComplex.HomComplex.δ 0 1 z₂) h₁ + (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ ⋯
@[simp]
theorem
CochainComplex.HomComplex.δ_zero_cochain_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(z : CochainComplex.HomComplex.Cochain F G 0)
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
:
(CochainComplex.HomComplex.δ 0 1 z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p p ⋯) (G.d p q) - CategoryTheory.CategoryStruct.comp (F.d p q) (z.v q q ⋯)
@[simp]
theorem
CochainComplex.HomComplex.δ_ofHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{p : ℤ}
(φ : F ⟶ G)
:
@[simp]
theorem
CochainComplex.HomComplex.δ_ofHomotopy
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{φ₁ : F ⟶ G}
{φ₂ : F ⟶ G}
(h : Homotopy φ₁ φ₂)
:
theorem
CochainComplex.HomComplex.δ_neg_one_cochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(z : CochainComplex.HomComplex.Cochain F G (-1))
:
CochainComplex.HomComplex.δ (-1) 0 z = CochainComplex.HomComplex.Cochain.ofHom
(Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) => z.v i j ⋯)
@[simp]
theorem
CochainComplex.HomComplex_X
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(i : ℤ)
:
(F.HomComplex G).X i = AddCommGrp.of (CochainComplex.HomComplex.Cochain F G i)
def
CochainComplex.HomComplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
:
The cochain complex of homomorphisms between two cochain complexes F and G.
In degree n : ℤ, it consists of the abelian group HomComplex.Cochain F G n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CochainComplex.HomComplex.cocycle
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
:
The subgroup of cocycles in Cochain F G n.
Equations
- CochainComplex.HomComplex.cocycle F G n = (CochainComplex.HomComplex.δ_hom ℤ F G n (n + 1)).toAddMonoidHom.ker
Instances For
def
CochainComplex.HomComplex.Cocycle
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
:
Type v
The type of n-cocycles, as a subtype of Cochain F G n.
Equations
- CochainComplex.HomComplex.Cocycle F G n = ↥(CochainComplex.HomComplex.cocycle F G n)
Instances For
instance
CochainComplex.HomComplex.instAddCommGroupCocycle
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
:
Equations
- CochainComplex.HomComplex.instAddCommGroupCocycle F G n = id inferInstance
theorem
CochainComplex.HomComplex.Cocycle.mem_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
(hnm : n + 1 = m)
(z : CochainComplex.HomComplex.Cochain F G n)
:
z ∈ CochainComplex.HomComplex.cocycle F G n ↔ CochainComplex.HomComplex.δ n m z = 0
instance
CochainComplex.HomComplex.Cocycle.instCoeCochain
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
:
Coe (CochainComplex.HomComplex.Cocycle F G n) (CochainComplex.HomComplex.Cochain F G n)
Equations
- CochainComplex.HomComplex.Cocycle.instCoeCochain = { coe := fun (x : CochainComplex.HomComplex.Cocycle F G n) => ↑x }
theorem
CochainComplex.HomComplex.Cocycle.ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
{z₁ : CochainComplex.HomComplex.Cocycle F G n}
{z₂ : CochainComplex.HomComplex.Cocycle F G n}
:
theorem
CochainComplex.HomComplex.Cocycle.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cocycle F G n)
(z₂ : CochainComplex.HomComplex.Cocycle F G n)
(h : ↑z₁ = ↑z₂)
:
z₁ = z₂
instance
CochainComplex.HomComplex.Cocycle.instSMul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
:
SMul R (CochainComplex.HomComplex.Cocycle F G n)
Equations
- CochainComplex.HomComplex.Cocycle.instSMul = { smul := fun (r : R) (z : CochainComplex.HomComplex.Cocycle F G n) => ⟨r • ↑z, ⋯⟩ }
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.coe_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(n : ℤ)
:
↑0 = 0
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.coe_add
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cocycle F G n)
(z₂ : CochainComplex.HomComplex.Cocycle F G n)
:
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.coe_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z : CochainComplex.HomComplex.Cocycle F G n)
:
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.coe_smul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z : CochainComplex.HomComplex.Cocycle F G n)
(x : R)
:
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.coe_units_smul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z : CochainComplex.HomComplex.Cocycle F G n)
(x : Rˣ)
:
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.coe_sub
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cocycle F G n)
(z₂ : CochainComplex.HomComplex.Cocycle F G n)
:
instance
CochainComplex.HomComplex.Cocycle.instModule
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type u_1}
[Ring R]
[CategoryTheory.Linear R C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
:
Module R (CochainComplex.HomComplex.Cocycle F G n)
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.mk_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z : CochainComplex.HomComplex.Cochain F G n)
(m : ℤ)
(hnm : n + 1 = m)
(h : CochainComplex.HomComplex.δ n m z = 0)
:
↑(CochainComplex.HomComplex.Cocycle.mk z m hnm h) = z
def
CochainComplex.HomComplex.Cocycle.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z : CochainComplex.HomComplex.Cochain F G n)
(m : ℤ)
(hnm : n + 1 = m)
(h : CochainComplex.HomComplex.δ n m z = 0)
:
Constructor for Cocycle F G n, taking as inputs z : Cochain F G n, an integer
m : ℤ such that n + 1 = m, and the relation δ n m z = 0.
Equations
- CochainComplex.HomComplex.Cocycle.mk z m hnm h = ⟨z, ⋯⟩
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.δ_eq_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{n : ℤ}
(z : CochainComplex.HomComplex.Cocycle F G n)
(m : ℤ)
:
CochainComplex.HomComplex.δ n m ↑z = 0
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.ofHom_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
:
def
CochainComplex.HomComplex.Cocycle.ofHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
:
The 0-cocycle associated to a morphism in CochainComplex C ℤ.
Equations
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.homOf_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(z : CochainComplex.HomComplex.Cocycle F G 0)
(i : ℤ)
:
z.homOf.f i = (↑z).v i i ⋯
def
CochainComplex.HomComplex.Cocycle.homOf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(z : CochainComplex.HomComplex.Cocycle F G 0)
:
F ⟶ G
The morphism in CochainComplex C ℤ associated to a 0-cocycle.
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.homOf_ofHom_eq_self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
:
(CochainComplex.HomComplex.Cocycle.ofHom φ).homOf = φ
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.ofHom_homOf_eq_self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(z : CochainComplex.HomComplex.Cocycle F G 0)
:
CochainComplex.HomComplex.Cocycle.ofHom z.homOf = z
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(z : CochainComplex.HomComplex.Cocycle F G 0)
:
CochainComplex.HomComplex.Cochain.ofHom z.homOf = ↑z
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.equivHom_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(φ : F ⟶ G)
:
@[simp]
theorem
CochainComplex.HomComplex.Cocycle.equivHom_symm_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
(z : CochainComplex.HomComplex.Cocycle F G 0)
:
(CochainComplex.HomComplex.Cocycle.equivHom F G).symm z = z.homOf
def
CochainComplex.HomComplex.Cocycle.equivHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(F : CochainComplex C ℤ)
(G : CochainComplex C ℤ)
:
(F ⟶ G) ≃+ CochainComplex.HomComplex.Cocycle F G 0
The additive equivalence between morphisms in CochainComplex C ℤ and 0-cocycles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
def
CochainComplex.HomComplex.Cocycle.diff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(K : CochainComplex C ℤ)
:
The 1-cocycle given by the differential on a cochain complex.
Equations
Instances For
@[simp]
theorem
CochainComplex.HomComplex.δ_comp_zero_cocycle
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n)
(z₂ : CochainComplex.HomComplex.Cocycle G K 0)
(m : ℤ)
:
CochainComplex.HomComplex.δ n m (z₁.comp ↑z₂ ⋯) = (CochainComplex.HomComplex.δ n m z₁).comp ↑z₂ ⋯
@[simp]
theorem
CochainComplex.HomComplex.δ_comp_ofHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n)
(f : G ⟶ K)
(m : ℤ)
:
CochainComplex.HomComplex.δ n m (z₁.comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯) = (CochainComplex.HomComplex.δ n m z₁).comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯
@[simp]
theorem
CochainComplex.HomComplex.δ_zero_cocycle_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n : ℤ}
(z₁ : CochainComplex.HomComplex.Cocycle F G 0)
(z₂ : CochainComplex.HomComplex.Cochain G K n)
(m : ℤ)
:
CochainComplex.HomComplex.δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (CochainComplex.HomComplex.δ n m z₂) ⋯
@[simp]
theorem
CochainComplex.HomComplex.δ_ofHom_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{K : CochainComplex C ℤ}
{n : ℤ}
(f : F ⟶ G)
(z : CochainComplex.HomComplex.Cochain G K n)
(m : ℤ)
:
CochainComplex.HomComplex.δ n m ((CochainComplex.HomComplex.Cochain.ofHom f).comp z ⋯) = (CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.HomComplex.δ n m z) ⋯
@[simp]
theorem
CochainComplex.HomComplex.Cochain.equivHomotopy_apply_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ₁ : F ⟶ G)
(φ₂ : F ⟶ G)
(ho : Homotopy φ₁ φ₂)
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ₁ : F ⟶ G)
(φ₂ : F ⟶ G)
(z : { z : CochainComplex.HomComplex.Cochain F G (-1) //
CochainComplex.HomComplex.Cochain.ofHom φ₁ = CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ })
(i : ℤ)
(j : ℤ)
:
((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂).symm z).hom i j = if hij : i + -1 = j then (↑z).v i j hij else 0
def
CochainComplex.HomComplex.Cochain.equivHomotopy
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ₁ : F ⟶ G)
(φ₂ : F ⟶ G)
:
Homotopy φ₁ φ₂ ≃ { z : CochainComplex.HomComplex.Cochain F G (-1) //
CochainComplex.HomComplex.Cochain.ofHom φ₁ = CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ }
Given two morphisms of complexes φ₁ φ₂ : F ⟶ G, the datum of an homotopy between φ₁ and
φ₂ is equivalent to the datum of a 1-cochain z such that δ (-1) 0 z is the difference
of the zero cochains associated to φ₂ and φ₁.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{φ₁ : F ⟶ G}
{φ₂ : F ⟶ G}
(h : φ₁ = φ₂)
:
↑((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂) (Homotopy.ofEq h)) = 0
theorem
CochainComplex.HomComplex.Cochain.ofHom_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
{f₁ : F ⟶ G}
{f₂ : F ⟶ G}
(h : CochainComplex.HomComplex.Cochain.ofHom f₁ = CochainComplex.HomComplex.Cochain.ofHom f₂)
:
f₁ = f₂
def
CochainComplex.HomComplex.Cochain.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n : ℤ}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
(z : CochainComplex.HomComplex.Cochain K L n)
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
:
CochainComplex.HomComplex.Cochain ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)
((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) n
If Φ : C ⥤ D is an additive functor, a cochain z : Cochain K L n between
cochain complexes in C can be mapped to a cochain between the cochain complexes
in D obtained by applying the functor
Φ.mapHomologicalComplex _ : CochainComplex C ℤ ⥤ CochainComplex D ℤ.
Equations
- z.map Φ = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + n = q) => Φ.map (z.v p q hpq)
Instances For
@[simp]
theorem
CochainComplex.HomComplex.Cochain.map_v
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n : ℤ}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
(z : CochainComplex.HomComplex.Cochain K L n)
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
(p : ℤ)
(q : ℤ)
(hpq : p + n = q)
:
(z.map Φ).v p q hpq = Φ.map (z.v p q hpq)
@[simp]
theorem
CochainComplex.HomComplex.Cochain.map_add
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n : ℤ}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
(z : CochainComplex.HomComplex.Cochain K L n)
(z' : CochainComplex.HomComplex.Cochain K L n)
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.map_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n : ℤ}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
(z : CochainComplex.HomComplex.Cochain K L n)
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.map_sub
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n : ℤ}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
(z : CochainComplex.HomComplex.Cochain K L n)
(z' : CochainComplex.HomComplex.Cochain K L n)
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.map_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(K : CochainComplex C ℤ)
(L : CochainComplex C ℤ)
(n : ℤ)
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
:
@[simp]
theorem
CochainComplex.HomComplex.Cochain.map_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(K : CochainComplex C ℤ)
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
{n₁ : ℤ}
{n₂ : ℤ}
{n₁₂ : ℤ}
(z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂)
(h : n₁ + n₂ = n₁₂)
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
:
(z₁.comp z₂ h).map Φ = (z₁.map Φ).comp (z₂.map Φ) h
@[simp]
theorem
CochainComplex.HomComplex.Cochain.map_ofHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(K : CochainComplex C ℤ)
(L : CochainComplex C ℤ)
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
(f : K ⟶ L)
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
:
(CochainComplex.HomComplex.Cochain.ofHom f).map Φ = CochainComplex.HomComplex.Cochain.ofHom ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).map f)
@[simp]
theorem
CochainComplex.HomComplex.δ_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(n : ℤ)
(m : ℤ)
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive D]
(z : CochainComplex.HomComplex.Cochain K L n)
(Φ : CategoryTheory.Functor C D)
[Φ.Additive]
:
CochainComplex.HomComplex.δ n m (z.map Φ) = (CochainComplex.HomComplex.δ n m z).map Φ