Exact sequences #
A sequence of n
composable arrows S : ComposableArrows C
(i.e. a functor
S : Fin (n + 1) ⥤ C
) is said to be exact (S.Exact
) if the composition
of two consecutive arrows are zero (S.IsComplex
) and the diagram is
exact at each i
for 1 ≤ i < n
.
Together with the inductive construction of composable arrows
ComposableArrows.precomp
, this is useful in order to state that certain
finite sequences of morphisms are exact (e.g the snake lemma), even though
in the applications it would usually be more convenient to use individual
lemmas expressing the exactness at a particular object.
This implementation is a refactor of exact_seq
with appeared in the
Liquid Tensor Experiment as a property of lists in Arrow C
.
The composable arrows associated to a short complex.
Equations
- S.toComposableArrows = CategoryTheory.ComposableArrows.mk₂ S.f S.g
F : ComposableArrows C n
is a complex if all compositions of
two consecutive arrows are zero.
The short complex consisting of maps S.map' i j
and S.map' j k
when we know
that S : ComposableArrows C n
satisfies S.IsComplex
.
Equations
- S.sc' hS i j k hij hjk hk = CategoryTheory.ShortComplex.mk (S.map' i j ⋯ ⋯) (S.map' j k ⋯ hk) ⋯
The short complex consisting of maps S.map' i (i + 1)
and S.map' (i + 1) (i + 2)
when we know that S : ComposableArrows C n
satisfies S.IsComplex
.
F : ComposableArrows C n
is exact if it is a complex and that all short
complexes consisting of two consecutive arrows are exact.
Functoriality maps for ComposableArrows.sc'
.
Equations
- CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k hij hjk hk = { τ₁ := φ.app ⟨i, ⋯⟩, τ₂ := φ.app ⟨j, ⋯⟩, τ₃ := φ.app ⟨k, ⋯⟩, comm₁₂ := ⋯, comm₂₃ := ⋯ }
Functoriality maps for ComposableArrows.sc
.
Equations
- CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i hi = CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i (i + 1) (i + 2) ⋯ ⋯ ⋯
The isomorphism S₁.sc' _ i j k ≅ S₂.sc' _ i j k
induced by an isomorphism S₁ ≅ S₂
in ComposableArrows C n
.
Equations
- One or more equations did not get rendered due to their size.
The isomorphism S₁.sc _ i ≅ S₂.sc _ i
induced by an isomorphism S₁ ≅ S₂
in ComposableArrows C n
.
Equations
- One or more equations did not get rendered due to their size.
If S : ComposableArrows C (n + 2)
is such that the first two arrows form
an exact sequence and that the tail S.δ₀
is exact, then S
is also exact.
See ShortComplex.SnakeInput.snake_lemma
in Algebra.Homology.ShortComplex.SnakeLemma
for a use of this lemma.