Homological complexes. #
A HomologicalComplex V c
with a "shape" controlled by c : ComplexShape ι
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 ChainComplex V α
for
α
-indexed chain complexes in which d i j ≠ 0
only if j + 1 = i
,
and similarly CochainComplex V α
, with i = j + 1
.
There is a category structure, where morphisms are chain maps.
For C : HomologicalComplex V c
, we define C.xNext 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.xPrev j
.
Defined in terms of these we have C.dFrom i : C.X i ⟶ C.xNext i
and
C.dTo j : C.xPrev j ⟶ C.X j
, which are either defined as C.d i j
, or zero, as needed.
A HomologicalComplex V c
with a "shape" controlled by c : ComplexShape ι
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.
- X : ι → V
- d : (i j : ι) → self.X i ⟶ self.X j
- d_comp_d' : ∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (self.d i j) (self.d j k) = 0
Instances For
The obvious isomorphism K.X p ≅ K.X q
when p = q
.
Equations
- K.XIsoOfEq h = CategoryTheory.eqToIso ⋯
Instances For
An α
-indexed chain complex is a HomologicalComplex
in which d i j ≠ 0
only if j + 1 = i
.
Equations
- ChainComplex V α = HomologicalComplex V (ComplexShape.down α)
Instances For
An α
-indexed cochain complex is a HomologicalComplex
in which d i j ≠ 0
only if i + 1 = j
.
Equations
- CochainComplex V α = HomologicalComplex V (ComplexShape.up α)
Instances For
A morphism of homological complexes consists of maps between the chain groups, commuting with the differentials.
- f : (i : ι) → A.X i ⟶ B.X i
- comm' : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (self.f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (self.f j)
Instances For
Equations
- A.instInhabitedHom B = { default := { f := fun (x : ι) => 0, comm' := ⋯ } }
Identity chain map.
Equations
- A.id = { f := fun (x : ι) => CategoryTheory.CategoryStruct.id (A.X x), comm' := ⋯ }
Instances For
Composition of chain maps.
Equations
- A.comp B C φ ψ = { f := fun (i : ι) => CategoryTheory.CategoryStruct.comp (φ.f i) (ψ.f i), comm' := ⋯ }
Instances For
Equations
- HomologicalComplex.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
Equations
- X.instZeroHom Y = { zero := { f := fun (x : ι) => 0, comm' := ⋯ } }
Equations
- HomologicalComplex.instHasZeroMorphisms = CategoryTheory.Limits.HasZeroMorphisms.mk ⋯ ⋯
The zero complex
Equations
- HomologicalComplex.zero = { X := fun (x : ι) => 0, d := fun (x x_1 : ι) => 0, shape := ⋯, d_comp_d' := ⋯ }
Instances For
Equations
- HomologicalComplex.instInhabitedOfHasZeroObject = { default := HomologicalComplex.zero }
The functor picking out the i
-th object of a complex.
Equations
- HomologicalComplex.eval V c i = { obj := fun (C : HomologicalComplex V c) => C.X i, map := fun {X Y : HomologicalComplex V c} (f : X ⟶ Y) => f.f i, map_id := ⋯, map_comp := ⋯ }
Instances For
The functor forgetting the differential in a complex, obtaining a graded object.
Equations
- HomologicalComplex.forget V c = { obj := fun (C : HomologicalComplex V c) => C.X, map := fun {X Y : HomologicalComplex V c} (f : X ⟶ Y) => f.f, map_id := ⋯, map_comp := ⋯ }
Instances For
Forgetting the differentials than picking out the i
-th object is the same as
just picking out the i
-th object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 eqToHom
.
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 eqToHom
.
Either C.X i
, if there is some i
with c.Rel i j
, or C.X j
.
Equations
- C.xPrev j = C.X (c.prev j)
Instances For
If c.Rel i j
, then C.xPrev j
is isomorphic to C.X i
.
Equations
- C.xPrevIso r = CategoryTheory.eqToIso ⋯
Instances For
If there is no i
so c.Rel i j
, then C.xPrev j
is isomorphic to C.X j
.
Equations
- C.xPrevIsoSelf h = CategoryTheory.eqToIso ⋯
Instances For
Either C.X j
, if there is some j
with c.rel i j
, or C.X i
.
Equations
- C.xNext i = C.X (c.next i)
Instances For
If c.Rel i j
, then C.xNext i
is isomorphic to C.X j
.
Equations
- C.xNextIso r = CategoryTheory.eqToIso ⋯
Instances For
If there is no j
so c.Rel i j
, then C.xNext i
is isomorphic to C.X i
.
Equations
- C.xNextIsoSelf h = CategoryTheory.eqToIso ⋯
Instances For
The differential mapping into C.X j
, or zero if there isn't one.
Equations
- C.dTo j = C.d (c.prev j) j
Instances For
The differential mapping out of C.X i
, or zero if there isn't one.
Equations
- C.dFrom i = C.d i (c.next i)
Instances For
The i
-th component of an isomorphism of chain complexes.
Equations
- HomologicalComplex.Hom.isoApp f i = (HomologicalComplex.eval V c i).mapIso f
Instances For
Construct an isomorphism of chain complexes from isomorphism of the objects which commute with the differentials.
Equations
- HomologicalComplex.Hom.isoOfComponents f hf = { hom := { f := fun (i : ι) => (f i).hom, comm' := hf }, inv := { f := fun (i : ι) => (f i).inv, comm' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
f.prev j
is f.f i
if there is some r i j
, and f.f j
otherwise.
Equations
- f.prev j = f.f (c.prev j)
Instances For
f.next i
is f.f j
if there is some r i j
, and f.f j
otherwise.
Equations
- f.next i = f.f (c.next i)
Instances For
A morphism of chain complexes induces a morphism of arrows of the differentials out of each object.
Equations
- f.sqFrom i = CategoryTheory.Arrow.homMk ⋯
Instances For
A morphism of chain complexes induces a morphism of arrows of the differentials into each object.
Equations
- f.sqTo j = CategoryTheory.Arrow.homMk ⋯
Instances For
Construct an α
-indexed chain complex from a dependently-typed differential.
Equations
- ChainComplex.of X d sq = { X := X, d := fun (i j : α) => if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (d j) else 0, shape := ⋯, d_comp_d' := ⋯ }
Instances For
A constructor for chain maps between α
-indexed chain complexes built using ChainComplex.of
,
from a dependently typed collection of morphisms.
Equations
- ChainComplex.ofHom X d_X sq_X Y d_Y sq_Y f comm = { f := f, comm' := ⋯ }
Instances For
Auxiliary definition for mk
.
Equations
- ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ 0 = CategoryTheory.ShortComplex.mk d₁ d₀ s
- ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n.succ = CategoryTheory.ShortComplex.mk (succ (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f ⋯
Instances For
An 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 appropriately to zero.
See also mk'
, which only sees the previous differential in the inductive step.
Equations
- ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ = ChainComplex.of (fun (n : ℕ) => (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₃) (fun (n : ℕ) => (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).g) ⋯
Instances For
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.
Equations
- ChainComplex.mk' X₀ X₁ d succ' = ChainComplex.mk X₀ X₁ (succ' d).fst d (succ' d).snd.fst ⋯ fun (S : CategoryTheory.ShortComplex V) => succ' S.f
Instances For
An auxiliary construction for mkHom
.
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 mkHom
.
Equations
Instances For
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.
Equations
Instances For
Construct an α
-indexed cochain complex from a dependently-typed differential.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A constructor for chain maps between α
-indexed cochain complexes built using CochainComplex.of
,
from a dependently typed collection of morphisms.
Equations
- CochainComplex.ofHom X d_X sq_X Y d_Y sq_Y f comm = { f := f, comm' := ⋯ }
Instances For
Auxiliary definition for mk
.
Equations
- One or more equations did not get rendered due to their size.
- CochainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ 0 = CategoryTheory.ShortComplex.mk d₀ d₁ s
Instances For
An 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 appropriately to zero.
See also mk'
, which only sees the previous differential in the inductive step.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- CochainComplex.mk' X₀ X₁ d succ' = CochainComplex.mk X₀ X₁ (succ' d).fst d (succ' d).snd.fst ⋯ fun (S : CategoryTheory.ShortComplex V) => succ' S.g
Instances For
An auxiliary construction for mkHom
.
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 mkHom
.
Equations
Instances For
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.