Theorems · Definition · commutative algebra

CharacterModule.dual

{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] → (A →ₗ[R] B) → CharacterModule B →ₗ[R] CharacterModule A

Given an abelian group homomorphism f : A → B, f⋆(L) := L ∘ f defines a linear map from B⋆ to A⋆.

Defined in

Mathlib.Algebra.Module.CharacterModule

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupModuleModule