noncomputable def complexStrIntertwiner {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J₀ J₁ : V →ₗ[ℝ] V) : V →ₗ[ℝ] V

The intertwiner $T = \tfrac{1}{2}(\mathrm{id} - J_1 J_0)$ between two complex structures $J_0, J_1$ on $V$, satisfying $T \circ J_0 = J_1 \circ T$.

theorem complexStr_intertwiner_commutes {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J₀ J₁ : V →ₗ[ℝ] V) (hJ₀ : SymplecticLinearAlgebra.IsComplexStructure J₀) (hJ₁ : SymplecticLinearAlgebra.IsComplexStructure J₁) : complexStrIntertwiner J₀ J₁ ∘ₗ J₀ = J₁ ∘ₗ complexStrIntertwiner J₀ J₁

The intertwiner $T = \tfrac{1}{2}(\mathrm{id} - J_1 J_0)$ commutes the complex structures: $T \circ J_0 = J_1 \circ T$.

noncomputable def firstChernClassRepManifold (Ω₂ : Type u_5) [AddCommGroup Ω₂] [Module ℝ Ω₂] (curvature : Ω₂) : Ω₂

A representative of the first Chern class $c_1(L) = \tfrac{1}{2\pi} R^\nabla$ obtained from a curvature 2-form.

theorem firstChernClass_tensor_product_additivity (Ω₂ : Type u_5) [AddCommGroup Ω₂] [Module ℝ Ω₂] (R_L R_L' : Ω₂) : firstChernClassRepManifold Ω₂ (R_L + R_L') = firstChernClassRepManifold Ω₂ R_L + firstChernClassRepManifold Ω₂ R_L'

Additivity of $c_1$ under tensor products: $c_1(L \otimes L') = c_1(L) + c_1(L')$, expressed on representatives as $\tfrac{1}{2\pi}(R + R') = \tfrac{1}{2\pi} R + \tfrac{1}{2\pi} R'$.

structure IsCompactOriented {EModel : Type u_9} [NormedAddCommGroup EModel] [NormedSpace ℝ EModel] {HModel : Type u_10} [TopologicalSpace HModel] (I : ModelWithCorners ℝ EModel HModel) (M : Type u_11) [TopologicalSpace M] [ChartedSpace HModel M] [IsManifold I ⊤ M] [CompactSpace M] (Ω : ℕ → Type u_12) [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] (d : {p : ℕ} → Ω p → Ω (p + 1)) : Type (max u_12 u_9)

Data certifying that the manifold $M$ is compact, oriented, of even real dimension $2 \dim$, and carries a non-exact volume form.

• dim : ℕ
• dim_pos : 0 < self.dim
• orientation : Orientation ℝ EModel (Fin (2 * self.dim))
• vol : Ω (2 * self.dim - 1 + 1)
• vol_not_exact : ¬∃ (β : Ω (2 * self.dim - 1)), d β = self.vol

structure IsIntegralCohomologyClass (Ω : ℕ → Type u_9) [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] (d : {p : ℕ} → Ω p → Ω (p + 1)) : Type u_9

An abstract notion of integrality of de Rham cohomology classes: a predicate isIntegral on forms closed under sums and negation, with $0$ integral and integral forms automatically closed.

• isIntegral {k : ℕ} : Ω k → Prop
• integral_closed {k : ℕ} (α : Ω k) : self.isIntegral α → d α = 0
• integral_zero (k : ℕ) : self.isIntegral 0
• integral_add {k : ℕ} (α β : Ω k) : self.isIntegral α → self.isIntegral β → self.isIntegral (α + β)
• integral_neg {k : ℕ} (α : Ω k) : self.isIntegral α → self.isIntegral (-α)

structure ComplexVectorBundleData {EModel : Type u_9} [NormedAddCommGroup EModel] [NormedSpace ℝ EModel] {HModel : Type u_10} [TopologicalSpace HModel] (I : ModelWithCorners ℝ EModel HModel) (M : Type u_11) [TopologicalSpace M] [ChartedSpace HModel M] [IsManifold I ⊤ M] (F : Type u_12) [NormedAddCommGroup F] [NormedSpace ℂ F] (E : M → Type u_13) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : M) → AddCommGroup (E x)] [(x : M) → Module ℂ (E x)] [(x : M) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle ℂ F E] (Ω : ℕ → Type u_14) [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] (d : {p : ℕ} → Ω p → Ω (p + 1)) (d_squared : ∀ {p : ℕ} (α : Ω p), d (d α) = 0) (intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d) (r : ℕ) (totalAlg : Type u_15) [CommRing totalAlg] : Type (max u_14 u_15)

