lift_map — Mathlib

English

The biproduct lift distributes over componentwise maps: lifting a family of arrows and then mapping is the same as lifting the componentwise compositions.

Русский

Лифт би-произведения распределяется по отображениям: поднять семейство стрелок и затем сопоставить равно подъему по компонентам.

LaTeX

$$$\forall J\, f g : J \to C [HasBiproduct f] [HasBiproduct g] (k : \forall j, P \to f j) (p : \forall j, f j \to g j) :\n biproduct.lift k \; \gg \; biproduct.map p = biproduct.lift (\lambda j, k j \circ p j)$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_map {f g : J → C} [HasBiproduct f] [HasBiproduct g] {P : C} (k : ∀ j, P ⟶ f j) (p : ∀ j, f j ⟶ g j) :
    biproduct.lift k ≫ biproduct.map p = biproduct.lift fun j => k j ≫ p j := by ext; simp

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