From 8edb598a0b0b913ae66bb4443f4c169cd4f1d1fc Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Wed, 23 Sep 2026 12:51:17 +0100 Subject: [PATCH 1/2] refactor: replace RatComplexNum by GaussianInt, rename ofRat to ofGaussianInt MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All components that went through `Physlib.RatComplexNum` are 0, ±1, ±i or integer Levi-Civita signs, so Mathlib's `GaussianInt` with `GaussianInt.toComplex` and `GaussianInt.toComplex_injective` replaces it. - Delete `Physlib/Mathematics/RatComplexNum.lean`. - Rename `ComplexTensor/OfRat.lean` to `ComplexTensor/OfGaussianInt.lean`; `ofRat` becomes `ofGaussianInt : (ComponentIdx c → GaussianInt) →ₛₗ[GaussianInt.toComplex] ℂT(c)`, and all `*_ofRat*` lemmas become `*_ofGaussianInt*`; `contr_basis_ratComplexNum` becomes `contr_basis_gaussianInt`. - `pauliContrComponent`, `pauliContrDownComponent` and the Levi-Civita components are now `GaussianInt`-valued. - Replace the `RatComplexNum` helper lemmas in `PauliMatrices/Relations.lean` by inline `show … from` rewrites, and close `toTensor_dualLeft_eq_ofGaussianInt` and `toTensor_dualLorentzLeft_eq_ofGaussianInt` with `congrArg` instead of `congr`. Heartbeats (v4.34): Relations.lean 770,274k -> 707,080k; ToTensor.lean (declarations above 20M) 538.6M -> 521.0M. Kernel `decide` is cheaper on integers than on rationals. Co-authored-by: Claude Opus 5.5 --- Physlib.lean | 3 +- Physlib/Mathematics/RatComplexNum.lean | 269 ------------------ .../Relativity/PauliMatrices/Relations.lean | 143 +++++----- .../Relativity/PauliMatrices/ToTensor.lean | 203 ++++++------- Physlib/Relativity/Tensors/API-map.yaml | 4 +- .../Tensors/ComplexTensor/Metrics/Basic.lean | 30 +- .../Tensors/ComplexTensor/Metrics/Lemmas.lean | 16 +- .../{OfRat.lean => OfGaussianInt.lean} | 98 ++++--- .../Tensors/ComplexTensor/Units/Basic.lean | 28 +- .../Tensors/LeviCivita/Complex.lean | 27 +- scripts/MetaPrograms/module_doc_no_lint.txt | 3 +- 11 files changed, 285 insertions(+), 539 deletions(-) delete mode 100644 Physlib/Mathematics/RatComplexNum.lean rename Physlib/Relativity/Tensors/ComplexTensor/{OfRat.lean => OfGaussianInt.lean} (58%) diff --git a/Physlib.lean b/Physlib.lean index 87750fed4..00908d6b6 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -150,7 +150,6 @@ public import Physlib.Mathematics.OneParameterSubgroups.Basic public import Physlib.Mathematics.OneParameterSubgroups.Unitary public import Physlib.Mathematics.OrthogonalMatrix public import Physlib.Mathematics.PiTensorProduct -public import Physlib.Mathematics.RatComplexNum public import Physlib.Mathematics.Resolvent public import Physlib.Mathematics.SO3.Basic public import Physlib.Mathematics.SchurTriangulation @@ -429,7 +428,7 @@ public import Physlib.Relativity.Tensors.ComplexTensor.Matrix.Pre public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Basic public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Lemmas public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Pre -public import Physlib.Relativity.Tensors.ComplexTensor.OfRat +public import Physlib.Relativity.Tensors.ComplexTensor.OfGaussianInt public import Physlib.Relativity.Tensors.ComplexTensor.Units.Basic public import Physlib.Relativity.Tensors.ComplexTensor.Units.Pre public import Physlib.Relativity.Tensors.ComplexTensor.Units.Symm diff --git a/Physlib/Mathematics/RatComplexNum.lean b/Physlib/Mathematics/RatComplexNum.lean deleted file mode 100644 index cec987263..000000000 --- a/Physlib/Mathematics/RatComplexNum.lean +++ /dev/null @@ -1,269 +0,0 @@ -/- -Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Robert Sneiderman, Joseph Tooby-Smith --/ -module - -public import Mathlib.Analysis.Complex.Basic -/-! -# Rational complex numbers - --/ - -@[expose] public section - -namespace Physlib - -/-- Rational complex numbers. This type is mainly used when decidability is needed. -/ -structure RatComplexNum where - /-- The real part of a `RatComplexNum`. -/ - fst : ℚ - /-- The imaginary part of a `RatComplexNum`. -/ - snd : ℚ - -namespace RatComplexNum - -@[ext] -lemma ext {x y : RatComplexNum} (h1 : x.1 = y.1) (h2 : x.2 = y.2) : x = y := by - cases x - cases y - simp only at h1 h2 - subst h1 h2 - rfl - -/-- The equivalence as a type of `RatComplexNum` with `ℚ × ℚ`. -/ -def equivToProd : RatComplexNum ≃ ℚ × ℚ where - toFun := fun x => (x.1, x.2) - invFun := fun x => ⟨x.1, x.2⟩ - left_inv := by - intro x - cases x - rfl - right_inv := by - intro x - cases x - rfl - -instance : DecidableEq RatComplexNum := Equiv.decidableEq equivToProd - -instance : Add RatComplexNum where - add := fun x y => ⟨x.fst + y.fst, x.snd + y.snd⟩ - -@[simp] -lemma add_fst (x y : RatComplexNum) : (x + y).fst = x.fst + y.fst := rfl - -@[simp] -lemma add_snd (x y : RatComplexNum) : (x + y).snd = x.snd + y.snd := rfl - -instance : AddCommGroup RatComplexNum where - add_assoc := by - intro a b c - ext - · simp only [add_fst] - ring - · simp only [add_snd] - ring - zero := ⟨0, 0⟩ - zero_add := by - intro a - match a with - | ⟨a1, a2⟩ => - ext - · change 0 + a1 = a1 - simp - · change 0 + a2 = a2 - simp - add_zero := by - intro a - match a with - | ⟨a1, a2⟩ => - ext - · change a1 + 0 = a1 - simp - · change a2 + 0 = a2 - simp - neg := fun x => ⟨-x.fst, -x.snd⟩ - nsmul := fun n x => ⟨n • x.fst, n • x.snd⟩ - zsmul := fun n x => ⟨n • x.1, n • x.2⟩ - neg_add_cancel := by - intro a - match a with - | ⟨a1, a2⟩ => - ext - · change -a1 + a1 = 0 - simp - · change -a2 + a2 = 0 - simp - add_comm := by - intro x y - ext - · simp only [add_fst] - ring - · simp only [add_snd] - ring - nsmul_zero := by intro x; ext <;> exact zero_nsmul _ - nsmul_succ := by intro n x; ext <;> exact succ_nsmul _ _ - zsmul_zero' := by intro a; ext <;> exact zero_zsmul _ - zsmul_succ' := by - intro n a - ext - · show ((n : ℤ) + 1) • a.fst = (n : ℤ) • a.fst + a.fst - exact add_one_zsmul _ _ - · show ((n : ℤ) + 1) • a.snd = (n : ℤ) • a.snd + a.snd - exact add_one_zsmul _ _ - zsmul_neg' := by intro n a; ext <;> exact negSucc_zsmul _ _ - -instance : Mul RatComplexNum where - mul := fun x y => ⟨x.fst * y.fst - x.snd * y.snd, x.fst * y.snd + x.snd * y.fst⟩ - -@[simp] -lemma mul_fst (x y : RatComplexNum) : (x * y).fst = x.fst * y.fst - x.snd * y.snd := rfl - -@[simp] -lemma mul_snd (x y : RatComplexNum) : (x * y).snd = x.fst * y.snd + x.snd * y.fst := rfl - -instance : Ring RatComplexNum where - one := ⟨1, 0⟩ - mul_assoc := by - intro x y z - ext - · simp only [mul_fst, mul_snd] - ring - · simp only [mul_fst, mul_snd] - ring - one_mul := by - intro x - match x with - | ⟨x1, x2⟩ => - ext - · change 1 * x1 - 0 * x2 = x1 - simp - · change 1 * x2 + 0 * x1 = x2 - simp - mul_one := by - intro x - match x with - | ⟨x1, x2⟩ => - ext - · change x1 * 1 - x2 * 0 = x1 - simp - · change x1 * 0 + x2 * 1 = x2 - simp - left_distrib := by - intro a b c - match a, b, c with - | ⟨a1, a2⟩, ⟨b1, b2⟩, ⟨c1, c2⟩ => - ext - · change a1 * (b1 + c1) - a2 * (b2 + c2) = - (a1 * b1 - a2 * b2) + (a1 * c1 - a2 * c2) - ring - · change a1 * (b2 + c2) + a2 * (b1 + c1) = - (a1 * b2 + a2 * b1) + (a1 * c2 + a2 * c1) - ring - right_distrib := by - intro a b c - match a, b, c with - | ⟨b1, b2⟩, ⟨c1, c2⟩, ⟨a1, a2⟩ => - ext - · change (b1 + c1) * a1 - (b2 + c2) * a2 = - (b1 * a1 - b2 * a2) + (c1 * a1 - c2 * a2) - ring - · change (b1 + c1) * a2 + (b2 + c2) * a1 = - (b1 * a2 + b2 * a1) + (c1 * a2 + c2 * a1) - ring - zero_mul := by - intro a - match a with - | ⟨a1, a2⟩ => - ext - · change 0 * a1 - 0 * a2 = 0 - simp - · change 0 * a2 + 0 * a1 = 0 - simp - mul_zero := by - intro a - match a with - | ⟨a1, a2⟩ => - ext - · change a1 * 0 - a2 * 0 = 0 - simp - · change a1 * 0 + a2 * 0 = 0 - simp - neg_add_cancel := by - intro a - match a with - | ⟨a1, a2⟩ => - ext - · change -a1 + a1 = 0 - simp - · change -a2 + a2 = 0 - simp - -@[simp] -lemma one_fst : (1 : RatComplexNum).fst = 1 := rfl - -@[simp] -lemma one_snd : (1 : RatComplexNum).snd = 0 := rfl - -@[simp] -lemma zero_fst : (0 : RatComplexNum).fst = 0 := rfl - -@[simp] -lemma zero_snd : (0 : RatComplexNum).snd = 0 := rfl - -open Complex - -/-- The inclusion of `RatComplexNum` into the complex numbers. -/ -noncomputable def toComplexNum : RatComplexNum →+* ℂ where - toFun := fun x => x.fst + x.snd * I - map_one' := by - simp - map_add' a b := by - simp only [add_fst, Rat.cast_add, add_snd] - ring - map_mul' a b := by - simp only [mul_fst, Rat.cast_sub, Rat.cast_mul, mul_snd, Rat.cast_add] - ring_nf - simp only [I_sq, mul_neg, mul_one] - ring - map_zero' := by - simp - -@[simp] -lemma I_mul_toComplexNum (a : RatComplexNum) : I * toComplexNum a = toComplexNum (⟨0, 1⟩ * a) := by - simp only [toComplexNum, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mul_fst, zero_mul, - one_mul, zero_sub, Rat.cast_neg, mul_snd, zero_add] - ring_nf - simp only [I_sq, neg_mul, one_mul] - ring - -/-- Multiplication by `-I` under the inclusion of `RatComplexNum` into the complex numbers. -/ -lemma neg_I_mul_toComplexNum (a : RatComplexNum) : - (-I) * toComplexNum a = toComplexNum (- (⟨0, 1⟩ * a)) := by - rw [neg_mul, I_mul_toComplexNum, ← map_neg] - -lemma ofNat_mul_toComplexNum (n : ℕ) (a : RatComplexNum) : - n * toComplexNum a = toComplexNum (n * a) := by - simp only [map_mul, map_natCast] - -lemma toComplexNum_injective : Function.Injective toComplexNum := by - intro a b ha - simp only [toComplexNum, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] at ha - rw [Complex.ext_iff] at ha - simp only [add_re, ratCast_re, mul_re, I_re, mul_zero, ratCast_im, I_im, mul_one, sub_self, - add_zero, Rat.cast_inj, add_im, mul_im, zero_add] at ha - ext - · exact ha.1 - · exact ha.2 - -/-- Equality with a four-term sum of rational complex numbers can be checked before their -inclusion into the complex numbers. -/ -lemma toComplexNum_eq_add_neg_add_add_iff {a b c d e : RatComplexNum} : - (toComplexNum a = toComplexNum b + -toComplexNum c + toComplexNum d + toComplexNum e) ↔ - a = b + -c + d + e := by - rw [← map_neg, ← map_add, ← map_add, ← map_add] - exact Function.Injective.eq_iff toComplexNum_injective - -end RatComplexNum -end Physlib diff --git a/Physlib/Relativity/PauliMatrices/Relations.lean b/Physlib/Relativity/PauliMatrices/Relations.lean index 272810bba..35212a7a0 100644 --- a/Physlib/Relativity/PauliMatrices/Relations.lean +++ b/Physlib/Relativity/PauliMatrices/Relations.lean @@ -50,90 +50,91 @@ lemma pauliCo_contr_pauliContr : rw (transparency := .instances) [prodT_basis_repr_apply] simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero, Function.comp_apply] - rw [leftMetric_eq_ofRat, rightMetric_eq_ofRat] + rw [leftMetric_eq_ofGaussianInt, rightMetric_eq_ofGaussianInt] simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero, - Function.comp_apply, cons_val_zero, cons_val_one, head_cons, ofRat_basis_repr_apply] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] + Function.comp_apply, cons_val_zero, cons_val_one, head_cons, ofGaussianInt_basis_repr_apply] + rw [← GaussianInt.toComplex.map_mul] change (2 : ℕ) * _ - rw [Physlib.RatComplexNum.ofNat_mul_toComplexNum 2] + rw [show ∀ a : GaussianInt, ((2 : ℕ) : ℂ) * GaussianInt.toComplex a = + GaussianInt.toComplex ((2 : ℕ) * a) from fun a => by rw [map_mul, map_natCast]] rw [contrT_basis_repr_apply] conv_lhs => enter [2, x] rw [prodT_basis_repr_apply] - simp only [pauliCo_eq_ofRat, toTensor_eq_ofRat] - simp only [Fin.isValue, Fin.cast_eq_self, ofRat_basis_repr_apply] + simp only [pauliCo_eq_ofGaussianInt, toTensor_eq_ofGaussianInt] + simp only [Fin.isValue, Fin.cast_eq_self, ofGaussianInt_basis_repr_apply] left - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] + rw [← GaussianInt.toComplex.map_mul] conv_lhs => enter [2, x] right - rw (transparency := .instances) [contr_basis_ratComplexNum] + rw (transparency := .instances) [contr_basis_gaussianInt] conv_lhs => enter [2, x] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← map_sum Physlib.RatComplexNum.toComplexNum] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + rw [← GaussianInt.toComplex.map_mul] + rw [← map_sum GaussianInt.toComplex] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr revert b decide +kernel lemma pauliCoDown_trace_pauliCo : {(σ___ | μ β α ⊗ σ_^^ | ν α β) = (2 •ₜ η' | μ ν)}ᵀ := by conv_lhs => - rw [pauliCoDown_eq_ofRat, pauliCo_eq_ofRat, prodT_ofRat_ofRat, - contrT_ofRat, contrT_ofRat] + rw [pauliCoDown_eq_ofGaussianInt, pauliCo_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, + contrT_ofGaussianInt, contrT_ofGaussianInt] conv_rhs => - rw [coMetric_eq_ofRat] + rw [coMetric_eq_ofGaussianInt] rw [← map_nsmul] apply (Tensor.basis _).repr.injective ext b conv_rhs => rw [permT_basis_repr_symm_apply] - simp only [ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + simp only [ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr revert b decide +kernel lemma pauliCo_trace_pauliCoDown: {σ_^^ | μ α β ⊗ σ___ | ν β α = 2 •ₜ η' | μ ν}ᵀ := by conv_lhs => - rw [pauliCoDown_eq_ofRat, pauliCo_eq_ofRat] - rw [prodT_ofRat_ofRat, - contrT_ofRat, contrT_ofRat] + rw [pauliCoDown_eq_ofGaussianInt, pauliCo_eq_ofGaussianInt] + rw [prodT_ofGaussianInt_ofGaussianInt, + contrT_ofGaussianInt, contrT_ofGaussianInt] conv_rhs => - rw [coMetric_eq_ofRat] + rw [coMetric_eq_ofGaussianInt] rw [← map_nsmul] apply (Tensor.basis _).repr.injective ext b conv_rhs => rw [permT_basis_repr_symm_apply] - simp only [ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + simp only [ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr decide +revert +kernel lemma pauliContr_mul_pauliContrDown_add : {((σ^^^ | μ α β ⊗ σ^__ | ν β α') + (σ^^^ | ν α β ⊗ σ^__ | μ β α')) = 2 •ₜ η | μ ν ⊗ δL | α α'}ᵀ := by conv_lhs => - rw [pauliContrDown_ofRat, toTensor_eq_ofRat, prodT_ofRat_ofRat, - contrT_ofRat, permT_ofRat, ← map_add] + rw [pauliContrDown_ofGaussianInt, toTensor_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, + contrT_ofGaussianInt, permT_ofGaussianInt, ← map_add] conv_rhs => - rw [leftDualLeftUnit_eq_ofRat, contrMetric_eq_ofRat, prodT_ofRat_ofRat, ← map_nsmul, - permT_ofRat] + rw [leftDualLeftUnit_eq_ofGaussianInt, contrMetric_eq_ofGaussianInt, + prodT_ofGaussianInt_ofGaussianInt, ← map_nsmul, permT_ofGaussianInt] apply (Tensor.basis _).repr.injective ext b - simp only [ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + simp only [ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr decide +revert +kernel lemma auliContrDown_pauliContr_mul_add : {((σ^__ | μ β α ⊗ σ^^^ | ν α β') + (σ^__ | ν β α ⊗ σ^^^ | μ α β')) = 2 •ₜ η | μ ν ⊗ δR' | β β'}ᵀ := by conv_lhs => - rw [pauliContrDown_ofRat, toTensor_eq_ofRat, prodT_ofRat_ofRat, - contrT_ofRat, permT_ofRat, ← map_add] + rw [pauliContrDown_ofGaussianInt, toTensor_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, + contrT_ofGaussianInt, permT_ofGaussianInt, ← map_add] conv_rhs => - rw [dualRightRightUnit_eq_ofRat, contrMetric_eq_ofRat, prodT_ofRat_ofRat, ← map_nsmul, - permT_ofRat] + rw [dualRightRightUnit_eq_ofGaussianInt, contrMetric_eq_ofGaussianInt, + prodT_ofGaussianInt_ofGaussianInt, ← map_nsmul, permT_ofGaussianInt] apply (Tensor.basis _).repr.injective ext b - simp only [ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + simp only [ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr decide +revert +kernel /-! @@ -142,22 +143,24 @@ lemma auliContrDown_pauliContr_mul_add : -/ -/-- Rational-complex components of a contraction of `σ^^^` with a copy whose Weyl indices +/-- Gaussian integer components of a contraction of `σ^^^` with a copy whose Weyl indices are dualized. -/ -lemma pauliContr_mul_dualWeyl_eq_ofRat : - {σ^^^ | μ α β ⊗ σ^^^ | ν τ(α') τ(β)}ᵀ = ofRat (fun b => +lemma pauliContr_mul_dualWeyl_eq_ofGaussianInt : + {σ^^^ | μ α β ⊗ σ^^^ | ν τ(α') τ(β)}ᵀ = ofGaussianInt (fun b => ∑ x : Fin 2, pauliContrComponent (b 0) (b 1) x * pauliContrDownComponent (b 2) x (b 3)) := by - rw [toTensor_dualWeyl_eq_ofRat, toTensor_eq_ofRat, prodT_ofRat_ofRat, contrT_ofRat] + rw [toTensor_dualWeyl_eq_ofGaussianInt, toTensor_eq_ofGaussianInt, + prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt] congr -/-- Rational-complex components of the reverse contraction of a Weyl-dualized `σ^^^` with +/-- Gaussian integer components of the reverse contraction of a Weyl-dualized `σ^^^` with `σ^^^`. -/ -lemma dualWeyl_mul_pauliContr_eq_ofRat : - {σ^^^ | μ τ(α) τ(β) ⊗ σ^^^ | ν α β'}ᵀ = ofRat (fun b => +lemma dualWeyl_mul_pauliContr_eq_ofGaussianInt : + {σ^^^ | μ τ(α) τ(β) ⊗ σ^^^ | ν α β'}ᵀ = ofGaussianInt (fun b => ∑ x : Fin 2, pauliContrDownComponent (b 0) (b 1) x * pauliContrComponent (b 2) x (b 3)) := by - rw [toTensor_dualWeyl_eq_ofRat, toTensor_eq_ofRat, prodT_ofRat_ofRat, contrT_ofRat] + rw [toTensor_dualWeyl_eq_ofGaussianInt, toTensor_eq_ofGaussianInt, + prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt] congr /-- Contracting `ε4ℂ` with a Lorentz-dualized `σ^^^` agrees with contracting it with @@ -166,15 +169,15 @@ lemma leviCivita_mul_pauliDual : ({ε4ℂ | μ ν ρ κ ⊗ σ^^^ | τ(κ) α β = ε4ℂ | μ ν ρ κ ⊗ σ_^^ | κ α β}ᵀ : Prop) := by conv_lhs => - simp only [leviCivita_eq_ofRat_prod, toTensor_dualLorentz_eq_ofRat] - rw [prodT_ofRat_ofRat, contrT_ofRat] + simp only [leviCivita_eq_ofGaussianInt_prod, toTensor_dualLorentz_eq_ofGaussianInt] + rw [prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt] conv_rhs => - simp only [leviCivita_eq_ofRat_prod, pauliCo_eq_ofRat] - rw [prodT_ofRat_ofRat, contrT_ofRat] + simp only [leviCivita_eq_ofGaussianInt_prod, pauliCo_eq_ofGaussianInt] + rw [prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt] apply (Tensor.basis _).repr.injective ext b - rw [ofRat_basis_repr_apply, permT_basis_repr_symm_apply, ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + rw [ofGaussianInt_basis_repr_apply, permT_basis_repr_symm_apply, ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr decide +revert +kernel /-- The three-Pauli identity @@ -187,21 +190,25 @@ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({ + (Complex.I •ₜ (ε4ℂ | μ ν ρ κ ⊗ σ^^^ | τ(κ) α β'))) }ᵀ : Prop) := by conv_lhs => - rw [pauliContr_mul_dualWeyl_eq_ofRat, toTensor_eq_ofRat, - prodT_ofRat_ofRat, contrT_ofRat] + rw [pauliContr_mul_dualWeyl_eq_ofGaussianInt, toTensor_eq_ofGaussianInt, + prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt] conv_rhs => rw [leviCivita_mul_pauliDual] - simp only [contrMetric_eq_ofRat, toTensor_eq_ofRat, prodT_ofRat_ofRat] - simp only [leviCivita_eq_ofRat_prod, pauliCo_eq_ofRat] - rw [prodT_ofRat_ofRat, contrT_ofRat, permT_ofRat] + simp only [contrMetric_eq_ofGaussianInt, toTensor_eq_ofGaussianInt, + prodT_ofGaussianInt_ofGaussianInt] + simp only [leviCivita_eq_ofGaussianInt_prod, pauliCo_eq_ofGaussianInt] + rw [prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt, permT_ofGaussianInt] apply (Tensor.basis _).repr.injective ext b - rw [ofRat_basis_repr_apply, permT_basis_repr_symm_apply] + rw [ofGaussianInt_basis_repr_apply, permT_basis_repr_symm_apply] simp only [map_add, Finsupp.coe_add, Pi.add_apply] simp only [permT_basis_repr_symm_apply, map_neg, Finsupp.coe_neg, Pi.neg_apply, - map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, ofRat_basis_repr_apply] - conv_rhs => arg 2; rw [Physlib.RatComplexNum.I_mul_toComplexNum] - apply Physlib.RatComplexNum.toComplexNum_eq_add_neg_add_add_iff.mpr + map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, ofGaussianInt_basis_repr_apply] + conv_rhs => arg 2; rw [show ∀ a : GaussianInt, Complex.I * GaussianInt.toComplex a = + GaussianInt.toComplex (⟨0, 1⟩ * a) from fun a => by simp [GaussianInt.toComplex_def']] + apply (show ∀ a b c d e : GaussianInt, a = b + -c + d + e → GaussianInt.toComplex a = + GaussianInt.toComplex b + -GaussianInt.toComplex c + GaussianInt.toComplex d + + GaussianInt.toComplex e from fun _ _ _ _ _ h => by simp [h]) decide +revert +kernel /-- The conjugate three-Pauli identity @@ -215,20 +222,24 @@ lemma pauliContrDown_mul_pauliContr_mul_pauliContrDown : ({ + ((-Complex.I) •ₜ (ε4ℂ | μ ν ρ κ ⊗ σ^^^ | τ(κ) τ(α') τ(β)))) }ᵀ : Prop) := by conv_lhs => - rw [dualWeyl_mul_pauliContr_eq_ofRat, toTensor_dualWeyl_eq_ofRat, - prodT_ofRat_ofRat, contrT_ofRat] + rw [dualWeyl_mul_pauliContr_eq_ofGaussianInt, toTensor_dualWeyl_eq_ofGaussianInt, + prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt] conv_rhs => - simp only [contrMetric_eq_ofRat, toTensor_dualWeyl_eq_ofRat, prodT_ofRat_ofRat] - simp only [leviCivita_eq_ofRat_prod, toTensor_dualAll_eq_ofRat] - rw [prodT_ofRat_ofRat, contrT_ofRat, permT_ofRat] + simp only [contrMetric_eq_ofGaussianInt, toTensor_dualWeyl_eq_ofGaussianInt, + prodT_ofGaussianInt_ofGaussianInt] + simp only [leviCivita_eq_ofGaussianInt_prod, toTensor_dualAll_eq_ofGaussianInt] + rw [prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt, permT_ofGaussianInt] apply (Tensor.basis _).repr.injective ext b - rw [ofRat_basis_repr_apply, permT_basis_repr_symm_apply] + rw [ofGaussianInt_basis_repr_apply, permT_basis_repr_symm_apply] simp only [map_add, Finsupp.coe_add, Pi.add_apply] simp only [permT_basis_repr_symm_apply, map_neg, Finsupp.coe_neg, Pi.neg_apply, - map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, ofRat_basis_repr_apply] - conv_rhs => arg 2; rw [Physlib.RatComplexNum.neg_I_mul_toComplexNum] - apply Physlib.RatComplexNum.toComplexNum_eq_add_neg_add_add_iff.mpr + map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, ofGaussianInt_basis_repr_apply] + conv_rhs => arg 2; rw [show ∀ a : GaussianInt, -Complex.I * GaussianInt.toComplex a = + GaussianInt.toComplex (-⟨0, 1⟩ * a) from fun a => by simp [GaussianInt.toComplex_def']] + apply (show ∀ a b c d e : GaussianInt, a = b + -c + d + e → GaussianInt.toComplex a = + GaussianInt.toComplex b + -GaussianInt.toComplex c + GaussianInt.toComplex d + + GaussianInt.toComplex e from fun _ _ _ _ _ h => by simp [h]) decide +revert +kernel end PauliMatrix diff --git a/Physlib/Relativity/PauliMatrices/ToTensor.lean b/Physlib/Relativity/PauliMatrices/ToTensor.lean index d23048a4a..a1c8c6675 100644 --- a/Physlib/Relativity/PauliMatrices/ToTensor.lean +++ b/Physlib/Relativity/PauliMatrices/ToTensor.lean @@ -160,8 +160,8 @@ lemma toTensor_eq_asConsTensor : simp only [fromTripleT_apply_basis] rfl -/-- Rational-complex components of the contravariant Pauli four-vector. -/ -def pauliContrComponent (mu : Fin 4) (a b : Fin 2) : Physlib.RatComplexNum := +/-- Gaussian integer components of the contravariant Pauli four-vector. -/ +def pauliContrComponent (mu : Fin 4) (a b : Fin 2) : GaussianInt := if mu.val = 0 ∧ a.val = b.val then ⟨1, 0⟩ else if mu.val = 1 ∧ a.val ≠ b.val then ⟨1, 0⟩ else if mu.val = 2 ∧ a.val = 0 ∧ b.val = 1 then ⟨0, -1⟩ else @@ -169,8 +169,8 @@ def pauliContrComponent (mu : Fin 4) (a b : Fin 2) : Physlib.RatComplexNum := if mu.val = 3 ∧ a.val = 0 ∧ b.val = 0 then ⟨1, 0⟩ else if mu.val = 3 ∧ a.val = 1 ∧ b.val = 1 then ⟨-1, 0⟩ else 0 -/-- Rational-complex components of the contravariant conjugate Pauli four-vector. -/ -def pauliContrDownComponent (mu : Fin 4) (a b : Fin 2) : Physlib.RatComplexNum := +/-- Gaussian integer components of the contravariant conjugate Pauli four-vector. -/ +def pauliContrDownComponent (mu : Fin 4) (a b : Fin 2) : GaussianInt := if mu.val = 0 ∧ a.val = b.val then ⟨1, 0⟩ else if mu.val = 1 ∧ a.val ≠ b.val then ⟨-1, 0⟩ else if mu.val = 2 ∧ a.val = 0 ∧ b.val = 1 then ⟨0, 1⟩ else @@ -179,118 +179,118 @@ def pauliContrDownComponent (mu : Fin 4) (a b : Fin 2) : Physlib.RatComplexNum : if mu.val = 3 ∧ a.val = 1 ∧ b.val = 1 then ⟨1, 0⟩ else 0 set_option backward.isDefEq.respectTransparency false in -lemma toTensor_eq_ofRat : σ^^^ = ofRat (fun b => +lemma toTensor_eq_ofGaussianInt : σ^^^ = ofGaussianInt (fun b => pauliContrComponent (b 0) (b 1) (b 2)) := by apply (Tensor.basis _).repr.injective ext b rw [toTensor_basis_expand] simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue] - repeat rw [basis_eq_ofRat] + repeat rw [basis_eq_ofGaussianInt] + have hI : I = GaussianInt.toComplex ⟨0, 1⟩ := by simp [GaussianInt.toComplex_def'] simp only [Fin.isValue, map_sub, map_add, _root_.map_smul, Finsupp.coe_sub, Finsupp.coe_add, - Finsupp.coe_smul, Pi.sub_apply, Pi.add_apply, ofRat_basis_repr_apply, Pi.smul_apply, - smul_eq_mul, Physlib.RatComplexNum.I_mul_toComplexNum, mul_ite, - Nat.succ_eq_add_one, Nat.reduceAdd] - simp only [Fin.isValue, ← map_add, ← map_sub] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + Finsupp.coe_smul, Pi.sub_apply, Pi.add_apply, ofGaussianInt_basis_repr_apply, Pi.smul_apply, + smul_eq_mul, hI, Nat.succ_eq_add_one, Nat.reduceAdd] + simp only [Fin.isValue, ← map_mul, ← map_add, ← map_sub] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr revert b decide +kernel set_option backward.isDefEq.respectTransparency false in -/-- Rational-complex components of `σ^^^` after dualizing its left-handed Weyl index. -/ -lemma toTensor_dualLeft_eq_ofRat : +/-- Gaussian integer components of `σ^^^` after dualizing its left-handed Weyl index. -/ +lemma toTensor_dualLeft_eq_ofGaussianInt : {σ^^^ | μ τ(α) β}ᵀ = - ofRat (fun b => + ofGaussianInt (fun b => ∑ x : Fin 2, pauliContrComponent (b 0) x (b 2) * (if x.val = 0 ∧ (b 1).val = 1 then 1 else if (b 1).val = 0 ∧ x.val = 1 then -1 else 0)) := by let M : ℂT[.downL, .downL] := εL' conv_lhs => - rw [toTensor_eq_ofRat, toDualMapAtIndex] - change crossToSlot 1 0 (by rfl) M (ofRat _) + rw [toTensor_eq_ofGaussianInt, toDualMapAtIndex] + change crossToSlot 1 0 (by rfl) M (ofGaussianInt _) erw [crossToSlot_eq_crossToEnd, crossToEnd] simp only [LinearMap.compr₂_apply, LinearMap.comp_apply] dsimp only [M] - rw [dualLeftMetric_eq_ofRat, prodT_ofRat_ofRat, permT_ofRat, contrT_ofRat, - permT_ofRat, permT_ofRat] - congr - funext b + rw [dualLeftMetric_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, permT_ofGaussianInt, + contrT_ofGaussianInt, permT_ofGaussianInt, permT_ofGaussianInt] + -- `congr` would first try `rfl` on the component functions, which is expensive here. + refine congrArg ofGaussianInt (funext fun b => ?_) decide +revert +kernel set_option backward.isDefEq.respectTransparency false in -/-- Rational-complex components of `σ^^^` after dualizing both Weyl indices. -/ -lemma toTensor_dualWeyl_eq_ofRat : +/-- Gaussian integer components of `σ^^^` after dualizing both Weyl indices. -/ +lemma toTensor_dualWeyl_eq_ofGaussianInt : {σ^^^ | μ τ(α) τ(β)}ᵀ = - ofRat (fun b => + ofGaussianInt (fun b => pauliContrDownComponent (b 0) (b 2) (b 1)) := by - rw [toTensor_dualLeft_eq_ofRat] + rw [toTensor_dualLeft_eq_ofGaussianInt] let M : ℂT[.downR, .downR] := εR' conv_lhs => rw [toDualMapAtIndex] - change crossToSlot 2 0 (by rfl) M (ofRat _) + change crossToSlot 2 0 (by rfl) M (ofGaussianInt _) erw [crossToSlot_eq_crossToEnd, crossToEnd] simp only [LinearMap.compr₂_apply, LinearMap.comp_apply] dsimp only [M] - rw [dualRightMetric_eq_ofRat, prodT_ofRat_ofRat, permT_ofRat, contrT_ofRat, - permT_ofRat, permT_ofRat] + rw [dualRightMetric_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, permT_ofGaussianInt, + contrT_ofGaussianInt, permT_ofGaussianInt, permT_ofGaussianInt] congr funext b decide +revert +kernel set_option backward.isDefEq.respectTransparency false in -/-- Rational-complex components of `σ^^^` after dualizing its Lorentz index. -/ -lemma toTensor_dualLorentz_eq_ofRat : +/-- Gaussian integer components of `σ^^^` after dualizing its Lorentz index. -/ +lemma toTensor_dualLorentz_eq_ofGaussianInt : {σ^^^ | τ(μ) α β}ᵀ = - ofRat (fun b => pauliContrDownComponent (b 0) (b 1) (b 2)) := by + ofGaussianInt (fun b => pauliContrDownComponent (b 0) (b 1) (b 2)) := by let M : ℂT[.down, .down] := η' conv_lhs => - rw [toTensor_eq_ofRat, toDualMapAtIndex] - change crossToSlot 0 0 (by rfl) M (ofRat _) + rw [toTensor_eq_ofGaussianInt, toDualMapAtIndex] + change crossToSlot 0 0 (by rfl) M (ofGaussianInt _) erw [crossToSlot_eq_crossToEnd, crossToEnd] simp only [LinearMap.compr₂_apply, LinearMap.comp_apply] dsimp only [M] - rw [coMetric_eq_ofRat, prodT_ofRat_ofRat, permT_ofRat, contrT_ofRat, - permT_ofRat, permT_ofRat] + rw [coMetric_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, permT_ofGaussianInt, + contrT_ofGaussianInt, permT_ofGaussianInt, permT_ofGaussianInt] congr funext b decide +revert +kernel set_option backward.isDefEq.respectTransparency false in -/-- Rational-complex components of `σ^^^` after dualizing its Lorentz and left-handed Weyl +/-- Gaussian integer components of `σ^^^` after dualizing its Lorentz and left-handed Weyl indices. -/ -lemma toTensor_dualLorentzLeft_eq_ofRat : - {σ^^^ | τ(μ) τ(α) β}ᵀ = ofRat (fun b => +lemma toTensor_dualLorentzLeft_eq_ofGaussianInt : + {σ^^^ | τ(μ) τ(α) β}ᵀ = ofGaussianInt (fun b => ∑ x : Fin 2, pauliContrDownComponent (b 0) x (b 2) * (if x.val = 0 ∧ (b 1).val = 1 then 1 else if (b 1).val = 0 ∧ x.val = 1 then -1 else 0)) := by - rw [toTensor_dualLorentz_eq_ofRat] + rw [toTensor_dualLorentz_eq_ofGaussianInt] let M : ℂT[.downL, .downL] := εL' conv_lhs => rw [toDualMapAtIndex] - change crossToSlot 1 0 (by rfl) M (ofRat _) + change crossToSlot 1 0 (by rfl) M (ofGaussianInt _) erw [crossToSlot_eq_crossToEnd, crossToEnd] simp only [LinearMap.compr₂_apply, LinearMap.comp_apply] dsimp only [M] - rw [dualLeftMetric_eq_ofRat, prodT_ofRat_ofRat, permT_ofRat, contrT_ofRat, - permT_ofRat, permT_ofRat] - congr - funext b + rw [dualLeftMetric_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, permT_ofGaussianInt, + contrT_ofGaussianInt, permT_ofGaussianInt, permT_ofGaussianInt] + -- `congr` would first try `rfl` on the component functions, which is expensive here. + refine congrArg ofGaussianInt (funext fun b => ?_) decide +revert +kernel set_option backward.isDefEq.respectTransparency false in -/-- Rational-complex components of `σ^^^` after dualizing all three indices. -/ -lemma toTensor_dualAll_eq_ofRat : +/-- Gaussian integer components of `σ^^^` after dualizing all three indices. -/ +lemma toTensor_dualAll_eq_ofGaussianInt : {σ^^^ | τ(μ) τ(α) τ(β)}ᵀ = - ofRat (fun b => pauliContrComponent (b 0) (b 2) (b 1)) := by - rw [toTensor_dualLorentzLeft_eq_ofRat] + ofGaussianInt (fun b => pauliContrComponent (b 0) (b 2) (b 1)) := by + rw [toTensor_dualLorentzLeft_eq_ofGaussianInt] let M : ℂT[.downR, .downR] := εR' conv_lhs => rw [toDualMapAtIndex] - change crossToSlot 2 0 (by rfl) M (ofRat _) + change crossToSlot 2 0 (by rfl) M (ofGaussianInt _) erw [crossToSlot_eq_crossToEnd, crossToEnd] simp only [LinearMap.compr₂_apply, LinearMap.comp_apply] dsimp only [M] - rw [dualRightMetric_eq_ofRat, prodT_ofRat_ofRat, permT_ofRat, contrT_ofRat, - permT_ofRat, permT_ofRat] + rw [dualRightMetric_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, permT_ofGaussianInt, + contrT_ofGaussianInt, permT_ofGaussianInt, permT_ofGaussianInt] congr funext b decide +revert +kernel @@ -341,7 +341,7 @@ scoped[PauliMatrix] notation "σ^__" => PauliMatrix.pauliContrDown open Lorentz set_option backward.isDefEq.respectTransparency false in -lemma pauliCo_eq_ofRat : pauliCo = ofRat (fun b => +lemma pauliCo_eq_ofGaussianInt : pauliCo = ofGaussianInt (fun b => pauliContrDownComponent (b 0) (b 1) (b 2)) := by apply (Tensor.basis _).repr.injective ext b @@ -350,19 +350,19 @@ lemma pauliCo_eq_ofRat : pauliCo = ofRat (fun b => rw [contrT_basis_repr_apply] conv_lhs => enter [2, x] - rw [contr_basis_ratComplexNum] + rw [contr_basis_gaussianInt] rw [prodT_basis_repr_apply] - simp only [coMetric_eq_ofRat, ofRat_basis_repr_apply, toTensor_eq_ofRat] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← map_sum Physlib.RatComplexNum.toComplexNum] - rw [ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + simp only [coMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, toTensor_eq_ofGaussianInt] + rw [← GaussianInt.toComplex.map_mul] + rw [← GaussianInt.toComplex.map_mul] + rw [← map_sum GaussianInt.toComplex] + rw [ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr revert b decide +kernel set_option backward.isDefEq.respectTransparency false in -lemma pauliCoDown_eq_ofRat : pauliCoDown = ofRat (fun b => +lemma pauliCoDown_eq_ofGaussianInt : pauliCoDown = ofGaussianInt (fun b => pauliContrComponent (b 0) (b 1) (b 2)) := by apply (Tensor.basis _).repr.injective ext b @@ -371,31 +371,31 @@ lemma pauliCoDown_eq_ofRat : pauliCoDown = ofRat (fun b => rw [contrT_basis_repr_apply] conv_lhs => enter [2, x] - rw [contr_basis_ratComplexNum] + rw [contr_basis_gaussianInt] rw [prodT_basis_repr_apply] rw [contrT_basis_repr_apply] - simp only [coMetric_eq_ofRat, ofRat_basis_repr_apply, - dualLeftMetric_eq_ofRat] + simp only [coMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, + dualLeftMetric_eq_ofGaussianInt] enter [1, 1, 2, y] - rw [contr_basis_ratComplexNum] + rw [contr_basis_gaussianInt] rw [prodT_basis_repr_apply] - simp only [coMetric_eq_ofRat, ofRat_basis_repr_apply, pauliCo_eq_ofRat, - dualRightMetric_eq_ofRat] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] + simp only [coMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, pauliCo_eq_ofGaussianInt, + dualRightMetric_eq_ofGaussianInt] + rw [← GaussianInt.toComplex.map_mul] + rw [← GaussianInt.toComplex.map_mul] conv_lhs => enter [2, x] - rw [← map_sum Physlib.RatComplexNum.toComplexNum] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← map_sum Physlib.RatComplexNum.toComplexNum] - rw [ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + rw [← map_sum GaussianInt.toComplex] + rw [← GaussianInt.toComplex.map_mul] + rw [← GaussianInt.toComplex.map_mul] + rw [← map_sum GaussianInt.toComplex] + rw [ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr revert b decide +kernel set_option backward.isDefEq.respectTransparency false in -lemma pauliContrDown_ofRat : pauliContrDown = ofRat (fun b => +lemma pauliContrDown_ofGaussianInt : pauliContrDown = ofGaussianInt (fun b => pauliContrDownComponent (b 0) (b 1) (b 2)) := by apply (Tensor.basis _).repr.injective ext b @@ -404,26 +404,26 @@ lemma pauliContrDown_ofRat : pauliContrDown = ofRat (fun b => rw [contrT_basis_repr_apply] conv_lhs => enter [2, x] - rw [contr_basis_ratComplexNum] + rw [contr_basis_gaussianInt] rw [prodT_basis_repr_apply] rw [contrT_basis_repr_apply] - simp only [coMetric_eq_ofRat, ofRat_basis_repr_apply, - dualLeftMetric_eq_ofRat] + simp only [coMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, + dualLeftMetric_eq_ofGaussianInt] enter [1, 1, 2, y] - rw [contr_basis_ratComplexNum] + rw [contr_basis_gaussianInt] rw [prodT_basis_repr_apply] - simp only [coMetric_eq_ofRat,ofRat_basis_repr_apply, toTensor_eq_ofRat, - dualRightMetric_eq_ofRat] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] + simp only [coMetric_eq_ofGaussianInt,ofGaussianInt_basis_repr_apply, toTensor_eq_ofGaussianInt, + dualRightMetric_eq_ofGaussianInt] + rw [← GaussianInt.toComplex.map_mul] + rw [← GaussianInt.toComplex.map_mul] conv_lhs => enter [2, x] - rw [← map_sum Physlib.RatComplexNum.toComplexNum] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← map_sum Physlib.RatComplexNum.toComplexNum] - rw [ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + rw [← map_sum GaussianInt.toComplex] + rw [← GaussianInt.toComplex.map_mul] + rw [← GaussianInt.toComplex.map_mul] + rw [← map_sum GaussianInt.toComplex] + rw [ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr revert b decide +kernel @@ -436,22 +436,22 @@ lemma pauliContrDown_ofRat : pauliContrDown = ofRat (fun b => /-- Dualizing both Weyl indices of `σ^^^` gives `σ^__`. -/ lemma toTensor_dualWeyl_eq_pauliContrDown : ({σ^^^ | μ τ(α) τ(β) = σ^__ | μ β α}ᵀ : Prop) := by - rw [toTensor_dualWeyl_eq_ofRat] - rw [pauliContrDown_ofRat, permT_ofRat] + rw [toTensor_dualWeyl_eq_ofGaussianInt] + rw [pauliContrDown_ofGaussianInt, permT_ofGaussianInt] congr /-- Dualizing all three indices of `σ^^^` gives `σ___`. -/ lemma toTensor_dualAll_eq_pauliCoDown : ({σ^^^ | τ(μ) τ(α) τ(β) = σ___ | μ β α}ᵀ : Prop) := by - rw [toTensor_dualAll_eq_ofRat] - rw [pauliCoDown_eq_ofRat, permT_ofRat] + rw [toTensor_dualAll_eq_ofGaussianInt] + rw [pauliCoDown_eq_ofGaussianInt, permT_ofGaussianInt] congr set_option backward.isDefEq.respectTransparency false in /-- Lowering the Lorentz index of `σ^^^` with `τ` gives `σ_^^`. -/ lemma pauliDual_eq_pauliCo : ({σ^^^ | τ(μ) α β = σ_^^ | μ α β}ᵀ : Prop) := by - rw [toTensor_dualLorentz_eq_ofRat, pauliCo_eq_ofRat, permT_ofRat] + rw [toTensor_dualLorentz_eq_ofGaussianInt, pauliCo_eq_ofGaussianInt, permT_ofGaussianInt] congr set_option backward.isDefEq.respectTransparency false in @@ -468,23 +468,24 @@ lemma pauliContrDownDual_eq_pauliCoDown : change (toDualMapAtIndex (S := complexLorentzTensor) 0) pauliContrDown = permT id h pauliCoDown conv_lhs => - rw [pauliContrDown_ofRat] + rw [pauliContrDown_ofGaussianInt] rw [toDualMapAtIndex] - change crossToSlot (S := complexLorentzTensor) 0 0 rfl η' (ofRat _) + change crossToSlot (S := complexLorentzTensor) 0 0 rfl η' (ofGaussianInt _) rw [crossToSlot_eq_crossToEnd, crossToEnd] simp only [LinearMap.compr₂_apply, LinearMap.comp_apply] - rw [coMetric_eq_ofRat] - rw [prodT_ofRat_ofRat, permT_ofRat, contrT_ofRat, permT_ofRat, permT_ofRat] + rw [coMetric_eq_ofGaussianInt] + rw [prodT_ofGaussianInt_ofGaussianInt, permT_ofGaussianInt, contrT_ofGaussianInt, + permT_ofGaussianInt, permT_ofGaussianInt] conv_rhs => - rw [pauliCoDown_eq_ofRat] + rw [pauliCoDown_eq_ofGaussianInt] apply (Tensor.basis _).repr.injective ext b conv_rhs => rw [permT_basis_repr_symm_apply h] - rw [ofRat_basis_repr_apply] + rw [ofGaussianInt_basis_repr_apply] conv_lhs => - rw [ofRat_basis_repr_apply] - apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr + rw [ofGaussianInt_basis_repr_apply] + apply (Function.Injective.eq_iff GaussianInt.toComplex_injective).mpr revert b decide +kernel rw [hDual] diff --git a/Physlib/Relativity/Tensors/API-map.yaml b/Physlib/Relativity/Tensors/API-map.yaml index a7907f3d6..6d48b1e5c 100644 --- a/Physlib/Relativity/Tensors/API-map.yaml +++ b/Physlib/Relativity/Tensors/API-map.yaml @@ -69,7 +69,7 @@ Requirements: - description: "The API contains explicit constructors of tensors from vectors, from elements of a tensor product of two or three carriers, and from invariant maps, together with tensors specified by integer or rational components in the standard basis." done: true location: | - Physlib/Relativity/Tensors/Constructors.lean (Pure.fromSingleP, fromSingleT, fromPairT, fromPairTContr, fromSingleTContrFromPairT, fromConstPair, fromTripleT, fromConstTriple); Physlib/Relativity/Tensors/OfInt.lean (TensorInt, TensorInt.toTensor, basis_eq_tensorInt); Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean (ofRat, basis_eq_ofRat, prodT_ofRat_ofRat, contrT_ofRat, permT_ofRat) + Physlib/Relativity/Tensors/Constructors.lean (Pure.fromSingleP, fromSingleT, fromPairT, fromPairTContr, fromSingleTContrFromPairT, fromConstPair, fromTripleT, fromConstTriple); Physlib/Relativity/Tensors/OfInt.lean (TensorInt, TensorInt.toTensor, basis_eq_tensorInt); Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean (ofGaussianInt, basis_eq_ofGaussianInt, prodT_ofGaussianInt_ofGaussianInt, contrT_ofGaussianInt, permT_ofGaussianInt) - description: "The API contains an elaborator turning pen-and-paper index expressions into tensor operations, and the class `Tensorial` carrying index notation to any type linearly equivalent to a tensor, with the induced group action, basis and products." done: true @@ -103,7 +103,7 @@ Requirements: - description: "The API contains the tensor species `complexLorentzTensor` of complex Lorentz tensors, with the left- and right-handed Weyl colors, their duals and the two Lorentz vector colors over SL(2, ℂ), together with the metric and unit tensors of each color in several equivalent forms and the identification of pairwise products of complex Lorentz vectors with matrices." done: true location: | - Physlib/Relativity/Tensors/ComplexTensor/Basic.lean (complexLorentzTensor, complexLorentzTensor.Color, repDim, basis, rep, contrPCoeff_basis); Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Modules.lean (ContrℂModule, CoℂModule, ContrℂModule.SL2CRep, CoℂModule.SL2CRep); Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Contraction.lean (contrCoContraction, coContrContraction); Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean (coMetric, contrMetric, leftMetric, rightMetric, dualLeftMetric, dualRightMetric, coMetric_eq_ofRat, leftMetric_eq_ofRat); Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean (coContrUnit, contrCoUnit, dualLeftLeftUnit, leftDualLeftUnit, dualRightRightUnit, rightDualRightUnit); Physlib/Relativity/Tensors/ComplexTensor/Units/Symm.lean (coContrUnit_symm, dualLeftLeftUnit_symm); Physlib/Relativity/Tensors/ComplexTensor/Matrix/Pre.lean (contrContrToMatrix, coCoToMatrix, contrCoToMatrix, coContrToMatrix); Physlib/Relativity/Tensors/ComplexTensor/Lemmas.lean (antiSymm_contr_symm); Physlib/Relativity/Tensors/LeviCivita/Complex.lean (leviCivita, notation ε4ℂ, leviCivita_eq_ofRat) + Physlib/Relativity/Tensors/ComplexTensor/Basic.lean (complexLorentzTensor, complexLorentzTensor.Color, repDim, basis, rep, contrPCoeff_basis); Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Modules.lean (ContrℂModule, CoℂModule, ContrℂModule.SL2CRep, CoℂModule.SL2CRep); Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Contraction.lean (contrCoContraction, coContrContraction); Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean (coMetric, contrMetric, leftMetric, rightMetric, dualLeftMetric, dualRightMetric, coMetric_eq_ofGaussianInt, leftMetric_eq_ofGaussianInt); Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean (coContrUnit, contrCoUnit, dualLeftLeftUnit, leftDualLeftUnit, dualRightRightUnit, rightDualRightUnit); Physlib/Relativity/Tensors/ComplexTensor/Units/Symm.lean (coContrUnit_symm, dualLeftLeftUnit_symm); Physlib/Relativity/Tensors/ComplexTensor/Matrix/Pre.lean (contrContrToMatrix, coCoToMatrix, contrCoToMatrix, coContrToMatrix); Physlib/Relativity/Tensors/ComplexTensor/Lemmas.lean (antiSymm_contr_symm); Physlib/Relativity/Tensors/LeviCivita/Complex.lean (leviCivita, notation ε4ℂ, leviCivita_eq_ofGaussianInt) - description: "The API contains a canonical injective semilinear map from real Lorentz tensors to complex Lorentz tensors, equivariant for the complexified Lorentz group and commuting with permutations, products, contractions and evaluations of indices." done: true diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean index a8e043342..983805980 100644 --- a/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean +++ b/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Relativity.Tensors.ComplexTensor.OfRat +public import Physlib.Relativity.Tensors.ComplexTensor.OfGaussianInt /-! ## Metrics as complex Lorentz tensors @@ -360,71 +360,73 @@ lemma dualRightMetric_eq_basis : εR' = /-! -### ofRat +### ofGaussianInt -/ set_option backward.isDefEq.respectTransparency false in -lemma coMetric_eq_ofRat : η' = ofRat fun f => +lemma coMetric_eq_ofGaussianInt : η' = ofGaussianInt fun f => if f 0 = Fin.cast (by rfl) (0 : Fin 4) ∧ f 1 = Fin.cast (by rfl) (0 : Fin 4) then 1 else if f 0 = f 1 then - 1 else 0 := by rw [coMetric_eq_basis] conv_lhs => - rw [basis_eq_ofRat, basis_eq_ofRat, basis_eq_ofRat, basis_eq_ofRat] + rw [basis_eq_ofGaussianInt, basis_eq_ofGaussianInt, basis_eq_ofGaussianInt, + basis_eq_ofGaussianInt] rw [← map_sub, ← map_sub, ← map_sub] congr with_unfolding_all decide set_option backward.isDefEq.respectTransparency false in -lemma contrMetric_eq_ofRat : η = ofRat fun f => +lemma contrMetric_eq_ofGaussianInt : η = ofGaussianInt fun f => if f 0 = Fin.cast (by rfl) (0 : Fin 4) ∧ f 1 = Fin.cast (by rfl) (0 : Fin 4) then 1 else if f 0 = f 1 then - 1 else 0 := by rw [contrMetric_eq_basis] conv_lhs => - rw [basis_eq_ofRat, basis_eq_ofRat, basis_eq_ofRat, basis_eq_ofRat] + rw [basis_eq_ofGaussianInt, basis_eq_ofGaussianInt, basis_eq_ofGaussianInt, + basis_eq_ofGaussianInt] rw [← map_sub, ← map_sub, ← map_sub] congr with_unfolding_all decide -lemma leftMetric_eq_ofRat : εL = ofRat fun f => +lemma leftMetric_eq_ofGaussianInt : εL = ofGaussianInt fun f => if f 0 = Fin.cast (by rfl) (0 : Fin 2) ∧ f 1 = Fin.cast (by rfl) (1 : Fin 2) then - 1 else if f 1 = Fin.cast (by rfl) (0 : Fin 2) ∧ f 0 = Fin.cast (by rfl) (1 : Fin 2) then 1 else 0 := by rw [leftMetric_eq_basis] conv_lhs => - rw [basis_eq_ofRat, basis_eq_ofRat] + rw [basis_eq_ofGaussianInt, basis_eq_ofGaussianInt] rw [← map_neg, ← map_add] congr with_unfolding_all decide -lemma dualLeftMetric_eq_ofRat : εL' = ofRat fun f => +lemma dualLeftMetric_eq_ofGaussianInt : εL' = ofGaussianInt fun f => if f 0 = Fin.cast (by rfl) (0 : Fin 2) ∧ f 1 = Fin.cast (by rfl) (1 : Fin 2) then 1 else if f 1 = Fin.cast (by rfl) (0 : Fin 2) ∧ f 0 = Fin.cast (by rfl) (1 : Fin 2) then - 1 else 0 := by rw [dualLeftMetric_eq_basis] conv_lhs => - rw [basis_eq_ofRat, basis_eq_ofRat] + rw [basis_eq_ofGaussianInt, basis_eq_ofGaussianInt] rw [← map_sub] congr with_unfolding_all decide -lemma rightMetric_eq_ofRat : εR = ofRat fun f => +lemma rightMetric_eq_ofGaussianInt : εR = ofGaussianInt fun f => if f 0 = Fin.cast (by rfl) (0 : Fin 2) ∧ f 1 = Fin.cast (by rfl) (1 : Fin 2) then - 1 else if f 1 = Fin.cast (by rfl) (0 : Fin 2) ∧ f 0 = Fin.cast (by rfl) (1 : Fin 2) then 1 else 0 := by rw [rightMetric_eq_basis] conv_lhs => - rw [basis_eq_ofRat, basis_eq_ofRat] + rw [basis_eq_ofGaussianInt, basis_eq_ofGaussianInt] rw [← map_neg, ← map_add] congr with_unfolding_all decide -lemma dualRightMetric_eq_ofRat : εR' = ofRat fun f => +lemma dualRightMetric_eq_ofGaussianInt : εR' = ofGaussianInt fun f => if f 0 = Fin.cast (by rfl) (0 : Fin 2) ∧ f 1 = Fin.cast (by rfl) (1 : Fin 2) then 1 else if f 1 = Fin.cast (by rfl) (0 : Fin 2) ∧ f 0 = Fin.cast (by rfl) (1 : Fin 2) then - 1 else 0 := by rw [dualRightMetric_eq_basis] conv_lhs => - rw [basis_eq_ofRat, basis_eq_ofRat] + rw [basis_eq_ofGaussianInt, basis_eq_ofGaussianInt] rw [← map_sub] congr with_unfolding_all decide diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Lemmas.lean b/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Lemmas.lean index ba4796ff7..e426e2a46 100644 --- a/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Lemmas.lean +++ b/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Lemmas.lean @@ -35,7 +35,7 @@ lemma coMetric_symm : {η' | μ ν = η' | ν μ}ᵀ := by apply (Tensor.basis _).repr.injective ext b rw [permT_basis_repr_symm_apply] - rw [coMetric_eq_ofRat, ofRat_basis_repr_apply, ofRat_basis_repr_apply] + rw [coMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, ofGaussianInt_basis_repr_apply] congr 1 revert b decide @@ -45,7 +45,7 @@ lemma contrMetric_symm : {η | μ ν = η | ν μ}ᵀ := by apply (Tensor.basis _).repr.injective ext b rw [permT_basis_repr_symm_apply] - rw [contrMetric_eq_ofRat, ofRat_basis_repr_apply, ofRat_basis_repr_apply] + rw [contrMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, ofGaussianInt_basis_repr_apply] congr 1 revert b decide @@ -55,7 +55,8 @@ lemma leftMetric_antisymm : {εL | α α' = - (εL| α' α)}ᵀ := by apply (Tensor.basis _).repr.injective ext b rw [permT_basis_repr_symm_apply] - rw [leftMetric_eq_ofRat, ofRat_basis_repr_apply, ← map_neg, ofRat_basis_repr_apply] + rw [leftMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, ← map_neg, + ofGaussianInt_basis_repr_apply] congr 1 revert b decide @@ -65,7 +66,8 @@ lemma rightMetric_antisymm : {εR | β β' = - (εR| β' β)}ᵀ := by apply (Tensor.basis _).repr.injective ext b rw [permT_basis_repr_symm_apply] - rw [rightMetric_eq_ofRat, ofRat_basis_repr_apply, ← map_neg, ofRat_basis_repr_apply] + rw [rightMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, ← map_neg, + ofGaussianInt_basis_repr_apply] congr 1 revert b decide @@ -75,7 +77,8 @@ lemma dualLeftMetric_antisymm : {εL' | α α' = - (εL' | α' α)}ᵀ := by apply (Tensor.basis _).repr.injective ext b rw [permT_basis_repr_symm_apply] - rw [dualLeftMetric_eq_ofRat, ofRat_basis_repr_apply, ← map_neg, ofRat_basis_repr_apply] + rw [dualLeftMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, ← map_neg, + ofGaussianInt_basis_repr_apply] congr 1 revert b decide @@ -85,7 +88,8 @@ lemma dualRightMetric_antisymm : {εR' | α α' = - (εR' | α' α)}ᵀ := by apply (Tensor.basis _).repr.injective ext b rw [permT_basis_repr_symm_apply] - rw [dualRightMetric_eq_ofRat, ofRat_basis_repr_apply, ← map_neg, ofRat_basis_repr_apply] + rw [dualRightMetric_eq_ofGaussianInt, ofGaussianInt_basis_repr_apply, ← map_neg, + ofGaussianInt_basis_repr_apply] congr 1 revert b decide diff --git a/Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean b/Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean similarity index 58% rename from Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean rename to Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean index ef90eb3d1..cd53dcdbc 100644 --- a/Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean +++ b/Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean @@ -6,11 +6,15 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.Tensors.ComplexTensor.Basic -public import Physlib.Mathematics.RatComplexNum -public import Physlib.Relativity.Tensors.Dual +public import Mathlib.NumberTheory.Zsqrtd.GaussianInt /-! -# Basis for tensors in a tensor species +# Complex Lorentz tensors with Gaussian integer components + +A complex Lorentz tensor whose components in the standard basis are Gaussian integers can be +written as `ofGaussianInt f` for a map `f` from component indices to `GaussianInt`. The +product, contraction and permutation of such tensors are again of this form, so identities +between them reduce to decidable equalities of Gaussian integers. -/ @@ -21,22 +25,20 @@ open CategoryTheory open MonoidalCategory namespace complexLorentzTensor -open Physlib.RatComplexNum -open Physlib open TensorSpecies open Tensor -/--A complex Lorentz tensor from a map - `(Π j, Fin (complexLorentzTensor.repDim (c j))) → RatComplexNum`. All - complex Lorentz tensors with rational coefficients with respect to the basis are of this - form. -/ -noncomputable def ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.Color} : - ((ComponentIdx (S := complexLorentzTensor) c) → RatComplexNum) →ₛₗ[toComplexNum] ℂT(c) where +/-- A complex Lorentz tensor from a map + `(Π j, Fin (complexLorentzTensor.repDim (c j))) → GaussianInt`. All complex Lorentz tensors + with Gaussian integer coefficients with respect to the basis are of this form. -/ +noncomputable def ofGaussianInt {n : ℕ} {c : Fin n → complexLorentzTensor.Color} : + ((ComponentIdx (S := complexLorentzTensor) c) → GaussianInt) →ₛₗ[GaussianInt.toComplex] + ℂT(c) where toFun f := (Tensor.basis c).repr.symm <| (Finsupp.linearEquivFunOnFinite ℂ ℂ ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j)))).symm <| - (fun j => toComplexNum (f j)) + (fun j => GaussianInt.toComplex (f j)) map_add' f f1 := by apply (Tensor.basis _).repr.injective ext b @@ -47,34 +49,29 @@ noncomputable def ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.Color} : simp @[simp] -lemma ofRat_basis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTensor.Color} - (f : (ComponentIdx c) → RatComplexNum) +lemma ofGaussianInt_basis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTensor.Color} + (f : (ComponentIdx c) → GaussianInt) (b :(ComponentIdx c)) : - (Tensor.basis c).repr (ofRat f) b = toComplexNum (f b) := by - simp [ofRat] + (Tensor.basis c).repr (ofGaussianInt f) b = GaussianInt.toComplex (f b) := by + simp [ofGaussianInt] -lemma basis_eq_ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.Color} +lemma basis_eq_ofGaussianInt {n : ℕ} {c : Fin n → complexLorentzTensor.Color} (b : (ComponentIdx c)) : Tensor.basis c b - = ofRat (fun b' => if b = b' then ⟨1, 0⟩ else ⟨0, 0⟩) := by + = ofGaussianInt (fun b' => if b = b' then 1 else 0) := by apply (Tensor.basis c).repr.injective - simp only [Basis.repr_self] ext b' - simp only [ofRat_basis_repr_apply] - rw [Finsupp.single_apply, toComplexNum] - simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] - split - simp only [Rat.cast_one, Rat.cast_zero, zero_mul, add_zero] - simp + rw [Basis.repr_self, ofGaussianInt_basis_repr_apply, Finsupp.single_apply] + split <;> simp set_option backward.isDefEq.respectTransparency false in -lemma contr_basis_ratComplexNum {c : complexLorentzTensor.Color} +lemma contr_basis_gaussianInt {c : complexLorentzTensor.Color} (i : Fin (complexLorentzTensor.repDim c)) (j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) : ((complexLorentzTensor.contr c) (complexLorentzTensor.basis c i ⊗ₜ complexLorentzTensor.basis (complexLorentzTensor.τ c) j)) - = toComplexNum (if i.val = j.val then 1 else 0) := by + = GaussianInt.toComplex (if i.val = j.val then 1 else 0) := by match c with | Color.upL => change Fermion.leftDualContraction @@ -109,22 +106,23 @@ lemma contr_basis_ratComplexNum {c : complexLorentzTensor.Color} open TensorSpecies open Tensor -lemma prodT_ofRat_ofRat {n n1 : ℕ} {c : Fin n → complexLorentzTensor.Color} - (f : (ComponentIdx c) → RatComplexNum) +lemma prodT_ofGaussianInt_ofGaussianInt {n n1 : ℕ} {c : Fin n → complexLorentzTensor.Color} + (f : (ComponentIdx c) → GaussianInt) {c1 : Fin n1 → complexLorentzTensor.Color} - (f1 : (ComponentIdx c1) → RatComplexNum) : - (prodT (ofRat f) (ofRat f1)) = - ((ofRat (fun b => f (ComponentIdx.prod b).1 * + (f1 : (ComponentIdx c1) → GaussianInt) : + (prodT (ofGaussianInt f) (ofGaussianInt f1)) = + ((ofGaussianInt (fun b => f (ComponentIdx.prod b).1 * f1 (ComponentIdx.prod b).2))) := by apply (Tensor.basis _).repr.injective ext b rw [prodT_basis_repr_apply] - simp only [ofRat_basis_repr_apply, map_mul] + simp only [ofGaussianInt_basis_repr_apply, map_mul] -lemma contrT_ofRat_eq_sum_dropPairSection {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.Color} +lemma contrT_ofGaussianInt_eq_sum_dropPairSection {n : ℕ} + {c : Fin (n + 1 + 1) → complexLorentzTensor.Color} {i j : Fin (n + 1 + 1)} {h : i ≠ j ∧ complexLorentzTensor.τ (c i) = c j } - (f : (ComponentIdx c) → RatComplexNum) : - (contrT n i j h (ofRat f)) = ((ofRat (fun b => + (f : (ComponentIdx c) → GaussianInt) : + (contrT n i j h (ofGaussianInt f)) = ((ofGaussianInt (fun b => (∑ x : ComponentIdx.DropPairSection b, f x.1 * if (x.1 i).1 = (x.1 j).1 then 1 else 0)))) := by apply (Tensor.basis _).repr.injective @@ -132,24 +130,24 @@ lemma contrT_ofRat_eq_sum_dropPairSection {n : ℕ} {c : Fin (n + 1 + 1) → com rw [contrT_basis_repr_apply] conv_lhs => enter [2, x] - rw [contr_basis_ratComplexNum] + rw [contr_basis_gaussianInt] simp only [Nat.succ_eq_add_one, Finset.univ_eq_attach, - ofRat_basis_repr_apply, Fin.val_cast, mul_one, + ofGaussianInt_basis_repr_apply, Fin.val_cast, mul_one, mul_zero, Function.comp_apply] - rw [← Physlib.RatComplexNum.toComplexNum.map_mul] - rw [← map_sum Physlib.RatComplexNum.toComplexNum] - rw [ofRat_basis_repr_apply] + rw [← GaussianInt.toComplex.map_mul] + rw [← map_sum GaussianInt.toComplex] + rw [ofGaussianInt_basis_repr_apply] simp [basisIdxCongr_eq_cast] open ComponentIdx -lemma contrT_ofRat {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.Color} +lemma contrT_ofGaussianInt {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.Color} {i j : Fin (n + 1 + 1)} {h : i ≠ j ∧ complexLorentzTensor.τ (c i) = c j } - (f : (ComponentIdx c) → RatComplexNum) : - (contrT n i j h (ofRat f)) = ((ofRat (fun b => + (f : (ComponentIdx c) → GaussianInt) : + (contrT n i j h (ofGaussianInt f)) = ((ofGaussianInt (fun b => (∑ x : Fin (complexLorentzTensor.repDim (c i)), f (DropPairSection.ofFinEquiv h.1 b (x, Fin.cast (by simp [← h.2, complexLorentzTensor.repDim_tau]) x)))))) := by - rw [contrT_ofRat_eq_sum_dropPairSection] + rw [contrT_ofGaussianInt_eq_sum_dropPairSection] congr funext b rw [← (DropPairSection.ofFinEquiv h.1 b).sum_comp] @@ -167,16 +165,16 @@ lemma contrT_ofRat {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.Color exact fun a => hy ((Eq.symm a)) · simp -lemma permT_ofRat {n m : ℕ} {c : Fin n → complexLorentzTensor.Color} +lemma permT_ofGaussianInt {n m : ℕ} {c : Fin n → complexLorentzTensor.Color} {c1 : Fin m → complexLorentzTensor.Color} {σ : Fin m → Fin n} (h : IsReindexing c c1 σ) - (f : ComponentIdx c → RatComplexNum) : - (permT σ h ((ofRat f))) = - ((ofRat (fun b => f (fun i => Fin.cast (by simp [IsReindexing.inv_perserve_color]) + (f : ComponentIdx c → GaussianInt) : + (permT σ h ((ofGaussianInt f))) = + ((ofGaussianInt (fun b => f (fun i => Fin.cast (by simp [IsReindexing.inv_perserve_color]) (b (h.inv σ i)))))) := by apply (Tensor.basis _).repr.injective ext b - simp only [permT_basis_repr_symm_apply, ofRat_basis_repr_apply] + simp only [permT_basis_repr_symm_apply, ofGaussianInt_basis_repr_apply] congr ext i simp [basisIdxCongr_eq_cast] diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean index b420b58cc..68b582b13 100644 --- a/Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean +++ b/Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Relativity.Tensors.ComplexTensor.OfRat +public import Physlib.Relativity.Tensors.ComplexTensor.OfGaussianInt /-! ## Unit tensors for complex Lorentz tensors @@ -274,72 +274,72 @@ lemma rightDualRightUnit_eq_tensor_basis : δR = /-! -### ofRat +### ofGaussianInt -/ set_option backward.isDefEq.respectTransparency false in -lemma coContrUnit_eq_ofRat : δ' = ofRat fun f => +lemma coContrUnit_eq_ofGaussianInt : δ' = ofGaussianInt fun f => if f 0 = f 1 then 1 else 0 := by rw [coContrUnit_eq_basis] conv_lhs => enter [2, x] - rw [basis_eq_ofRat] + rw [basis_eq_ofGaussianInt] rw [← map_sum] congr with_unfolding_all decide set_option backward.isDefEq.respectTransparency false in -lemma contrCoUnit_eq_ofRat : δ = ofRat fun f => +lemma contrCoUnit_eq_ofGaussianInt : δ = ofGaussianInt fun f => if f 0 = f 1 then 1 else 0 := by rw [contrCoUnit_eq_basis] conv_lhs => enter [2, x] - rw [basis_eq_ofRat] + rw [basis_eq_ofGaussianInt] rw [← map_sum] congr with_unfolding_all decide set_option backward.isDefEq.respectTransparency false in -lemma dualLeftLeftUnit_eq_ofRat : δL' = ofRat fun f => +lemma dualLeftLeftUnit_eq_ofGaussianInt : δL' = ofGaussianInt fun f => if f 0 = f 1 then 1 else 0 := by rw [dualLeftLeftUnit_eq_tensor_basis] conv_lhs => enter [2, x] - rw [basis_eq_ofRat] + rw [basis_eq_ofGaussianInt] rw [← map_sum] congr with_unfolding_all decide set_option backward.isDefEq.respectTransparency false in -lemma leftDualLeftUnit_eq_ofRat : δL = ofRat fun f => +lemma leftDualLeftUnit_eq_ofGaussianInt : δL = ofGaussianInt fun f => if f 0 = f 1 then 1 else 0 := by rw [leftDualLeftUnit_eq_tensor_basis] conv_lhs => enter [2, x] - rw [basis_eq_ofRat] + rw [basis_eq_ofGaussianInt] rw [← map_sum] congr with_unfolding_all decide set_option backward.isDefEq.respectTransparency false in -lemma dualRightRightUnit_eq_ofRat : δR' = ofRat fun f => +lemma dualRightRightUnit_eq_ofGaussianInt : δR' = ofGaussianInt fun f => if f 0 = f 1 then 1 else 0 := by rw [dualRightRightUnit_eq_tensor_basis] conv_lhs => enter [2, x] - rw [basis_eq_ofRat] + rw [basis_eq_ofGaussianInt] rw [← map_sum] congr with_unfolding_all decide set_option backward.isDefEq.respectTransparency false in -lemma rightDualRightUnit_eq_ofRat : δR = ofRat fun f => +lemma rightDualRightUnit_eq_ofGaussianInt : δR = ofGaussianInt fun f => if f 0 = f 1 then 1 else 0 := by rw [rightDualRightUnit_eq_tensor_basis] conv_lhs => enter [2, x] - rw [basis_eq_ofRat] + rw [basis_eq_ofGaussianInt] rw [← map_sum] congr with_unfolding_all decide diff --git a/Physlib/Relativity/Tensors/LeviCivita/Complex.lean b/Physlib/Relativity/Tensors/LeviCivita/Complex.lean index 4b25942f6..6948657f0 100644 --- a/Physlib/Relativity/Tensors/LeviCivita/Complex.lean +++ b/Physlib/Relativity/Tensors/LeviCivita/Complex.lean @@ -5,7 +5,7 @@ Authors: Robert Sneiderman -/ module -public import Physlib.Relativity.Tensors.ComplexTensor.OfRat +public import Physlib.Relativity.Tensors.ComplexTensor.OfGaussianInt public import Physlib.Relativity.Tensors.LeviCivita.Basic public import Physlib.Relativity.Tensors.RealTensor.ToComplex /-! @@ -13,7 +13,7 @@ public import Physlib.Relativity.Tensors.RealTensor.ToComplex # The Levi-Civita tensor as a complex Lorentz tensor This file complexifies the real Lorentz Levi-Civita tensor and records its components in the -rational complex tensor basis. +Gaussian integer tensor basis. -/ @@ -61,17 +61,17 @@ scoped[complexLorentzTensor] notation "ε4ℂ" => leviCivita /-- The complex Levi-Civita tensor has the Levi-Civita symbol as its real component and zero imaginary component in the standard basis. -/ -lemma leviCivita_eq_ofRat : ε4ℂ = ofRat (fun +lemma leviCivita_eq_ofGaussianInt : ε4ℂ = ofGaussianInt (fun b : ComponentIdx (S := complexLorentzTensor) ![Color.up, Color.up, Color.up, Color.up] => - ⟨generalizedKroneckerDelta - (fun i => Fin.cast (by fin_cases i <;> rfl) (b i)) (id : Fin 4 → Fin 4), 0⟩) := by + (generalizedKroneckerDelta + (fun i => Fin.cast (by fin_cases i <;> rfl) (b i)) (id : Fin 4 → Fin 4) : GaussianInt)) := by apply (Tensor.basis _).repr.injective ext b rw [leviCivita, permT_basis_repr_symm_apply] have hinv (i : Fin 4) : IsReindexing.inv id leviCivita_isReindexing i = i := by have h := IsReindexing.inv_apply_apply id leviCivita_isReindexing i simpa using h - rw [ofRat_basis_repr_apply] + rw [ofGaussianInt_basis_repr_apply] let j : ComponentIdx (S := complexLorentzTensor) (realLorentzTensor.colorToComplex ∘ ![realLorentzTensor.Color.up, realLorentzTensor.Color.up, @@ -84,7 +84,7 @@ lemma leviCivita_eq_ofRat : ε4ℂ = ofRat (fun (ComponentIdx.complexify.symm j) rw [Equiv.apply_symm_apply] at hrepr rw [hrepr, realLorentzTensor.leviCivita_basis_repr_apply] - simp [Physlib.RatComplexNum.toComplexNum] + simp only [map_intCast, Complex.ofReal_intCast, Int.cast_inj] apply congrArg (fun f : Fin 4 → Fin 4 => generalizedKroneckerDelta f id) funext i have hcomplexify : @@ -103,16 +103,17 @@ lemma leviCivita_eq_ofRat : ε4ℂ = ofRat (fun /-- The components of the complex Levi-Civita tensor as the product over pairs `i < j` of the sign of `b j - b i`, from `leviCivitaSymbol_eq_prod_prod_Ioi`. Unlike the determinant appearing -in `leviCivita_eq_ofRat`, these components are cheap to evaluate, e.g. by `decide`. -/ -lemma leviCivita_eq_ofRat_prod : ε4ℂ = ofRat (fun +in `leviCivita_eq_ofGaussianInt`, these components are cheap to evaluate, e.g. by `decide`. -/ +lemma leviCivita_eq_ofGaussianInt_prod : ε4ℂ = ofGaussianInt (fun b : ComponentIdx (S := complexLorentzTensor) ![Color.up, Color.up, Color.up, Color.up] => - ⟨((∏ i : Fin 4, ∏ j ∈ Finset.Ioi i, + (((∏ i : Fin 4, ∏ j ∈ Finset.Ioi i, (if (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4) < (Fin.cast (by fin_cases j <;> rfl) (b j) : Fin 4) then 1 else if (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4) = - (Fin.cast (by fin_cases j <;> rfl) (b j) : Fin 4) then 0 else -1) : ℤ) : ℚ), 0⟩) := by - rw [leviCivita_eq_ofRat] - refine congrArg ofRat (funext fun b => ?_) + (Fin.cast (by fin_cases j <;> rfl) (b j) : Fin 4) then 0 else -1) : ℤ) : + GaussianInt))) := by + rw [leviCivita_eq_ofGaussianInt] + refine congrArg ofGaussianInt (funext fun b => ?_) have h := leviCivitaSymbol_eq_prod_prod_Ioi (fun i : Fin 4 => (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4)) rw [← h] diff --git a/scripts/MetaPrograms/module_doc_no_lint.txt b/scripts/MetaPrograms/module_doc_no_lint.txt index a56c78b8b..4b562a489 100644 --- a/scripts/MetaPrograms/module_doc_no_lint.txt +++ b/scripts/MetaPrograms/module_doc_no_lint.txt @@ -44,7 +44,6 @@ Physlib/Mathematics/List.lean Physlib/Mathematics/List/InsertIdx.lean Physlib/Mathematics/List/InsertionSort.lean Physlib/Mathematics/PiTensorProduct.lean -Physlib/Mathematics/RatComplexNum.lean Physlib/Mathematics/SO3/Basic.lean Physlib/Mathematics/SchurTriangulation.lean Physlib/Mathematics/SpecialFunctions/PhysHermite.lean @@ -239,7 +238,7 @@ Physlib/Relativity/Tensors/ComplexTensor/Matrix/Pre.lean Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean Physlib/Relativity/Tensors/ComplexTensor/Metrics/Lemmas.lean Physlib/Relativity/Tensors/ComplexTensor/Metrics/Pre.lean -Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean +Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean Physlib/Relativity/Tensors/ComplexTensor/Units/Pre.lean Physlib/Relativity/Tensors/ComplexTensor/Units/Symm.lean From 561fedaabe7e3a0b1aa963433154ed9cdc43c0f3 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Wed, 23 Sep 2026 12:51:43 +0100 Subject: [PATCH 2/2] refactor(ComplexTensor): define ofGaussianInt via Tensor.ofComponents `ofGaussianInt f` is now `ofComponents c (fun b => GaussianInt.toComplex (f b))` instead of going through `(Tensor.basis c).repr.symm` and `Finsupp.linearEquivFunOnFinite`; `ofGaussianInt_basis_repr_apply` follows from `componentMap_ofComponents`. Performance neutral (Relations.lean and ToTensor.lean within 0.2%). Co-authored-by: Claude Opus 5.5 --- .../Tensors/ComplexTensor/OfGaussianInt.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean b/Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean index cd53dcdbc..41b0d5024 100644 --- a/Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean +++ b/Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean @@ -35,17 +35,16 @@ open Tensor noncomputable def ofGaussianInt {n : ℕ} {c : Fin n → complexLorentzTensor.Color} : ((ComponentIdx (S := complexLorentzTensor) c) → GaussianInt) →ₛₗ[GaussianInt.toComplex] ℂT(c) where - toFun f := (Tensor.basis c).repr.symm <| - (Finsupp.linearEquivFunOnFinite ℂ ℂ - ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j)))).symm <| - (fun j => GaussianInt.toComplex (f j)) - map_add' f f1 := by - apply (Tensor.basis _).repr.injective - ext b + toFun f := ofComponents c (fun b => GaussianInt.toComplex (f b)) + map_add' f g := by + rw [← map_add] + congr 1 + funext b simp map_smul' r f := by - apply (Tensor.basis _).repr.injective - ext b + rw [← LinearMap.map_smul] + congr 1 + funext b simp @[simp] @@ -53,6 +52,7 @@ lemma ofGaussianInt_basis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTens (f : (ComponentIdx c) → GaussianInt) (b :(ComponentIdx c)) : (Tensor.basis c).repr (ofGaussianInt f) b = GaussianInt.toComplex (f b) := by + rw [← componentMap_eq_repr] simp [ofGaussianInt] lemma basis_eq_ofGaussianInt {n : ℕ} {c : Fin n → complexLorentzTensor.Color}