Data packaging a complex vector bundle $E \to M$ of rank $r$ with a connection and curvature matrix, plus the Chern–Weil machinery (embed, extract, chernWeilParam) producing the top Chern form $c_r(E, \nabla)$ as an integral cohomology class.

• rank_pos : 0 < r
• connectionForm : Ω 1
• curvatureRep : Ω 2
• curvature_eq : d self.connectionForm = self.curvatureRep
• curvatureMatrix : Matrix (Fin r) (Fin r) (Ω 2)
• curvatureMatrix_closed (i j : Fin r) : d (self.curvatureMatrix i j) = 0
• embed : Ω 2 → totalAlg
• extract : totalAlg → Ω (2 * r - 1 + 1)
• chernWeilParam : totalAlg
• embed_add (a b : Ω 2) : self.embed (a + b) = self.embed a + self.embed b
• extract_add (a b : totalAlg) : self.extract (a + b) = self.extract a + self.extract b
• extract_one : self.extract 1 = 0
• chernWeil_zero : self.extract (totalChernForm (Matrix.map 0 self.embed) self.chernWeilParam) = 0
• chernWeil_closed (A : Matrix (Fin r) (Fin r) (Ω 2)) : (∀ (i j : Fin r), d (A i j) = 0) → d (self.extract (totalChernForm (A.map self.embed) self.chernWeilParam)) = 0
• chernWeil_smul (c : ℝ) (A : Matrix (Fin r) (Fin r) (Ω 2)) : self.extract (totalChernForm ((c • A).map self.embed) self.chernWeilParam) = c ^ r • self.extract (totalChernForm (A.map self.embed) self.chernWeilParam)
• chernWeil_nontrivial : ∃ (A : Matrix (Fin r) (Fin r) (Ω 2)), self.extract (totalChernForm (A.map self.embed) self.chernWeilParam) ≠ 0
• chernWeil_perm (σ : Equiv.Perm (Fin r)) (A : Matrix (Fin r) (Fin r) (Ω 2)) : self.extract (totalChernForm ((A.submatrix ⇑σ ⇑σ).map self.embed) self.chernWeilParam) = self.extract (totalChernForm (A.map self.embed) self.chernWeilParam)
• chernWeil_alternating (A : Matrix (Fin r) (Fin r) (Ω 2)) (i j : Fin r) : i ≠ j → (∀ (k : Fin r), A i k = A j k) → self.extract (totalChernForm (A.map self.embed) self.chernWeilParam) = 0
• topChernRep_integral : intCoh.isIntegral (self.extract (totalChernForm (self.curvatureMatrix.map self.embed) self.chernWeilParam))

structure EulerClassData (Ω : ℕ → Type u_9) [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] (d : {p : ℕ} → Ω p → Ω (p + 1)) (intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d) (r : ℕ) (curvatureMatrix : Matrix (Fin r) (Fin r) (Ω 2)) : Type u_9

Data carrying a representative of the Euler class $e(E) \in H^{2r}(M, \mathbb{Z})$ via the Pfaffian of the curvature matrix, together with the signed count of zeros of a generic section.

• pfaffianMap : Matrix (Fin r) (Fin r) (Ω 2) → Ω (2 * r - 1 + 1)
• eulerRep : Ω (2 * r - 1 + 1)
• eulerRep_eq_pfaffian : self.eulerRep = self.pfaffianMap curvatureMatrix
• eulerRep_closed : d self.eulerRep = 0
• pfaffian_zero : self.pfaffianMap 0 = 0
• pfaffian_homogeneous (c : ℝ) (A : Matrix (Fin r) (Fin r) (Ω 2)) : self.pfaffianMap (c • A) = c ^ r • self.pfaffianMap A
• pfaffian_closed (A : Matrix (Fin r) (Fin r) (Ω 2)) : (∀ (i j : Fin r), d (A i j) = 0) → d (self.pfaffianMap A) = 0
• eulerRep_integral : intCoh.isIntegral self.eulerRep
• sectionZeroCount : ℤ
• sectionZeroCount_spec : curvatureMatrix = 0 → self.sectionZeroCount = 0

