--
-- 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 ω

Ω