map_comp_inlAlgHom — Mathlib

English

Composition of fstHom with map equals composition of map with fstHom, reflecting naturality of projections with respect to map.

Русский

Композиция fstHom с map равна композиции map с fstHom, отражая естественность проекций по отношению к map.

LaTeX

$$$\\text{fstHom}_{R'} \\circ (\\mathrm{map}\\ f) = (\\mathrm{fstHom}_{R'})$$$

Lean4

@[simp]
theorem map_comp_inlAlgHom (f : M →ₗ[R'] N) : (map f).comp (inlAlgHom R' R' M) = inlAlgHom R' R' N :=
  AlgHom.ext <| map_inl _

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