docs: More doc strings
This commit is contained in:
jstoobysmith
parent
a00a1020a8
commit
c24029c9ca
7 changed files with 47 additions and 0 deletions
|
|
@ -137,14 +137,17 @@ class IsFinitePreFeynmanRule (P : PreFeynmanRule) where
|
|||
/-- The type of half-edges associated with an edge is decidable. -/
|
||||
edgeMapDecidable : ∀ v : P.EdgeLabel, DecidableEq (P.edgeLabelMap v).left
|
||||
|
||||
/-- If `P` is a finite pre feynman rule, then equality of edge labels of `P` is decidable. -/
|
||||
instance preFeynmanRuleDecEq𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
|
||||
DecidableEq P.EdgeLabel :=
|
||||
IsFinitePreFeynmanRule.edgeLabelDecidable
|
||||
|
||||
/-- If `P` is a finite pre feynman rule, then equality of vertex labels of `P` is decidable. -/
|
||||
instance preFeynmanRuleDecEq𝓥 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
|
||||
DecidableEq P.VertexLabel :=
|
||||
IsFinitePreFeynmanRule.vertexLabelDecidable
|
||||
|
||||
/-- If `P` is a finite pre feynman rule, then equality of half-edge labels of `P` is decidable. -/
|
||||
instance preFeynmanRuleDecEq𝓱𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
|
||||
DecidableEq P.HalfEdgeLabel :=
|
||||
IsFinitePreFeynmanRule.halfEdgeLabelDecidable
|
||||
|
|
@ -425,27 +428,37 @@ instance {𝓔 𝓥 𝓱𝓔 : Type} [h1 : Fintype 𝓔] [h2 : DecidableEq 𝓔]
|
|||
IsFiniteDiagram (mk' 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 C) :=
|
||||
⟨h1, h2, h3, h4, h5, h6⟩
|
||||
|
||||
/-- If `F` is a finite Feynman diagram, then its edges are finite. -/
|
||||
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓔 :=
|
||||
IsFiniteDiagram.𝓔Fintype
|
||||
|
||||
/-- If `F` is a finite Feynman diagram, then its edges are decidable. -/
|
||||
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓔 :=
|
||||
IsFiniteDiagram.𝓔DecidableEq
|
||||
|
||||
/-- If `F` is a finite Feynman diagram, then its vertices are finite. -/
|
||||
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓥 :=
|
||||
IsFiniteDiagram.𝓥Fintype
|
||||
|
||||
/-- If `F` is a finite Feynman diagram, then its vertices are decidable. -/
|
||||
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓥 :=
|
||||
IsFiniteDiagram.𝓥DecidableEq
|
||||
|
||||
/-- If `F` is a finite Feynman diagram, then its half-edges are finite. -/
|
||||
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 :=
|
||||
IsFiniteDiagram.𝓱𝓔Fintype
|
||||
|
||||
/-- If `F` is a finite Feynman diagram, then its half-edges are decidable. -/
|
||||
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 :=
|
||||
IsFiniteDiagram.𝓱𝓔DecidableEq
|
||||
|
||||
/-- The proposition of whether the given an half-edge and an edge,
|
||||
the edge corresponding to the half edges is the given edge is decidable. -/
|
||||
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] (i : F.𝓱𝓔) (j : F.𝓔) :
|
||||
Decidable (F.𝓱𝓔To𝓔.hom i = j) := IsFiniteDiagram.𝓔DecidableEq (F.𝓱𝓔To𝓔.hom i) j
|
||||
|
||||
/-- For a finite feynman diagram, the type of half edge lables, edges and vertices
|
||||
is decidable. -/
|
||||
instance fintypeProdHalfEdgeLabel𝓔𝓥 {F : FeynmanDiagram P} [IsFinitePreFeynmanRule P]
|
||||
[IsFiniteDiagram F] : DecidableEq (P.HalfEdgeLabel × F.𝓔 × F.𝓥) :=
|
||||
instDecidableEqProd
|
||||
|
|
@ -557,10 +570,16 @@ lemma cond_symm {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.
|
|||
simp only [Functor.const_obj_obj, Equiv.apply_symm_apply] at h1
|
||||
exact (edgeVertexEquiv 𝓔 𝓥).apply_eq_iff_eq_symm_apply.mp (h1).symm
|
||||
|
||||
/-- If `𝓔` is a map between the edges of one finite Feynman diagram and another Feynman diagram,
|
||||
then deciding whether `𝓔` froms a morphism in `Over P.EdgeLabel` between the edge
|
||||
maps is decidable. -/
|
||||
instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
|
||||
(𝓔 : F.𝓔 → G.𝓔) : Decidable (∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) :=
|
||||
@Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓔 P _ _) _
|
||||
|
||||
/-- If `𝓥` is a map between the vertices of one finite Feynman diagram and another Feynman diagram,
|
||||
then deciding whether `𝓥` froms a morphism in `Over P.VertexLabel` between the vertex
|
||||
maps is decidable. -/
|
||||
instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
|
||||
(𝓥 : F.𝓥 → G.𝓥) : Decidable (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) :=
|
||||
@Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓥 P _ _) _
|
||||
|
|
|
|||
|
|
@ -32,15 +32,19 @@ def complexScalarFeynmanRules : PreFeynmanRule where
|
|||
| 1 => Over.mk ![1]
|
||||
| 2 => Over.mk ![0, 0, 1, 1]
|
||||
|
||||
/-- An instance allowing us to use integers for edge labels for complex scalar theory. -/
|
||||
instance (a : ℕ) : OfNat complexScalarFeynmanRules.EdgeLabel a where
|
||||
ofNat := (a : Fin _)
|
||||
|
||||
/-- An instance allowing us to use integers for half-edge labels for complex scalar theory. -/
|
||||
instance (a : ℕ) : OfNat complexScalarFeynmanRules.HalfEdgeLabel a where
|
||||
ofNat := (a : Fin _)
|
||||
|
||||
/-- An instance allowing us to use integers for vertex labels for complex scalar theory. -/
|
||||
instance (a : ℕ) : OfNat complexScalarFeynmanRules.VertexLabel a where
|
||||
ofNat := (a : Fin _)
|
||||
|
||||
/-- The pre feynman rules for complex scalars are finite. -/
|
||||
instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
|
||||
edgeLabelDecidable := instDecidableEqFin _
|
||||
vertexLabelDecidable := instDecidableEqFin _
|
||||
|
|
|
|||
|
|
@ -34,15 +34,19 @@ def phi4PreFeynmanRules : PreFeynmanRule where
|
|||
| 0 => Over.mk ![0]
|
||||
| 1 => Over.mk ![0, 0, 0, 0]
|
||||
|
||||
/-- An instance allowing us to use integers for edge labels for Phi-4. -/
|
||||
instance (a : ℕ) : OfNat phi4PreFeynmanRules.EdgeLabel a where
|
||||
ofNat := (a : Fin _)
|
||||
|
||||
/-- An instance allowing us to use integers for half edge labels for Phi-4. -/
|
||||
instance (a : ℕ) : OfNat phi4PreFeynmanRules.HalfEdgeLabel a where
|
||||
ofNat := (a : Fin _)
|
||||
|
||||
/-- An instance allowing us to use integers for vertex labels for Phi-4. -/
|
||||
instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where
|
||||
ofNat := (a : Fin _)
|
||||
|
||||
/-- The pre feynman rules for Phi-4 are finite. -/
|
||||
instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
|
||||
edgeLabelDecidable := instDecidableEqFin _
|
||||
vertexLabelDecidable := instDecidableEqFin _
|
||||
|
|
|
|||
|
|
@ -48,8 +48,10 @@ We define the direct sum of the edge and vertex momentum spaces.
|
|||
Corresponding to that spanned by its momentum. -/
|
||||
def HalfEdgeMomenta : Type := F.𝓱𝓔 → ℝ
|
||||
|
||||
/-- The half momenta carries the structure of an addative commutative group. -/
|
||||
instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup
|
||||
|
||||
/-- The half momenta carries the structure of a module over `ℝ`. Defined via its target. -/
|
||||
instance : Module ℝ F.HalfEdgeMomenta := Pi.module _ _ _
|
||||
|
||||
/-- An auxiliary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
|
||||
|
|
@ -81,16 +83,20 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ]
|
|||
Corresponding to that spanned by its total outflowing momentum. -/
|
||||
def EdgeMomenta : Type := F.𝓔 → ℝ
|
||||
|
||||
/-- The edge momenta form an addative commuative group. -/
|
||||
instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
|
||||
|
||||
/-- The edge momenta form a module over `ℝ`. -/
|
||||
instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
|
||||
|
||||
/-- The type which assocaites to each ege a `1`-dimensional vector space.
|
||||
Corresponding to that spanned by its total inflowing momentum. -/
|
||||
def VertexMomenta : Type := F.𝓥 → ℝ
|
||||
|
||||
/-- The vertex momenta carries the structure of an addative commuative group. -/
|
||||
instance : AddCommGroup F.VertexMomenta := Pi.addCommGroup
|
||||
|
||||
/-- The vertex momenta carries the structure of a module over `ℝ`. -/
|
||||
instance : Module ℝ F.VertexMomenta := Pi.module _ _ _
|
||||
|
||||
/-- The map from `Fin 2` to `Type` landing on `EdgeMomenta` and `VertexMomenta`. -/
|
||||
|
|
@ -99,11 +105,15 @@ def EdgeVertexMomentaMap : Fin 2 → Type := fun i =>
|
|||
| 0 => F.EdgeMomenta
|
||||
| 1 => F.VertexMomenta
|
||||
|
||||
/-- The target of the map `EdgeVertexMomentaMap` is either the type of edge momenta
|
||||
or vertex momenta and thus carries the structure of an addative commuative group. -/
|
||||
instance (i : Fin 2) : AddCommGroup (EdgeVertexMomentaMap F i) :=
|
||||
match i with
|
||||
| 0 => instAddCommGroupEdgeMomenta F
|
||||
| 1 => instAddCommGroupVertexMomenta F
|
||||
|
||||
/-- The target of the map `EdgeVertexMomentaMap` is either the type of edge momenta
|
||||
or vertex momenta and thus carries the structure of a module over `ℝ`. -/
|
||||
instance (i : Fin 2) : Module ℝ (EdgeVertexMomentaMap F i) :=
|
||||
match i with
|
||||
| 0 => instModuleRealEdgeMomenta F
|
||||
|
|
|
|||
|
|
@ -199,6 +199,8 @@ namespace complexLorentzTensor
|
|||
/-- Color for complex Lorentz tensors is decidable. -/
|
||||
instance : DecidableEq complexLorentzTensor.C := complexLorentzTensor.instDecidableEqColor
|
||||
|
||||
/-- Contracting two basis elements gives `1` if the index for the basis elements is the same,
|
||||
and `0` otherwise. Holds for any color of index. -/
|
||||
lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.repDim c))
|
||||
(j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) :
|
||||
complexLorentzTensor.castToField
|
||||
|
|
@ -213,9 +215,11 @@ lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.re
|
|||
| Color.up => Lorentz.contrCoContraction_basis _ _
|
||||
| Color.down => Lorentz.coContrContraction_basis _ _
|
||||
|
||||
/-- For any object in the over color category, with source `Fin n`, has a decidable source. -/
|
||||
instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
|
||||
DecidableEq (OverColor.mk c).left := instDecidableEqFin n
|
||||
|
||||
/-- For any object in the over color category, with source `Fin n`, has a finite source. -/
|
||||
instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
|
||||
Fintype (OverColor.mk c).left := Fin.fintype n
|
||||
|
||||
|
|
|
|||
|
|
@ -30,6 +30,8 @@ open minkowskiMatrix
|
|||
Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
|
||||
def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
|
||||
|
||||
/-- The representation of contrvariant Lorentz vectors forms a topological space, induced
|
||||
by its equivalence to `Fin 1 ⊕ Fin d → ℝ`. -/
|
||||
instance : TopologicalSpace (Contr d) := TopologicalSpace.induced
|
||||
ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
|
||||
|
||||
|
|
|
|||
|
|
@ -154,11 +154,15 @@ lemma induction_mod_tmul
|
|||
# Dependent type version of PiTensorProduct.tmulEquiv
|
||||
-/
|
||||
|
||||
/-- Given two maps `s1` and `s2` whose targets carry an instance of an addative commutative
|
||||
monoid, the target of the sum of these two maps also carry an instance thereof. -/
|
||||
instance : (i : ι1 ⊕ ι2) → AddCommMonoid ((fun i => Sum.elim s1 s2 i) i) := fun i =>
|
||||
match i with
|
||||
| Sum.inl i => inst1 i
|
||||
| Sum.inr i => inst2 i
|
||||
|
||||
/-- Given two maps `s1` and `s2` whose targets carry an instance of a module over `R`,
|
||||
the target of the sum of these two maps also carry an instance thereof. -/
|
||||
instance : (i : ι1 ⊕ ι2) → Module R ((fun i => Sum.elim s1 s2 i) i) := fun i =>
|
||||
match i with
|
||||
| Sum.inl i => inst1' i
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue