Skip to content

Commit e7a5ef0

Browse files
kastchkastch
authored
Remove sorry: Prove realLorentzTensor.toComplex_equivariant (#1007)
* Remove sorry: Prove realLorentzTensor.toComplex_equivariant * Linter fix for realLorentzTensor.toComplex_equivariant * Fixed authoring * Review fix for realLorentzTensor.toComplex_equivariant * Review fix for realLorentzTensor.toComplex_equivariant * Linter fix and additional decomposition of sublemmas of realLorentzTensor.toComplex_equivariant proof * Review fix for realLorentzTensor.toComplex_equivariant * Naming fix for realLorentzTensor.toComplex_equivariant * Simplified lemmas fix for realLorentzTensor.toComplex_equivariant * Moved SlotRepr to ComplexTensor/Basic.lean * Linter fix --------- Co-authored-by: kastch <kastch>
1 parent 269f77b commit e7a5ef0

5 files changed

Lines changed: 436 additions & 5 deletions

File tree

‎PhysLean/Relativity/Tensors/ComplexTensor/Basic.lean‎

Lines changed: 115 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,13 @@
11
/-
22
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Joseph Tooby-Smith
4+
Authors: Joseph Tooby-Smith, Nikolai Kashcheev
55
-/
66
module
77

88
public import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Pre
99
public import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Metric
10+
public import PhysLean.Relativity.Tensors.Basic
1011
/-!
1112
1213
## Complex Lorentz tensors
@@ -253,6 +254,28 @@ lemma basis_up_eq {i : Fin 4} :
253254
lemma basis_down_eq {i : Fin 4} :
254255
complexLorentzTensor.basis Color.down i = Lorentz.complexCoBasisFin4 i := rfl
255256

257+
@[simp]
258+
lemma basis_eq_complexContrBasisFin4 :
259+
complexLorentzTensor.basis Color.up = Lorentz.complexContrBasisFin4 := by
260+
ext i
261+
exact basis_up_eq
262+
263+
@[simp]
264+
lemma basis_eq_complexCoBasisFin4 :
265+
complexLorentzTensor.basis Color.down = Lorentz.complexCoBasisFin4 := by
266+
ext i
267+
exact basis_down_eq
268+
269+
@[simp]
270+
lemma FD_obj_up (Λ : SL(2, ℂ)) :
271+
(complexLorentzTensor.FD.obj { as := Color.up }).ρ Λ = Lorentz.complexContr.ρ Λ :=
272+
rfl
273+
274+
@[simp]
275+
lemma FD_obj_down (Λ : SL(2, ℂ)) :
276+
(complexLorentzTensor.FD.obj { as := Color.down }).ρ Λ = Lorentz.complexCo.ρ Λ :=
277+
rfl
278+
256279
lemma basis_upL_eq {i : Fin 2} :
257280
complexLorentzTensor.basis Color.upL i = Fermion.leftBasis i := rfl
258281

@@ -265,5 +288,96 @@ lemma basis_upR_eq {i : Fin 2} :
265288
lemma basis_downR_eq {i : Fin 2} :
266289
complexLorentzTensor.basis Color.downR i = Fermion.altRightBasis i := rfl
267290

291+
/-!
292+
293+
## Vector slot component formulas (`Color.up` / `Color.down`)
294+
295+
The colors `Color.up` and `Color.down` are the standard Lorentz vector colors. The lemmas
296+
`repr_ρ_basis_vector_up` and `repr_ρ_basis_vector_down` are stated for `Fin 4` indices
297+
(definitionally `Fin (repDim Color.up)` and `Fin (repDim Color.down)`).
298+
299+
When a slot is only known up to `c₀ = Color.up` or `Color.down`, use
300+
`repr_ρ_basis_vector_up_of_eq` / `repr_ρ_basis_vector_down_of_eq`.
301+
302+
-/
303+
304+
section vectorSlotRepr
305+
306+
open TensorSpecies Tensor Lorentz Lorentz.SL2C Module
307+
308+
/--
309+
Component formula for the standard contravariant vector slot `Color.up`.
310+
311+
For `b, i : Fin 4`, the `i`-component of `ρ Λ` on `basis Color.up b` equals the corresponding entry
312+
of `LorentzGroup.toComplex (SL2C.toLorentzGroup Λ)` in `Fin 1 ⊕ Fin 3` coordinates.
313+
-/
314+
lemma repr_ρ_basis_vector_up (Λ : SL(2, ℂ)) (b i : Fin 4) :
315+
((complexLorentzTensor.basis Color.up).repr
316+
(((complexLorentzTensor.FD.obj { as := Color.up }).ρ Λ)
317+
(complexLorentzTensor.basis Color.up b))) i =
318+
(LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ))
319+
(finSumFinEquiv.symm i) (finSumFinEquiv.symm b) := by
320+
simp only [basis_up_eq]
321+
erw [Lorentz.complexContrBasis_reindex_apply_eq_fin4]
322+
simp_rw [basis_eq_complexContrBasisFin4, Lorentz.complexContrBasisFin4_eq_reindex]
323+
rw [Basis.repr_reindex_apply, Basis.reindex_apply]
324+
simp_rw [FD_obj_up]
325+
conv_lhs => erw [← LinearMap.toMatrix_apply]
326+
exact Lorentz.complexContrBasis_ρ_apply (M := Λ) (i := finSumFinEquiv.symm i)
327+
(j := finSumFinEquiv.symm b)
328+
329+
/--
330+
Transport version of `repr_ρ_basis_vector_up` for a color `c₀` that is propositionally `Color.up`.
331+
-/
332+
lemma repr_ρ_basis_vector_up_of_eq (c₀ : Color) (h : c₀ = Color.up) (Λ : SL(2, ℂ))
333+
(b i : Fin (complexLorentzTensor.repDim c₀)) :
334+
((complexLorentzTensor.basis c₀).repr
335+
(((complexLorentzTensor.FD.obj { as := c₀ }).ρ Λ)
336+
(complexLorentzTensor.basis c₀ b))) i =
337+
(LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ))
338+
(finSumFinEquiv.symm (Fin.cast (by rw [h]; rfl) i))
339+
(finSumFinEquiv.symm (Fin.cast (by rw [h]; rfl) b)) := by
340+
subst h
341+
simpa using repr_ρ_basis_vector_up Λ b i
342+
343+
/--
344+
Component formula for the standard covariant vector slot `Color.down`.
345+
346+
For `b, i : Fin 4`, the `i`-component of `ρ Λ` on `basis Color.down b` matches the inverse complex
347+
Lorentz matrix as in `Lorentz.complexCoBasis_ρ_apply` (with transpose indexing on `Fin 1 ⊕ Fin 3`).
348+
-/
349+
lemma repr_ρ_basis_vector_down (Λ : SL(2, ℂ)) (b i : Fin 4) :
350+
((complexLorentzTensor.basis Color.down).repr
351+
(((complexLorentzTensor.FD.obj { as := Color.down }).ρ Λ)
352+
(complexLorentzTensor.basis Color.down b))) i =
353+
(LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ))⁻¹
354+
(finSumFinEquiv.symm b) (finSumFinEquiv.symm i) := by
355+
simp only [basis_down_eq]
356+
erw [Lorentz.complexCoBasis_reindex_apply_eq_fin4]
357+
simp_rw [basis_eq_complexCoBasisFin4, Lorentz.complexCoBasisFin4_eq_reindex]
358+
rw [Basis.repr_reindex_apply, Basis.reindex_apply]
359+
simp_rw [FD_obj_down]
360+
conv_lhs => erw [← LinearMap.toMatrix_apply]
361+
erw [Lorentz.complexCoBasis_ρ_apply (M := Λ) (i := finSumFinEquiv.symm i)
362+
(j := finSumFinEquiv.symm b)]
363+
simp only [Matrix.transpose_apply]
364+
365+
/--
366+
Transport version of `repr_ρ_basis_vector_down` for a color `c₀` that is propositionally
367+
`Color.down`.
368+
-/
369+
lemma repr_ρ_basis_vector_down_of_eq (c₀ : Color) (h : c₀ = Color.down) (Λ : SL(2, ℂ))
370+
(b i : Fin (complexLorentzTensor.repDim c₀)) :
371+
((complexLorentzTensor.basis c₀).repr
372+
(((complexLorentzTensor.FD.obj { as := c₀ }).ρ Λ)
373+
(complexLorentzTensor.basis c₀ b))) i =
374+
(LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ))⁻¹
375+
(finSumFinEquiv.symm (Fin.cast (by rw [h]; rfl) b))
376+
(finSumFinEquiv.symm (Fin.cast (by rw [h]; rfl) i)) := by
377+
subst h
378+
simpa using repr_ρ_basis_vector_down Λ b i
379+
380+
end vectorSlotRepr
381+
268382
end complexLorentzTensor
269383
end

