Documentation

Mathlib.RingTheory.PolynomialLaw.Basic

Polynomial laws on modules #

Let M and N be a modules over a commutative ring R. A polynomial law f : PolynomialLaw R M N, with notation f : M →ₚₗₗ[R] N, is a “law” that assigns a natural map PolynomialLaw.toFun' f S : S ⊗[R] M → S ⊗[R] N for every R-algebra S.

For type theoretic reasons, if R : Type u, then the definition of the polynomial map f is restricted to R-algebras S such that S : Type u. Using the fact that a module is the direct limit of its finitely generated submodules, that a finitely generated subalgebra is a quotient of a polynomial ring in the universe u, plus the commutation of tensor products with direct limits, we will extend the functor to all R-algebras (TODO).

Main definitions/lemmas #

Instance : Module R (M →ₚₗ[R] N) shows that polynomial laws form a R-module.
PolynomialLaw.ground f is the map M → N corresponding to PolynomialLaw.toFun' f R under the isomorphisms R ⊗[R] M ≃ₗ[R] M, and similarly for N.

In further works, we construct the coefficients of a polynomial law and show the relation with polynomials (when the module M is free and finite).

Implementation notes #

In the literature, the theory is written for commutative rings, but this implementation only assumes R is a commutative semiring.

References #

Roby, Norbert. 1963. « Lois polynomes et lois formelles en théorie des modules ». Annales scientifiques de l’École Normale Supérieure 80 (3): 213‑348

structure PolynomialLaw (R : Type u) [CommSemiring R] (M : Type u_1) [AddCommMonoid M] [Module R M] (N : Type u_2) [AddCommMonoid N] [Module R N] :

Type (max (max (u + 1) u_1) u_2)

A polynomial law M →ₚₗ[R] N between R-modules is a functorial family of maps S ⊗[R] M → S ⊗[R] N, for all R-algebras S.

For universe reasons, S has to be restricted to the same universe as R.

