Shifting cochains
Let C
be a preadditive category. Given two cochain complexes (indexed by ℤ
),
the type of cochains HomComplex.Cochain K L n
of degree n
was introduced
in Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
. In this file, we
study how these cochains behave with respect to the shift on the complexes K
and L
.
When n
, a
, n'
are integers such that h : n' + a = n
,
we obtain rightShiftAddEquiv K L n a n' h : Cochain K L n ≃+ Cochain K (L⟦a⟧) n'
.
This definition does not involve signs, but the analogous definition
of leftShiftAddEquiv K L n a n' h' : Cochain K L n ≃+ Cochain (K⟦a⟧) L n'
when h' : n + a = n'
does involve signs, as we follow the 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]
The map Cochain K L n → Cochain K (L⟦a⟧) n'
when n' + a = n
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map Cochain K L n → Cochain (K⟦a⟧) L n'
when n + a = n'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map Cochain K (L⟦a⟧) n' → Cochain K L n
when n' + a = n
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map Cochain (K⟦a⟧) L n' → Cochain K L n
when n + a = n'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map Cochain K L n → Cochain (K⟦a⟧) (L⟦a⟧) n
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The additive equivalence Cochain K L n ≃+ Cochain K L⟦a⟧ n'
when n' + a = n
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The additive equivalence Cochain K L n ≃+ Cochain (K⟦a⟧) L n'
when n + a = n'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The additive map Cochain K L n →+ Cochain (K⟦a⟧) (L⟦a⟧) n
.
Equations
- CochainComplex.HomComplex.Cochain.shiftAddHom K L n a = AddMonoidHom.mk' (fun (γ : CochainComplex.HomComplex.Cochain K L n) => CochainComplex.HomComplex.Cochain.shift γ a) ⋯
Instances For
The linear equivalence Cochain K L n ≃+ Cochain K L⟦a⟧ n'
when n' + a = n
and
the category is R
-linear.
Equations
- CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv R K L n a n' hn' = AddEquiv.toLinearEquiv (CochainComplex.HomComplex.Cochain.rightShiftAddEquiv K L n a n' hn') ⋯
Instances For
The additive equivalence Cochain K L n ≃+ Cochain (K⟦a⟧) L n'
when n + a = n'
and
the category is R
-linear.
Equations
- CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv R K L n a n' hn = AddEquiv.toLinearEquiv (CochainComplex.HomComplex.Cochain.leftShiftAddEquiv K L n a n' hn) ⋯
Instances For
The linear map Cochain K L n ≃+ Cochain (K⟦a⟧) (L⟦a⟧) n
when the category is R
-linear.
Equations
- CochainComplex.HomComplex.Cochain.shiftLinearMap R K L n a = { toAddHom := ↑(CochainComplex.HomComplex.Cochain.shiftAddHom K L n a), map_smul' := ⋯ }
Instances For
The left and right shift of cochains commute only up to a sign.
The map Cocycle K L n → Cocycle K (L⟦a⟧) n'
when n' + a = n
.
Equations
- CochainComplex.HomComplex.Cocycle.rightShift γ a n' hn' = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.Cochain.rightShift (↑γ) a n' hn') (n' + 1) ⋯ ⋯
Instances For
The map Cocycle K (L⟦a⟧) n' → Cocycle K L n
when n' + a = n
.
Equations
- CochainComplex.HomComplex.Cocycle.rightUnshift γ n hn = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.Cochain.rightUnshift (↑γ) n hn) (n + 1) ⋯ ⋯
Instances For
The map Cocycle K L n → Cocycle (K⟦a⟧) L n'
when n + a = n'
.
Equations
- CochainComplex.HomComplex.Cocycle.leftShift γ a n' hn' = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.Cochain.leftShift (↑γ) a n' hn') (n' + 1) ⋯ ⋯
Instances For
The map Cocycle (K⟦a⟧) L n' → Cocycle K L n
when n + a = n'
.
Equations
- CochainComplex.HomComplex.Cocycle.leftUnshift γ n hn = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.Cochain.leftUnshift (↑γ) n hn) (n + 1) ⋯ ⋯
Instances For
The map Cocycle K L n → Cocycle (K⟦a⟧) (L⟦a⟧) n
.