map_toCoalgHom — Mathlib

English

The underlying map map f g is equal to the coalgebra map obtained by applying Coalgebra.TensorProduct.map to the linear maps underlying f and g.

Русский

Основное отображение map f g совпадает с коалгебральным отображением, полученным применением Coalgebra.TensorProduct.map к линейным отображениям, лежащим в основе f и g.

LaTeX

$$$\text{map } f\ g = \mathrm{Coalgebra.TensorProduct.map} (f : A \to_l[S] C) (g : B \to_l[R] D)$$$

Lean4

@[simp]
theorem map_toCoalgHom (f : A →ₐc[S] C) (g : B →ₐc[R] D) :
    map f g = Coalgebra.TensorProduct.map (f : A →ₗc[S] C) (g : B →ₗc[R] D) :=
  rfl

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