hom₂ — Mathlib

English

The operation Hom₂ on ModuleCat recovers exactly the original bilinear map when mapped back via ofHom₂.

Русский

Операция Hom₂ восстанавливает исходную билинейную карту при обратном отображении через ofHom₂.

LaTeX

$$$\mathrm{hom}_2(\mathrm{ofHom_2}(f)) = f$.$$

Lean4

/-- Turn a homomorphism into a bilinear map. -/
@[simps!]
def hom₂
    {M N P : ModuleCat.{u} R}
      -- We write `Hom` instead of `M ⟶ (of R (N ⟶ P))`, otherwise dot notation breaks
          -- since it is expecting the type of `f` to be `ModuleCat.Hom`, not `Quiver.Hom`.

    (f : Hom M (of R (N ⟶ P))) : M →ₗ[R] N →ₗ[R] P :=
  Hom.hom (by convert (f ≫ ofHom homLinearEquiv.toLinearMap))

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