EXTERIOR DERIVATIVE TYPE

The type represents the exterior derivative, a fundamental operation in differential geometry that maps a differential -form to an -form on a smooth set. It is essential for modeling differential cohomology and physical systems involving fields, such as electromagnetism.

interacts with the type, operating within the cohesive type system’s smooth sets (), and ensures properties like the nilpotency of the derivative, critical for exactness and cohomology.

Formation

(-Formation). The exterior derivative type is formed for a differential -form on a smooth set , yielding an -form .

type exp =
  | Diff of int * exp  (* Diff n ω *)

Introduction

(-Introduction). A term of type is introduced by applying the exterior derivative to a differential -form , producing .

let diff_intro (n : int) (omega : exp) : exp =
    Diff (n, omega)

Elimination

(-Elimination). The eliminator for enables reasoning about -forms by relating them to their preimages under the exterior derivative, supporting properties like exactness or applications of Stokes’ theorem.

let diff_ind (n : int) (x : exp) (beta : exp) (h : exp) : exp =
    (* Hypothetical eliminator *)
    App (Var "DiffInd", Diff (n, Var "omega"))

Computation

(-Computation). The exterior derivative is nilpotent, satisfying , so applying to yields the zero -form.

let reduce env ctx = function
  | Diff (n, Diff (m, omega)) -> Forms (n + 2, Var "X") (* Simplified to zero form *)
  | _ -> ...

Theorems

(Stokes’ Theorem). For a differential -form on a smooth set with boundary , the exterior derivative satisfies Stokes’ theorem, relating the integral of over the boundary to the integral of over .

let stokes_theorem (n : int) (x : exp) (omega : exp) : exp =
    (* Hypothetical boundary integral *)
    App (Var "integral", Diff (n, omega))