Multiplicative polynomial laws

For R-algebras A and B, associative and unital but not necessarily commutative, a polynomial law f : A →ₚₗ[R] B is multiplicative if f 1 = 1 and f (x * y) = f x * f y for every commutative R-algebra S and all x y : S ⊗[R] A, where S ⊗[R] A and S ⊗[R] B carry the ring structures of Algebra.TensorProduct. As for homogeneity, the condition is imposed after every scalar extension: the determinant Mₙ(R) → R is the motivating example, and det (X * Y) = det X * det Y is an identity of matrices with entries in every commutative R-algebra, not only in R.

Multiplicative laws homogeneous of degree d are the objects classified by the Roby algebra Γ^d_R(A), with its internal multiplication. This file treats the degree-one case: a law which is homogeneous of degree one and multiplicative is exactly the polynomial law of an R-algebra map A →ₐ[R] B.

Main declarations

• PolynomialLaw.IsMultiplicative f: the law f is multiplicative.
• PolynomialLaw.IsMultiplicative.toFun_one, PolynomialLaw.IsMultiplicative.toFun_mul: multiplicativity holds after scalar extension to algebras in every universe.
• PolynomialLaw.IsMultiplicative.ground_one, PolynomialLaw.IsMultiplicative.ground_mul: the ground map of a multiplicative law preserves 1 and products.
• PolynomialLaw.isMultiplicative_id, PolynomialLaw.IsMultiplicative.comp: the identity law is multiplicative, and multiplicative laws compose.
• PolynomialLaw.not_isMultiplicative_zero: the zero law to a nontrivial algebra is not multiplicative.
• AlgHom.isMultiplicative_toPolynomialLaw: the polynomial law of an algebra map is multiplicative.
• PolynomialLaw.IsHomogeneousOfDegree.toAlgHom: the ground map of a multiplicative law homogeneous of degree one, as an algebra map, whose polynomial law is the original law.
• PolynomialLaw.isHomogeneousOfDegree_one_and_isMultiplicative_iff: a law is homogeneous of degree one and multiplicative if and only if it is the polynomial law of an algebra map.
• PolynomialLaw.algHomEquiv: A →ₐ[R] B is identified with the multiplicative laws A →ₚₗ[R] B homogeneous of degree one.

References

• G. Chenevier, The p-adic analytic space of pseudocharacters of a profinite group and pseudorepresentations over arbitrary rings, §1.1

structure PolynomialLaw.IsMultiplicative {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₚₗ[R] B) : Prop

A polynomial law f : A →ₚₗ[R] B between R-algebras is multiplicative if f 1 = 1 and f (x * y) = f x * f y for every commutative R-algebra S and all x y : S ⊗[R] A. See IsMultiplicative.toFun_one and IsMultiplicative.toFun_mul for algebras in other universes.

• toFun'_one (S : Type u) [CommSemiring S] [Algebra R S] : f.toFun' S 1 = 1
• toFun'_mul {S : Type u} [CommSemiring S] [Algebra R S] (x y : TensorProduct R S A) : f.toFun' S (x * y) = f.toFun' S x * f.toFun' S y

@[simp]

theorem PolynomialLaw.IsMultiplicative.toFun_one {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} (hf : f.IsMultiplicative) (S : Type u_4) [CommSemiring S] [Algebra R S] : toFun S f 1 = 1

A multiplicative law sends 1 to 1 after scalar extension to a commutative R-algebra in an arbitrary universe.

@[simp]

theorem PolynomialLaw.IsMultiplicative.toFun_mul {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} (hf : f.IsMultiplicative) {S : Type u_4} [CommSemiring S] [Algebra R S] (x y : TensorProduct R S A) : toFun S f (x * y) = toFun S f x * toFun S f y

A multiplicative law preserves products after scalar extension to a commutative R-algebra in an arbitrary universe.

@[simp]

theorem PolynomialLaw.IsMultiplicative.ground_one {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} (hf : f.IsMultiplicative) : f.ground 1 = 1

The ground map of a multiplicative law sends 1 to 1.

@[simp]

theorem PolynomialLaw.IsMultiplicative.ground_mul {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} (hf : f.IsMultiplicative) (a b : A) : f.ground (a * b) = f.ground a * f.ground b

