DIFFERENTIAL K-THEORY TYPE

The type represents differential K-theory, a refinement of generalized K-theory that incorporates differential forms and connections. It is a key construct in physics, particularly for modeling topological invariants in quantum field theory and string theory. By combining K-theory classes with differential data, it enables precise descriptions of phenomena like gauge fields and anomalies.

operates within the cohesive type system, interacting with smooth sets and groupoids , and is typed as a spectrum, reflecting its role in stable homotopy theory.

Formation

(-Formation). The differential K-theory type is formed over a smooth set , a groupoid , a twist , and a connection , yielding a type in the spectrum universe.

type exp =
  | DiffKU^G of exp * exp * exp * exp  (* DiffKU^G X G τ conn *)

Introduction

(-Introduction). A term of type is introduced by constructing a differential K-theory class, combining an underlying K-theory class in with a compatible connection .

let diffKU^G-intro (x : exp) (g : exp) (tau : exp) (conn : exp) : exp =
    DiffKU^G (x, g, tau, conn)

Elimination

(-Elimination). The eliminator for allows reasoning about differential K-theory classes by projecting them to their underlying K-theory classes in and their differential data in , preserving the spectrum structure.

let KU_\flat^G_ind (x : exp) (g : exp) (tau : exp) (beta : exp) (h : exp) : exp =
    (* Hypothetical eliminator *)
    App (Var "KU_\flat^GInd", DiffKU^G (x, g, tau, Var "conn"))

Theorems

(Differential K-Theory Refinement). The type refines by incorporating a connection , with a projection map preserving the underlying K-theory class.

let diffKU^G_to_KU^G (x : exp) (g : exp) (tau : exp) (conn : exp) : exp =
    KU^G (x, g, tau)