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 extend the functor to all R-algebras.

The two fields involving the definition of PolynomialLaw, PolynomialLaw.toFun' and PolynomialLaw.isCompat' are primed. They are superseded by their universe-polymorphic counterparts, the definition PolynomialLaw.toFun and the lemma PolynomialLaw.isCompat which should be used once the theory is properly stated.

For constructions of general definitions of PolynomialLaw at a universe-polymorphic level, one needs to lift elements in a tensor product to smaller universes. For this, one can make use of PolynomialLaw.exists_lift or PolynomialLaw.exists_lift', or establish appropriate generalizations.

Main definitions/lemmas

• Instance : Module R (M →ₚₗ[R] N) shows that polynomial laws form an 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, mul_smul := ⋯, one_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.67) (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

def PolynomialLaw.lifts (R : Type u) [CommSemiring R] (M : Type u_1) [AddCommMonoid M] [Module R M] (S : Type v) : Type (max (max u_1 u) v)

The type of lifts of S ⊗[R] M to a polynomial ring.

Equations

• PolynomialLaw.lifts R M S = ((s : Finset S) × TensorProduct R (MvPolynomial (Fin s.card) R) M)

def PolynomialLaw.φ (R : Type u) [CommSemiring R] {S : Type v} [CommSemiring S] [Algebra R S] (s : Finset S) : MvPolynomial (Fin s.card) R →ₐ[R] S

The lift of f.toFun to the type lifts`

Equations

• PolynomialLaw.φ R s = MvPolynomial.aeval fun (n : Fin s.card) => ↑(s.equivFin.symm n)

theorem PolynomialLaw.range_φ (R : Type u) [CommSemiring R] {S : Type v} [CommSemiring S] [Algebra R S] (s : Finset S) : (φ R s).range = Algebra.adjoin R ↑s

def PolynomialLaw.π (R : Type u) [CommSemiring R] (M : Type u_1) [AddCommMonoid M] [Module R M] (S : Type v) [CommSemiring S] [Algebra R S] : lifts R M S → TensorProduct R S M

The projection from φ to S ⊗[R] M.

Equations

• PolynomialLaw.π R M S ⟨s, p⟩ = (LinearMap.rTensor M (PolynomialLaw.φ R s).toLinearMap) p

def PolynomialLaw.toFunLifted {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 v) [CommSemiring S] [Algebra R S] (f : M →ₚₗ[R] N) : lifts R M S → TensorProduct R S N

The auxiliary lift of PolynomialLaw.toFun' on PolynomialLaw.lifts

Equations

• PolynomialLaw.toFunLifted S f ⟨s, p⟩ = (LinearMap.rTensor N (PolynomialLaw.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p)

def PolynomialLaw.toFun {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 v) [CommSemiring S] [Algebra R S] (f : M →ₚₗ[R] N) : TensorProduct R S M → TensorProduct R S N

The extension of PolynomialLaw.toFun' to all universes.

Equations

• PolynomialLaw.toFun S f = Function.extend (PolynomialLaw.π R M S) (PolynomialLaw.toFunLifted S f) fun (x : TensorProduct R S M) => 0

theorem PolynomialLaw.exists_range_φ_eq_of_fg {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] [Algebra R S] {B : Subalgebra R S} (hB : B.FG) : ∃ (s : Finset S), (φ R s).range = B

theorem PolynomialLaw.toFun'_eq_of_diagram {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 v} [CommSemiring S] [Algebra R S] (f : M →ₚₗ[R] N) {A : Type u} [CommSemiring A] [Algebra R A] {φ : A →ₐ[R] S} (p : TensorProduct R A M) {T : Type w} [CommSemiring T] [Algebra R T] {B : Type u} [CommSemiring B] [Algebra R B] {ψ : B →ₐ[R] T} (q : TensorProduct R B M) (h : S →ₐ[R] T) (h' : ↥φ.range →ₐ[R] ↥ψ.range) (hh' : ψ.range.val.comp h' = h.comp φ.range.val) (hpq : (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q) : (LinearMap.rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)

Compare the values of `PolynomialLaw.toFun' in a square diagram

theorem PolynomialLaw.toFun'_eq_of_inclusion {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 v} [CommSemiring S] [Algebra R S] (f : M →ₚₗ[R] N) {A : Type u} [CommSemiring A] [Algebra R A] {φ : A →ₐ[R] S} (p : TensorProduct R A M) {B : Type u} [CommSemiring B] [Algebra R B] (q : TensorProduct R B M) {ψ : B →ₐ[R] S} (h : φ.range ≤ ψ.range) (hpq : (LinearMap.rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q) : (LinearMap.rTensor N φ.toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)

Compare the values of `PolynomialLaw.toFun' in a square diagram, when one of the maps is a subalgebra inclusion.

theorem PolynomialLaw.factorsThrough_toFunLifted_π {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 v} [CommSemiring S] [Algebra R S] (f : M →ₚₗ[R] N) : Function.FactorsThrough (toFunLifted S f) (π R M S)

theorem PolynomialLaw.toFun_eq_rTensor_φ_toFun' {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 v} [CommSemiring S] [Algebra R S] (f : M →ₚₗ[R] N) {t : TensorProduct R S M} {s : Finset S} {p : TensorProduct R (MvPolynomial (Fin s.card) R) M} (ha : π R M S ⟨s, p⟩ = t) : toFun S f t = (LinearMap.rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p)

theorem PolynomialLaw.exists_lift_of_mem_range_rTensor {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {S : Type v} [CommSemiring S] [Algebra R S] {T : Type u_3} [CommSemiring T] [Algebra R T] (A : Subalgebra R T) {φ : S →ₐ[R] T} (hφ : A ≤ φ.range) {t : TensorProduct R T M} (ht : t ∈ LinearMap.range (LinearMap.rTensor M A.val.toLinearMap)) : ∃ (s : TensorProduct R S M), (LinearMap.rTensor M φ.toLinearMap) s = t

theorem PolynomialLaw.π_surjective {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {S : Type v} [CommSemiring S] [Algebra R S] : Function.Surjective (π R M S)

Tensor products in S ⊗[R] M can be lifted to some MvPolynomial R n ⊗[R] M, for a finite n.

theorem PolynomialLaw.exists_lift {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {S : Type v} [CommSemiring S] [Algebra R S] (t : TensorProduct R S M) : ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : TensorProduct R (MvPolynomial (Fin n) R) M), (LinearMap.rTensor M ψ.toLinearMap) p = t

Lift an element of a tensor product

theorem PolynomialLaw.exists_lift' {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {S : Type v} [CommSemiring S] [Algebra R S] (t : TensorProduct R S M) (s : S) : ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : TensorProduct R (MvPolynomial (Fin n) R) M) (q : MvPolynomial (Fin n) R), (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

Lift an element of a tensor product and a scalar

@[simp]

theorem PolynomialLaw.toFun'_eq_toFun {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] : f.toFun' S = toFun S f

For semirings in the universe u, PolynomialLaw.toFun coincides with PolynomialLaw.toFun'.

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] {S : Type v} [CommSemiring S] [Algebra R S] (f : M →ₚₗ[R] N) {T : Type w} [CommSemiring T] [Algebra R T] (h : S →ₐ[R] T) (t : TensorProduct R S M) : (LinearMap.rTensor N h.toLinearMap) (toFun S f t) = toFun T f ((LinearMap.rTensor M h.toLinearMap) t)

Extends PolynomialLaw.isCompat_apply' to all universes.

theorem PolynomialLaw.isCompat {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 v} [CommSemiring S] [Algebra R S] (f : M →ₚₗ[R] N) {T : Type w} [CommSemiring T] [Algebra R T] (h : S →ₐ[R] T) : ⇑(LinearMap.rTensor N h.toLinearMap) ∘ toFun S f = toFun T f ∘ ⇑(LinearMap.rTensor M h.toLinearMap)

Extends PolynomialLaw.isCompat to all universes

@[simp]

theorem PolynomialLaw.toFun_zero {R : Type u} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {S : Type u_5} [CommSemiring S] [Algebra R S] : toFun S 0 = 0

Extension of PolynomialLaw.zero_def

@[simp]

theorem PolynomialLaw.toFun_add_apply {R : Type u} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (f g : M →ₚₗ[R] N) {S : Type u_5} [CommSemiring S] [Algebra R S] (t : TensorProduct R S M) : toFun S (f + g) t = toFun S f t + toFun S g t

Extension of PolynomialLaw.add_def_apply

@[simp]

theorem PolynomialLaw.toFun_add {R : Type u} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (f g : M →ₚₗ[R] N) {S : Type u_5} [CommSemiring S] [Algebra R S] : toFun S (f + g) = toFun S f + toFun S g

Extension of PolynomialLaw.add_def

@[simp]

theorem PolynomialLaw.toFun_neg {R : Type u} [CommRing R] {M : Type u_6} [AddCommGroup M] [Module R M] {N : Type u_7} [AddCommGroup N] [Module R N] (f : M →ₚₗ[R] N) (S : Type u_8) [CommSemiring S] [Algebra R S] : toFun S (-f) = -1 • toFun S f

@[simp]

theorem PolynomialLaw.toFun_smul {R : Type u} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (r : R) (f : M →ₚₗ[R] N) (S : Type u_5) [CommSemiring S] [Algebra R S] : toFun S (r • f) = r • toFun S f

Extension of PolynomialLaw.smul_def

theorem PolynomialLaw.one_tmul_ground {R : Type u} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (f : M →ₚₗ[R] N) (S : Type u_5) [CommSemiring S] [Algebra R S] (x : M) : 1 ⊗ₜ[R] f.ground x = toFun S f (1 ⊗ₜ[R] x)

@[simp]

theorem PolynomialLaw.toFun_comp {R : Type u} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_5} [AddCommMonoid P] [Module R P] (f : M →ₚₗ[R] N) (g : N →ₚₗ[R] P) (S : Type u_7) [CommSemiring S] [Algebra R S] : toFun S (g.comp f) = toFun S g ∘ toFun S f

Extension of MvPolynomial.comp_toFun'

theorem PolynomialLaw.toFun_comp_apply {R : Type u} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_5} [AddCommMonoid P] [Module R P] (f : M →ₚₗ[R] N) (g : N →ₚₗ[R] P) (S : Type u_7) [CommSemiring S] [Algebra R S] (m : TensorProduct R S M) : toFun S (g.comp f) m = toFun S g (toFun S f m)