The ground map of a multiplicative law preserves products.

theorem PolynomialLaw.IsMultiplicative.comp {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} {C : Type u_3} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] {f : A →ₚₗ[R] B} {g : B →ₚₗ[R] C} (hg : g.IsMultiplicative) (hf : f.IsMultiplicative) : (g.comp f).IsMultiplicative

Multiplicative laws compose.

theorem PolynomialLaw.isMultiplicative_id {R : Type u} [CommSemiring R] {A : Type u_1} [Semiring A] [Algebra R A] : id.IsMultiplicative

The identity law is multiplicative.

theorem PolynomialLaw.not_isMultiplicative_zero {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Nontrivial B] : ¬IsMultiplicative 0

The zero law to a nontrivial algebra is not multiplicative: it preserves products but sends 1 to 0.

theorem AlgHom.isMultiplicative_toPolynomialLaw {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) : φ.toLinearMap.toPolynomialLaw.IsMultiplicative

The polynomial law of an algebra map is multiplicative: after scalar extension to S, it is the algebra map Algebra.TensorProduct.map (AlgHom.id R S) φ.

def PolynomialLaw.IsHomogeneousOfDegree.toAlgHom {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} (hf : IsHomogeneousOfDegree 1 f) (hm : f.IsMultiplicative) : A →ₐ[R] B

The ground map of a multiplicative polynomial law homogeneous of degree one, as an algebra map, whose polynomial law is the original law.

@[simp]

theorem PolynomialLaw.IsHomogeneousOfDegree.coe_toAlgHom {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} (hf : IsHomogeneousOfDegree 1 f) (hm : f.IsMultiplicative) : ⇑(hf.toAlgHom hm) = f.ground

@[simp]

theorem PolynomialLaw.IsHomogeneousOfDegree.toLinearMap_toAlgHom {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} (hf : IsHomogeneousOfDegree 1 f) (hm : f.IsMultiplicative) : (hf.toAlgHom hm).toLinearMap = hf.toLinearMap

theorem PolynomialLaw.IsHomogeneousOfDegree.toPolynomialLaw_toAlgHom {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} (hf : IsHomogeneousOfDegree 1 f) (hm : f.IsMultiplicative) : (hf.toAlgHom hm).toLinearMap.toPolynomialLaw = f

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

theorem PolynomialLaw.isHomogeneousOfDegree_one_and_isMultiplicative_iff {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₚₗ[R] B} : IsHomogeneousOfDegree 1 f ∧ f.IsMultiplicative ↔ ∃ (φ : A →ₐ[R] B), φ.toLinearMap.toPolynomialLaw = f

A polynomial law is homogeneous of degree one and multiplicative if and only if it is the polynomial law of an algebra map, namely of its ground map IsHomogeneousOfDegree.toAlgHom.

@[simp]

theorem AlgHom.toAlgHom_isHomogeneousOfDegree_toPolynomialLaw {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) : ⋯.toAlgHom ⋯ = φ

The algebra map recovered from the polynomial law of an algebra map φ is φ.

def PolynomialLaw.algHomEquiv (R : Type u) [CommSemiring R] (A : Type u_1) (B : Type u_2) [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : (A →ₐ[R] B) ≃ { f : A →ₚₗ[R] B // IsHomogeneousOfDegree 1 f ∧ f.IsMultiplicative }

Algebra maps A →ₐ[R] B are identified with the multiplicative polynomial laws A →ₚₗ[R] B homogeneous of degree one, by φ ↦ φ.toLinearMap.toPolynomialLaw with inverse IsHomogeneousOfDegree.toAlgHom.

@[simp]

theorem PolynomialLaw.coe_algHomEquiv_apply {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) : ↑((algHomEquiv R A B) φ) = φ.toLinearMap.toPolynomialLaw

@[simp]

theorem PolynomialLaw.algHomEquiv_symm_apply {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : { f : A →ₚₗ[R] B // IsHomogeneousOfDegree 1 f ∧ f.IsMultiplicative }) : (algHomEquiv R A B).symm f = ⋯.toAlgHom ⋯