ι_totalShift₁Iso_inv_f — Mathlib

English

Theorem asserting reflexivity in the totalShift1Iso_hom_f identification when the shift is trivial.

Русский

Теорема о тождественности в случае нулевого сдвига для ι_totalShift1Iso_hom_f.

LaTeX

$$$ι\\_totalShift₁Iso\_hom\_f (a,b,n,h,a',ha',n',hn') = \\text{Id}$$$

Lean4

@[reassoc]
theorem ι_totalShift₁Iso_inv_f (a b n : ℤ) (h : a + b = n) (a' n' : ℤ) (ha' : a' + b = n') (hn' : n' = n + x) :
    K.ιTotal (up ℤ) a' b n' ha' ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv ≫ (K.totalShift₁Iso x).inv.f n =
      (K.shiftFunctor₁XXIso a x a' (by cutsat) b).inv ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h :=
  by
  subst hn'
  obtain rfl : a = a' - x := by cutsat
  dsimp [totalShift₁Iso, totalShift₁XIso, shiftFunctor₁XXIso, XXIsoOfEq]
  simp only [id_comp, ι_totalDesc]

Похожие утверждения