From 8150209d2aaa0034b3dca9d82be1aeb11a12b5ea Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Thu, 31 Oct 2019 16:22:35 +0100 Subject: Interface for commutative and commutative-unitary algebras Initial properties of polynomials in R-algebras --- mathcomp/algebra/poly.v | 48 +++++++++++ mathcomp/algebra/ssralg.v | 199 +++++++++++++++++++++++++++++++++++++++++++++- mathcomp/field/fieldext.v | 44 ++++++---- 3 files changed, 273 insertions(+), 18 deletions(-) (limited to 'mathcomp') 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. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index bb566bb..3ecd00a 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -108,11 +108,15 @@ Definition base1 := ComRing.Class (@comm_ext T c). Definition base2 := @ComUnitRing.Class T base1 c. Definition base3 := @IntegralDomain.Class T base2 (@idomain_ext T c). Definition base4 := @Field.Class T base3 (@field_ext T c). +Definition base5 := @ComAlgebra.Class R T (@base T c) (@comm_ext T c). +Definition base6 := @ComUnitAlgebra.Class R T base5 c. End Bases. Local Coercion base1 : class_of >-> ComRing.class_of. Local Coercion base2 : class_of >-> ComUnitRing.class_of. Local Coercion base3 : class_of >-> IntegralDomain.class_of. Local Coercion base4 : class_of >-> Field.class_of. +Local Coercion base5 : class_of >-> ComAlgebra.class_of. +Local Coercion base6 : class_of >-> ComUnitAlgebra.class_of. Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. @@ -149,36 +153,40 @@ 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 unitAlgType := @UnitAlgebra.Pack R phR cT xclass. +Definition comAlgType := @ComAlgebra.Pack R phR cT xclass. +Definition comUnitAlgType := @ComUnitAlgebra.Pack R phR cT xclass. Definition vectType := @Vector.Pack R phR cT xclass. Definition FalgType := @Falgebra.Pack R phR cT xclass. Definition Falg_comRingType := @ComRing.Pack FalgType xclass. Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass. +Definition Falg_comAlgType := @ComAlgebra.Pack R phR FalgType xclass. +Definition Falg_comUnitAlgType := @ComUnitAlgebra.Pack R phR FalgType xclass. Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass. Definition Falg_fieldType := @Field.Pack FalgType xclass. Definition vect_comRingType := @ComRing.Pack vectType xclass. Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass. +Definition vect_comAlgType := @ComAlgebra.Pack R phR vectType xclass. +Definition vect_comUnitAlgType := @ComUnitAlgebra.Pack R phR vectType xclass. Definition vect_idomainType := @IntegralDomain.Pack vectType xclass. Definition vect_fieldType := @Field.Pack vectType xclass. -Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass. -Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass. +Definition comUnitAlg_idomainType := @IntegralDomain.Pack comUnitAlgType xclass. +Definition comUnitAlg_fieldType := @Field.Pack comUnitAlgType xclass. + Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass. Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass. -Definition alg_comRingType := @ComRing.Pack algType xclass. -Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass. +Definition comAlg_idomainType := @IntegralDomain.Pack comAlgType xclass. +Definition comAlg_fieldType := @Field.Pack comAlgType xclass. + Definition alg_idomainType := @IntegralDomain.Pack algType xclass. Definition alg_fieldType := @Field.Pack algType xclass. -Definition lalg_comRingType := @ComRing.Pack lalgType xclass. -Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass. Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass. Definition lalg_fieldType := @Field.Pack lalgType xclass. -Definition lmod_comRingType := @ComRing.Pack lmodType xclass. -Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass. Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass. Definition lmod_fieldType := @Field.Pack lmodType xclass. @@ -216,6 +224,10 @@ Coercion algType : type >-> Algebra.type. Canonical algType. Coercion unitAlgType : type >-> UnitAlgebra.type. Canonical unitAlgType. +Coercion comAlgType : type >-> ComAlgebra.type. +Canonical comAlgType. +Coercion comUnitAlgType : type >-> ComUnitAlgebra.type. +Canonical comUnitAlgType. Coercion vectType : type >-> Vector.type. Canonical vectType. Coercion FalgType : type >-> Falgebra.type. @@ -223,26 +235,26 @@ Canonical FalgType. Canonical Falg_comRingType. Canonical Falg_comUnitRingType. +Canonical Falg_comAlgType. +Canonical Falg_comUnitAlgType. Canonical Falg_idomainType. Canonical Falg_fieldType. Canonical vect_comRingType. Canonical vect_comUnitRingType. +Canonical vect_comAlgType. +Canonical vect_comUnitAlgType. Canonical vect_idomainType. Canonical vect_fieldType. -Canonical unitAlg_comRingType. -Canonical unitAlg_comUnitRingType. +Canonical comUnitAlg_idomainType. +Canonical comUnitAlg_fieldType. Canonical unitAlg_idomainType. Canonical unitAlg_fieldType. -Canonical alg_comRingType. -Canonical alg_comUnitRingType. +Canonical comAlg_idomainType. +Canonical comAlg_fieldType. Canonical alg_idomainType. Canonical alg_fieldType. -Canonical lalg_comRingType. -Canonical lalg_comUnitRingType. Canonical lalg_idomainType. Canonical lalg_fieldType. -Canonical lmod_comRingType. -Canonical lmod_comUnitRingType. Canonical lmod_idomainType. Canonical lmod_fieldType. Notation fieldExtType R := (type (Phant R)). -- cgit v1.2.3