ext_from — Mathlib

English

Dually, two morphisms f,g: (mappingCone φ).X_j → A are equal if their inl and inr-induced compositions with the respective projections coincide.

Русский

С двояким аналогом: два морфизма f,g: (mappingCone φ).X_j → A равны, если их композиции через inl φ и through inr φ совпадают.

LaTeX

$$$\forall i,j:\ hij: j+1=i:\ f,g:(mappingCone φ)X_j\to A:\ (inl φ)_{i,j}\circ f = (inl φ)_{i,j}\circ g\land (inr φ)_{j}\circ f = (inr φ)_{j}\circ g\Rightarrow f=g.$$$

Lean4

theorem ext_from (i j : ℤ) (hij : j + 1 = i) {A : C} {f g : (mappingCone φ).X j ⟶ A}
    (h₁ : (inl φ).v i j (by cutsat) ≫ f = (inl φ).v i j (by cutsat) ≫ g) (h₂ : (inr φ).f j ≫ f = (inr φ).f j ≫ g) :
    f = g :=
  homotopyCofiber.ext_from_X φ i j hij h₁ h₂

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