metric_to_matrix

formal source

  46      · have h_rev : low 1 ≠ low 0 := fun heq => h heq.symm
  47        rw [if_neg h, if_neg h, if_neg h_rev, if_neg h_rev] }
  48
  49noncomputable def metric_to_matrix (g : MetricTensor) (x : Fin 4 → ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
  50  fun i j => g.g x (fun _ => 0) (fun k => if (k : ℕ) = 0 then i else j)
  51
  52/-- The metric matrix is symmetric because the metric tensor is symmetric. -/
  53lemma metric_to_matrix_symmetric (g : MetricTensor) (x : Fin 4 → ℝ) :
  54    (metric_to_matrix g x).transpose = metric_to_matrix g x := by
  55  ext i j
  56  unfold metric_to_matrix Matrix.transpose
  57  dsimp
  58  -- Apply the metric tensor symmetry: g x up low = g x up (swap low)
  59  have h := g.symmetric x (fun _ => 0) (fun k => if (k : ℕ) = 0 then j else i)
  60  -- The RHS evaluates to (fun k => if k.val = 0 then i else j) since 1 ≠ 0 and 0 = 0
  61  simp only [Fin.val_one, Fin.val_zero, one_ne_zero, ite_false, ite_true] at h
  62  exact h
  63
  64noncomputable def metric_det (g : MetricTensor) (x : Fin 4 → ℝ) : ℝ :=
  65  (metric_to_matrix g x).det
  66
  67noncomputable def inverse_metric (g : MetricTensor) : ContravariantBilinear :=
  68  fun x up _ =>
  69    (metric_to_matrix g x)⁻¹ (up 0) (up 1)
  70
  71/-- Inverse Minkowski metric components. -/
  72lemma inverse_minkowski_apply (x : Fin 4 → ℝ) (μ ν : Fin 4) :
  73    inverse_metric minkowski_tensor x (fun i => if (i : ℕ) = 0 then μ else ν) (fun _ => 0) =
  74    if μ = ν then (if (μ : ℕ) = 0 then -1 else 1) else 0 := by
  75  unfold inverse_metric
  76  dsimp
  77  have h_mat : metric_to_matrix minkowski_tensor x = Matrix.diagonal (fun i : Fin 4 => if (i : ℕ) = 0 then (-1 : ℝ) else 1) := by
  78    ext i j
  79    unfold metric_to_matrix minkowski_tensor eta