diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean index e9636635c3..f3ac357874 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean @@ -28,9 +28,13 @@ noncomputable section namespace Lorentz -/-- Real contravariant Lorentz vector. -/ +/-- Real covariant Lorentz vector. -/ +@[implicit_reducible] def CoVector (d : ℕ := 3) := Fin 1 ⊕ Fin d → ℝ +/- As for `Vector`, `CoVector d` is applied directly as a function throughout the library; + marking it implicit-reducible lets such applications typecheck at implicit transparency. -/ + namespace CoVector instance {d} : AddCommMonoid (CoVector d) := @@ -89,6 +93,7 @@ instance (d : ℕ) : Inner ℝ (CoVector d) where lemma inner_eq_equivEuclid (d : ℕ) (v w : CoVector d) : ⟪v, w⟫_ℝ = ⟪equivEuclid d v, equivEuclid d w⟫_ℝ := rfl + /-- The Euclidean inner product structure on `CoVector`. -/ instance innerProductSpace (d : ℕ) : InnerProductSpace ℝ (CoVector d) where norm_sq_eq_re_inner v := by @@ -148,14 +153,14 @@ def basis {d : ℕ} : Basis (Fin 1 ⊕ Fin d) ℝ (CoVector d) := lemma basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : basis μ ν = if μ = ν then 1 else 0 := by simp [basis] - erw [Pi.basisFun_apply, Pi.single_apply] + rw [Pi.basisFun_apply, Pi.single_apply] congr 1 exact Lean.Grind.eq_congr' rfl rfl lemma basis_repr_apply {d : ℕ} (p : CoVector d) (μ : Fin 1 ⊕ Fin d) : basis.repr p μ = p μ := by simp [basis] - erw [Pi.basisFun_repr] + rw [Pi.basisFun_repr] lemma map_apply_eq_basis_mulVec {d : ℕ} (f : CoVector d →ₗ[ℝ] CoVector d) (p : CoVector d) : (f p) = (LinearMap.toMatrix basis basis) f *ᵥ p := by diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean index ecc73a9cd1..952e264e61 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean +++ b/Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean @@ -71,7 +71,6 @@ lemma rep_injective (d : ℕ) (Λ : LorentzGroup d) : Function.Injective (rep Λ rw [rep_apply_eq_mulVec, rep_apply_eq_mulVec] at h exact Matrix.mulVec_injective_of_isUnit (isUnit_of_invertible _) h -set_option backward.isDefEq.respectTransparency false in lemma rep_surjective (d : ℕ) (Λ : LorentzGroup d) : Function.Surjective (rep Λ) := by intro v use (LorentzGroup.transpose Λ) *ᵥ v diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean index 9d25fb9f05..6f3de12bc0 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean +++ b/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean @@ -154,7 +154,6 @@ lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : CoV · intro t1 t2 h1 h2 simp only [actionT_add, map_add, h1, h2, apply_add, mul_add, Finset.sum_add_distrib] -set_option backward.isDefEq.respectTransparency false in lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : CoVector d) : Λ • p = (LorentzGroup.transpose Λ⁻¹).1 *ᵥ p := by funext i @@ -166,18 +165,15 @@ lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : CoVector d) : lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : CoVector d) : Λ • (p + q) = Λ • p + Λ • q := by simp -set_option backward.isDefEq.respectTransparency false in @[simp] lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : CoVector d) : Λ • (p - q) = Λ • p - Λ • q := by rw [smul_eq_mulVec, smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_sub] -set_option backward.isDefEq.respectTransparency false in lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) : Λ • (0 : CoVector d) = 0 := by rw [smul_eq_mulVec, Matrix.mulVec_zero] -set_option backward.isDefEq.respectTransparency false in lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) : Λ • (-p) = - (Λ • p) := by rw [smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_neg] @@ -195,7 +191,6 @@ def actionCLM {d : ℕ} (Λ : LorentzGroup d) : lemma actionCLM_apply {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) : actionCLM Λ p = Λ • p := rfl -set_option backward.isDefEq.respectTransparency false in lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) : Λ • basis μ = ∑ ν, Λ⁻¹.1 μ ν • basis ν := by funext i diff --git a/Physlib/Relativity/Tensors/RealTensor/Representation/Contraction.lean b/Physlib/Relativity/Tensors/RealTensor/Representation/Contraction.lean index b018736d02..4993bb5bc8 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Representation/Contraction.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Representation/Contraction.lean @@ -40,7 +40,6 @@ TODO "In a similar way to `Vector.contract` and `CoVector.contract`, we want to define metrics and units as intertwining maps of representations. This should copy (and eventually replace) the definitions e.g. `./Units/Pre.lean`." -set_option backward.isDefEq.respectTransparency false in /-- The intertwining map defining the contraction of a contravariant Lorentz vector with a covariant Lorentz vector. -/ def Vector.contract : (Vector.rep.tprod CoVector.rep).IntertwiningMap @@ -61,7 +60,6 @@ def Vector.contract : (Vector.rep.tprod CoVector.rep).IntertwiningMap vecMul_transpose, mulVec_mulVec, LorentzGroup.coe_inv, inv_mul_of_invertible Λ.1] rfl -set_option backward.isDefEq.respectTransparency false in /-- The intertwining map defining the contraction of a covariant Lorentz vector with a contravariant Lorentz vector. -/ def CoVector.contract : (CoVector.rep.tprod Vector.rep).IntertwiningMap @@ -94,19 +92,15 @@ lemma Vector.contract_tmul (φ : Vector d) (ψ : CoVector d) : lemma CoVector.contract_tmul (φ : CoVector d) (ψ : Vector d) : CoVector.contract (φ ⊗ₜ ψ) = ∑ i, φ i * ψ i := rfl -set_option backward.isDefEq.respectTransparency false in lemma Vector.contract_basis_left (μ : Fin 1 ⊕ Fin d) (ψ : CoVector d) : Vector.contract (basis μ ⊗ₜ ψ) = ψ μ := by simp [Vector.contract_tmul, basis_apply] -set_option backward.isDefEq.respectTransparency false in lemma CoVector.contract_basis_left (μ : Fin 1 ⊕ Fin d) (φ : Vector d) : CoVector.contract (basis μ ⊗ₜ φ) = φ μ := by simp [CoVector.contract_tmul, basis_apply] -set_option backward.isDefEq.respectTransparency false in lemma Vector.contract_basis_right (φ : Vector d) (μ : Fin 1 ⊕ Fin d) : Vector.contract (φ ⊗ₜ basis μ) = φ μ := by simp [Vector.contract_tmul, basis_apply] -set_option backward.isDefEq.respectTransparency false in lemma CoVector.contract_basis_right (ψ : CoVector d) (μ : Fin 1 ⊕ Fin d) : CoVector.contract (ψ ⊗ₜ basis μ) = ψ μ := by simp [CoVector.contract_tmul, basis_apply] diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean index 368da39502..0e40391384 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean @@ -29,8 +29,14 @@ noncomputable section namespace Lorentz /-- Real contravariant Lorentz vector. -/ +@[implicit_reducible] def Vector (d : ℕ := 3) := Fin 1 ⊕ Fin d → ℝ +/- `Vector d` is applied directly as a function throughout the library. Marking it + implicit-reducible lets such applications typecheck at implicit transparency, so that + `rw` and `simp` can match patterns containing them (see the Lean 4.33 release notes on + `backward.isDefEq.respectTransparency.types`). -/ + namespace Vector instance {d} : AddCommMonoid (Vector d) := @@ -116,6 +122,11 @@ instance innerProductSpace (d : ℕ) : InnerProductSpace ℝ (Vector d) where simp only [inner_eq_equivEuclid, map_smul] exact InnerProductSpace.smul_left (equivEuclid d x) (equivEuclid d y) r +/-- The inner product on `Vector d` as a sum over components. -/ +lemma inner_eq_sum {d : ℕ} (v w : Vector d) : ⟪v, w⟫_ℝ = ∑ μ, v μ * w μ := by + rw [inner_eq_equivEuclid, PiLp.inner_apply] + simp [mul_comm] + /-- The instance of a `ChartedSpace` on `Vector d`. -/ instance : ChartedSpace (Vector d) (Vector d) := chartedSpaceSelf (Vector d) @@ -278,14 +289,14 @@ def basis {d : ℕ} : Basis (Fin 1 ⊕ Fin d) ℝ (Vector d) := lemma basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : basis μ ν = if μ = ν then 1 else 0 := by simp [basis] - erw [Pi.basisFun_apply, Pi.single_apply] + rw [Pi.basisFun_apply, Pi.single_apply] congr 1 exact Lean.Grind.eq_congr' rfl rfl lemma basis_repr_apply {d : ℕ} (p : Vector d) (μ : Fin 1 ⊕ Fin d) : basis.repr p μ = p μ := by simp [basis] - erw [Pi.basisFun_repr] + rw [Pi.basisFun_repr] lemma map_apply_eq_basis_mulVec {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) (p : Vector d) : (f p) = (LinearMap.toMatrix basis basis) f *ᵥ p := by @@ -431,19 +442,13 @@ def asSmoothManifold (d : ℕ) : ModelWithCorners ℝ (Vector d) (Vector d) := -/ open InnerProductSpace -set_option backward.isDefEq.respectTransparency false in lemma basis_inner {d : ℕ} (μ : Fin 1 ⊕ Fin d) (p : Lorentz.Vector d) : ⟪Lorentz.Vector.basis μ, p⟫_ℝ = p μ := by - simp [inner_eq_equivEuclid] - rw [PiLp.inner_apply] - simp [-Fintype.sum_sum_type] + simp [inner_eq_sum] -set_option backward.isDefEq.respectTransparency false in lemma inner_basis {d : ℕ} (p : Lorentz.Vector d) (μ : Fin 1 ⊕ Fin d) : ⟪p, Lorentz.Vector.basis μ⟫_ℝ = p μ := by - simp [inner_eq_equivEuclid] - rw [PiLp.inner_apply] - simp [-Fintype.sum_sum_type] + simp [inner_eq_sum] end Vector diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean index 1b6cbc5924..e0a852daf7 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean @@ -60,7 +60,6 @@ lemma rep_toMatrix (d : ℕ) (Λ : LorentzGroup d) : lemma rep_injective (d : ℕ) (Λ : LorentzGroup d) : Function.Injective (rep Λ) := fun _ _ h => Matrix.mulVec_injective_of_isUnit (isUnit_of_invertible Λ.1) h -set_option backward.isDefEq.respectTransparency false in lemma rep_surjective (d : ℕ) (Λ : LorentzGroup d) : Function.Surjective (rep Λ) := fun v => ⟨Λ⁻¹ *ᵥ v, by simp [rep_apply_eq_mulVec]⟩ diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean index 1b9d9018ca..8bc056801e 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean @@ -151,7 +151,6 @@ lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : Vec · intro t1 t2 h1 h2 simp only [actionT_add, map_add, apply_add, h1, h2, mul_add, Finset.sum_add_distrib] -set_option backward.isDefEq.respectTransparency false in lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : Vector d) : Λ • p = Λ.1 *ᵥ p := by funext i @@ -162,18 +161,15 @@ lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : Vector d) : lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) : Λ • (p + q) = Λ • p + Λ • q := by simp -set_option backward.isDefEq.respectTransparency false in @[simp] lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) : Λ • (p - q) = Λ • p - Λ • q := by rw [smul_eq_mulVec, smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_sub] -set_option backward.isDefEq.respectTransparency false in lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) : Λ • (0 : Vector d) = 0 := by rw [smul_eq_mulVec, Matrix.mulVec_zero] -set_option backward.isDefEq.respectTransparency false in lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : Vector d) : Λ • (-p) = - (Λ • p) := by rw [smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_neg] @@ -183,7 +179,6 @@ lemma neg_smul {d} (Λ : LorentzGroup d) (p : Vector d) : funext i simp [smul_eq_sum, neg_apply] -set_option backward.isDefEq.respectTransparency false in lemma _root_.LorentzGroup.eq_of_action_vector_eq {d : ℕ} {Λ Λ' : LorentzGroup d} (h : ∀ p : Vector d, Λ • p = Λ' • p) : Λ = Λ' := by @@ -221,7 +216,6 @@ lemma actionCLM_surjective {d : ℕ} (Λ : LorentzGroup d) : use (actionCLM Λ⁻¹) x1 simp [actionCLM_apply] -set_option backward.isDefEq.respectTransparency false in lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) : Λ • basis μ = ∑ ν, Λ.1 ν μ • basis ν := by funext i