‎PhysLean/Relativity/Tensors/ComplexTensor/Vector/Pre/Basic.lean‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,14 @@ lemma complexContrBasis_ρ_val (M : SL(2,ℂ)) (v : complexContr) :
6161
def complexContrBasisFin4 : Basis (Fin 4) ℂ complexContr :=
6262
Basis.reindex complexContrBasis finSumFinEquiv
6363

64+
lemma complexContrBasisFin4_eq_reindex :
65+
complexContrBasisFin4 = complexContrBasis.reindex finSumFinEquiv :=
66+
rfl
67+
68+
lemma complexContrBasis_reindex_apply_eq_fin4 (j : Fin 4) :
69+
(complexContrBasis.reindex finSumFinEquiv) j = complexContrBasisFin4 j :=
70+
rfl
71+
6472
@[simp]
6573
lemma complexContrBasisFin4_apply_zero :
6674
complexContrBasisFin4 0 = complexContrBasis (Sum.inl 0) := by
@@ -114,6 +122,14 @@ lemma complexCoBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
114122
def complexCoBasisFin4 : Basis (Fin 4) ℂ complexCo :=
115123
Basis.reindex complexCoBasis finSumFinEquiv
116124

125+
lemma complexCoBasisFin4_eq_reindex :
126+
complexCoBasisFin4 = complexCoBasis.reindex finSumFinEquiv :=
127+
rfl
128+
129+
lemma complexCoBasis_reindex_apply_eq_fin4 (j : Fin 4) :
130+
(complexCoBasis.reindex finSumFinEquiv) j = complexCoBasisFin4 j :=
131+
rfl
132+
117133
@[simp]
118134
lemma complexCoBasisFin4_apply_zero :
119135
complexCoBasisFin4 0 = complexCoBasis (Sum.inl 0) := by

‎PhysLean/Relativity/Tensors/RealTensor/Basic.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,26 @@ lemma repDim_eq_one_plus_dim {d : ℕ} {c : realLorentzTensor.Color} :
145145

146146
/-!
147147
148+
## Basis and discrete functor objects
149+
150+
These re-express fields of `realLorentzTensor d` in terms of `Lorentz` data.
151+
152+
-/
153+
154+
lemma basis_eq_contrBasisFin {d : ℕ} :
155+
(realLorentzTensor d).basis Color.up = Lorentz.contrBasisFin (d := d) := rfl
156+
157+
lemma basis_eq_coBasisFin {d : ℕ} :
158+
(realLorentzTensor d).basis Color.down = Lorentz.coBasisFin (d := d) := rfl
159+
160+
lemma FD_obj_up {d : ℕ} :
161+
(realLorentzTensor d).FD.obj { as := Color.up } = Lorentz.Contr d := rfl
162+
163+
lemma FD_obj_down {d : ℕ} :
164+
(realLorentzTensor d).FD.obj { as := Color.down } = Lorentz.Co d := rfl
165+
166+
/-!
167+
148168
## Simplifying τ
149169
150170
-/

0 commit comments

Comments
 (0)