diag_map — Mathlib

English

For morphism f: X → Y, the diagonal maps interact with prod.map as diag X ≫ prod.map f f = f ≫ diag Y.

Русский

Для морфизма f: X → Y диагональ и отображение prod взаимодействуют так, что diag X ≫ prod.map f f = f ≫ diag Y.

LaTeX

$$$diag X \\circ prod.map f f = f \\circ diag Y$$$

Lean4

@[reassoc]
theorem diag_map {X Y : C} (f : X ⟶ Y) [HasBinaryProduct X X] [HasBinaryProduct Y Y] :
    diag X ≫ prod.map f f = f ≫ diag Y := by simp

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