Homogeneous polynomial laws

A polynomial law f : M →ₚₗ[R] N is homogeneous of degree n if f (s • x) = s ^ n • f x for every commutative R-algebra S, every s : S and every x : S ⊗[R] M. The condition is imposed after every scalar extension, not only on M itself: over a finite field 𝔽_q the identity law satisfies s • m = s ^ q • m for all s ∈ 𝔽_q and m ∈ M, yet it is not homogeneous of degree q, as T • x ≠ T ^ q • x over 𝔽_q[T] for nonzero x.

Homogeneous laws of degree d are the objects represented by the degree-d divided powers Γ^d_R(M) (Roby), and the degree-one laws are exactly the base changes of linear maps.

Main declarations

• PolynomialLaw.IsHomogeneousOfDegree n f: the law f is homogeneous of degree n.
• PolynomialLaw.IsHomogeneousOfDegree.toFun_smul: homogeneity holds after scalar extension to algebras in every universe.
• PolynomialLaw.homogeneousSubmodule R M N n: the submodule of laws homogeneous of degree n; in particular the zero law is homogeneous of every degree.
• PolynomialLaw.IsHomogeneousOfDegree.comp: composing laws of degrees p and q gives a law of degree p * q.
• PolynomialLaw.IsHomogeneousOfDegree.toFun'_add, PolynomialLaw.IsHomogeneousOfDegree.toFun_add: a law homogeneous of degree one is additive after every scalar extension.
• PolynomialLaw.IsHomogeneousOfDegree.toLinearMap: the ground map of a law homogeneous of degree one, as a linear map, whose polynomial law is the original law.
• LinearMap.toLinearMap_isHomogeneousOfDegree_toPolynomialLaw: conversely, the linear map recovered from u.toPolynomialLaw is u.
• PolynomialLaw.isHomogeneousOfDegree_one_iff: a law is homogeneous of degree one if and only if it is the polynomial law u.toPolynomialLaw of a linear map u.
• PolynomialLaw.range_toPolynomialLawₗ, PolynomialLaw.homogeneousSubmoduleOneEquiv: the laws homogeneous of degree one are the image of LinearMap.toPolynomialLawₗ, which identifies M →ₗ[R] N with homogeneousSubmodule R M N 1.

References

• N. Roby, Lois polynômes et lois formelles en théorie des modules, Ann. Sci. École Norm. Sup. (3) 80 (1963), 213-348
• G. Chenevier, The p-adic analytic space of pseudocharacters of a profinite group and pseudorepresentations over arbitrary rings, §1.1

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

A polynomial law f : M →ₚₗ[R] N is homogeneous of degree n if f (s • x) = s ^ n • f x for every commutative R-algebra S, every s : S and every x : S ⊗[R] M. See IsHomogeneousOfDegree.toFun_smul for algebras in other universes.

theorem PolynomialLaw.isHomogeneousOfDegree_iff {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} {f : M →ₚₗ[R] N} : IsHomogeneousOfDegree n f ↔ ∀ (S : Type u) [inst : CommSemiring S] [inst_1 : Algebra R S] (s : S) (x : TensorProduct R S M), f.toFun' S (s • x) = s ^ n • f.toFun' S x

theorem PolynomialLaw.IsHomogeneousOfDegree.toFun'_smul {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree n f) {S : Type u} [CommSemiring S] [Algebra R S] (s : S) (x : TensorProduct R S M) : f.toFun' S (s • x) = s ^ n • f.toFun' S x

theorem PolynomialLaw.IsHomogeneousOfDegree.toFun_smul {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree n f) {S : Type u_4} [CommSemiring S] [Algebra R S] (s : S) (x : TensorProduct R S M) : toFun S f (s • x) = s ^ n • toFun S f x

Homogeneity of a polynomial law holds after scalar extension to a commutative R-algebra in an arbitrary universe.

theorem PolynomialLaw.IsHomogeneousOfDegree.ground_smul {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree n f) (r : R) (m : M) : f.ground (r • m) = r ^ n • f.ground m

The ground map of a law homogeneous of degree n is homogeneous of degree n.

theorem PolynomialLaw.IsHomogeneousOfDegree.add {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} {f g : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree n f) (hg : IsHomogeneousOfDegree n g) : IsHomogeneousOfDegree n (f + g)

theorem PolynomialLaw.IsHomogeneousOfDegree.smul {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree n f) (r : R) : IsHomogeneousOfDegree n (r • f)

theorem PolynomialLaw.IsHomogeneousOfDegree.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] {f : M →ₚₗ[R] N} {g : N →ₚₗ[R] P} {p q : ℕ} (hg : IsHomogeneousOfDegree q g) (hf : IsHomogeneousOfDegree p f) : IsHomogeneousOfDegree (p * q) (g.comp f)