theorem EulerClassData.eulerRep_trivial {Ω : ℕ → Type u_9} [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] {d : {p : ℕ} → Ω p → Ω (p + 1)} {intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d} {r : ℕ} {curvatureMatrix : Matrix (Fin r) (Fin r) (Ω 2)} (euler : EulerClassData Ω (fun {p : ℕ} => d) intCoh r curvatureMatrix) (h : curvatureMatrix = 0) : euler.eulerRep = 0

If the curvature matrix vanishes then the Euler representative vanishes: $\mathrm{Pf}(0) = 0$.

def ComplexVectorBundleData.chernWeilMapDef {EModel : Type u_2} [NormedAddCommGroup EModel] [NormedSpace ℝ EModel] {HModel : Type u_3} [TopologicalSpace HModel] {I : ModelWithCorners ℝ EModel HModel} {M : Type u_4} [TopologicalSpace M] [ChartedSpace HModel M] [IsManifold I ⊤ M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : M) → AddCommGroup (E x)] [(x : M) → Module ℂ (E x)] [(x : M) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle ℂ F E] {Ω : ℕ → Type u_7} [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] {d : {p : ℕ} → Ω p → Ω (p + 1)} {d_squared : ∀ {p : ℕ} (α : Ω p), d (d α) = 0} {r : ℕ} {totalAlg : Type u_8} [CommRing totalAlg] {intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d} (bundle : ComplexVectorBundleData I M F E Ω (fun {p : ℕ} => d) ⋯ intCoh r totalAlg) (A : Matrix (Fin r) (Fin r) (Ω 2)) : Ω (2 * r - 1 + 1)

The Chern–Weil map applied to a curvature-like matrix $A$, producing the corresponding characteristic form via embed and extract.

def ComplexVectorBundleData.topChernRep {EModel : Type u_2} [NormedAddCommGroup EModel] [NormedSpace ℝ EModel] {HModel : Type u_3} [TopologicalSpace HModel] {I : ModelWithCorners ℝ EModel HModel} {M : Type u_4} [TopologicalSpace M] [ChartedSpace HModel M] [IsManifold I ⊤ M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : M) → AddCommGroup (E x)] [(x : M) → Module ℂ (E x)] [(x : M) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle ℂ F E] {Ω : ℕ → Type u_7} [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] {d : {p : ℕ} → Ω p → Ω (p + 1)} {d_squared : ∀ {p : ℕ} (α : Ω p), d (d α) = 0} {r : ℕ} {totalAlg : Type u_8} [CommRing totalAlg] {intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d} (bundle : ComplexVectorBundleData I M F E Ω (fun {p : ℕ} => d) ⋯ intCoh r totalAlg) : Ω (2 * r - 1 + 1)

The top Chern form representative $c_r(E, \nabla)$ obtained from the bundle's curvature matrix via Chern–Weil.

theorem ComplexVectorBundleData.topChernRep_closed {EModel : Type u_2} [NormedAddCommGroup EModel] [NormedSpace ℝ EModel] {HModel : Type u_3} [TopologicalSpace HModel] {I : ModelWithCorners ℝ EModel HModel} {M : Type u_4} [TopologicalSpace M] [ChartedSpace HModel M] [IsManifold I ⊤ M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : M) → AddCommGroup (E x)] [(x : M) → Module ℂ (E x)] [(x : M) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle ℂ F E] {Ω : ℕ → Type u_7} [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] {d : {p : ℕ} → Ω p → Ω (p + 1)} {d_squared : ∀ {p : ℕ} (α : Ω p), d (d α) = 0} {r : ℕ} {totalAlg : Type u_8} [CommRing totalAlg] {intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d} (bundle : ComplexVectorBundleData I M F E Ω (fun {p : ℕ} => d) ⋯ intCoh r totalAlg) : d bundle.topChernRep = 0

The top Chern form $c_r(E, \nabla)$ is closed, $d c_r = 0$.

