ProjectivelyEquivalentToZeroAt

formal source

  28  if i = j ∧ j = k then -(x i)⁻¹ else 0
  29
  30/-- Projective equivalence to the zero connection. -/
  31def ProjectivelyEquivalentToZeroAt {n : ℕ}
  32    (Γ : Fin n → Fin n → Fin n → ℝ) : Prop :=
  33  ∃ ψ : Vec n, ∀ i j k : Fin n,
  34    Γ i j k = delta i j * ψ k + delta i k * ψ j
  35
  36@[simp] theorem xFlatConnection_apply {n : ℕ} (x : Vec n) (i j k : Fin n) :
  37    xFlatConnection x i j k = 0 := rfl
  38
  39theorem tPulledConnection_diag {n : ℕ} (x : Vec n) (i : Fin n) :
  40    tPulledConnection x i i i = -(x i)⁻¹ := by
  41  unfold tPulledConnection
  42  simp
  43
  44theorem tPulledConnection_offDiag {n : ℕ} (x : Vec n) {i j k : Fin n}
  45    (hijk : ¬ (i = j ∧ j = k)) :
  46    tPulledConnection x i j k = 0 := by
  47  unfold tPulledConnection
  48  simp [hijk]
  49
  50theorem projectivelyEquivalent_one_dim {x : Vec 1} :
  51    ProjectivelyEquivalentToZeroAt (tPulledConnection x) := by
  52  refine ⟨fun _ => -((x 0)⁻¹) / 2, ?_⟩
  53  intro i j k
  54  fin_cases i
  55  fin_cases j
  56  fin_cases k
  57  simp [delta, tPulledConnection]
  58
  59theorem not_projectivelyEquivalentToZeroAt_tPulledConnection {n : ℕ}
  60    (hn : 2 ≤ n) (x : Vec n) (hx : ∀ i : Fin n, x i ≠ 0) :
  61    ¬ ProjectivelyEquivalentToZeroAt (tPulledConnection x) := by