A connection $\nabla: C^\infty(M, E) \to \Omega^1(M, E)$ on a vector bundle: an $\mathbb{R}$-linear map satisfying the Leibniz rule $\nabla(f\sigma) = df \cdot \sigma + f \nabla \sigma$.
- nabla : Sections → FormsWithValues
Instances For
The trivial zero connection on $\mathbb{R}$, serving as a base example.
Instances For
The space of connections is an affine space: adding an $\mathrm{End}(E)$-valued one-form $B$ to a connection $\nabla$ gives a new connection $\nabla + B$.
Instances For
The covariant derivative $\nabla_v \sigma$ of a section $\sigma$ along a vector field $v$, obtained by evaluating $\nabla\sigma \in \Omega^1(M, E)$ on $v$.
Instances For
A connection $\nabla$ is metric-compatible with a metric $\langle\cdot,\cdot\rangle$ iff $d\langle \sigma, \sigma'\rangle = \langle \nabla\sigma, \sigma'\rangle + \langle \sigma, \nabla\sigma'\rangle$.
Instances For
A ring $R$ equipped with a differential $d$ satisfying $d \circ d = 0$, abstracting the exterior derivative on matrix-valued forms.
Instances
The curvature tensor $R^\nabla: \mathfrak{X}(M) \times \mathfrak{X}(M) \to \mathrm{End}(E)$, which is antisymmetric in its two vector-field arguments.
- R : VectorFields → VectorFields → EndSections
Instances For
Gauge transformation law for curvature (Proposition 2): under a change of frame $g$ with $g \cdot A' = A \cdot g + dg$, the curvature transforms as $dA' + A' \wedge A' = g^{-1}(dA + A \wedge A) g$.
The Chern normalization constant $\frac{i}{2\pi}$ appearing in $c(E,\nabla) = \det(I + \frac{i}{2\pi} R^\nabla)$.
Instances For
Definitional equality between totalChernFormWithScalar and totalChernForm evaluated at $\frac{i}{2\pi}$.
Bundle of data required to define Chern forms on a vector bundle of rank $r$: a connection, its curvature 2-form (antisymmetric in $X, Y$), and the local curvature matrix in some frame.
- connection : CovariantDerivative I F V
- curvature (x : M) : TangentSpace I x → TangentSpace I x → V x →L[𝕜] V x
Instances For
The total Chern form of a connection, computed from its curvature matrix via the $\frac{i}{2\pi}$-normalized $\det(I + \cdot)$ formula.
Instances For
A graded form algebra: a commutative ring with a notion of homogeneous degree-$p$ elements, projection maps onto each degree, and the usual graded multiplication property. Used to encode the bidegree structure of $\Omega^\bullet(M)$.
Instances
Assertion that the curvature matrix has every entry of homogeneous degree 2 (i.e., a 2-form).
Instances For
The $j$-th Chern class form $c_j$: the degree-$2j$ component of the total Chern form.
Instances For
The $j$-th Chern class form is homogeneous of degree $2j$.
The total Chern form has no components of odd degree, since the curvature is a 2-form.
Decomposition of the total Chern form: $c(E,\nabla) = \sum_{j=0}^{r} c_j(E,\nabla)$.
Assertion that the Chern normalization scalar $\frac{i}{2\pi}$ has graded degree 0.
Instances For
Odd-degree components of the Chern form (with $\frac{i}{2\pi}$ normalization) vanish.
The $j$-th Chern class form with the $\frac{i}{2\pi}$ normalization: the degree-$2j$ part of $\det(I + \frac{i}{2\pi} R^\nabla)$.
Instances For
Decomposition $c(E,\nabla) = \sum_{j=0}^{r} c_j(E,\nabla)$ with $\frac{i}{2\pi}$ normalization.
The normalized $j$-th Chern class form is homogeneous of degree $2j$.
A connection on a line bundle, given locally by a connection 1-form $A \in \Omega^1$ with curvature $R^\nabla = dA \in \Omega^2$ automatically closed.
- A : Ω 1
- curvature : Ω 2
Instances For
A representative of the first Chern class of a line bundle: $c_1(L) = [\frac{1}{2\pi} R^\nabla]$.
Instances For
Unfolding lemma: $c_1$ representative equals $\frac{1}{2\pi} R^\nabla$ by definition.
The first Chern class representative of a line bundle connection: $\frac{1}{2\pi} R^\nabla$.
Instances For
The first Chern class form $\frac{1}{2\pi} R^\nabla$ is closed if the curvature is closed.
Data for the Chern connection in a holomorphic frame: a connection form $A$ with the decomposition $d = \partial + \bar\partial$ and the identity $\partial A = -A \wedge A$.
- A : R
- d : R → R
- del : R → R
- dbar : R → R
Instances For
Construction of holomorphic frame data starting from a Hermitian metric, with connection form $A = h^{-1} \partial h$.
Instances For
Opaque predicate stating that a vector bundle admits a holomorphic structure.
Opaque predicate stating that $\bar\partial_\nabla^2 = 0$ for the $(0,1)$-part of $\nabla$.
Opaque predicate stating that the $(0,2)$-part of the curvature vanishes.
A vector bundle admits a holomorphic structure iff $\bar\partial_\nabla^2 = 0$.
The condition $\bar\partial_\nabla^2 = 0$ is equivalent to the vanishing of the $(0,2)$-part of the curvature.
A holomorphic vector bundle: a graded space of bundle-valued forms equipped with a Dolbeault operator $\bar\partial_E$ satisfying $\bar\partial_E^2 = 0$.
Instances For
A $\bar\partial_E$-closed form of bidegree $(0,q)$ with values in $E$, representing a Dolbeault cohomology class in $H^{0,q}(M, E)$.
- representative : BundleValuedForms q
Instances For
Cohomological equivalence: two $(0,q+1)$-forms represent the same Dolbeault class iff their difference is $\bar\partial_E$-exact.
Instances For
The Chern connection on a Hermitian holomorphic bundle: the unique connection compatible with the Hermitian metric $h$ whose $(0,1)$-part is $\bar\partial$, with connection form $A = h^{-1} \partial h$.
- del : R → R
- dbar : R → R
- d : R → R
- h : R
- h_inv : R
- A : R