From 9bfbb24d293375f18bf1665dacf6aa8248022bfb Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 19 Sep 2024 07:55:35 -0400
Subject: [PATCH] feat: Add start to Spin10

---
 HepLean.lean                                  |  1 +
 .../BeyondTheStandardModel/Spin10/Basic.lean  | 32 +++++++++++++++++++
 README.md                                     |  1 +
 3 files changed, 34 insertions(+)
 create mode 100644 HepLean/BeyondTheStandardModel/Spin10/Basic.lean

diff --git a/HepLean.lean b/HepLean.lean
index cb6f939..8b426be 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -47,6 +47,7 @@ import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
 import HepLean.BeyondTheStandardModel.PatiSalam.Basic
+import HepLean.BeyondTheStandardModel.Spin10.Basic
 import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.FeynmanDiagrams.Basic
 import HepLean.FeynmanDiagrams.Instances.ComplexScalar
diff --git a/HepLean/BeyondTheStandardModel/Spin10/Basic.lean b/HepLean/BeyondTheStandardModel/Spin10/Basic.lean
new file mode 100644
index 0000000..f37e9fa
--- /dev/null
+++ b/HepLean/BeyondTheStandardModel/Spin10/Basic.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.BeyondTheStandardModel.PatiSalam.Basic
+import HepLean.Meta.Informal
+/-!
+
+# The Spin(10) Model
+
+Note: By physicists this is usually called SO(10). However, the true gauge group involved
+is Spin(10).
+
+-/
+
+namespace Spin10Model
+
+informal_definition GaugeGroupI where
+  math :≈ "The group `Spin(10)`."
+  physics :≈ "The gauge group of the Spin(10) model (aka SO(10)-model.)"
+
+informal_definition embedPatiSalam where
+  physics :≈ "The embedding of the Pati-Salam gauge group into Spin(10)."
+  math :≈ "The lift of the embedding `SO(6) x SO(4) → SO(10)` to universal covers,
+    giving a homomorphism `Spin(6) x Spin(4) → Spin(10)`. Precomposed with the isomorphism,
+    ``PatiSalam.gaugeGroupISpinEquiv,
+    between `SU(4) x SU(2) x SU(2)` and `Spin(6) x Spin(4)`."
+  ref :≈ "Page 56 of https://math.ucr.edu/home/baez/guts.pdf"
+  deps :≈ [``GaugeGroupI, ``PatiSalam.GaugeGroupI, ``PatiSalam.gaugeGroupISpinEquiv]
+
+end Spin10Model
diff --git a/README.md b/README.md
index 747ca57..1d1f79c 100644
--- a/README.md
+++ b/README.md
@@ -4,6 +4,7 @@
 [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
 [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
 [![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList)
+[![](https://img.shields.io/badge/Informal_dependencies-Graph-green)](https://heplean.github.io/HepLean/graph.svg)
 [![](https://img.shields.io/badge/Lean-v4.11.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.11.0)
 
 A project to digitalize high energy physics.