The canonical truncation #
Given an embedding e : Embedding c c'
of complex shapes which
satisfies e.IsTruncLE
and K : HomologicalComplex C c'
,
we define K.truncGE' e : HomologicalComplex C c
and K.truncLE e : HomologicalComplex C c'
which are the canonical
truncations of K
relative to e
.
In order to achieve this, we dualize the constructions from the file
Embedding.TruncGE
.
The canonical truncation of a homological complex relative to an embedding
of complex shapes e
which satisfies e.IsTruncLE
.
Instances For
The isomorphism (K.truncLE' e).X i ≅ K.X i'
when e.f i = i'
and e.BoundaryLE i
does not hold.
Equations
Instances For
The isomorphism (K.truncLE' e).X i ≅ K.cycles i'
when e.f i = i'
and e.BoundaryLE i
holds.
Equations
Instances For
The canonical truncation of a homological complex relative to an embedding
of complex shapes e
which satisfies e.IsTruncLE
.
Instances For
The canonical isomorphism K.truncLE e ≅ (K.truncLE' e).extend e
.
Equations
Instances For
The isomorphism (K.truncLE e).X i' ≅ K.X i'
when e.f i = i'
and e.BoundaryLE i
does not hold.
Equations
Instances For
The isomorphism (K.truncLE e).X i' ≅ K.cycles i'
when e.f i = i'
and e.BoundaryLE i
holds.
Equations
Instances For
The morphism K.truncLE' e ⟶ L.truncLE' e
induced by a morphism K ⟶ L
.
Equations
Instances For
The morphism K.truncLE e ⟶ L.truncLE e
induced by a morphism K ⟶ L
.
Equations
Instances For
The canonical morphism K.truncLE' e ⟶ K.restriction e
.
Equations
Instances For
(K.truncLE'ToRestriction e).f i
is an isomorphism when ¬ e.BoundaryLE i
.
The canonical morphism K.truncLE e ⟶ K
when e
is an embedding of complex
shapes which satisfy e.IsTruncLE
.
Equations
Instances For
Given an embedding e : Embedding c c'
of complex shapes which satisfy e.IsTruncLE
,
this is the (canonical) truncation functor
HomologicalComplex C c' ⥤ HomologicalComplex C c
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural transformation K.truncGE' e ⟶ K.restriction e
for all K
.
Equations
Instances For
Given an embedding e : Embedding c c'
of complex shapes which satisfy e.IsTruncLE
,
this is the (canonical) truncation functor
HomologicalComplex C c' ⥤ HomologicalComplex C c'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural transformation K.ιTruncLE e : K.truncLE e ⟶ K
for all K
.
Equations
- e.ιTruncLENatTrans C = { app := fun (K : HomologicalComplex C c') => K.ιTruncLE e, naturality := ⋯ }