structure SpinCConnection {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (spinc : SpinCStructure M Ω1 Ω2) : Type u_2

A spin-c connection on a spin-c structure: a pair of additive connections $\nabla^\pm$ on the positive/negative spinor bundles $S^\pm$, compatible with Clifford multiplication in the Leibniz sense $\nabla^-_v(\gamma(u)\psi) = \gamma(u)(\nabla^+_v\psi)$.

• nabla_plus : Ω1 → spinc.SectionsPlus → spinc.SectionsPlus
• nabla_minus : Ω1 → spinc.SectionsMinus → spinc.SectionsMinus
• nabla_plus_add (v : Ω1) (ψ₁ ψ₂ : spinc.SectionsPlus) : self.nabla_plus v (ψ₁ + ψ₂) = self.nabla_plus v ψ₁ + self.nabla_plus v ψ₂
• nabla_minus_add (v : Ω1) (φ₁ φ₂ : spinc.SectionsMinus) : self.nabla_minus v (φ₁ + φ₂) = self.nabla_minus v φ₁ + self.nabla_minus v φ₂
• leibniz_clifford (v u : Ω1) (ψ : spinc.SectionsPlus) : self.nabla_minus v (spinc.γ_plus_to_minus u ψ) = spinc.γ_plus_to_minus u (self.nabla_plus v ψ)

structure SpinCConnectionDifference {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (spinc : SpinCStructure M Ω1 Ω2) : Type u_2

The "difference" of two spin-c connections is recorded by a real $1$-form $a$ together with an imaginary factor $i$, so two spin-c connections differ by $i a \otimes \mathrm{id}_{S^\pm}$.

• a : Ω1
• imaginary_factor : ℂ

class SpinCConnectionsAffine {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (spinc : SpinCStructure M Ω1 Ω2) : Type (max 1 u_2)

The space of spin-c connections is an affine space over $\Omega^1(M)$: any two connections differ by a $1$-form, translation by $0$ is the identity, and translation is additive. This is the abstract statement that "any two spin-c connections differ by $ia \otimes \mathrm{id}_{S^\pm}$".

• ConnectionSpace : Type
• translate : Ω1 → ConnectionSpace spinc → ConnectionSpace spinc
• difference : ConnectionSpace spinc → ConnectionSpace spinc → Ω1
• translate_difference (A B : ConnectionSpace spinc) : translate (difference A B) B = A
• difference_translate (a : Ω1) (A : ConnectionSpace spinc) : difference (translate a A) A = a
• translate_zero (A : ConnectionSpace spinc) : translate 0 A = A
• translate_add (a b : Ω1) (A : ConnectionSpace spinc) : translate a (translate b A) = translate (a + b) A

noncomputable def spinc_connections_affine {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (spinc : SpinCStructure M Ω1 Ω2) : SpinCConnectionsAffine spinc

Construction of the affine-space-over-$\Omega^1$ structure on spin-c connections, for an arbitrary spin-c structure on $M$.

structure DeterminantLineBundle {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (spinc : SpinCStructure M Ω1 Ω2) : Type 1

The determinant line bundle $L = \wedge^2 S^+$: sections are antisymmetric wedge products $\psi \wedge \varphi$ of positive spinors, with $\psi \wedge \varphi = -\varphi \wedge \psi$.

• SectionsL : Type
• instACGL : AddCommGroup self.SectionsL
• instModL : Module ℝ self.SectionsL
• wedge_product : spinc.SectionsPlus → spinc.SectionsPlus → self.SectionsL
• wedge_antisymm (ψ φ : spinc.SectionsPlus) : self.wedge_product ψ φ = -self.wedge_product φ ψ

class SpinCConnectionDetermination {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (spinc : SpinCStructure M Ω1 Ω2) [aff : SpinCConnectionsAffine spinc] : Type 1

A spin-c connection is determined by its induced connection on the determinant line bundle $L = \wedge^2 S^+$. The map sending a spin-c connection $A$ to the induced connection on $L$ is a bijection.

• ConnectionOnL : Type
• induced_on_L : SpinCConnectionsAffine.ConnectionSpace spinc → ConnectionOnL spinc
• connection_determines_spinc (A₁ A₂ : SpinCConnectionsAffine.ConnectionSpace spinc) : induced_on_L A₁ = induced_on_L A₂ → A₁ = A₂
• connection_surjective (B : ConnectionOnL spinc) : ∃ (A : SpinCConnectionsAffine.ConnectionSpace spinc), induced_on_L A = B