FGModuleCatCoevaluation_apply_one

English

The evaluation of the canonical coevaluation at 1 equals the standard basis expansion in the tensor product: 1 maps to the sum of basis vectors tensored with their duals.

Русский

Оценка канонической кооценки в 1 даёт разложение по базису: 1 переходит в сумму базисных элементов в сочетании с их дуальными.

LaTeX

$$FGModuleCatCoevaluation_apply_one : (FGModuleCatCoevaluation K V).hom (1 : K) = ∑ i : Basis.ofVectorSpaceIndex K V, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i$$

Lean4

theorem FGModuleCatCoevaluation_apply_one :
    (FGModuleCatCoevaluation K V).hom (1 : K) =
      ∑ i : Basis.ofVectorSpaceIndex K V, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i :=
  coevaluation_apply_one K V

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