SUPERSMOOTH SETS

The type represents supersmooth sets, defined as sheaves on the category of super Cartesian spaces with values in . Supersmooth sets extend by incorporating supersymmetry with bosonic and fermionic coordinates, used in supergeometry and quantum physics.

In Urs, interacts with graded types from , bosonic/fermionic modalities from and , differential forms in , and quantum fields in .

Formation

(Supersmooth Set Formation). The type represents supersmooth sets as sheaves on super Cartesian spaces, living in universe . The category is defined as .

def SupSmthSet : U₁ := Sh(SupCrtSp, Set)
def SupCrtSp : U₀ := ℝ^(n|q)  -- Indexed by (n, q : Nat)

Introduction

(Supersmooth Set Constructors). Terms of are constructed via plots, precomposition, gluing, and mapping spaces, reflecting the sheaf structure.

def sup-plt (n q : Nat) (X : SupSmthSet) : Set := Plt(ℝ^(n|q), X)
def sup-precomp (n q m r : Nat) (X : SupSmthSet) (f : ℝ^(m|r) → ℝ^(n|q)) (φ : sup-plt n q X)
  : sup-plt m r X := φ ∘ f
def sup-glue (n q : Nat) (X : SupSmthSet) (U : OpenCover n) (φs : Π (i : I), sup-plt (U i) q X)
    (coh : Π (i j : I), Path (sup-plt (U i ∩ U j) q X) (φs i | U i ∩ U j) (φs j | U i ∩ U j))
  : sup-plt n q X := glue U φs coh
def Maps (A B : SupSmthSet) : SupSmthSet := λ (n q : Nat), Π (x : sup-plt n q A), sup-plt n q B
def map (A B : SupSmthSet) (f : Π (n q : Nat), sup-plt n q A → sup-plt n q B) : Maps A B
 := λ (n q : Nat) (x : sup-plt n q A), f n q x
def app-map (A B : SupSmthSet) (f : Maps A B) (n q : Nat) (x : sup-plt n q A) : sup-plt n q B := f n q x
(* Supersmooth constructors: plots, precomposition, gluing, mapping spaces *)

Elimination

(Supersmooth Set Eliminators). Eliminators for extract bosonic and fermionic components of plots, linking to \mathbf{bosonic.pug} and \mathbf{fermionic.pug}.

def bosonic (n q : Nat) (X : SupSmthSet) (φ : sup-plt n q X) : plt n X := φ.1
def fermionic (n q : Nat) (X : SupSmthSet) (φ : sup-plt n q X) : ∧^q (ℝ^q)* → X := φ.2
(* Eliminators: bosonic and fermionic components *)

Theorems

(Precomposition Identity). Precomposition with the identity map on is the identity on plots.

def sup-precomp-id (n q : Nat) (X : SupSmthSet) (φ : sup-plt n q X)
  : Path (sup-plt n q X) (sup-precomp n q n q X id φ) φ := idp (sup-plt n q X) φ
(* Precomposition identity *)

(Mapping Space Beta Reduction). Application of a map matches the original function, ensuring consistency of the mapping space.

def sup-map-β (A B : SupSmthSet) (f : Π (n q : Nat), sup-plt n q A → sup-plt n q B) (n q : Nat) (x : sup-plt n q A)
  : Path (sup-plt n q B) (app-map A B (map A B f) n q x) (f n q x) := idp (sup-plt n q B) (f n q x)
(* Mapping space beta reduction *)

(Super Plot Test). A super plot on incorporates both bosonic and fermionic coordinates, with .

def test-super (X : SupSmthSet) : sup-plt 1 1 X := λ (x, θ), x + θ  -- θ² = 0
def test-super-precomp (m r : Nat) (X : SupSmthSet) (f : ℝ^(m|r) → ℝ^(>1|1))
  : sup-plt m r X := sup-precomp 1 1 m r X f (test-super X)
def test-super-id (X : SupSmthSet)
  : Path (sup-plt 1 1 X) (sup-precomp 1 1 1 1 X id (test-super X)) (test-super X)
 := sup-precomp-id 1 1 X (test-super X)
(* Super plot test *)

(Bosonic and Fermionic Components). The bosonic and fermionic components of a super plot can be extracted, linking to \mathbf{smthset.pug}.

def test-bosonic (X : SupSmthSet) : plt 1 X := bosonic 1 1 X (test-super X)
def test-fermionic (X : SupSmthSet) : ∧^1 (ℝ^1)* → X := fermionic 1 1 X (test-super X)
(* Bosonic and fermionic components *)

(Spinor Fields). For a spinor bundle , the mapping space to smooth -valued functions models spinor fields, applicable to .

def spinor-map (S : SpinorBundle) : Maps (ΠS) (λ k, C^∞(ℝ^k, ℝ))
 := map _ _ (λ n q φ, λ x, φ x)  -- Maps from super smooth set ΠS to smooth ℝ-valued functions
(* Spinor fields lemma *)