lift_sub_lift — Mathlib

English

Let a, b, c, d be morphisms X → Y in a non-preadditive abelian category. Then the difference between the two product lifts is the product lift of the differences: prod.lift a b − prod.lift c d = prod.lift (a − c) (b − d).

Русский

Пусть X, Y — объекты в неабелевой абелевой категории; для морфизмов a, b, c, d: X ⟶ Y выполняется: prod.lift a b − prod.lift c d = prod.lift (a − c) (b − d).

LaTeX

$$$ \operatorname{prod.lift}(a,b) - \operatorname{prod.lift}(c,d) = \operatorname{prod.lift}(a-c,\, b-d) $$$

Lean4

theorem lift_sub_lift {X Y : C} (a b c d : X ⟶ Y) : prod.lift a b - prod.lift c d = prod.lift (a - c) (b - d) :=
  by
  simp only [sub_def]
  ext
  · rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_fst, prod.lift_fst, prod.lift_fst]
  · rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_snd, prod.lift_snd, prod.lift_snd]

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