Theorems · Definition · ring theory

TensorAlgebra.lift

(R : Type u_1) →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_3} → [inst_3 : Semiring A] → [inst_4 : Algebra R A] → (M →ₗ[R] A) ≃ (TensorAlgebra R M →ₐ[R] A)

Given a linear map f : M → A where A is an R-algebra, lift R f is the unique lift of f to a morphism of R-algebras TensorAlgebra R M → A.

Defined in

Mathlib.LinearAlgebra.TensorAlgebra.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleSemiringAlgebra