structure ComplexDifferentialFormAlgebra (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] (R : Type u_3) [CommRing R] [Algebra ℂ R] [IsGradedFormAlgebra R] : Type (max u_1 u_3)

A $\mathbb{C}$-algebra $R$ realizing the graded algebra of complex differential forms: each $\Omega^p$ embeds $\mathbb{R}$-linearly into a homogeneous component of degree $p$ in $R$, with an inverse extraction map.

• embed (p : ℕ) : Ω p → R
• embed_linear (p : ℕ) (a b : Ω p) (c : ℝ) : self.embed p (c • a + b) = (algebraMap ℝ R) c * self.embed p a + self.embed p b
• embed_homog (p : ℕ) (α : Ω p) : IsGradedFormAlgebra.IsHomog (self.embed p α) p
• extract (p : ℕ) : R → Ω p
• extract_embed (p : ℕ) (α : Ω p) : self.extract p (self.embed p α) = α

structure ChernFormGeometricData (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E_mod : Type u_2) [NormedAddCommGroup E_mod] [NormedSpace 𝕜 E_mod] (H : Type u_3) [TopologicalSpace H] (I : ModelWithCorners 𝕜 E_mod H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : M → Type u_6) [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] (r : ℕ) (Ω : ℕ → Type u_7) (VF : Type u_8) [DifferentialFormSpace Ω VF] (R : Type u_9) [CommRing R] [Algebra ℂ R] [IsGradedFormAlgebra R] : Type (max (max (max (max u_2 u_4) u_6) u_7) u_9)

All geometric data needed to define the Chern forms of a rank-$r$ vector bundle $V \to M$ with connection $\nabla$: the connection, its curvature $R^\nabla$ (antisymmetric in tangent vectors), an embedding of the form algebra into a $\mathbb{C}$-algebra $R$, the $r \times r$ curvature matrix realised in $R$ (with each entry homogeneous of degree $2$), and a "degree-$0$ scalar" hypothesis on the leading Chern scalar.

• connection : CovariantDerivative I F V
• curvature (x : M) : TangentSpace I x → TangentSpace I x → V x →L[𝕜] V x
• curvature_antisymm (x : M) (X Y : TangentSpace I x) : self.curvature x X Y = -self.curvature x Y X
• formAlgebra : ComplexDifferentialFormAlgebra Ω VF R
• curvatureMatrix : Matrix (Fin r) (Fin r) R
• curvatureMatrix_deg2 : CurvatureMatrixDegreeTwo self.curvatureMatrix
• chernScalar_deg0 : ChernScalarHomogZero

noncomputable def totalChernFormGeometric {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E_mod : Type u_2} [NormedAddCommGroup E_mod] [NormedSpace 𝕜 E_mod] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E_mod H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [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] {r : ℕ} {Ω : ℕ → Type u_7} {VF : Type u_8} [DifferentialFormSpace Ω VF] {R : Type u_9} [CommRing R] [Algebra ℂ R] [IsGradedFormAlgebra R] (data : ChernFormGeometricData 𝕜 E_mod H I M F V r Ω VF R) : R

The total Chern form of $(E, \nabla)$: $$c(E, \nabla) = \det\!\left(I + \frac{i}{2\pi} R^\nabla\right) \in \Omega^\bullet(M, \mathbb{C}),$$ defined via the curvature matrix and the appropriate scalar normalization.

noncomputable def chernFormDegree {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E_mod : Type u_2} [NormedAddCommGroup E_mod] [NormedSpace 𝕜 E_mod] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E_mod H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [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] {r : ℕ} {Ω : ℕ → Type u_7} {VF : Type u_8} [DifferentialFormSpace Ω VF] {R : Type u_9} [CommRing R] [Algebra ℂ R] [IsGradedFormAlgebra R] (data : ChernFormGeometricData 𝕜 E_mod H I M F V r Ω VF R) (j : ℕ) : R

The $j$-th Chern form $c_j(E, \nabla) \in \Omega^{2j}(M, \mathbb{C})$, obtained as the degree-$2j$ component of the total Chern form $\det(I + \frac{i}{2\pi} R^\nabla) = \sum_j c_j$.