map_comp_comul_apply — Mathlib

English

If f is a morphism in F and x ∈ A, then the map applying f to both factors in the comultiplication equals comul of f x.

Русский

Если f — морфизм в F, и x ∈ A, то отображение, применяющее f к обеим факторам в разложении comul(x), равно comul(f(x)).

LaTeX

$$$\\mathrm{TensorProduct.map}(f,f)(\\Delta x) = \\Delta(f x)$$$

Lean4

@[simp]
theorem map_comp_comul_apply (f : F) (x : A) : TensorProduct.map f f (σ₁₂ := .id _) (comul x) = comul (R := R) (f x) :=
  LinearMap.congr_fun (map_comp_comul f) _

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