xFlatConnection_apply

formal source

  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
  62  let i0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hn⟩
  63  let i1 : Fin n := ⟨1, lt_of_lt_of_le (by decide : 1 < 2) hn⟩
  64  have hi01 : i0 ≠ i1 := by
  65    simp [i0, i1]
  66  intro hproj