Composing a law homogeneous of degree q with one homogeneous of degree p gives a law homogeneous of degree p * q.

theorem PolynomialLaw.isHomogeneousOfDegree_zero {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (n : ℕ) : IsHomogeneousOfDegree n 0

The zero law is homogeneous of every degree.

theorem PolynomialLaw.isHomogeneousOfDegree_id {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] : IsHomogeneousOfDegree 1 id

def PolynomialLaw.homogeneousSubmodule (R : Type u) [CommSemiring R] (M : Type u_1) (N : Type u_2) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (n : ℕ) : Submodule R (M →ₚₗ[R] N)

The submodule of polynomial laws M →ₚₗ[R] N which are homogeneous of degree n.

@[simp]

theorem PolynomialLaw.mem_homogeneousSubmodule {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} {f : M →ₚₗ[R] N} : f ∈ homogeneousSubmodule R M N n ↔ IsHomogeneousOfDegree n f

theorem LinearMap.isHomogeneousOfDegree_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) : PolynomialLaw.IsHomogeneousOfDegree 1 u.toPolynomialLaw

The polynomial law of a linear map is homogeneous of degree one.

theorem PolynomialLaw.IsHomogeneousOfDegree.toFun'_add {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree 1 f) (S : Type u) [CommSemiring S] [Algebra R S] (x y : TensorProduct R S M) : f.toFun' S (x + y) = f.toFun' S x + f.toFun' S y

A polynomial law homogeneous of degree one is additive after every scalar extension.

theorem PolynomialLaw.IsHomogeneousOfDegree.toFun'_tmul {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree 1 f) {S : Type u} [CommSemiring S] [Algebra R S] (s : S) (m : M) : f.toFun' S (s ⊗ₜ[R] m) = s ⊗ₜ[R] f.ground m

A polynomial law homogeneous of degree one sends s ⊗ₜ m to s ⊗ₜ f.ground m.

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

The ground map of a polynomial law homogeneous of degree one, as a linear map.

@[simp]

theorem PolynomialLaw.IsHomogeneousOfDegree.coe_toLinearMap {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree 1 f) : ⇑hf.toLinearMap = f.ground

@[simp]

theorem PolynomialLaw.IsHomogeneousOfDegree.toPolynomialLaw_toLinearMap {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree 1 f) : hf.toLinearMap.toPolynomialLaw = f

A polynomial law homogeneous of degree one is the polynomial law of its ground map.

theorem PolynomialLaw.IsHomogeneousOfDegree.toFun_add {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₚₗ[R] N} (hf : IsHomogeneousOfDegree 1 f) (S : Type u_3) [CommSemiring S] [Algebra R S] (x y : TensorProduct R S M) : toFun S f (x + y) = toFun S f x + toFun S f y

A polynomial law homogeneous of degree one is additive after scalar extension to a commutative R-algebra in an arbitrary universe.

theorem PolynomialLaw.isHomogeneousOfDegree_one_iff {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₚₗ[R] N} : IsHomogeneousOfDegree 1 f ↔ ∃ (u : M →ₗ[R] N), u.toPolynomialLaw = f

A polynomial law is homogeneous of degree one if and only if it is the polynomial law of a linear map, namely of its ground map IsHomogeneousOfDegree.toLinearMap.

@[simp]

theorem LinearMap.toLinearMap_isHomogeneousOfDegree_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) : ⋯.toLinearMap = u

The linear map recovered from the polynomial law of a linear map u is u.

theorem PolynomialLaw.range_toPolynomialLawₗ (R : Type u) [CommSemiring R] (M : Type u_1) (N : Type u_2) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : (LinearMap.toPolynomialLawₗ R M N).range = homogeneousSubmodule R M N 1

The polynomial laws homogeneous of degree one are exactly those of linear maps.

def PolynomialLaw.homogeneousSubmoduleOneEquiv (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] ↥(homogeneousSubmodule R M N 1)

Linear maps M →ₗ[R] N are identified with polynomial laws homogeneous of degree one, by LinearMap.toPolynomialLaw with inverse IsHomogeneousOfDegree.toLinearMap.

@[simp]

theorem PolynomialLaw.coe_homogeneousSubmoduleOneEquiv_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) : ↑((homogeneousSubmoduleOneEquiv R M N) u) = u.toPolynomialLaw

@[simp]

theorem PolynomialLaw.homogeneousSubmoduleOneEquiv_symm_apply {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ↥(homogeneousSubmodule R M N 1)) : (homogeneousSubmoduleOneEquiv R M N).symm f = ⋯.toLinearMap