def CPnSetoid (n : ℕ) : Setoid { v : Fin (n + 1) → ℂ // v ≠ 0 }

The setoid on nonzero vectors in $\mathbb{C}^{n+1}$: $v \sim w$ iff $w = c v$ for some $c \in \mathbb{C}^\times$, used to define $\mathbb{CP}^n$.

def ComplexProjectiveSpace (n : ℕ) : Type

Complex projective space $\mathbb{CP}^n = (\mathbb{C}^{n+1} \setminus \{0\}) / \mathbb{C}^\times$.

@[implicit_reducible]

noncomputable instance CPn_topologicalSpace (n : ℕ) : TopologicalSpace (ComplexProjectiveSpace n)

$\mathbb{CP}^n$ carries the quotient topology from $\mathbb{C}^{n+1} \setminus \{0\}$.

@[implicit_reducible]

instance CPn_chartedSpace (n : ℕ) : ChartedSpace (EuclideanSpace ℝ (Fin (2 * n))) (ComplexProjectiveSpace n)

The smooth atlas on $\mathbb{CP}^n$ making it a $(2n)$-dimensional real charted space (via affine charts $U_i = \{[z_0 : \cdots : z_n] : z_i \ne 0\}$).

instance CPn_isManifold (n : ℕ) : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin (2 * n)))) (↑⊤) (ComplexProjectiveSpace n)

$\mathbb{CP}^n$ is a smooth (real) manifold of dimension $2n$.

@[reducible, inline]

abbrev CPn_Ω (n : ℕ) : ℕ → Type

Graded differential forms $\Omega^\bullet(\mathbb{CP}^n)$ in the DFS framework.

@[reducible, inline]

abbrev CPn_VF (n : ℕ) : Type

Vector fields $\mathfrak{X}(\mathbb{CP}^n)$ in the DFS framework.

@[implicit_reducible]

noncomputable instance instCPnDFS (n : ℕ) : DifferentialFormSpace (CPn_Ω n) (CPn_VF n)

The differential-form-space structure on $\mathbb{CP}^n$.

noncomputable def CPn_fubiniStudy (n : ℕ) : CPn_Ω n 2

The Fubini–Study $2$-form $\omega_{\mathrm{FS}}$ on $\mathbb{CP}^n$: the canonical Kähler form, locally $\omega_{\mathrm{FS}} = \frac{i}{2} \partial \bar\partial \log(1 + |z|^2)$.

noncomputable def CPn_complexStr (n : ℕ) : AlmostComplexStr

The canonical (integrable) almost complex structure $J$ on $\mathbb{CP}^n$ coming from its complex-manifold structure.

theorem CPn_fubiniStudy_closed (n : ℕ) : DifferentialFormSpace.d (CPn_VF n) (CPn_fubiniStudy n) = 0

The Fubini–Study form is closed: $d\omega_{\mathrm{FS}} = 0$.

theorem CPn_fubiniStudy_nondegenerate (n : ℕ) : Function.Injective fun (X : CPn_VF n) => DifferentialFormSpace.ι X (CPn_fubiniStudy n)

The Fubini–Study form is nondegenerate: $\iota_X \omega_{\mathrm{FS}} = 0 \implies X = 0$.

noncomputable def CPn_symplectic (n : ℕ) : SymplecticManifold (CPn_Ω n) (CPn_VF n)

$(\mathbb{CP}^n, \omega_{\mathrm{FS}})$ is a symplectic manifold.

theorem CPn_fubiniStudy_J_preserves (n : ℕ) (u v : CPn_VF n) : DifferentialFormSpace.ι ((CPn_complexStr n).J u) (DifferentialFormSpace.ι ((CPn_complexStr n).J v) (CPn_symplectic n).ω) = DifferentialFormSpace.ι u (DifferentialFormSpace.ι v (CPn_symplectic n).ω)

$J$-compatibility of $\omega_{\mathrm{FS}}$: $\omega_{\mathrm{FS}}(Ju, Jv) = \omega_{\mathrm{FS}}(u, v)$.

theorem CPn_fubiniStudy_taming (n : ℕ) : Function.Injective fun (v : CPn_VF n) => DifferentialFormSpace.ι ((CPn_complexStr n).J v) (CPn_symplectic n).ω

The Fubini–Study form tames $J$: the map $v \mapsto \omega_{\mathrm{FS}}(Jv, \cdot)$ is injective (so $g(u,v) = \omega_{\mathrm{FS}}(u, Jv)$ is a Riemannian metric).

@[implicit_reducible]

noncomputable instance instCPnHasLieBracket (n : ℕ) : HasLieBracket (CPn_Ω n) (CPn_VF n)

Vector fields on $\mathbb{CP}^n$ form a Lie algebra under the Lie bracket.

noncomputable def CPn_nijenhuisTensor (n : ℕ) : NijenhuisTensor (CPn_complexStr n)

The Nijenhuis tensor $N_J$ associated to the almost complex structure $J$ on $\mathbb{CP}^n$.

noncomputable def CPn_isNijenhuisOf (n : ℕ) : IsNijenhuisOf (CPn_complexStr n) (CPn_nijenhuisTensor n)

Witness that CPn_nijenhuisTensor n is genuinely the Nijenhuis tensor of $J$.

noncomputable def CPn_isIntegrable (n : ℕ) : IsIntegrable (CPn_complexStr n) (CPn_nijenhuisTensor n)

The almost complex structure $J$ on $\mathbb{CP}^n$ is integrable: $N_J = 0$ (so $\mathbb{CP}^n$ is a complex manifold, hence Kähler).

@[reducible]

noncomputable def CPn_compactSymplectic (n : ℕ) (_hn : 0 < n) : IsCompactSymplectic (CPn_Ω n) (CPn_VF n)

For $n \geq 1$, $\mathbb{CP}^n$ is a compact symplectic manifold.

theorem CPn_fubiniStudy_not_exact (n : ℕ) (hn : 0 < n) : ¬DifferentialFormSpace.IsExact' (CPn_VF n) (CPn_fubiniStudy n)

For $n \geq 1$, the Fubini–Study form is not exact: $[\omega_{\mathrm{FS}}] \ne 0 \in H^2(\mathbb{CP}^n)$ (otherwise the symplectic form's top power $\omega^n$ would be exact, contradicting compactness).

theorem CPn_fubiniStudy_nonzero (n : ℕ) (hn : 0 < n) : CPn_fubiniStudy n ≠ 0

For $n \geq 1$, the Fubini–Study form is nonzero (an immediate consequence of non-exactness).