Decomposition of the Q endomorphisms #
In this file, we obtain a lemma decomposition_Q which expresses
explicitly the projection (Q q).f (n+1) : X _[n+1] ⟶ X _[n+1]
(X : SimplicialObject C with C a preadditive category) as
a sum of terms which are postcompositions with degeneracies.
(TODO @joelriou: when C is abelian, define the degenerate
subcomplex of the alternating face map complex of X and show
that it is a complement to the normalized Moore complex.)
Then, we introduce an ad hoc structure MorphComponents X n Z which
can be used in order to define morphisms X _[n+1] ⟶ Z using the
decomposition provided by decomposition_Q. This shall play a critical
role in the proof that the functor
N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ))
reflects isomorphisms.
(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
In each positive degree, this lemma decomposes the idempotent endomorphism
Q q as a sum of morphisms which are postcompositions with suitable degeneracies.
As Q q is the complement projection to P q, this implies that in the case of
simplicial abelian groups, any $(n+1)$-simplex $x$ can be decomposed as
$x = x' + \sum (i=0}^{q-1} σ_{n-i}(y_i)$ where $x'$ is in the image of P q and
the $y_i$ are in degree $n$.
The structure MorphComponents is an ad hoc structure that is used in
the proof that N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ))
reflects isomorphisms. The fields are the data that are needed in order to
construct a morphism X _[n+1] ⟶ Z (see φ) using the decomposition of the
identity given by decomposition_Q n (n+1).
- a : X.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z
- b : Fin (n + 1) → (X.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z)
Instances For
The morphism X _[n+1] ⟶ Z associated to f : MorphComponents X n Z.
Equations
- One or more equations did not get rendered due to their size.
Instances For
the canonical MorphComponents whose associated morphism is the identity
(see F_id) thanks to decomposition_Q n (n+1)
Equations
- AlgebraicTopology.DoldKan.MorphComponents.id X n = { a := AlgebraicTopology.DoldKan.PInfty.f (n + 1), b := fun (i : Fin (n + 1)) => X.σ i }
Instances For
A MorphComponents can be postcomposed with a morphism.
Equations
- f.postComp h = { a := CategoryTheory.CategoryStruct.comp f.a h, b := fun (i : Fin (n + 1)) => CategoryTheory.CategoryStruct.comp (f.b i) h }
Instances For
A MorphComponents can be precomposed with a morphism of simplicial objects.
Equations
- One or more equations did not get rendered due to their size.