theorem ComplexVectorBundleData.curvature_closed {EModel : Type u_2} [NormedAddCommGroup EModel] [NormedSpace ℝ EModel] {HModel : Type u_3} [TopologicalSpace HModel] {I : ModelWithCorners ℝ EModel HModel} {M : Type u_4} [TopologicalSpace M] [ChartedSpace HModel M] [IsManifold I ⊤ M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : M) → AddCommGroup (E x)] [(x : M) → Module ℂ (E x)] [(x : M) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle ℂ F E] {Ω : ℕ → Type u_7} [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] {d : {p : ℕ} → Ω p → Ω (p + 1)} {d_squared : ∀ {p : ℕ} (α : Ω p), d (d α) = 0} {r : ℕ} {totalAlg : Type u_8} [CommRing totalAlg] {intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d} (bundle : ComplexVectorBundleData I M F E Ω (fun {p : ℕ} => d) ⋯ intCoh r totalAlg) : d bundle.curvatureRep = 0

The curvature 2-form $R^\nabla$ is closed: since $R = d \omega$ and $d^2 = 0$.

theorem top_chern_eq_euler_axiom {EModel : Type u_9} [NormedAddCommGroup EModel] [NormedSpace ℝ EModel] {HModel : Type u_10} [TopologicalSpace HModel] {I : ModelWithCorners ℝ EModel HModel} {M : Type u_11} [TopologicalSpace M] [ChartedSpace HModel M] [IsManifold I ⊤ M] [CompactSpace M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : M → Type u_13} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : M) → AddCommGroup (E x)] [(x : M) → Module ℂ (E x)] [(x : M) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle ℂ F E] {Ω : ℕ → Type u_14} [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] {d : {p : ℕ} → Ω p → Ω (p + 1)} {d_squared : ∀ {p : ℕ} (α : Ω p), d (d α) = 0} (intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d) (hCO : IsCompactOriented I M Ω fun {p : ℕ} => d) (r : ℕ) {totalAlg : Type u_15} [CommRing totalAlg] (bundle : ComplexVectorBundleData I M F E Ω (fun {p : ℕ} => d) ⋯ intCoh r totalAlg) (euler : EulerClassData Ω (fun {p : ℕ} => d) intCoh r bundle.curvatureMatrix) : ∃ (β : Ω (2 * r - 1)), d β = bundle.topChernRep - euler.eulerRep

Axiomatic form of Proposition 1: on a compact oriented manifold, the top Chern class equals the Euler class, $c_r(E) = e(E) \in H^{2r}(M, \mathbb{Z})$ — equivalently, $c_r - e$ is exact.

theorem top_chern_eq_euler_class {EModel : Type u_9} [NormedAddCommGroup EModel] [NormedSpace ℝ EModel] {HModel : Type u_10} [TopologicalSpace HModel] {I : ModelWithCorners ℝ EModel HModel} {M : Type u_11} [TopologicalSpace M] [ChartedSpace HModel M] [IsManifold I ⊤ M] [CompactSpace M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace ℂ F] {E : M → Type u_13} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : M) → AddCommGroup (E x)] [(x : M) → Module ℂ (E x)] [(x : M) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle ℂ F E] {Ω : ℕ → Type u_14} [(p : ℕ) → AddCommGroup (Ω p)] [(p : ℕ) → Module ℝ (Ω p)] {d : {p : ℕ} → Ω p → Ω (p + 1)} {d_squared : ∀ {p : ℕ} (α : Ω p), d (d α) = 0} (intCoh : IsIntegralCohomologyClass Ω fun {p : ℕ} => d) (hCO : IsCompactOriented I M Ω fun {p : ℕ} => d) (r : ℕ) {totalAlg : Type u_15} [CommRing totalAlg] (bundle : ComplexVectorBundleData I M F E Ω (fun {p : ℕ} => d) ⋯ intCoh r totalAlg) (euler : EulerClassData Ω (fun {p : ℕ} => d) intCoh r bundle.curvatureMatrix) : ∃ (β : Ω (2 * r - 1)), d β = bundle.topChernRep - euler.eulerRep

Proposition 1: on a compact oriented manifold of real dimension $2r$, the top Chern class of a rank-$r$ complex vector bundle equals its Euler class, $c_r(E) = e(E) \in H^{2r}(M, \mathbb{Z})$.