lift_desc — Mathlib

English

A compatibility result connecting lift and desc: when you compose a biproduct lift with a biproduct desc, you obtain a finite sum of the composites g_j ≫ h_j, where g_j comes from the lift side and h_j from the desc side.

Русский

Соотношение между операторами lift и desc: композиция biproduct.lift g ≫ biproduct.desc h равна сумме по j от g_j ≫ h_j.

LaTeX

$$$\operatorname{biproduct.lift} g \\; \gg \\; \operatorname{biproduct.desc} h = \sum_{j \in J} g\, j \, \gg \, h\, j$$$

Lean4

@[reassoc]
theorem lift_desc {T U : C} {g : ∀ j, T ⟶ f j} {h : ∀ j, f j ⟶ U} :
    biproduct.lift g ≫ biproduct.desc h = ∑ j : J, g j ≫ h j := by
  classical simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite, dite_comp]

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