decomp_from — Mathlib

English

Equivalent restatement of ext_to_iff at another index choice; two maps are equal iff their fst- and snd-compositions match with adjusted indices.

Русский

Эквивалентное переформулирование ext_to_iff при другом выборе индексов; равенство двух отображений эквивалентно совпадению их fst- и snd-композиций с поправкой индексов.

LaTeX

$$$\forall i,j:\ hij: i+1=j:\ f=g\iff\ (f\circ fst φ)_{i,j,hij}=(g\circ fst φ)_{i,j,hij}\land (f\circ snd φ)_{i,i}=(g\circ snd φ)_{i,i}.$$$

Lean4

theorem decomp_from {j : ℤ} {A : C} (f : (mappingCone φ).X j ⟶ A) (i : ℤ) (hij : j + 1 = i) :
    ∃ (a : F.X i ⟶ A) (b : G.X j ⟶ A), f = (fst φ).1.v j i hij ≫ a + (snd φ).v j j (add_zero j) ≫ b :=
  ⟨(inl φ).v i j (by cutsat) ≫ f, (inr φ).f j ≫ f, by apply ext_from φ i j hij <;> simp⟩

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