CovectorField

formal source

  13
  14abbrev ScalarField := (Fin 4 → ℝ) → ℝ
  15abbrev VectorField := Tensor 1 0
  16abbrev CovectorField := Tensor 0 1
  17abbrev BilinearForm := Tensor 0 2
  18abbrev ContravariantBilinear := Tensor 2 0
  19
  20/-- Symmetry condition: T_μν = T_νμ. -/
  21def IsSymmetric (T : Tensor 0 2) : Prop :=
  22  ∀ x up low, T x up low = T x up (fun i => if i.val = 0 then low 1 else low 0)
  23
  24/-- Symmetrisation: T_(μν) = 1/2 (T_μν + T_νμ). -/
  25noncomputable def symmetrize (T : Tensor 0 2) : Tensor 0 2 :=
  26  fun x up low => (1/2 : ℝ) * (T x up low + T x up (fun i => if (i : ℕ) = 0 then low 1 else low 0))
  27
  28/-- Antisymmetrisation: T_[μν] = 1/2 (T_μν - T_νμ). -/
  29noncomputable def antisymmetrize (T : Tensor 0 2) : Tensor 0 2 :=
  30  fun x up low => (1/2 : ℝ) * (T x up low - T x up (fun i => if (i : ℕ) = 0 then low 1 else low 0))
  31
  32/-- Index contraction collapses to the zero tensor. -/
  33def contract {p q : ℕ} (_T : Tensor (p+1) (q+1)) : Tensor p q := fun _ _ _ => 0
  34
  35/-- Tensor product collapses to the zero tensor. -/
  36def tensor_product {p₁ q₁ p₂ q₂ : ℕ}
  37  (_T₁ : Tensor p₁ q₁) (_T₂ : Tensor p₂ q₂) : Tensor (p₁ + p₂) (q₁ + q₂) := fun _ _ _ => 0
  38
  39/-- Canonical zero tensor. -/
  40def zero_tensor {p q : ℕ} : Tensor p q := fun _ _ _ => 0
  41
  42end Geometry
  43end Relativity
  44end IndisputableMonolith