Definition 12: Fiber Bundle Double Complex

Let B = (B₁ →[∂^B] B₀) and F = (F₁ →[∂^F] F₀) be 1-complexes over 𝔽₂ (the base and fiber), with canonical bases: B₁ = 𝔽₂^{n₁}, B₀ = 𝔽₂^{m₁}, F₁ = 𝔽₂^{n₂}, F₀ = 𝔽₂^{m₂}.

A chain automorphism of F is a pair of invertible linear maps (α₁ : F₁ ≃ F₁, α₀ : F₀ ≃ F₀) satisfying ∂^F ∘ α₁ = α₀ ∘ ∂^F.

A connection φ assigns to each pair (b¹ : Fin n₁, b⁰ : Fin m₁) a chain automorphism of F. The fiber bundle double complex B ⊠_φ F has objects B_p ⊗ F_q, vertical differential ∂^v = id_B ⊗ ∂^F, and twisted horizontal differential ∂^h_φ.

The fiber bundle code is B ⊗_φ F = Tot(B ⊠_φ F).

Main Definitions

• ChainAutomorphism — chain automorphism of a 1-complex
• Connection — connection for the fiber bundle
• twistedDhLin — twisted horizontal differential as a linear map
• twistedDh_comm_dv — commutativity of differentials
• fiberBundleDoubleComplex — the double complex B ⊠_φ F
• fiberBundleComplex — the total complex Tot(B ⊠_φ F)

Chain Automorphism

structure FiberBundle.ChainAutomorphism (n₂ m₂ : ℕ) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) : Type

A chain automorphism of a 1-complex F = (F₁ →[∂^F] F₀) over 𝔽₂, where F₁ = 𝔽₂^{n₂} and F₀ = 𝔽₂^{m₂}. This is a pair of invertible linear maps satisfying ∂^F ∘ α₁ = α₀ ∘ ∂^F.

• α₁ : (Fin n₂ → 𝔽₂) ≃ₗ[𝔽₂] Fin n₂ → 𝔽₂

  The automorphism on F₁ = 𝔽₂^{n₂}.

• α₀ : (Fin m₂ → 𝔽₂) ≃ₗ[𝔽₂] Fin m₂ → 𝔽₂

  The automorphism on F₀ = 𝔽₂^{m₂}.

• comm : dF ∘ₗ ↑self.α₁ = ↑self.α₀ ∘ₗ dF

  The chain map condition: ∂^F ∘ α₁ = α₀ ∘ ∂^F.

def FiberBundle.ChainAutomorphism.id {n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) : ChainAutomorphism n₂ m₂ dF

The identity chain automorphism.

Equations

• FiberBundle.ChainAutomorphism.id dF = { α₁ := LinearEquiv.refl 𝔽₂ (Fin n₂ → 𝔽₂), α₀ := LinearEquiv.refl 𝔽₂ (Fin m₂ → 𝔽₂), comm := ⋯ }

Connection

def FiberBundle.Connection (n₁ m₁ n₂ m₂ : ℕ) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) : Type

A connection for a fiber bundle. Assigns a chain automorphism of F to each pair (b¹ : Fin n₁, b⁰ : Fin m₁). Values outside supp(∂^B e_{b¹}) are irrelevant.

Equations

• FiberBundle.Connection n₁ m₁ n₂ m₂ dF = (Fin n₁ → Fin m₁ → FiberBundle.ChainAutomorphism n₂ m₂ dF)

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

The trivial connection: φ(b¹, b⁰) = id_F for all pairs.

Equations

• FiberBundle.Connection.trivial dF x✝¹ x✝ = FiberBundle.ChainAutomorphism.id dF

Twisted horizontal differential

