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 writen for commutative rings, but this implementation only assume 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 map 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 {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.61) [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.39) (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.73) (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.71) (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 = MulAction.mk ⋯ ⋯

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

• PolynomialLaw.instAddCommMonoid = AddCommMonoid.mk ⋯

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 = Module.mk ⋯ ⋯

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.65) (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

• PolynomialLaw.instAddCommGroup = AddCommGroup.mk ⋯

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.89) (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) : g.comp id = g

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) : id.comp f = f