Construction of cochains by induction #
Let K and L be cochain complexes in a preadditive category C.
We provide an API to construct a cochain in Cochain K L d in the following
situation. Assume that X n : Set (Cochain K L d) is a sequence of subsets
of Cochain K L d, and φ n : X n → X (n + 1) is a sequence of maps such
that for a certain p₀ : ℕ and any x : X n, φ n x and x coincide
up to the degree p₀ + n, then we construct a cochain
InductionUp.limitSequence in Cochain K L d which coincides with the
nth-iteration of φ evaluated on x₀ up to the degree p₀ + n for any n : ℕ.
Given p₀ : ℤ, this is the condition on two cochains α and β in Cochain K L N
saying that α.v p q _ = β.v p q _ when p ≤ p₀.
Instances For
Assuming we have a sequence of subsets X n : Set (Cochain K L d) for all n : ℕ,
a sequence of maps φ n : X n → X (n + 1) for n : ℕ, and an element x₀ : X 0,
this is the dependent sequence in ∀ (n : ℕ), X n obtained by evaluation iterations of φ
on x₀.
Equations
Instances For
Assuming we have a sequence of subsets X n : Set (Cochain K L d) for all n : ℕ,
a sequence of maps φ n : X n → X (n + 1) for n : ℕ, and an element x₀ : X 0,
and under the assumption that for any x : X n the cochain φ n x coincides
with x up to the degree p₀ + n, this is a cochain in Cochain K L d which
can be understood as the "limit" of the sequence of cochains obtained by
evaluating iterations of φ on x₀.
Equations
- One or more equations did not get rendered due to their size.