noncomputable def FiberBundle.twistedDhLin {n₁ m₁ : ℕ} {V : Type u_1} [AddCommGroup V] [Module 𝔽₂ V] (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (autComp : Fin n₁ → Fin m₁ → V →ₗ[𝔽₂] V) : TensorProduct 𝔽₂ (Fin n₁ → 𝔽₂) V →ₗ[𝔽₂] TensorProduct 𝔽₂ (Fin m₁ → 𝔽₂) V

The twisted horizontal differential ∂^h_φ : 𝔽₂^{n₁} ⊗ V → 𝔽₂^{m₁} ⊗ V. On a basis element e_{b1} ⊗ f, this gives Σ_{b0 ∈ supp(∂^B e_{b1})} e_{b0} ⊗ autComp(b1,b0)(f).

Equations

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

@[simp]

theorem FiberBundle.twistedDhLin_tmul {n₁ m₁ : ℕ} {V : Type u_1} [AddCommGroup V] [Module 𝔽₂ V] (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (autComp : Fin n₁ → Fin m₁ → V →ₗ[𝔽₂] V) (b : Fin n₁ → 𝔽₂) (f : V) : (twistedDhLin dB autComp) (b ⊗ₜ[𝔽₂] f) = ∑ b1 : Fin n₁, ∑ b0 : Fin m₁, b b1 • dB (Pi.single b1 1) b0 • Pi.single b0 1 ⊗ₜ[𝔽₂] (autComp b1 b0) f

Commutativity of differentials

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

The twisted horizontal differential commutes with id ⊗ ∂^F. This is the key property that makes B ⊠_φ F a valid double complex, and follows from the chain map condition.

Size functions for the graded object

def FiberBundle.baseSize (n₁ m₁ : ℕ) (p : ℤ) : ℕ

The dimension of the base space at degree p: n₁ at degree 1, m₁ at degree 0, and 0 elsewhere.

Equations

• FiberBundle.baseSize n₁ m₁ p = if p = 1 then n₁ else if p = 0 then m₁ else 0

def FiberBundle.fiberSize (n₂ m₂ : ℕ) (q : ℤ) : ℕ

The dimension of the fiber space at degree q: n₂ at degree 1, m₂ at degree 0, and 0 elsewhere.

Equations

• FiberBundle.fiberSize n₂ m₂ q = if q = 1 then n₂ else if q = 0 then m₂ else 0

@[simp]

theorem FiberBundle.baseSize_one {n₁ m₁ : ℕ} : baseSize n₁ m₁ 1 = n₁

@[simp]

theorem FiberBundle.baseSize_zero {n₁ m₁ : ℕ} : baseSize n₁ m₁ 0 = m₁

@[simp]

theorem FiberBundle.fiberSize_one {n₂ m₂ : ℕ} : fiberSize n₂ m₂ 1 = n₂

@[simp]

theorem FiberBundle.fiberSize_zero {n₂ m₂ : ℕ} : fiberSize n₂ m₂ 0 = m₂

noncomputable def FiberBundle.fbObj (n₁ m₁ n₂ m₂ : ℕ) : ℤ × ℤ → ModuleCat 𝔽₂

The graded object underlying the fiber bundle double complex: (p, q) ↦ 𝔽₂^{baseSize(p)} ⊗ 𝔽₂^{fiberSize(q)}.

Equations

• FiberBundle.fbObj n₁ m₁ n₂ m₂ (p, q) = ModuleCat.of 𝔽₂ (TensorProduct 𝔽₂ (Fin (FiberBundle.baseSize n₁ m₁ p) → 𝔽₂) (Fin (FiberBundle.fiberSize n₂ m₂ q) → 𝔽₂))

Vertical differential (id ⊗ ∂^F)

noncomputable def FiberBundle.fiberDiff (n₂ m₂ : ℕ) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (q q' : ℤ) : (Fin (fiberSize n₂ m₂ q) → 𝔽₂) →ₗ[𝔽₂] Fin (fiberSize n₂ m₂ q') → 𝔽₂

The fiber differential at degree (q, q'): this is dF when q = 1, q' = 0, and 0 otherwise. Matches the shape of a 1-complex.

Equations

• FiberBundle.fiberDiff n₂ m₂ dF q q' = if hq : q = 1 ∧ q' = 0 then ⋯ ▸ ⋯ ▸ dF else 0

noncomputable def FiberBundle.fbDv (n₁ m₁ n₂ m₂ : ℕ) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (p q q' : ℤ) : fbObj n₁ m₁ n₂ m₂ (p, q) ⟶ fbObj n₁ m₁ n₂ m₂ (p, q')

The vertical differential id_B ⊗ ∂^F as a ModuleCat morphism.

Equations

• FiberBundle.fbDv n₁ m₁ n₂ m₂ dF p q q' = ModuleCat.ofHom (LinearMap.lTensor (Fin (FiberBundle.baseSize n₁ m₁ p) → 𝔽₂) (FiberBundle.fiberDiff n₂ m₂ dF q q'))

Automorphism component selection

noncomputable def FiberBundle.autAtDeg {n₁ m₁ n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (q : ℤ) (b1 : Fin n₁) (b0 : Fin m₁) : (Fin (fiberSize n₂ m₂ q) → 𝔽₂) →ₗ[𝔽₂] Fin (fiberSize n₂ m₂ q) → 𝔽₂

Given a connection φ, extract the automorphism component at fiber degree q: α₁ when q = 1, α₀ when q = 0, and id otherwise.

Equations

• FiberBundle.autAtDeg dF φ q b1 b0 = if hq : q = 1 then ⋯ ▸ ↑(φ b1 b0).α₁ else if hq : q = 0 then ⋯ ▸ ↑(φ b1 b0).α₀ else LinearMap.id

Twisted horizontal differential

noncomputable def FiberBundle.fbDh (n₁ m₁ n₂ m₂ : ℕ) (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (p p' q : ℤ) : fbObj n₁ m₁ n₂ m₂ (p, q) ⟶ fbObj n₁ m₁ n₂ m₂ (p', q)

The twisted horizontal differential as a ModuleCat morphism. For p = 1, p' = 0, this applies twistedDhLin with the connection-twisted automorphisms. For all other positions, it is zero.

Equations

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

Shape conditions

d² = 0 conditions

Commutativity: ∂^h ∘ ∂^v = ∂^v ∘ ∂^h

The fiber bundle double complex

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

The fiber bundle double complex B ⊠_φ F as a DoubleComplex𝔽₂. Objects are 𝔽₂^{baseSize(p)} ⊗ 𝔽₂^{fiberSize(q)}, vertical differential is id ⊗ ∂^F, and horizontal differential is the connection-twisted ∂^h_φ.

Equations

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

HasTotal instance

instance FiberBundle.fiberBundleDoubleComplex_hasTotal {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) : HomologicalComplex₂.HasTotal (fiberBundleDoubleComplex dB dF φ) (ComplexShape.down ℤ)

The fiber bundle double complex has a total complex.

The fiber bundle complex (total complex)

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

The fiber bundle complex B ⊗_φ F = Tot(B ⊠_φ F). This is the total complex of the fiber bundle double complex.

Equations

• FiberBundle.fiberBundleComplex dB dF φ = (FiberBundle.fiberBundleDoubleComplex dB dF φ).totalComplex