decomp_to — Mathlib

English

Every map f: A → (mappingCone φ).X_i factors as a sum of two maps, one through F.X_j and one through G.X_i, with explicit formulas using inl and inr components.

Русский

Любое отображение f: A → (mappingCone φ).X_i разлагается в сумму двух отображений: через F.X_j и через G.X_i, с явными формулами через компоненты inl и inr.

LaTeX

$$$\forall i,j:\ hij: i+1=j:\ exists\ a:A\to F.X_j, b:A\to G.X_i:\ f=a\circ (inl φ)_{j,i,hij}+b\circ (inr φ)_{i,i}\,. $$$

Lean4

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

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