Documentation

TauCeti.RingTheory.PolynomialLaw.Basic

The polynomial law of a linear map #

An R-linear map u : M →ₗ[R] N induces the polynomial law u.toPolynomialLaw : M →ₚₗ[R] N whose component at a commutative R-algebra S is the base change u.baseChange S : S ⊗[R] M → S ⊗[R] N. These are exactly the polynomial laws which are homogeneous of degree one (see TauCeti.RingTheory.PolynomialLaw.Homogeneous).

Main declarations #

References #

source
def LinearMap.toPolynomialLaw {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (u : M →ₗ[R] N) :
M →ₚₗ[R] N

The polynomial law M →ₚₗ[R] N induced by an R-linear map u: its component at a commutative R-algebra S is the base change u.baseChange S : S ⊗[R] M → S ⊗[R] N.

Instances For
    source
    theorem LinearMap.toPolynomialLaw_toFun' {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (u : M →ₗ[R] N) (S : Type u) [CommSemiring S] [Algebra R S] :
    u.toPolynomialLaw.toFun' S = ⇑(baseChange S u)
    source
    @[simp]
    theorem LinearMap.toPolynomialLaw_toFun {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (u : M →ₗ[R] N) (S : Type u_4) [CommSemiring S] [Algebra R S] :
    PolynomialLaw.toFun S u.toPolynomialLaw = ⇑(baseChange S u)

    The component of u.toPolynomialLaw at an R-algebra in an arbitrary universe is the base change of u.

    source
    @[simp]
    theorem LinearMap.ground_toPolynomialLaw {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (u : M →ₗ[R] N) :
    u.toPolynomialLaw.ground = ⇑u

    The ground map of the polynomial law of a linear map u is u.

    source
    theorem LinearMap.toPolynomialLaw_injective {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
    Function.Injective toPolynomialLaw

    A linear map is determined by its polynomial law.

    source
    @[simp]
    theorem LinearMap.toPolynomialLaw_inj {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {u v : M →ₗ[R] N} :
    u.toPolynomialLaw = v.toPolynomialLaw ↔ u = v
    source
    @[simp]
    theorem LinearMap.toPolynomialLaw_id {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] :
    id.toPolynomialLaw = PolynomialLaw.id

    The identity linear map induces the identity polynomial law.

    source
    @[simp]
    theorem LinearMap.toPolynomialLaw_comp {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (v : N →ₗ[R] P) (u : M →ₗ[R] N) :
    (v ∘ₗ u).toPolynomialLaw = v.toPolynomialLaw.comp u.toPolynomialLaw

    The polynomial law of v ∘ₗ u is the composite of the polynomial laws of v and u.

    source
    @[simp]
    theorem LinearMap.toPolynomialLaw_zero {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
    toPolynomialLaw 0 = 0
    source
    @[simp]
    theorem LinearMap.toPolynomialLaw_add {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (u v : M →ₗ[R] N) :
    (u + v).toPolynomialLaw = u.toPolynomialLaw + v.toPolynomialLaw
    source
    @[simp]
    theorem LinearMap.toPolynomialLaw_smul {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (r : R) (u : M →ₗ[R] N) :
    (r • u).toPolynomialLaw = r • u.toPolynomialLaw
    source
    def LinearMap.toPolynomialLawₗ (R : Type u) [CommSemiring R] (M : Type u_1) (N : Type u_2) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
    (M →ₗ[R] N) →ₗ[R] M →ₚₗ[R] N

    LinearMap.toPolynomialLaw, bundled as an R-linear map.

    Instances For
      source
      @[simp]
      theorem LinearMap.toPolynomialLawₗ_apply {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (u : M →ₗ[R] N) :
      (toPolynomialLawₗ R M N) u = u.toPolynomialLaw
      source
      theorem LinearMap.toPolynomialLawₗ_injective {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] :
      Function.Injective ⇑(toPolynomialLawₗ R M N)