class SmoothVectorBundleDFS {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] (I : ModelWithCorners ℝ EM HM) (M : Type u_3) [TopologicalSpace M] [ChartedSpace HM M] (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (V : M → Type u_5) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle ℝ F V] : Prop

Typeclass wrapper recording that a vector bundle $V \to M$ has smooth transition functions (modeled in the DFS framework).

• smoothTransitions : ContMDiffVectorBundle ⊤ F V I

def SmoothSections {M : Type u_1} (V : M → Type u_2) : Type (max u_1 u_2)

The space of (smooth) sections of a vector bundle $V \to M$, identified with the dependent function type $\prod_{x \in M} V_x$.

@[implicit_reducible]

instance SmoothSections.instAddCommGroup {M : Type u_1} {V : M → Type u_2} [(x : M) → AddCommGroup (V x)] : AddCommGroup (SmoothSections V)

Sections form an abelian group under pointwise addition.

@[implicit_reducible]

instance SmoothSections.instModule {M : Type u_1} {V : M → Type u_2} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] : Module ℝ (SmoothSections V)

Sections form a real vector space under pointwise scalar multiplication.

def SmoothSections.eval {M : Type u_1} {V : M → Type u_2} (σ : SmoothSections V) (x : M) : V x

Evaluation of a section $\sigma$ at a point $x \in M$.

@[implicit_reducible]

instance SmoothSections.instZero {M : Type u_1} {V : M → Type u_2} [(x : M) → Zero (V x)] : Zero (SmoothSections V)

The zero section of a vector bundle.

structure ConnectionDFS {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] (I : ModelWithCorners ℝ EM HM) (M : Type u_3) [TopologicalSpace M] [ChartedSpace HM M] (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (V : M → Type u_5) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] : Type (max (max u_1 u_3) u_5)

A connection $\nabla$ on a vector bundle $V \to M$: a covariant derivative sending a section $\sigma$ and a tangent vector $X_x$ to $\nabla_X \sigma \in V_x$.

• nabla : ((x : M) → V x) → (x : M) → TangentSpace I x →L[ℝ] V x
• isCovariantDerivative : IsCovariantDerivativeOn F self.nabla

noncomputable def ConnectionDFS.apply {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_3} [TopologicalSpace M] [ChartedSpace HM M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] (conn : ConnectionDFS I M F V) (σ : (x : M) → V x) (x : M) (X : TangentSpace I x) : V x

Apply a connection: $(\nabla_X \sigma)_x = \mathtt{conn.apply}\ \sigma\ x\ X$.

noncomputable def ConnectionDFS.difference {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_3} [TopologicalSpace M] [ChartedSpace HM M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] (conn₁ conn₂ : ConnectionDFS I M F V) : ((x : M) → V x) → (x : M) → TangentSpace I x →L[ℝ] V x

The difference $\nabla_1 - \nabla_2$ of two connections (an $\mathrm{End}(V)$-valued $1$-form).

structure NormalBundleData {EN : Type u_1} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_2} [TopologicalSpace HN] (IN : ModelWithCorners ℝ EN HN) (N : Type u_3) [TopologicalSpace N] [ChartedSpace HN N] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] (IM : ModelWithCorners ℝ EM HM) (M : Type u_6) [TopologicalSpace M] [ChartedSpace HM M] : Type (max (max u_3 u_6) (u_7 + 1))

Data for the normal bundle of an embedding $\iota : N \hookrightarrow M$: fibers $\mathcal{N}_x$, module structure, and the normal rank.

• ι : N → M
• NormalFiber : N → Type u_7
• instACG (x : N) : AddCommGroup (self.NormalFiber x)
• instMod (x : N) : Module ℝ (self.NormalFiber x)
• normalRank : ℕ

structure SpinCStructureDFS {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] (I : ModelWithCorners ℝ EM HM) (M : Type u_3) [TopologicalSpace M] [ChartedSpace HM M] [IsManifold I ⊤ M] : Type (max (max (max u_1 u_3) (u_4 + 1)) (u_5 + 1))

A $\operatorname{Spin}^{\mathbb{C}}$ structure on $M$: complex spinor bundles $W^+, W^-$ with Clifford multiplication maps $\gamma_{\pm} : TM \otimes W^{\pm} \to W^{\mp}$ and first Chern class $c_1$ of the determinant line bundle.

• SpinorPlusFiber : M → Type u_4
• SpinorMinusFiber : M → Type u_5
• instACG_plus (x : M) : AddCommGroup (self.SpinorPlusFiber x)
• instMod_plus (x : M) : Module ℂ (self.SpinorPlusFiber x)
• instACG_minus (x : M) : AddCommGroup (self.SpinorMinusFiber x)
• instMod_minus (x : M) : Module ℂ (self.SpinorMinusFiber x)
• γ_plus_to_minus (x : M) : TangentSpace I x → self.SpinorPlusFiber x →ₗ[ℂ] self.SpinorMinusFiber x
• γ_minus_to_plus (x : M) : TangentSpace I x → self.SpinorMinusFiber x →ₗ[ℂ] self.SpinorPlusFiber x
• c₁ : ℤ

@[implicit_reducible]

instance SpinCStructureDFS.instACGPlus {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_3} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold I ⊤ M] (spinc : SpinCStructureDFS I M) (x : M) : AddCommGroup (spinc.SpinorPlusFiber x)

The positive spinor fiber $W^+_x$ inherits an abelian group structure.

@[implicit_reducible]

instance SpinCStructureDFS.instModPlus {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_3} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold I ⊤ M] (spinc : SpinCStructureDFS I M) (x : M) : Module ℂ (spinc.SpinorPlusFiber x)

The positive spinor fiber $W^+_x$ is a complex vector space.

@[implicit_reducible]

instance SpinCStructureDFS.instACGMinus {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_3} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold I ⊤ M] (spinc : SpinCStructureDFS I M) (x : M) : AddCommGroup (spinc.SpinorMinusFiber x)

The negative spinor fiber $W^-_x$ inherits an abelian group structure.

@[implicit_reducible]

instance SpinCStructureDFS.instModMinus {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_3} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold I ⊤ M] (spinc : SpinCStructureDFS I M) (x : M) : Module ℂ (spinc.SpinorMinusFiber x)

The negative spinor fiber $W^-_x$ is a complex vector space.

def SpinCStructureDFS.SectionsPlus {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_3} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold I ⊤ M] (spinc : SpinCStructureDFS I M) : Type (max u_4 u_3)

Sections $\Gamma(W^+)$ of the positive spinor bundle.

def SpinCStructureDFS.SectionsMinus {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_2} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_3} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold I ⊤ M] (spinc : SpinCStructureDFS I M) : Type (max u_5 u_3)

Sections $\Gamma(W^-)$ of the negative spinor bundle.