ihom_coev_app_hom — Mathlib

English

The coevaluation app_hom for IHom is implemented via TensorProduct.mk flipping.

Русский

Ковариация IHom через coev реализована через TensorProduct.mk.flip.

LaTeX

$$$$ (\\ihom.coev A).app B) = ModuleCat.ofHom (TensorProduct.mk k A.V.carrier ((CategoryTheory.Functor.id (Rep k G)).obj B).1.carrier).flip $$$$

Lean4

@[simp]
theorem ihom_coev_app_hom (A B : Rep k G) :
    Action.Hom.hom ((ihom.coev A).app B) = ModuleCat.ofHom (TensorProduct.mk k _ _).flip :=
  ModuleCat.hom_ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => rfl

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