DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Some docs

Browse source
This commit is contained in:
jstoobysmith 2024-11-11 11:58:48 +00:00
parent 63fcbf3da7
commit dd8554a080
4 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/AnomalyCancellation/SMNu/Permutations.lean
View file

@ -29,6 +29,7 @@ def PermGroup (n : ℕ) := Fin 6 → Equiv.Perm (Fin n)
variable {n : ℕ} variable {n : ℕ}
/-- The instance of a group on `PermGroup n` through the target space `Equiv.Perm (Fin n)`. -/
@[simp] @[simp]
instance : Group (PermGroup n) := Pi.group instance : Group (PermGroup n) := Pi.group

4
HepLean/Lorentz/Weyl/Basic.lean
View file

@ -274,10 +274,14 @@ def leftHandedAltEquiv : leftHanded ≅ altLeftHanded where
rw [one_mulVec] rw [one_mulVec]
rfl rfl
/-- `leftHandedAltEquiv` acting on an element `ψ : leftHanded` corresponds
to multiplying `ψ` by the matrix `!![0, 1; -1, 0]`. -/
lemma leftHandedAltEquiv_hom_hom_apply (ψ : leftHanded) : lemma leftHandedAltEquiv_hom_hom_apply (ψ : leftHanded) :
leftHandedAltEquiv.hom.hom ψ = leftHandedAltEquiv.hom.hom ψ =
AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ) := rfl AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ) := rfl
/-- The inverse of `leftHandedAltEquiv` acting on an element`ψ : altLeftHanded` corresponds
to multiplying `ψ` by the matrix `!![0, -1; 1, 0]`. -/
lemma leftHandedAltEquiv_inv_hom_apply (ψ : altLeftHanded) : lemma leftHandedAltEquiv_inv_hom_apply (ψ : altLeftHanded) :
leftHandedAltEquiv.inv.hom ψ = leftHandedAltEquiv.inv.hom ψ =
LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl

4
HepLean/StandardModel/HiggsBoson/Basic.lean
View file

@ -87,15 +87,13 @@ We also define the Higgs bundle.
/-- The trivial vector bundle 𝓡² × ℂ². -/ /-- The trivial vector bundle 𝓡² × ℂ². -/
abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec
/-- The instance of a smooth vector bundle with total space `HiggsBundle` and fiber `HiggsVec`. -/
instance : SmoothVectorBundle HiggsVec HiggsBundle SpaceTime.asSmoothManifold := instance : SmoothVectorBundle HiggsVec HiggsBundle SpaceTime.asSmoothManifold :=
Bundle.Trivial.smoothVectorBundle HiggsVec Bundle.Trivial.smoothVectorBundle HiggsVec
/-- A Higgs field is a smooth section of the Higgs bundle. -/ /-- A Higgs field is a smooth section of the Higgs bundle. -/
abbrev HiggsField : Type := SmoothSection SpaceTime.asSmoothManifold HiggsVec HiggsBundle abbrev HiggsField : Type := SmoothSection SpaceTime.asSmoothManifold HiggsVec HiggsBundle
instance : NormedAddCommGroup (Fin 2 → ℂ) := by
exact Pi.normedAddCommGroup
/-- Given a vector in `HiggsVec` the constant Higgs field with value equal to that /-- Given a vector in `HiggsVec` the constant Higgs field with value equal to that
section. -/ section. -/
def HiggsVec.toField (φ : HiggsVec) : HiggsField where def HiggsVec.toField (φ : HiggsVec) : HiggsField where

3
HepLean/Tensors/Tree/Basic.lean
View file

@ -110,10 +110,13 @@ open OverColor
variable (S : TensorSpecies) variable (S : TensorSpecies)
/-- The field `k` of a TensorSpecies has the instance of a commuative ring. -/
instance : CommRing S.k := S.k_commRing instance : CommRing S.k := S.k_commRing
/-- The field `G` of a TensorSpecies has the instance of a group. -/
instance : Group S.G := S.G_group instance : Group S.G := S.G_group
/-- The field `repDim` of a TensorSpecies is non-zero for all colors. -/
instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c
/-- The lift of the functor `S.F` to a monoidal functor. -/ /-- The lift of the functor `S.F` to a monoidal functor. -/