Definition 13: Augmented Complex

A 1-complex F = (F₁ →[∂^F] F₀) is augmented if there is a linear map ε : F₀ → 𝔽₂ such that ε ∘ ∂^F = 0. The augmentation gives a chain map π : F → 𝔽₂ with π₀ = ε and π₁ = 0.

Given a fiber bundle complex B ⊗_φ F, the augmentation induces:

• A chain map π_* : Tot(B ⊠_φ F)_n → B_n sending b ⊗ f ↦ π_q(f) · b
• A cochain map π^* : B*_n → Tot(B ⊠_φ F)*_n as the dual of π_*

Main Definitions

• AugmentedComplex — augmentation structure on a 1-complex
• augMap — the augmentation map at each fiber degree
• piStarSummandLin — the linear map b ⊗ f ↦ π_q(f) · b
• piStarMor — the chain map π_* assembled from summands
• baseDiff — the base differential
• cochainPiStar — the cochain map π^* (dual of π_*)

Augmented Complex

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

A complex F = (F₁ →[∂^F] F₀) is augmented if there is a linear map ε : F₀ → 𝔽₂ such that ε ∘ ∂^F = 0.

• ε : (Fin m₂ → 𝔽₂) →ₗ[𝔽₂] 𝔽₂

  The augmentation map ε : F₀ → 𝔽₂.

• comp_eq_zero : self.ε ∘ₗ dF = 0

  The chain map condition: ε ∘ ∂^F = 0.

Augmentation map at each degree

def FiberBundle.augMap {n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (aug : AugmentedComplex n₂ m₂ dF) (q : ℤ) : (Fin (fiberSize n₂ m₂ q) → 𝔽₂) →ₗ[𝔽₂] 𝔽₂

The augmentation map at fiber degree q:

• At q = 0: ε : F₀ → 𝔽₂ (= π₀)
• At q = 1: 0 : F₁ → 𝔽₂ (= π₁, since π₁ = 0)
• At other q: 0 (spaces are trivial)

Equations

• FiberBundle.augMap dF aug q = if hq : q = 0 then ⋯ ▸ aug.ε else 0

@[simp]

theorem FiberBundle.augMap_zero {n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (aug : AugmentedComplex n₂ m₂ dF) : augMap dF aug 0 = aug.ε

@[simp]

theorem FiberBundle.augMap_one {n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (aug : AugmentedComplex n₂ m₂ dF) : augMap dF aug 1 = 0

The π_* map on summands

def FiberBundle.piStarSummandLin {n₁ m₁ n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (aug : AugmentedComplex n₂ m₂ dF) (p q : ℤ) : TensorProduct 𝔽₂ (Fin (baseSize n₁ m₁ p) → 𝔽₂) (Fin (fiberSize n₂ m₂ q) → 𝔽₂) →ₗ[𝔽₂] Fin (baseSize n₁ m₁ p) → 𝔽₂

The linear map underlying π_* on the (p, q)-summand: b ⊗ f ↦ π_q(f) · b. Uses TensorProduct.rid to identify M ⊗ 𝔽₂ ≅ M after applying the augmentation.

Equations

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

theorem FiberBundle.piStarSummandLin_tmul_q0 {n₁ m₁ n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (aug : AugmentedComplex n₂ m₂ dF) (p : ℤ) (b : Fin (baseSize n₁ m₁ p) → 𝔽₂) (f : Fin (fiberSize n₂ m₂ 0) → 𝔽₂) : (piStarSummandLin dF aug p 0) (b ⊗ₜ[𝔽₂] f) = aug.ε f • b

theorem FiberBundle.piStarSummandLin_q_ne_zero {n₁ m₁ n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (aug : AugmentedComplex n₂ m₂ dF) (p q : ℤ) (hq : q ≠ 0) : piStarSummandLin dF aug p q = 0

The (p,q)-component as a ModuleCat morphism

def FiberBundle.piStarSummandMor {n₁ m₁ n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (aug : AugmentedComplex n₂ m₂ dF) (n p q : ℤ) (hpq : p + q = n) : fbObj n₁ m₁ n₂ m₂ (p, q) ⟶ ModuleCat.of 𝔽₂ (Fin (baseSize n₁ m₁ n) → 𝔽₂)

The (p, q)-component of π_* as a ModuleCat morphism, targeting 𝔽₂^{baseSize(n)} with type transport from the proof p + q = n. When q = 0, p = n and this sends b ⊗ f ↦ ε(f) · b. When q ≠ 0, this is zero.

Equations

• FiberBundle.piStarSummandMor dF aug n p q hpq = if hq : q = 0 then ModuleCat.ofHom (LinearMap.funLeft 𝔽₂ 𝔽₂ (Fin.cast ⋯) ∘ₗ FiberBundle.piStarSummandLin dF aug p q) else 0

The chain map π_*

def FiberBundle.piStarMor {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (aug : AugmentedComplex n₂ m₂ dF) (n : ℤ) : (fiberBundleDoubleComplex dB dF φ).totalComplex.X n ⟶ ModuleCat.of 𝔽₂ (Fin (baseSize n₁ m₁ n) → 𝔽₂)

The chain map π_* : Tot(B ⊠_φ F)_n → 𝔽₂^{baseSize(n)} at degree n, assembled from the summand maps using totalDesc.

Equations

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

Base differential

def FiberBundle.baseDiff (n₁ m₁ : ℕ) (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (n n' : ℤ) : (Fin (baseSize n₁ m₁ n) → 𝔽₂) →ₗ[𝔽₂] Fin (baseSize n₁ m₁ n') → 𝔽₂

The base differential at degrees (n, n'): dB when n = 1, n' = 0, 0 otherwise.

Equations

• FiberBundle.baseDiff n₁ m₁ dB n n' = if hn : n = 1 ∧ n' = 0 then ⋯ ▸ ⋯ ▸ dB else 0

Augmentation compatibility with connection

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

The augmentation ε is compatible with a chain automorphism ψ if ε ∘ α₀ = ε. This follows from ActsAsIdOnHomology: since α₀(y) - y ∈ im(dF) and ε ∘ dF = 0, we get ε(α₀(y)) = ε(y).

theorem FiberBundle.aug_preserved_by_connection {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (aug : AugmentedComplex n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) (b1 : Fin n₁) (b0 : Fin m₁) (hne : dB (Pi.single b1 1) b0 ≠ 0) : aug.ε ∘ₗ ↑(φ b1 b0).α₀ = aug.ε

The augmentation is preserved by all connection automorphisms in the support of ∂^B, assuming the connection acts as identity on homology.

Helper lemmas

@[simp]

theorem FiberBundle.autAtDeg_zero {n₁ m₁ n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (b1 : Fin n₁) (b0 : Fin m₁) : autAtDeg dF φ 0 b1 b0 = ↑(φ b1 b0).α₀

Helper: autAtDeg at degree 0 is α₀.

Chain map properties of π_*

theorem FiberBundle.piStarChainMap_q0_horizontal {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (aug : AugmentedComplex n₂ m₂ dF) (hφ : ActsAsIdentityOnHomology dB dF φ) : (piStarSummandLin dF aug 0 0 ∘ₗ twistedDhLin dB fun (b1 : Fin n₁) (b0 : Fin (baseSize n₁ m₁ 0)) => autAtDeg dF φ 0 b1 b0) = dB ∘ₗ piStarSummandLin dF aug 1 0

On the (p, 0) summand, π_* intertwines the horizontal differential with the base differential: piStar ∘ dh = dB ∘ piStar.

theorem FiberBundle.piStarChainMap_q1_vertical {n₁ m₁ n₂ m₂ : ℕ} (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (aug : AugmentedComplex n₂ m₂ dF) (p : ℤ) : piStarSummandLin dF aug p 0 ∘ₗ LinearMap.lTensor (Fin (baseSize n₁ m₁ p) → 𝔽₂) (fiberDiff n₂ m₂ dF 1 0) = 0

On the (p, 1) summand, the vertical part of the chain map sends b ⊗ f via id ⊗ dF to the (p, 0) summand, and then piStar applies ε. The composition equals zero because ε ∘ dF = 0.

Cochain map π^*

def FiberBundle.cochainPiStar {n₁ m₁ n₂ m₂ : ℕ} (dB : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dF : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) (φ : Connection n₁ m₁ n₂ m₂ dF) (aug : AugmentedComplex n₂ m₂ dF) (n : ℤ) : Module.Dual 𝔽₂ (Fin (baseSize n₁ m₁ n) → 𝔽₂) →ₗ[𝔽₂] Module.Dual 𝔽₂ ↑((fiberBundleDoubleComplex dB dF φ).totalComplex.X n)

The cochain map π* : Dual(𝔽₂^{baseSize(n)}) → Dual(Tot(B ⊠_φ F)_n) at degree n, defined as the dual (transpose) of π_*. On a cochain β ∈ B*_p, this gives π*(β)(b ⊗ f) = β(b) · ε(f) for f ∈ F₀ and π*(β)(b ⊗ f) = 0 for f ∈ F₁.

Equations

• FiberBundle.cochainPiStar dB dF φ aug n = Module.Dual.transpose (ModuleCat.Hom.hom (FiberBundle.piStarMor dB dF φ aug n))