egison-5.0.0: sample/math/geometry/chern-form-of-CP2.egi
--
-- Chern form of CP2 (Fubini-Study connection)
--
-- z1, z2: holomorphic coordinates
-- z1b, z2b: anti-holomorphic coordinates (z-bar)
--
declare symbol z1, z2, z1b, z2b
-- Holomorphic exterior derivative (∂)
def dh (X : MathExpr) : DiffForm MathExpr := !(flip ∂/∂) [| z1, z2 |] X
-- Anti-holomorphic exterior derivative (∂̄)
def da (X : MathExpr) : DiffForm MathExpr := !(flip ∂/∂) [| z1b, z2b |] X
def h := 1 + z1 * z1b + z2 * z2b
-- Connection 1-form: ω = ∂ log(h)
-- ω = [z1b/h, z2b/h]
def ω := dh (log h)
assertEqual "ω"
ω
[| z1b / (1 + z1 * z1b + z2 * z2b)
, z2b / (1 + z1 * z1b + z2 * z2b) |]
-- Curvature 2-form: Ω = ∂̄ω = ∂̄∂ log(h)
-- Ω_ij = ∂ωi/∂z̄j = (h*δij - z̄i*zj) / h²
def Ω := da ω
Ω