← all areas

Namespace DoubleComplex 15 theorems

— 14 · Convergence 1

directly in DoubleComplex 14

• Convergence data for bounded double complexes DoubleComplex.boundedSpectralSequence 0 below · cited by 1 · depth 18
• Pinned edge isomorphism Hⁿ(A) ≅ Hⁿ(Tot D) DoubleComplex.exists_HTot_equiv_mk_eq_mk_single_of_rows_exact_of_augmentation 0 below · cited by 2 · depth 33
• Pinned functoriality of total cohomology of double complexes DoubleComplex.exists_HTot_equiv_of_levelwise_equiv_pinned 0 below · cited by 3 · depth 33
• Signed transposition on total cohomology of a bounded double complex DoubleComplex.exists_HTot_transpose_equiv_mk_eq_mk_swap 0 below · cited by 2 · depth 33
• Bounded double complex with exact columns has acyclic total complex DoubleComplex.subsingleton_HTot_of_forall_subsingleton_colH 0 below · cited by 2 · depth 33
• Levelwise isomorphic bounded double complexes have isomorphic total cohomology DoubleComplex.nonempty_HTot_equiv_of_levelwise_equiv 0 below · cited by 3 · depth 34
• Augmented staircase lemma for bounded double complexes DoubleComplex.nonempty_HTot_equiv_of_rows_exact_of_augmentation 2 below · cited by 2 · depth 34
• Transposing a bounded double complex preserves total cohomology DoubleComplex.nonempty_HTot_transpose_equiv 0 below · cited by 3 · depth 34
• Euler characteristic of a bounded double complex via columns DoubleComplex.finite_HTot_and_sum_finrank_HTot_eq_sum_finrank_colH 4 below · cited by 1 · depth 35
• Total cohomology equals ''E₂^{0,n} for rows exact in positive degree DoubleComplex.nonempty_HTot_equiv_E2II_zero_of_forall_subsingleton_colH_transpose 0 below · cited by 1 · depth 35
• Total cohomology of a bounded double complex is additive DoubleComplex.nonempty_HTot_equiv_prod_of_levelwise_equiv_prod 1 below · cited by 1 · depth 35
• Total complex acyclic from a horizontal-equivariant vertical contraction DoubleComplex.subsingleton_HTot_of_colContraction 0 below · cited by 1 · depth 35
• Row contraction kills total cohomology of a bounded double complex DoubleComplex.subsingleton_HTot_of_rowContraction 0 below · cited by 1 · depth 35
• Peeling off the bottom row of a bounded double complex DoubleComplex.finite_HTot_and_sum_finrank_HTot_eq_sub_of_rowShift 1 below · cited by 1 · depth 36

DoubleComplex.Convergence 1

• Finiteness of E₂^{p,0} from finite Hⁿ and finite higher rows DoubleComplex.Convergence.finite_E2_q0 0 below · cited by 1 · depth 18