Theorem 4: Projection Induces Isomorphism

Under the assumptions that (1) the connection φ acts as identity on homology of F, (2) the augmentation ε̄ : H₀(F) → 𝔽₂ is an isomorphism, and (3) H₀(B) = 0, the projection π_* induces an isomorphism H₁(B ⊗_φ F) ≅ H₁(B), and dually π^* induces an isomorphism H^1(B) ≅ H^1(B ⊗_φ F).

Main Results

• piStarDeg1Lin — the linear map π_* at degree 1: (b ⊗ f, b' ⊗ f') ↦ ε(f) · b
• piStarH1 — the induced map H₁(π_*) : H₁(B ⊗_φ F) → ker(dB)
• piStarH1_isLinearEquiv — H₁(π_*) is an isomorphism
• piUpperStarH1 — the induced map H¹(π*) : H¹(B) → H¹(B ⊗_φ F)
• piUpperStarH1_isLinearEquiv — H¹(π*) is an isomorphism

Helper: tensor with zero module

theorem FiberBundle.tensorProduct_eq_zero_of_subsingleton_left {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module 𝔽₂ M] [AddCommGroup N] [Module 𝔽₂ N] [Subsingleton M] (x : TensorProduct 𝔽₂ M N) : x = 0

M ⊗ N is zero when M is subsingleton.

instance FiberBundle.tensorProduct_subsingleton_left (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module 𝔽₂ M] [AddCommGroup N] [Module 𝔽₂ N] [Subsingleton M] : Subsingleton (TensorProduct 𝔽₂ M N)

If M = 0 (subsingleton), then M ⊗ N is subsingleton.

def FiberBundle.tensorProduct_zero_left_equiv (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module 𝔽₂ M] [AddCommGroup N] [Module 𝔽₂ N] [Subsingleton M] : TensorProduct 𝔽₂ M N ≃ₗ[𝔽₂] PUnit.{u_3 + 1}

If M is subsingleton, M ⊗ N ≃ₗ 0 (the trivial module).

Equations

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

Helper: quotient by top is subsingleton

instance FiberBundle.quotient_top_subsingleton (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] : Subsingleton (M ⧸ ⊤)

instance FiberBundle.quotient_range_top_subsingleton {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module 𝔽₂ M] [AddCommGroup N] [Module 𝔽₂ N] (f : M →ₗ[𝔽₂] N) (hf : f.range = ⊤) : Subsingleton (N ⧸ f.range)

range f = ⊤ implies the quotient M / range f is subsingleton.

Helper: product with zero

def FiberBundle.prod_punit_equiv (M : Type u_1) [AddCommGroup M] [Module 𝔽₂ M] : (M × PUnit.{u_2 + 1}) ≃ₗ[𝔽₂] M

M × PUnit ≃ₗ M.

Equations

• FiberBundle.prod_punit_equiv M = { toFun := fun (p : M × PUnit.{?u.18 + 1}) => p.1, map_add' := ⋯, map_smul' := ⋯, invFun := fun (m : M) => (m, PUnit.unit), left_inv := ⋯, right_inv := ⋯ }

Definition of π_* at degree 1

The projection map π_* from Def_13: on the (p,0) summand B_p ⊗ F_0, it sends b ⊗ f ↦ ε(f) · b. On the (p,1) summand B_p ⊗ F_1, it is zero. At degree 1 of the total complex, Tot₁ = A₁₀ × A₀₁ = (B₁ ⊗ F₀) × (B₀ ⊗ F₁). So π_*(x₁₀, x₀₁) = (rid ∘ (id ⊗ ε))(x₁₀).

