Skip to content

doc(Relativity): Correct documentation for realLorentzTensor #1712

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

Merged
jstoobysmith merged 3 commits into from
Oct 2, 2026
Merged

doc(Relativity): Correct documentation for realLorentzTensor #1712

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ab56f32
doc(Relativity): Correct documentation for realLorentzTensor
ereinhardt8 Oct 2, 2026
0500dd9
Merge remote-tracking branch 'upstream/master' into pr/1712
jstoobysmith Oct 2, 2026
b14830e
doc: Update group in Physlib/Relativity/Tensors/RealTensor/Basic.lean
ereinhardt8 Oct 2, 2026
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
7 changes: 3 additions & 4 deletions Physlib/Relativity/Tensors/RealTensor/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,21 +20,20 @@ which are used to define `realLorentzTensor`.

open Matrix
open MatrixGroups
open Complex
open TensorProduct

namespace realLorentzTensor

set_option backward.isDefEq.respectTransparency false in
/-- The colors associated with complex representations of SL(2, ℂ) of interest to physics. -/
/-- The colors associated with real representations of O(1, 3) of interest to physics. -/
inductive Color
/-- The color associated with contravariant Lorentz vectors. -/
| up : Color
/-- The color associated with covariant Lorentz vectors. -/
| down : Color
deriving Fintype

/-- Color for complex Lorentz tensors is decidable. -/
/-- Color for real Lorentz tensors is decidable. -/
instance : DecidableEq Color := fun x y =>
match x, y with
| Color.up, Color.up => isTrue rfl
Expand Down Expand Up @@ -64,7 +63,7 @@ TODO "Replace Lorentz.ContrMod and Lorentz.CoMod in the definition of realLorent

noncomputable section
open realLorentzTensor in
/-- The tensor structure for complex Lorentz tensors. -/
/-- The tensor structure for real Lorentz tensors. -/
def realLorentzTensor (d : ℕ := 3) : TensorSpecies
ℝ realLorentzTensor.Color (LorentzGroup d)
(fun | Color.up => Lorentz.ContrMod d | Color.down => Lorentz.CoMod d)
Expand Down
8 changes: 4 additions & 4 deletions Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,11 +29,11 @@ namespace realLorentzTensor

-/

/-- The metric `ηᵢᵢ` as a complex Lorentz tensor. -/
/-- The metric `ηᵢᵢ` as a real Lorentz tensor. -/
abbrev coMetric (d : ℕ := 3) : ℝT[d, .down, .down] :=
(realLorentzTensor d).metricTensor .down

/-- The metric `ηⁱⁱ` as a complex Lorentz tensor. -/
/-- The metric `ηⁱⁱ` as a real Lorentz tensor. -/
abbrev contrMetric (d : ℕ := 3) : ℝT[d, .up, .up] :=
(realLorentzTensor d).metricTensor .up

Expand All @@ -43,10 +43,10 @@ abbrev contrMetric (d : ℕ := 3) : ℝT[d, .up, .up] :=

-/

/-- The metric `ηᵢᵢ` as a complex Lorentz tensors. -/
/-- The metric `ηᵢᵢ` as a real Lorentz tensors. -/
scoped[realLorentzTensor] notation "η'" => @coMetric

/-- The metric `ηⁱⁱ` as a complex Lorentz tensors. -/
/-- The metric `ηⁱⁱ` as a real Lorentz tensors. -/
scoped[realLorentzTensor] notation "η" => @contrMetric

/-!
Expand Down
Loading