toFun' (S : Type u) [CommSemiring S] [Algebra R S] : TensorProduct R S M → TensorProduct R S N
The functions S ⊗[R] M → S ⊗[R] N underlying a polynomial law
isCompat' {S : Type u} [CommSemiring S] [Algebra R S] {S' : Type u} [CommSemiring S'] [Algebra R S'] (φ : S →ₐ[R] S') : ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ self.toFun' S = self.toFun' S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)
The compatibility relations between the functions underlying a polynomial law

theorem PolynomialLaw.ext_iff {R : Type u} {inst✝ : CommSemiring R} {M : Type u_1} {inst✝¹ : AddCommMonoid M} {inst✝² : Module R M} {N : Type u_2} {inst✝³ : AddCommMonoid N} {inst✝⁴ : Module R N} {x y : M →ₚₗ[R] N} :

x = y ↔ x.toFun' = y.toFun'

theorem PolynomialLaw.ext {R : Type u} {inst✝ : CommSemiring R} {M : Type u_1} {inst✝¹ : AddCommMonoid M} {inst✝² : Module R M} {N : Type u_2} {inst✝³ : AddCommMonoid N} {inst✝⁴ : Module R N} {x y : M →ₚₗ[R] N} (toFun' : x.toFun' = y.toFun') :

x = y

def «term_→ₚₗ[_]_» :

Lean.TrailingParserDescr

M →ₚₗ[R] N is the type of R-polynomial laws from M to N.

Equations

One or more equations did not get rendered due to their size.

theorem PolynomialLaw.isCompat_apply' {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] {f : M →ₚₗ[R] N} {S : Type u} [CommSemiring S] [Algebra R S] {S' : Type u} [CommSemiring S'] [Algebra R S'] (φ : S →ₐ[R] S') (x : TensorProduct R S M) :

(LinearMap.rTensor N φ.toLinearMap) (f.toFun' S x) = f.toFun' S' ((LinearMap.rTensor M φ.toLinearMap) x)

instance PolynomialLaw.instZero {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

Zero (M →ₚₗ[R] N)

Equations

PolynomialLaw.instZero = { zero := { toFun' := fun (x : Type ?u.42) [CommSemiring x] [Algebra R x] => 0, isCompat' := ⋯ } }

@[simp]

theorem PolynomialLaw.zero_def {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (S : Type u) [CommSemiring S] [Algebra R S] :

toFun' 0 S = 0

instance PolynomialLaw.instInhabited {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

Inhabited (M →ₚₗ[R] N)

Equations

PolynomialLaw.instInhabited = { default := Zero.zero }

def PolynomialLaw.id {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] :

M →ₚₗ[R] M

The identity as a polynomial law

Equations

PolynomialLaw.id = { toFun' := fun (S : Type ?u.26) (x : CommSemiring S) (x_1 : Algebra R S) => id, isCompat' := ⋯ }

theorem PolynomialLaw.id_apply' {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {S : Type u} [CommSemiring S] [Algebra R S] :

id.toFun' S = _root_.id

noncomputable def PolynomialLaw.add {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f g : M →ₚₗ[R] N) :

M →ₚₗ[R] N

The sum of two polynomial laws

Equations

f.add g = { toFun' := fun (S : Type ?u.50) (x : CommSemiring S) (x_1 : Algebra R S) => f.toFun' S + g.toFun' S, isCompat' := ⋯ }

instance PolynomialLaw.instAdd {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

Add (M →ₚₗ[R] N)

Equations

PolynomialLaw.instAdd = { add := PolynomialLaw.add }

@[simp]

theorem PolynomialLaw.add_def {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f g : M →ₚₗ[R] N) (S : Type u) [CommSemiring S] [Algebra R S] :

(f + g).toFun' S = f.toFun' S + g.toFun' S

theorem PolynomialLaw.add_def_apply {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f g : M →ₚₗ[R] N) (S : Type u) [CommSemiring S] [Algebra R S] (m : TensorProduct R S M) :

(f + g).toFun' S m = f.toFun' S m + g.toFun' S m

def PolynomialLaw.smul {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (r : R) (f : M →ₚₗ[R] N) :

M →ₚₗ[R] N

External multiplication of a f : M →ₚₗ[R] N by r : R

Equations

PolynomialLaw.smul r f = { toFun' := fun (S : Type ?u.48) (x : CommSemiring S) (x_1 : Algebra R S) => r • f.toFun' S, isCompat' := ⋯ }

instance PolynomialLaw.instSMul {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

SMul R (M →ₚₗ[R] N)

Equations

PolynomialLaw.instSMul = { smul := PolynomialLaw.smul }

@[simp]

theorem PolynomialLaw.smul_def {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (r : R) (f : M →ₚₗ[R] N) (S : Type u) [CommSemiring S] [Algebra R S] :

(r • f).toFun' S = r • f.toFun' S

theorem PolynomialLaw.smul_def_apply {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (r : R) (f : M →ₚₗ[R] N) (S : Type u) [CommSemiring S] [Algebra R S] (m : TensorProduct R S M) :

(r • f).toFun' S m = r • f.toFun' S m

theorem PolynomialLaw.add_smul {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (a b : R) (f : M →ₚₗ[R] N) :

(a + b) • f = a • f + b • f

theorem PolynomialLaw.zero_smul {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f : M →ₚₗ[R] N) :

0 • f = 0

theorem PolynomialLaw.one_smul {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f : M →ₚₗ[R] N) :

1 • f = f

instance PolynomialLaw.instMulAction {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

MulAction R (M →ₚₗ[R] N)

Equations

PolynomialLaw.instMulAction = { toSMul := PolynomialLaw.instSMul, one_smul := ⋯, mul_smul := ⋯ }

instance PolynomialLaw.instAddCommMonoid {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

AddCommMonoid (M →ₚₗ[R] N)

Equations

One or more equations did not get rendered due to their size.

instance PolynomialLaw.instModule {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

Module R (M →ₚₗ[R] N)

Equations

PolynomialLaw.instModule = { toMulAction := PolynomialLaw.instMulAction, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def PolynomialLaw.neg {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] {N : Type u_2} [AddCommGroup N] [Module R N] (f : M →ₚₗ[R] N) :

M →ₚₗ[R] N

The opposite of a polynomial law

Equations

f.neg = { toFun' := fun (S : Type ?u.44) (x : CommSemiring S) (x_1 : Algebra R S) => -1 • f.toFun' S, isCompat' := ⋯ }

instance PolynomialLaw.instNeg {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] {N : Type u_2} [AddCommGroup N] [Module R N] :

Neg (M →ₚₗ[R] N)

Equations

PolynomialLaw.instNeg = { neg := PolynomialLaw.neg }

@[simp]

theorem PolynomialLaw.neg_def {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] {N : Type u_2} [AddCommGroup N] [Module R N] (f : M →ₚₗ[R] N) (S : Type u) [CommSemiring S] [Algebra R S] :

(-f).toFun' S = -1 • f.toFun' S

instance PolynomialLaw.instAddCommGroup {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] {N : Type u_2} [AddCommGroup N] [Module R N] :

AddCommGroup (M →ₚₗ[R] N)

Equations

One or more equations did not get rendered due to their size.

def PolynomialLaw.ground {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f : M →ₚₗ[R] N) :

M → N

The map M → N associated with a f : M →ₚₗ[R] N (essentially, f.toFun' R)

Equations

f.ground = ⇑(TensorProduct.lid R N) ∘ f.toFun' R ∘ ⇑(TensorProduct.lid R M).symm

theorem PolynomialLaw.ground_apply {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f : M →ₚₗ[R] N) (m : M) :

f.ground m = (TensorProduct.lid R N) (f.toFun' R (1 ⊗ₜ[R] m))

instance PolynomialLaw.instCoeFunForall {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

CoeFun (M →ₚₗ[R] N) fun (x : M →ₚₗ[R] N) => M → N

Equations

PolynomialLaw.instCoeFunForall = { coe := PolynomialLaw.ground }

theorem PolynomialLaw.one_tmul_ground_apply' {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f : M →ₚₗ[R] N) {S : Type u} [CommSemiring S] [Algebra R S] (x : M) :

1 ⊗ₜ[R] f.ground x = f.toFun' S (1 ⊗ₜ[R] x)

def PolynomialLaw.lground {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] :

(M →ₚₗ[R] N) →ₗ[R] M → N

The map ground assigning a function M → N to a polynomial map f : M →ₚₗ[R] N as a linear map.

Equations

PolynomialLaw.lground = { toFun := PolynomialLaw.ground, map_add' := ⋯, map_smul' := ⋯ }

theorem PolynomialLaw.ground_id {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] :

id.ground = _root_.id

theorem PolynomialLaw.ground_id_apply {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] (m : M) :

id.ground m = m

def PolynomialLaw.comp {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] {P : Type u_3} [AddCommMonoid P] [Module R P] (g : N →ₚₗ[R] P) (f : M →ₚₗ[R] N) :

M →ₚₗ[R] P

Composition of polynomial maps.

Equations

g.comp f = { toFun' := fun (S : Type ?u.60) (x : CommSemiring S) (x_1 : Algebra R S) => g.toFun' S ∘ f.toFun' S, isCompat' := ⋯ }

theorem PolynomialLaw.comp_toFun' {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] {P : Type u_3} [AddCommMonoid P] [Module R P] (f : M →ₚₗ[R] N) (g : N →ₚₗ[R] P) (S : Type u) [CommSemiring S] [Algebra R S] :

(g.comp f).toFun' S = g.toFun' S ∘ f.toFun' S

theorem PolynomialLaw.comp_assoc {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] {P : Type u_3} [AddCommMonoid P] [Module R P] {Q : Type u_4} [AddCommMonoid Q] [Module R Q] (f : M →ₚₗ[R] N) (g : N →ₚₗ[R] P) (h : P →ₚₗ[R] Q) :

h.comp (g.comp f) = (h.comp g).comp f

theorem PolynomialLaw.comp_id {R : Type u} [CommSemiring R] {N : Type u_2} [AddCommMonoid N] [Module R N] {P : Type u_3} [AddCommMonoid P] [Module R P] (g : N →ₚₗ[R] P) :

theorem PolynomialLaw.id_comp {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {N : Type u_2} [AddCommMonoid N] [Module R N] (f : M →ₚₗ[R] N) :