Dimensions of boundaries of complexes of vector spaces

In a homological complex of vector spaces, a homology group has dimension at most that of the finite-dimensional term it is computed from (HomologicalComplex.finrank_homology_le_finrank_X).

Let C be a homological complex of vector spaces over a field F. If C.X j is finite-dimensional, C is exact in degree j exactly when the dimensions of the images of the incoming and outgoing differentials add up to the dimension of C.X j (HomologicalComplex.exactAt_iff_finrank_add_finrank). The boundaries of a based complex vanish in a degree where its basis is empty (HomologicalComplex.finrank_range_d_eq_zero), so for a bounded based complex the signs (-1) ^ (dim Bⱼ · f j) have finite multiplicative support (HomologicalComplex.hasFiniteMulSupport_neg_one_pow_finrank_mul).

Let φ : F →+* K be a homomorphism of fields and let D be a complex of vector spaces over K of the same shape. If C and D have bases in which the matrices of the differentials of D are the images under φ of those of C, then the images of the differentials have the same dimensions (HomologicalComplex.finrank_range_d_eq_of_toMatrix_eq), since rank is invariant under φ (Matrix.rank_map). Consequently D is acyclic exactly when C is (HomologicalComplex.acyclic_iff_of_toMatrix_eq).

Let L be a field extension of F with an ordered F-basis β a, a : Fin m, let C be a complex of vector spaces over L with bases c i, and let D be a complex of vector spaces over F with bases e i in which the matrix of each differential is the block matrix obtained from the matrix of the corresponding differential of C by replacing each entry x with Algebra.leftMulMatrix β x; that is, (D, e) is the restriction of scalars of (C, c) to F, based by the vectors β a • c i k. Then the boundaries of D have m times the dimension of those of C (HomologicalComplex.finrank_range_d_eq_mul_of_toMatrix_eq_leftMulMatrix), and D is acyclic exactly when C is (HomologicalComplex.acyclic_iff_of_toMatrix_eq_leftMulMatrix).

theorem HomologicalComplex.finrank_homology_le_finrank_X {k : Type u_1} [DivisionRing k] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat k) c) (i : ι) [Module.Finite k ↑(K.X i)] : Module.finrank k ↑(K.homology i) ≤ Module.finrank k ↑(K.X i)

The weak Morse inequality. In a homological complex of vector spaces, a homology group has dimension at most that of the finite-dimensional term it is computed from.

theorem HomologicalComplex.exactAt_iff_finrank_add_finrank {F : Type u_1} [Field F] {ι : Type u_2} {s : ComplexShape ι} (C : HomologicalComplex (ModuleCat F) s) {i j k : ι} (hi : s.prev j = i) (hk : s.next j = k) [Module.Finite F ↑(C.X j)] : C.ExactAt j ↔ Module.finrank F ↥(ModuleCat.Hom.hom (C.d i j)).range + Module.finrank F ↥(ModuleCat.Hom.hom (C.d j k)).range = Module.finrank F ↑(C.X j)

A complex of vector spaces with finite-dimensional term in degree j is exact in degree j exactly when the dimensions of the images of the incoming and outgoing differentials add up to the dimension of the term.

theorem HomologicalComplex.finrank_range_d_eq_zero {F : Type u_1} [Field F] (C : ChainComplex (ModuleCat F) ℤ) {n : ℤ → ℕ} (c : (i : ℤ) → Module.Basis (Fin (n i)) F ↑(C.X i)) {j : ℤ} (hj : n j = 0) : Module.finrank F ↥(ModuleCat.Hom.hom (C.d (j + 1) j)).range = 0

The boundaries vanish in a degree where the based complex vanishes.

theorem HomologicalComplex.hasFiniteMulSupport_neg_one_pow_finrank_mul {F : Type u_1} [Field F] (C : ChainComplex (ModuleCat F) ℤ) {n : ℤ → ℕ} (c : (i : ℤ) → Module.Basis (Fin (n i)) F ↑(C.X i)) (hn : {i : ℤ | n i ≠ 0}.Finite) (f : ℤ → ℕ) : Function.HasFiniteMulSupport fun (j : ℤ) => (-1) ^ (Module.finrank F ↥(ModuleCat.Hom.hom (C.d (j + 1) j)).range * f j)

The signs (-1) ^ (dim Bⱼ · f j), where Bⱼ is the space of boundaries of a bounded based complex C in degree j, have finite multiplicative support.

