ext_to_iff — Mathlib

English

Two morphisms f,g: A → (mappingCone φ).X_i are equal if and only if their fst-projections agree and their snd-components agree, under the degree-shift hij.

Русский

Два морфизма f,g: A → (mappingCone φ).X_i равны тогда и только тогда, когда их проекции на fst φ совпадают и их snd-части совпадают при соответствующем hij.

LaTeX

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

Lean4

theorem ext_to_iff (i j : ℤ) (hij : i + 1 = j) {A : C} (f g : A ⟶ (mappingCone φ).X i) :
    f = g ↔
      f ≫ (fst φ).1.v i j hij = g ≫ (fst φ).1.v i j hij ∧
        f ≫ (snd φ).v i i (add_zero i) = g ≫ (snd φ).v i i (add_zero i) :=
  by
  constructor
  · rintro rfl
    tauto
  · rintro ⟨h₁, h₂⟩
    exact ext_to φ i j hij h₁ h₂

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