Interface for commutative and commutative-unitary algebras

Initial properties of polynomials in R-algebras

2 files changed, 245 insertions, 2 deletions

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index a3b9211..eb96da2 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -74,6 +74,9 @@ From mathcomp Require Import fintype bigop div ssralg countalg binomial tuple.
 (*      horner_eval u == the function mapping p to p.[u]; this function can   *)
 (*                       only be used for u in a commutative ring, so it is   *)
 (*                       always a linear ring morphism from {poly R} to R.    *)
+(*       horner_alg a == given a in some R-algebra A, the function evaluating *)
+(*                       a polynomial p at a; it is always a linear ring      *)
+(*                       morphism from {poly R} to A.                         *)
 (*     diff_roots x y == x and y are distinct roots; if R is a field, this    *)
 (*                       just means x != y, but this concept is generalized   *)
 (*                       to the case where R is only a ring with units (i.e., *)
@@ -2060,6 +2063,7 @@ Canonical polynomial_comRingType :=
 Canonical poly_algType := Eval hnf in CommAlgType R {poly R}.
 Canonical polynomial_algType :=
   Eval hnf in [algType R of polynomial R for poly_algType].
+Canonical poly_comAlgType := Eval hnf in [comAlgType R of {poly R}].
 
 Lemma hornerM p q x : (p * q).[x] = p.[x] * q.[x].
 Proof. by rewrite hornerM_comm //; apply: mulrC. Qed.
@@ -2091,6 +2095,50 @@ Canonical horner_eval_rmorphism x := RMorphism (horner_eval_is_lrmorphism x).
 Canonical horner_eval_linear x := AddLinear (horner_eval_is_lrmorphism x).
 Canonical horner_eval_lrmorphism x := [lrmorphism of horner_eval x].
 
+Section HornerAlg.
+
+Variable A : algType R. (* For univariate polys, commutativity is not needed *)
+
+Section Defs.
+
+Variable a : A.
+
+Lemma in_alg_comm : commr_rmorph (in_alg A) a.
+Proof. move=> r /=; by rewrite /GRing.comm comm_alg. Qed.
+
+Definition horner_alg := horner_morph in_alg_comm.
+
+Lemma horner_algC c : horner_alg c%:P = c%:A.
+Proof. exact: horner_morphC. Qed.
+
+Lemma horner_algX : horner_alg 'X = a.
+Proof. exact:  horner_morphX. Qed.
+
+Fact horner_alg_is_lrmorphism : lrmorphism horner_alg.
+Proof.
+rewrite /horner_alg; split=> [|c p]; last by rewrite linearZ /= mulr_algl.
+split=> [p q|]; first by rewrite rmorphB.
+split=> [p q|]; last by rewrite rmorph1.
+by rewrite rmorphM.
+Qed.
+Canonical horner_alg_additive := Additive horner_alg_is_lrmorphism.
+Canonical horner_alg_rmorphism := RMorphism horner_alg_is_lrmorphism.
+Canonical horner_alg_linear := AddLinear horner_alg_is_lrmorphism.
+Canonical horner_alg_lrmorphism := [lrmorphism of horner_alg].
+
+End Defs.
+
+Variable (pf : {lrmorphism {poly R} -> A}).
+
+Lemma poly_alg_initial : pf =1 horner_alg (pf 'X).
+Proof.
+apply: poly_ind => [|p a IHp]; first by rewrite !rmorph0.
+rewrite !rmorphD !rmorphM /= -{}IHp horner_algC ?horner_algX.
+by rewrite -alg_polyC rmorph_alg.
+Qed.
+
+End HornerAlg.
+
 Fact comp_poly_multiplicative q : multiplicative (comp_poly q).
 Proof.
 split=> [p1 p2|]; last by rewrite comp_polyC.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 486b12e..2cf0a23 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -358,6 +358,21 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
 (*                           property, provided S's key is a divringPred;     *)
 (*                           divalg_closed coerces to all the prerequisites.  *)
 (*                                                                            *)
+(*  * ComAlgebra (commutative algebra):                                       *)
+(*       comUnitAlgType R == interface type for ComAlgebra structure with     *)
+(*                           scalars in R; R should have a comRingType        *)
+(*                           structure.                                       *)
+(*    [comAlgType R of V] == a comAlgType R structure for V created by        *)
+(*                           merging canonical algType and comRingType on V.  *)
+(*                                                                            *)
+(*  * ComUnitAlgebra (commutative algebra with computable inverses):          *)
+(*           comAlgType R == interface type for ComUnitAlgebra structure with *)
+(*                           scalars in R; R should have a comUnitRingType    *)
+(*                           structure.                                       *)
+(*    [comAlgType R of V] == a comAlgType R structure for V created by        *)
+(*                           merging canonical algType and                    *)
+(*                           comUnitRingType on V.                            *)
+(*                                                                            *)
 (*   In addition to this structure hierarchy, we also develop a separate,     *)
 (* parallel hierarchy for morphisms linking these structures:                 *)
 (*                                                                            *)
@@ -2680,6 +2695,79 @@ End Exports.
 End Algebra.
 Import Algebra.Exports.
 
+Module ComAlgebra.
+
+Section ClassDef.
+
+Variable R : ringType.
+
+Record class_of (T : Type) : Type := Class {
+  base : Algebra.class_of R T;
+  mixin : commutative (Ring.mul base)
+}.
+Definition base2 R m := ComRing.Class (@mixin R m).
+Local Coercion base : class_of >-> Algebra.class_of.
+Local Coercion base2 : class_of >-> ComRing.class_of.
+
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
+Local Coercion sort : type >-> Sortclass.
+Variable (phR : phant R) (T : Type) (cT : type phR).
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition pack :=
+  fun bT b & phant_id (@Algebra.class R phR bT) (b : Algebra.class_of R T) =>
+  fun mT m & phant_id (ComRing.mixin (ComRing.class mT)) m =>
+  Pack (Phant R) (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition comRingType := @ComRing.Pack cT xclass.
+Definition lmodType := @Lmodule.Pack R phR cT xclass.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass.
+Definition algType := @Algebra.Pack R phR cT xclass.
+Definition lmod_comRingType := @Lmodule.Pack R phR comRingType xclass.
+Definition lalg_comRingType := @Lalgebra.Pack R phR comRingType xclass.
+Definition alg_comRingType := @Algebra.Pack R phR comRingType xclass.
+
+End ClassDef.
+
+Module Exports.
+Coercion base : class_of >-> Algebra.class_of.
+Coercion base2 : class_of >-> ComRing.class_of.
+Coercion sort : type >-> Sortclass.
+Bind Scope ring_scope with sort.
+Coercion eqType : type >-> Equality.type.
+Canonical eqType.
+Coercion choiceType : type >-> Choice.type.
+Canonical choiceType.
+Coercion zmodType : type >-> Zmodule.type.
+Canonical zmodType.
+Coercion ringType : type >-> Ring.type.
+Canonical ringType.
+Coercion comRingType : type >-> ComRing.type.
+Canonical comRingType.
+Coercion lmodType : type >-> Lmodule.type.
+Canonical lmodType.
+Coercion lalgType : type >-> Lalgebra.type.
+Canonical lalgType.
+Coercion algType : type >-> Algebra.type.
+Canonical algType.
+Canonical lmod_comRingType.
+Canonical lalg_comRingType.
+Canonical alg_comRingType.
+
+Notation comAlgType R := (type (Phant R)).
+Notation "[ 'comAlgType' R 'of' T ]" := (@pack _ (Phant R) T _ _ id _ _ id)
+  (at level 0, format "[ 'comAlgType'  R  'of'  T ]") : form_scope.
+End Exports.
+
+End ComAlgebra.
+Import ComAlgebra.Exports.
+
 Section AlgebraTheory.
 
 Variables (R : comRingType) (A : algType R).
@@ -2694,6 +2782,9 @@ Proof. by rewrite -scalerAl scalerAr. Qed.
 Lemma mulr_algr a x : x * a%:A = a *: x.
 Proof. by rewrite -scalerAr mulr1. Qed.
 
+Lemma comm_alg a x : comm a%:A x.
+Proof. by rewrite /comm mulr_algr mulr_algl. Qed.
+
 Lemma exprZn k x n : (k *: x) ^+ n = k ^+ n *: x ^+ n.
 Proof.
 elim: n => [|n IHn]; first by rewrite !expr0 scale1r.
@@ -2718,6 +2809,7 @@ Proof. by rewrite scaler_prod prodr_const. Qed.
 
 Canonical regular_comRingType := [comRingType of R^o].
 Canonical regular_algType := CommAlgType R R^o.
+Canonical regular_comAlgType := [comAlgType R of R^o].
 
 Variables (U : lmodType R) (a : A) (f : {linear U -> A}).
 
@@ -3202,6 +3294,107 @@ End Exports.
 End UnitAlgebra.
 Import UnitAlgebra.Exports.
 
+Module ComUnitAlgebra.
+
+Section ClassDef.
+
+Variable R : ringType.
+
+Record class_of (T : Type) : Type := Class {
+  base : ComAlgebra.class_of R T;
+  mixin : GRing.UnitRing.mixin_of (ComRing.Pack base)
+}.
+Definition base2 R m := UnitAlgebra.Class (@mixin R m).
+(* I'm not sure this base3 is needed but can't manage to get things working *)
+(* without it                                                               *)
+Definition base3 R m := ComUnitRing.Class (@mixin R m).
+Local Coercion base : class_of >-> ComAlgebra.class_of.
+Local Coercion base2 : class_of >-> UnitAlgebra.class_of.
+Local Coercion base3 : class_of >-> ComUnitRing.class_of.
+
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
+Local Coercion sort : type >-> Sortclass.
+Variable (phR : phant R) (T : Type) (cT : type phR).
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition pack :=
+  fun bT b & phant_id (@Algebra.class R phR bT) (b : ComAlgebra.class_of R T) =>
+  fun mT m & phant_id (UnitRing.mixin (UnitRing.class mT)) m =>
+  Pack (Phant R) (@Class T b m).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition unitRingType := @UnitRing.Pack cT xclass.
+Definition comRingType := @ComRing.Pack cT xclass.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass. (* Coercion base3 *)
+Definition lmodType := @Lmodule.Pack R phR cT xclass.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass.
+Definition algType := @Algebra.Pack R phR cT xclass.
+Definition comAlgType := @ComAlgebra.Pack R phR cT xclass.
+Definition unitAlgType := @UnitAlgebra.Pack R phR cT xclass.
+Definition comalg_unitRingType := @ComAlgebra.Pack R phR unitRingType xclass.
+Definition comalg_comUnitRingType :=
+  @ComAlgebra.Pack R phR comUnitRingType xclass.
+Definition comalg_unitAlgType := @ComAlgebra.Pack R phR unitAlgType xclass.
+Definition unitalg_comRingType := @UnitAlgebra.Pack R phR comRingType xclass.
+Definition unitalg_comUnitRingType :=
+  @UnitAlgebra.Pack R phR comUnitRingType xclass.
+Definition lmod_comUnitRingType := @Lmodule.Pack R phR comUnitRingType xclass.
+Definition lalg_comUnitRingType := @Lalgebra.Pack R phR comUnitRingType xclass.
+Definition alg_comUnitRingType := @Algebra.Pack R phR comUnitRingType xclass.
+
+End ClassDef.
+
+Module Exports.
+Coercion base : class_of >-> ComAlgebra.class_of.
+Coercion base2 : class_of >-> UnitAlgebra.class_of.
+Coercion sort : type >-> Sortclass.
+Bind Scope ring_scope with sort.
+Coercion eqType : type >-> Equality.type.
+Canonical eqType.
+Coercion choiceType : type >-> Choice.type.
+Canonical choiceType.
+Coercion zmodType : type >-> Zmodule.type.
+Canonical zmodType.
+Coercion ringType : type >-> Ring.type.
+Canonical ringType.
+Coercion unitRingType : type >-> UnitRing.type.
+Canonical unitRingType.
+Coercion comRingType : type >-> ComRing.type.
+Canonical comRingType.
+Coercion comUnitRingType : type >-> ComUnitRing.type.
+Canonical comUnitRingType.
+Coercion lmodType : type >-> Lmodule.type.
+Canonical lmodType.
+Coercion lalgType : type >-> Lalgebra.type.
+Canonical lalgType.
+Coercion algType : type >-> Algebra.type.
+Canonical algType.
+Coercion comAlgType : type >-> ComAlgebra.type.
+Canonical comAlgType.
+Coercion unitAlgType : type >-> UnitAlgebra.type.
+Canonical unitAlgType.
+Canonical comalg_unitRingType.
+Canonical comalg_comUnitRingType.
+Canonical comalg_unitAlgType.
+Canonical unitalg_comRingType.
+Canonical unitalg_comUnitRingType.
+Canonical lmod_comUnitRingType.
+Canonical lalg_comUnitRingType.
+Canonical alg_comUnitRingType.
+
+Notation comUnitAlgType R := (type (Phant R)).
+Notation "[ 'comUnitAlgType' R 'of' T ]" := (@pack _ (Phant R) T _ _ id _ _ id)
+  (at level 0, format "[ 'comUnitAlgType'  R  'of'  T ]") : form_scope.
+End Exports.
+
+End ComUnitAlgebra.
+Import ComUnitAlgebra.Exports.
+
 Section ComUnitRingTheory.
 
 Variable R : comUnitRingType.
@@ -5754,6 +5947,7 @@ Definition signrZK := signrZK.
 Definition scalerCA := scalerCA.
 Definition scalerAr := scalerAr.
 Definition mulr_algr := mulr_algr.
+Definition comm_alg := comm_alg.
 Definition exprZn := exprZn.
 Definition scaler_prodl := scaler_prodl.
 Definition scaler_prodr := scaler_prodr.
@@ -5797,8 +5991,9 @@ End GRing.
 
 Export Zmodule.Exports Ring.Exports Lmodule.Exports Lalgebra.Exports.
 Export Additive.Exports RMorphism.Exports Linear.Exports LRMorphism.Exports.
-Export ComRing.Exports Algebra.Exports UnitRing.Exports UnitAlgebra.Exports.
-Export ComUnitRing.Exports IntegralDomain.Exports Field.Exports.
+Export Algebra.Exports UnitRing.Exports UnitAlgebra.Exports.
+Export ComRing.Exports ComAlgebra.Exports ComUnitRing.Exports.
+Export ComUnitAlgebra.Exports IntegralDomain.Exports Field.Exports.
 Export DecidableField.Exports ClosedField.Exports.
 Export Pred.Exports SubType.Exports.
 Notation QEdecFieldMixin := QEdecFieldMixin.