theorem HomologicalComplex.finrank_range_d_eq_of_toMatrix_eq {F : Type u_1} [Field F] {ι : Type u_2} {s : ComplexShape ι} {K : Type u_3} [Field K] (φ : F →+* K) {C : HomologicalComplex (ModuleCat F) s} {D : HomologicalComplex (ModuleCat K) s} {κ : ι → Type u_4} [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] {c : (i : ι) → Module.Basis (κ i) F ↑(C.X i)} {e : (i : ι) → Module.Basis (κ i) K ↑(D.X i)} {i j : ι} (hd : (LinearMap.toMatrix (e i) (e j)) (ModuleCat.Hom.hom (D.d i j)) = ((LinearMap.toMatrix (c i) (c j)) (ModuleCat.Hom.hom (C.d i j))).map ⇑φ) : Module.finrank K ↥(ModuleCat.Hom.hom (D.d i j)).range = Module.finrank F ↥(ModuleCat.Hom.hom (C.d i j)).range

If the matrix of a differential of D is the image under a homomorphism of fields φ of the matrix of the corresponding differential of C, then the images of the two differentials have the same dimension.

theorem HomologicalComplex.acyclic_iff_of_toMatrix_eq {F : Type u_1} [Field F] {ι : Type u_2} {s : ComplexShape ι} {K : Type u_3} [Field K] (φ : F →+* K) {C : HomologicalComplex (ModuleCat F) s} {D : HomologicalComplex (ModuleCat K) s} {κ : ι → Type u_4} [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] {c : (i : ι) → Module.Basis (κ i) F ↑(C.X i)} {e : (i : ι) → Module.Basis (κ i) K ↑(D.X i)} (hd : ∀ (i j : ι), s.Rel i j → (LinearMap.toMatrix (e i) (e j)) (ModuleCat.Hom.hom (D.d i j)) = ((LinearMap.toMatrix (c i) (c j)) (ModuleCat.Hom.hom (C.d i j))).map ⇑φ) : D.Acyclic ↔ C.Acyclic

If, in bases indexed by the same types, the matrices of the differentials of D are the images under a homomorphism of fields φ of the matrices of the differentials of C, then D is acyclic exactly when C is.

theorem HomologicalComplex.finrank_range_d_eq_mul_of_toMatrix_eq_leftMulMatrix {F : Type u_1} [Field F] {ι : Type u_2} {s : ComplexShape ι} {L : Type u_3} [Field L] [Algebra F L] {m : ℕ} (β : Module.Basis (Fin m) F L) {C : HomologicalComplex (ModuleCat L) s} {D : HomologicalComplex (ModuleCat F) s} {n : ι → ℕ} {c : (i : ι) → Module.Basis (Fin (n i)) L ↑(C.X i)} {e : (i : ι) → Module.Basis (Fin (n i * m)) F ↑(D.X i)} {i j : ι} (hd : (LinearMap.toMatrix (e i) (e j)) (ModuleCat.Hom.hom (D.d i j)) = (Matrix.reindex finProdFinEquiv finProdFinEquiv) ((Matrix.comp (Fin (n j)) (Fin (n i)) (Fin m) (Fin m) F) (((LinearMap.toMatrix (c i) (c j)) (ModuleCat.Hom.hom (C.d i j))).map ⇑(Algebra.leftMulMatrix β)))) : Module.finrank F ↥(ModuleCat.Hom.hom (D.d i j)).range = Module.finrank L ↥(ModuleCat.Hom.hom (C.d i j)).range * m

If the matrix of a differential of D is obtained from the matrix of the corresponding differential of C by replacing each entry x with the matrix Algebra.leftMulMatrix β x of multiplication by x, the indices (k, a) being ordered by finProdFinEquiv, then the image of the differential of D has m times the dimension of the image of that of C.

theorem HomologicalComplex.acyclic_iff_of_toMatrix_eq_leftMulMatrix {F : Type u_1} [Field F] {ι : Type u_2} {s : ComplexShape ι} {L : Type u_3} [Field L] [Algebra F L] {m : ℕ} (β : Module.Basis (Fin m) F L) {C : HomologicalComplex (ModuleCat L) s} {D : HomologicalComplex (ModuleCat F) s} {n : ι → ℕ} {c : (i : ι) → Module.Basis (Fin (n i)) L ↑(C.X i)} {e : (i : ι) → Module.Basis (Fin (n i * m)) F ↑(D.X i)} (hd : ∀ (i j : ι), s.Rel i j → (LinearMap.toMatrix (e i) (e j)) (ModuleCat.Hom.hom (D.d i j)) = (Matrix.reindex finProdFinEquiv finProdFinEquiv) ((Matrix.comp (Fin (n j)) (Fin (n i)) (Fin m) (Fin m) F) (((LinearMap.toMatrix (c i) (c j)) (ModuleCat.Hom.hom (C.d i j))).map ⇑(Algebra.leftMulMatrix β)))) : D.Acyclic ↔ C.Acyclic

If, in the bases c i and e i, the matrix of each differential of D is obtained from the matrix of the corresponding differential of C by replacing each entry x with the matrix Algebra.leftMulMatrix β x of multiplication by x, the indices (k, a) being ordered by finProdFinEquiv, then D is acyclic exactly when C is.