Theorem 3: Fiber Bundle Homology

Let B ⊗_φ F be a fiber bundle complex (Def_12). If the connection φ acts as the identity on the homology of F, then H_n(B ⊗_φ F) ≅ ⊕_{p+q=n} H_p(B) ⊗ H_q(F) for each n.

Main Definitions

• ChainAutomorphism.ActsAsIdOnHomology — a chain automorphism induces the identity on homology
• ActsAsIdentityOnHomology — the connection acts as identity on homology
• fiberBundleSmallDC — the fiber bundle as a 2×2 double complex (SmallDC)
• fiberBundleHomology_n0/n1/n2 — the main isomorphisms at each degree

Acts as identity on homology

structure FiberBundle.ChainAutomorphism.ActsAsIdOnHomology {n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (ψ : ChainAutomorphism n₂ m₂ dF) : Prop

A chain automorphism ψ of F = (F₁ →[dF] F₀) acts as the identity on homology if:

• At degree 1: α₁(f) = f for all f ∈ ker(dF) (since H₁(F) = ker(dF))
• At degree 0: α₀(y) - y ∈ im(dF) for all y (so [α₀(y)] = [y] in H₀(F) = F₀/im(dF))

• deg1 (f : Fin n₂ → 𝔽₂) : f ∈ dF.ker → ψ.α₁ f = f

  At degree 1: α₁ fixes ker(dF).

• deg0 (y : Fin m₂ → 𝔽₂) : ψ.α₀ y - y ∈ dF.range

  At degree 0: α₀(y) - y ∈ im(dF) for all y.

def FiberBundle.ActsAsIdentityOnHomology {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) : Prop

The connection φ acts as identity on homology if for every basis element b¹ and every b⁰ ∈ supp(∂^B b¹), the chain automorphism φ(b¹, b⁰) acts as identity on H_q(F).

Equations

• FiberBundle.ActsAsIdentityOnHomology dB dF φ = ∀ (b1 : Fin n₁) (b0 : Fin m₁), dB (Pi.single b1 1) b0 ≠ 0 → FiberBundle.ChainAutomorphism.ActsAsIdOnHomology dF (φ b1 b0)

SmallDC from fiber bundle

def FiberBundle.fiberBundleSmallDC {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) : SmallDC

The fiber bundle double complex as a concrete 2×2 double complex.

Equations

• One or more equations did not get rendered due to their size.

Flatness lemmas

Over 𝔽₂ (a field), every module is free hence flat. This gives:

• ker(id_M ⊗ f) ≅ M ⊗ ker(f)
• (M ⊗ N) / im(id_M ⊗ f) ≅ M ⊗ (N / im f)

def FiberBundle.lTensor_ker_equiv {n₂ m₂ : ℕ} (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] [Module.Free 𝔽₂ M] (f : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) : ↥(LinearMap.lTensor M f).ker ≃ₗ[𝔽₂] TensorProduct 𝔽₂ M ↥f.ker

ker(id_M ⊗ f) ≅ M ⊗ ker(f) when M is free (hence flat).

Equations

• One or more equations did not get rendered due to their size.

def FiberBundle.lTensor_quotient_equiv {n₂ m₂ : ℕ} (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] (f : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) : (TensorProduct 𝔽₂ M (Fin m₂ → 𝔽₂) ⧸ (LinearMap.lTensor M f).range) ≃ₗ[𝔽₂] TensorProduct 𝔽₂ M ((Fin m₂ → 𝔽₂) ⧸ f.range)

(M ⊗ N) / im(id_M ⊗ f) ≅ M ⊗ (N / im f).

Equations

• FiberBundle.lTensor_quotient_equiv M f = lTensor.equiv M ⋯ ⋯

def FiberBundle.rTensor_ker_equiv {n₁ m₁ : ℕ} (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] [Module.Free 𝔽₂ M] (f : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) : ↥(LinearMap.rTensor M f).ker ≃ₗ[𝔽₂] TensorProduct 𝔽₂ (↥f.ker) M

ker(f ⊗ id_M) ≅ ker(f) ⊗ M when M is free (hence flat).

Equations

• One or more equations did not get rendered due to their size.

def FiberBundle.rTensor_quotient_equiv {n₁ m₁ : ℕ} (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] (f : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) : (TensorProduct 𝔽₂ (Fin m₁ → 𝔽₂) M ⧸ (LinearMap.rTensor M f).range) ≃ₗ[𝔽₂] TensorProduct 𝔽₂ ((Fin m₁ → 𝔽₂) ⧸ f.range) M

(N ⊗ M) / im(f ⊗ id_M) ≅ (N / im f) ⊗ M.

Equations

• FiberBundle.rTensor_quotient_equiv M f = rTensor.equiv M ⋯ ⋯

Key lemma: twisted dh on ker(dF)

When the connection acts as identity on H₁(F) = ker(dF), the twisted horizontal differential restricted to B₁ ⊗ ker(dF) equals the untwisted dB ⊗ id_{ker(dF)}.

theorem FiberBundle.pi_tmul_eq_sum {V : Type u_1} [AddCommGroup V] [Module 𝔽₂ V] {n : ℕ} (g : Fin n → 𝔽₂) (v : V) : g ⊗ₜ[𝔽₂] v = ∑ i : Fin n, g i • Pi.single i 1 ⊗ₜ[𝔽₂] v

Decompose a function as a sum over basis in a tensor product.

theorem FiberBundle.twistedDh1_single_tmul {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) (i : Fin n₁) (f : Fin n₂ → 𝔽₂) (hf : f ∈ dF.ker) : (twistedDhLin dB fun (b1 : Fin n₁) (b0 : Fin m₁) => ↑(φ b1 b0).α₁) (Pi.single i 1 ⊗ₜ[𝔽₂] f) = dB (Pi.single i 1) ⊗ₜ[𝔽₂] f

The twisted dh₁ on basis elements Pi.single i 1 ⊗ₜ f equals dB(eᵢ) ⊗ₜ f when f ∈ ker(dF) and identity-on-homology holds.

theorem FiberBundle.twistedDh1_comp_lTensor_eq {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) : (twistedDhLin dB fun (b1 : Fin n₁) (b0 : Fin m₁) => ↑(φ b1 b0).α₁) ∘ₗ LinearMap.lTensor (Fin n₁ → 𝔽₂) dF.ker.subtype = LinearMap.lTensor (Fin m₁ → 𝔽₂) dF.ker.subtype ∘ₗ LinearMap.rTensor (↥dF.ker) dB

The twisted dh₁ agrees with rTensor · dB on B₁ ⊗ ker(dF). Key commutativity diagram.

Characterizing properties of flatness equivalences

theorem FiberBundle.lTensor_ker_equiv_symm_val {n₂ m₂ : ℕ} (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] [Module.Free 𝔽₂ M] (f : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (y : TensorProduct 𝔽₂ M ↥f.ker) : ↑((lTensor_ker_equiv M f).symm y) = (LinearMap.lTensor M f.ker.subtype) y

The symm direction of lTensor_ker_equiv: underlying value is lTensor M subtype y.

theorem FiberBundle.lTensor_ker_equiv_apply_val {n₂ m₂ : ℕ} (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] [Module.Free 𝔽₂ M] (f : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (x : ↥(LinearMap.lTensor M f).ker) : (LinearMap.lTensor M f.ker.subtype) ((lTensor_ker_equiv M f) x) = ↑x

Forward direction: lTensor M subtype (lTensor_ker_equiv M f x) = x.val.

theorem FiberBundle.rTensor_ker_equiv_symm_val {n₁ m₁ : ℕ} (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] [Module.Free 𝔽₂ M] (f : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (y : TensorProduct 𝔽₂ (↥f.ker) M) : ↑((rTensor_ker_equiv M f).symm y) = (LinearMap.rTensor M f.ker.subtype) y

The symm direction of rTensor_ker_equiv: underlying value is rTensor M subtype y.

Kernel equivalence from commutative diagram

def FiberBundle.kerEquivOfConjugate {M₁ : Type u_1} {M₂ : Type u_2} {N₁ : Type u_3} {N₂ : Type u_4} [AddCommGroup M₁] [Module 𝔽₂ M₁] [AddCommGroup M₂] [Module 𝔽₂ M₂] [AddCommGroup N₁] [Module 𝔽₂ N₁] [AddCommGroup N₂] [Module 𝔽₂ N₂] (e₁ : M₁ ≃ₗ[𝔽₂] N₁) (e₂ : M₂ ≃ₗ[𝔽₂] N₂) (f : M₁ →ₗ[𝔽₂] M₂) (g : N₁ →ₗ[𝔽₂] N₂) (h : ↑e₂ ∘ₗ f = g ∘ₗ ↑e₁) : ↥f.ker ≃ₗ[𝔽₂] ↥g.ker

If e₂ ∘ f = g ∘ e₁ (as linear maps), then ker f ≃ ker g.

Equations

• One or more equations did not get rendered due to their size.

def FiberBundle.quotientEquivOfConjugate {M₁ : Type u_1} {M₂ : Type u_2} {N₁ : Type u_3} {N₂ : Type u_4} [AddCommGroup M₁] [Module 𝔽₂ M₁] [AddCommGroup M₂] [Module 𝔽₂ M₂] [AddCommGroup N₁] [Module 𝔽₂ N₁] [AddCommGroup N₂] [Module 𝔽₂ N₂] (e₁ : M₁ ≃ₗ[𝔽₂] N₁) (e₂ : M₂ ≃ₗ[𝔽₂] N₂) (f : M₁ →ₗ[𝔽₂] M₂) (g : N₁ →ₗ[𝔽₂] N₂) (h : ↑e₂ ∘ₗ f = g ∘ₗ ↑e₁) : (M₂ ⧸ f.range) ≃ₗ[𝔽₂] N₂ ⧸ g.range

If e₂ ∘ f = g ∘ e₁, then coker(f) ≃ coker(g).

Equations

• FiberBundle.quotientEquivOfConjugate e₁ e₂ f g h = Submodule.Quotient.equiv f.range g.range e₂ ⋯

Commutativity diagrams for fiber bundle

theorem FiberBundle.fiberBundleSmallDC_dh₁_eq {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) : (fiberBundleSmallDC dB dF φ).dh₁ = twistedDhLin dB fun (b1 : Fin n₁) (b0 : Fin m₁) => ↑(φ b1 b0).α₁

dh₁ in the fiber bundle SmallDC equals the twistedDhLin with α₁.

theorem FiberBundle.fiberBundleSmallDC_barDh₁_conj {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) : let E := fiberBundleSmallDC dB dF φ; ↑(lTensor_ker_equiv (Fin m₁ → 𝔽₂) dF) ∘ₗ E.barDh₁ = LinearMap.rTensor (↥dF.ker) dB ∘ₗ ↑(lTensor_ker_equiv (Fin n₁ → 𝔽₂) dF)

The commutativity: lTensor_ker_equiv B₀ dF ∘ barDh₁ = rTensor dB ∘ lTensor_ker_equiv B₁ dF for the fiber bundle SmallDC.

Twisted dh₀ on quotient: identity on homology at degree 0

When the connection acts as identity on H₀(F) = coker(dF), the twisted horizontal differential dh₀ composed with the quotient map equals rTensor coker(dF) dB.

theorem FiberBundle.twistedDh0_single_tmul_quotient {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) (i : Fin n₁) (f : Fin m₂ → 𝔽₂) : (LinearMap.lTensor (Fin m₁ → 𝔽₂) dF.range.mkQ) ((twistedDhLin dB fun (b1 : Fin n₁) (b0 : Fin m₁) => ↑(φ b1 b0).α₀) (Pi.single i 1 ⊗ₜ[𝔽₂] f)) = dB (Pi.single i 1) ⊗ₜ[𝔽₂] dF.range.mkQ f

The twisted dh₀ on basis elements Pi.single i 1 ⊗ₜ f, composed with the quotient map lTensor B₀ mkQ, equals dB(eᵢ) ⊗ₜ [f] when identity-on-homology holds.

theorem FiberBundle.twistedDh0_comp_lTensor_quotient_eq {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) : (LinearMap.lTensor (Fin m₁ → 𝔽₂) dF.range.mkQ ∘ₗ twistedDhLin dB fun (b1 : Fin n₁) (b0 : Fin m₁) => ↑(φ b1 b0).α₀) = LinearMap.rTensor ((Fin m₂ → 𝔽₂) ⧸ dF.range) dB ∘ₗ LinearMap.lTensor (Fin n₁ → 𝔽₂) dF.range.mkQ

The full commutativity: lTensor B₀ mkQ ∘ dh₀ = rTensor coker(dF) dB ∘ lTensor B₁ mkQ.

Main theorems

theorem FiberBundle.fiberBundleHomology_n2 {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) : Nonempty ((fiberBundleSmallDC dB dF φ).totH₂ ≃ₗ[𝔽₂] TensorProduct 𝔽₂ ↥dB.ker ↥dF.ker)

theorem FiberBundle.barDh₀_lTensor_quotient_conj {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) : let E := fiberBundleSmallDC dB dF φ; ↑(lTensor_quotient_equiv (Fin m₁ → 𝔽₂) dF) ∘ₗ E.barDh₀ = LinearMap.rTensor ((Fin m₂ → 𝔽₂) ⧸ dF.range) dB ∘ₗ ↑(lTensor_quotient_equiv (Fin n₁ → 𝔽₂) dF)

The commutativity: lTensor_quotient_equiv B₀ dF ∘ barDh₀ = rTensor dB ∘ lTensor_quotient_equiv B₁ dF. This follows from twistedDh0_comp_lTensor_quotient_eq and the definitions of barDh₀ (mapQ) and lTensor_quotient_equiv (lTensor.equiv), by diagram chasing on the quotient.

theorem FiberBundle.fiberBundleHomology_n0 {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) : Nonempty ((fiberBundleSmallDC dB dF φ).totH₀ ≃ₗ[𝔽₂] TensorProduct 𝔽₂ ((Fin m₁ → 𝔽₂) ⧸ dB.range) ((Fin m₂ → 𝔽₂) ⧸ dF.range))

theorem FiberBundle.fiberBundleHomology_n1 {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) : Nonempty ((fiberBundleSmallDC dB dF φ).totH₁ ≃ₗ[𝔽₂] TensorProduct 𝔽₂ (↥dB.ker) ((Fin m₂ → 𝔽₂) ⧸ dF.range) × TensorProduct 𝔽₂ ((Fin m₁ → 𝔽₂) ⧸ dB.range) ↥dF.ker)