def FiberBundle.piStarDeg1Lin {n₁ m₁ n₂ m₂ : ℕ} (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) : TensorProduct 𝔽₂ (Fin n₁ → 𝔽₂) (Fin m₂ → 𝔽₂) × TensorProduct 𝔽₂ (Fin m₁ → 𝔽₂) (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin n₁ → 𝔽₂

The projection π_* at degree 1: (x₁₀, x₀₁) ↦ (TensorProduct.rid (id ⊗ ε))(x₁₀). This sends b ⊗ f ↦ ε(f) · b on the B₁ ⊗ F₀ component and is zero on B₀ ⊗ F₁.

Equations

• FiberBundle.piStarDeg1Lin ε = (↑(TensorProduct.rid 𝔽₂ (Fin n₁ → 𝔽₂)) ∘ₗ LinearMap.lTensor (Fin n₁ → 𝔽₂) ε).coprod 0

theorem FiberBundle.piStarDeg1Lin_tmul {n₁ m₁ n₂ m₂ : ℕ} (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (b : Fin n₁ → 𝔽₂) (f : Fin m₂ → 𝔽₂) : (piStarDeg1Lin ε) (b ⊗ₜ[𝔽₂] f, 0) = ε f • b

π_* sends b ⊗ f to ε(f) • b on the first component.

theorem FiberBundle.piStarDeg1Lin_snd {n₁ m₁ n₂ m₂ : ℕ} (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (x : TensorProduct 𝔽₂ (Fin m₁ → 𝔽₂) (Fin n₂ → 𝔽₂)) : (piStarDeg1Lin ε) (0, x) = 0

π_* is zero on the second component (B₀ ⊗ F₁).

Helper: ε is invariant under the connection

theorem FiberBundle.epsilon_comp_alpha0_eq {n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (ψ : ChainAutomorphism n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hψ : ChainAutomorphism.ActsAsIdOnHomology dF ψ) : ε ∘ₗ ↑ψ.α₀ = ε

When φ(b1,b0) acts as identity on homology and ε ∘ dF = 0, we get ε ∘ α₀ = ε (the augmentation is invariant under the connection).

theorem FiberBundle.epsilon_autAtDeg_smul_eq {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) (b1 : Fin n₁) (b0 : Fin m₁) (f : Fin m₂ → 𝔽₂) : dB (Pi.single b1 1) b0 • ε ((autAtDeg dF φ 0 b1 b0) f) = dB (Pi.single b1 1) b0 • ε f

Per-term epsilon invariance: dB(e_{b1})(b0) • ε(autAtDeg f) = dB(e_{b1})(b0) • ε(f).

theorem FiberBundle.linearMap_basis_expand {n₁ m₁ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (b : Fin n₁ → 𝔽₂) : dB b = ∑ b1 : Fin n₁, b b1 • dB (Pi.single b1 1)

Basis expansion of a linear map: dB b = ∑ i, b i • dB (Pi.single i 1).

theorem FiberBundle.piStar_chainmap_twistedDh {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) (x : TensorProduct 𝔽₂ (Fin n₁ → 𝔽₂) (Fin m₂ → 𝔽₂)) : (TensorProduct.rid 𝔽₂ (Fin m₁ → 𝔽₂)) ((LinearMap.lTensor (Fin m₁ → 𝔽₂) ε) ((fiberBundleSmallDC dB dF φ).dh₀ x)) = dB ((TensorProduct.rid 𝔽₂ (Fin n₁ → 𝔽₂)) ((LinearMap.lTensor (Fin n₁ → 𝔽₂) ε) x))

The chain map property for the twisted differential: (rid ∘ (id ⊗ ε)) ∘ dh₀ = dB ∘ (rid ∘ (id ⊗ ε)) on B₁ ⊗ F₀.

π_* maps cycles to ker(dB) and boundaries to 0

theorem FiberBundle.piStarDeg1_maps_cycles {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) (z : ↥(fiberBundleSmallDC dB dF φ).totZ₁) : (piStarDeg1Lin ε) ↑z ∈ dB.ker

π_* maps total 1-cycles to ker(dB). This is because π_* is a chain map: dB ∘ π_* = π_* ∘ d₁, and d₁(z) = 0 for z ∈ totZ₁.

def FiberBundle.piStarOnCycles {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) : ↥(fiberBundleSmallDC dB dF φ).totZ₁ →ₗ[𝔽₂] ↥dB.ker

The restriction of π_* to totZ₁, landing in ker(dB).

Equations

• FiberBundle.piStarOnCycles dB dF φ ε hε hφ = { toFun := fun (z : ↥(FiberBundle.fiberBundleSmallDC dB dF φ).totZ₁) => ⟨(FiberBundle.piStarDeg1Lin ε) ↑z, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem FiberBundle.piStarOnCycles_maps_boundaries {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) : (fiberBundleSmallDC dB dF φ).totB₁InZ₁ ≤ (piStarOnCycles dB dF φ ε hε hφ).ker

π_* maps total 1-boundaries to 0 in ker(dB). Since B has no degree-2 terms, the image of π_* on boundaries is 0 (boundaries come from d₂ which involves B₁ ⊗ F₁, and π₁ = 0 on F₁): ε ∘ dF = 0 ensures π_*(dv₁(x)) = 0 and π_* is zero on the A₀₁ component.

The induced map on homology H₁(π_*)

def FiberBundle.piStarH1 {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) : (fiberBundleSmallDC dB dF φ).totH₁ →ₗ[𝔽₂] ↥dB.ker

The induced map H₁(π_) : H₁(B ⊗φ F) → ker(dB) = H₁(B). This is the map on quotients induced by π restricted to cycles.

Equations

• FiberBundle.piStarH1 dB dF φ ε hε hφ = (FiberBundle.fiberBundleSmallDC dB dF φ).totB₁InZ₁.liftQ (FiberBundle.piStarOnCycles dB dF φ ε hε hφ) ⋯

Surjectivity helpers for H₁(π_*)

theorem FiberBundle.twistedDh_kerDB_tmul_mem_range_dv₀ {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) (v : ↥dB.ker) (f₀ : Fin m₂ → 𝔽₂) : (fiberBundleSmallDC dB dF φ).dh₀ (↑v ⊗ₜ[𝔽₂] f₀) ∈ (fiberBundleSmallDC dB dF φ).dv₀.range

The twisted horizontal differential sends v ⊗ f₀ (with v ∈ ker dB) into the range of the vertical differential dv₀ = lTensor _ dF. This is because the twisting only changes f₀ by elements in im(dF).

theorem FiberBundle.piStarH1_surjective {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) (hε_surj : Function.Surjective ⇑ε) : Function.Surjective ⇑(piStarH1 dB dF φ ε hε hφ)

piStarH1 is surjective: for any v ∈ ker dB, there exists a class in totH₁ mapping to v.

Dimension argument: finrank totH₁ = finrank (ker dB)

theorem FiberBundle.finrank_totH1_eq_finrank_kerDB {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) (hεbar : ((Fin m₂ → 𝔽₂) ⧸ dF.range) ≃ₗ[𝔽₂] 𝔽₂) (hH0B : dB.range = ⊤) : Module.finrank 𝔽₂ (fiberBundleSmallDC dB dF φ).totH₁ = Module.finrank 𝔽₂ ↥dB.ker

The finrank of totH₁ equals that of ker dB under the fiber bundle hypotheses.

Main theorem: H₁(π_*) is an isomorphism

theorem FiberBundle.piStarH1_isLinearEquiv {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) (hεbar : ((Fin m₂ → 𝔽₂) ⧸ dF.range) ≃ₗ[𝔽₂] 𝔽₂) (hH0B : dB.range = ⊤) (hε_surj : Function.Surjective ⇑ε) : Function.Bijective ⇑(piStarH1 dB dF φ ε hε hφ)

Under assumptions: (1) connection φ acts as identity on homology of F, (2) ε̄ : H₀(F) → 𝔽₂ is an isomorphism (the augmentation ε induces an iso on H₀(F)), (3) H₀(B) = 0, i.e., range dB = ⊤ (dB is surjective), the map H₁(π_) : H₁(B ⊗φ F) → H₁(B) = ker(dB) is a linear isomorphism. This is the specific isomorphism induced by the chain map π from Def_13.

def FiberBundle.piStarH1Equiv {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) (hεbar : ((Fin m₂ → 𝔽₂) ⧸ dF.range) ≃ₗ[𝔽₂] 𝔽₂) (hH0B : dB.range = ⊤) (hε_surj : Function.Surjective ⇑ε) : (fiberBundleSmallDC dB dF φ).totH₁ ≃ₗ[𝔽₂] ↥dB.ker

The isomorphism H₁(π_*) as a LinearEquiv.

Equations

• FiberBundle.piStarH1Equiv dB dF φ ε hε hφ hεbar hH0B hε_surj = LinearEquiv.ofBijective (FiberBundle.piStarH1 dB dF φ ε hε hφ) ⋯

Cohomology version via duality (π^*)

def FiberBundle.piUpperStarDeg1Lin {n₁ m₁ n₂ m₂ : ℕ} (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) : Module.Dual 𝔽₂ (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Module.Dual 𝔽₂ (TensorProduct 𝔽₂ (Fin n₁ → 𝔽₂) (Fin m₂ → 𝔽₂) × TensorProduct 𝔽₂ (Fin m₁ → 𝔽₂) (Fin n₂ → 𝔽₂))

The cochain map π^* at degree 1: the dual/transpose of π_* at degree 1. For β ∈ B₁ = Dual(B₁), π^(β) ∈ Tot₁* is defined by π^(β)(b ⊗ f) = β(b) · ε(f) for f ∈ F₀, and π^(β)(b ⊗ f) = 0 for f ∈ F₁.

Equations

• FiberBundle.piUpperStarDeg1Lin ε = (FiberBundle.piStarDeg1Lin ε).dualMap

def FiberBundle.dualEquivOfEquiv {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] [FiniteDimensional 𝔽₂ V] [FiniteDimensional 𝔽₂ W] (e : V ≃ₗ[𝔽₂] W) : Module.Dual 𝔽₂ W ≃ₗ[𝔽₂] Module.Dual 𝔽₂ V

For finite-dimensional spaces, an isomorphism V ≃ₗ W dualizes to W* ≃ₗ V*.

Equations

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

def FiberBundle.piUpperStarH1Equiv {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) (hεbar : ((Fin m₂ → 𝔽₂) ⧸ dF.range) ≃ₗ[𝔽₂] 𝔽₂) (hH0B : dB.range = ⊤) (hε_surj : Function.Surjective ⇑ε) [FiniteDimensional 𝔽₂ (fiberBundleSmallDC dB dF φ).totH₁] [FiniteDimensional 𝔽₂ ↥dB.ker] : Module.Dual 𝔽₂ ↥dB.ker ≃ₗ[𝔽₂] Module.Dual 𝔽₂ (fiberBundleSmallDC dB dF φ).totH₁

The induced map H¹(π^) on cohomology. Since π^ is the transpose of π_, and H₁(π_) is an isomorphism between finite-dimensional spaces, the transpose H¹(π^*) : H¹(B) → H¹(B ⊗_φ F) is also an isomorphism.

Equations

• FiberBundle.piUpperStarH1Equiv dB dF φ ε hε hφ hεbar hH0B hε_surj = FiberBundle.dualEquivOfEquiv (FiberBundle.piStarH1Equiv dB dF φ ε hε hφ hεbar hH0B hε_surj)

theorem FiberBundle.piUpperStarH1_isLinearEquiv {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂) (hε : ε ∘ₗ dF = 0) (hφ : ActsAsIdentityOnHomology dB dF φ) (hεbar : ((Fin m₂ → 𝔽₂) ⧸ dF.range) ≃ₗ[𝔽₂] 𝔽₂) (hH0B : dB.range = ⊤) (hε_surj : Function.Surjective ⇑ε) [FiniteDimensional 𝔽₂ (fiberBundleSmallDC dB dF φ).totH₁] [FiniteDimensional 𝔽₂ ↥dB.ker] : Function.Bijective ⇑↑(piUpperStarH1Equiv dB dF φ ε hε hφ hεbar hH0B hε_surj)

H¹(π^) is an isomorphism: the transpose of the isomorphism H₁(π_).