ι_map — Mathlib

English

The j-th projection after mapping is compatible with the component map: π_j after map equals p_j after π_j.

Русский

Проекция j после отображения совместима с отображением по компонентам: π_j ∘ map = p_j ∘ π_j.

LaTeX

$$$\forall J\, {f g : J \to C} [HasBiproduct f] [HasBiproduct g] (p : \forall j, f j \to g j) (j : J) :\n biproduct.ι f j \; \gg \; biproduct.map p = p j \; \gg \; biproduct.ι g j$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_map {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) (j : J) :
    biproduct.ι f j ≫ biproduct.map p = p j ≫ biproduct.ι g j :=
  by
  rw [biproduct.map_eq_map']
  apply
    Limits.IsColimit.ι_map (biproduct.isColimit f) (biproduct.bicone g).toCocone (Discrete.natTrans fun j => p j.as)
      (Discrete.mk j)

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