eval_comp_comp_evalEquiv_eq — Mathlib

English

The natural composition identity holds: Dual.eval ∘ f ∘ evalEquiv.symm = f.dualMap.dualMap for linear maps f: M → M′.

Русский

Естественная композиционная тождественность: Dual.eval ∘ f ∘ evalEquiv.symm = f.dualMap.dualMap для линейного отображения f: M → M′.

LaTeX

$$$$ \\operatorname{Dual.eval}_{R,M'} \\circ f \\circ (\\operatorname{evalEquiv}_{R,M})^{-1} = f.dualMap.dualMap. $$$$

Lean4

@[simp]
theorem eval_comp_comp_evalEquiv_eq {M' : Type*} [AddCommMonoid M'] [Module R M'] {f : M →ₗ[R] M'} :
    Dual.eval R M' ∘ₗ f ∘ₗ (evalEquiv R M).symm = f.dualMap.dualMap := by
  rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq, evalEquiv_toLinearMap, eval_naturality]

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