Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: basic structures for Two Real Scalars #243

Merged
merged 1 commit into from
Nov 19, 2024
Merged

feat: basic structures for Two Real Scalars #243

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions HepLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ import HepLean.BeyondTheStandardModel.TwoHDM.GaugeOrbits
import HepLean.FeynmanDiagrams.Basic
import HepLean.FeynmanDiagrams.Instances.ComplexScalar
import HepLean.FeynmanDiagrams.Instances.Phi4
import HepLean.FeynmanDiagrams.Instances.TwoRealScalar
import HepLean.FeynmanDiagrams.Momentum
import HepLean.FlavorPhysics.CKMMatrix.Basic
import HepLean.FlavorPhysics.CKMMatrix.Invariants
Expand Down
48 changes: 48 additions & 0 deletions HepLean/FeynmanDiagrams/Instances/TwoRealScalar.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
/-
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.FeynmanDiagrams.Basic
/-!

# Feynman rules for a two complex scalar fields

This file serves as a demonstration of a new approach to Feynman rules.

-/

namespace TwoComplexScalar
open CategoryTheory
open FeynmanDiagram
open PreFeynmanRule

/-- The colors of edges which one can associate with a vertex for a theory
with two complex scalar fields. -/
inductive 𝓔 where
/-- Corresponds to the first complex scalar field flowing out of a vertex. -/
| complexScalarOut₁ : 𝓔
/-- Corresponds to the first complex scalar field flowing into a vertex. -/
| complexScalarIn₁ : 𝓔
/-- Corresponds to the second complex scalar field flowing out of a vertex. -/
| complexScalarOut₂ : 𝓔
/-- Corresponds to the second complex scalar field flowing into a vertex. -/
| complexScalarIn₂ : 𝓔

/-- The map taking each color to it's dual, specifying how we can contract edges. -/
def ξ : 𝓔 → 𝓔
| 𝓔.complexScalarOut₁ => 𝓔.complexScalarIn₁
| 𝓔.complexScalarIn₁ => 𝓔.complexScalarOut₁
| 𝓔.complexScalarOut₂ => 𝓔.complexScalarIn₂
| 𝓔.complexScalarIn₂ => 𝓔.complexScalarOut₂

/-- The function `ξ` is an involution. -/
lemma ξ_involutive : Function.Involutive ξ := by
intro x
match x with
| 𝓔.complexScalarOut₁ => rfl
| 𝓔.complexScalarIn₁ => rfl
| 𝓔.complexScalarOut₂ => rfl
| 𝓔.complexScalarIn₂ => rfl

end TwoComplexScalar