Theorems · Definition · commutative algebra

CharacterModule.curry

{R : Type uR} →
  [inst : CommRing R] →
    {A : Type uA} →
      [inst_1 : AddCommGroup A] →
        {B : Type uB} →
          [inst_2 : AddCommGroup B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] → CharacterModule (TensorProduct R A B) →ₗ[R] A →ₗ[R] CharacterModule B

Any character c in (A ⊗ B)⋆ induces a linear map A → B⋆ by a ↦ b ↦ c (a ⊗ b).

Defined in

Mathlib.Algebra.Module.CharacterModule

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupAddCommGroupModuleModule