From 6ba0e77cd7f8d68647790fe2b704f35ae76ad1f8 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Mon, 4 Nov 2019 13:42:59 +0100 Subject: Fixed inheritance of fieldExt / fieldOver / splitting field --- mathcomp/algebra/ssralg.v | 15 +++++++-------- mathcomp/field/fieldext.v | 3 +++ mathcomp/field/galois.v | 6 ++++++ 3 files changed, 16 insertions(+), 8 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 2cf0a23..4d32364 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -359,19 +359,19 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial. (* divalg_closed coerces to all the prerequisites. *) (* *) (* * ComAlgebra (commutative algebra): *) -(* comUnitAlgType R == interface type for ComAlgebra structure with *) +(* comAlgType 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 *) +(* comUnitAlgType 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. *) +(* merging canonical comAlgType and *) +(* unitRingType on V. *) (* *) (* In addition to this structure hierarchy, we also develop a separate, *) (* parallel hierarchy for morphisms linking these structures: *) @@ -3305,8 +3305,6 @@ Record class_of (T : Type) : Type := Class { 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. @@ -3320,7 +3318,7 @@ 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 bT b & phant_id (@ComAlgebra.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). @@ -3330,7 +3328,7 @@ 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 comUnitRingType := @ComUnitRing.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. @@ -3423,6 +3421,7 @@ Proof. by rewrite exprMn exprVn. Qed. Canonical regular_comUnitRingType := [comUnitRingType of R^o]. Canonical regular_unitAlgType := [unitAlgType R of R^o]. +Canonical regular_comUnitAlgType := [comUnitAlgType R of R^o]. End ComUnitRingTheory. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 3ecd00a..64239f3 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -198,6 +198,7 @@ Coercion sort : type >-> Sortclass. Bind Scope ring_scope with sort. Coercion base : class_of >-> Falgebra.class_of. Coercion base4 : class_of >-> Field.class_of. +Coercion base6 : class_of >-> ComUnitAlgebra.class_of. Coercion eqType : type >-> Equality.type. Canonical eqType. Coercion choiceType : type >-> Choice.type. @@ -837,6 +838,8 @@ Proof. exact: mulrCA. Qed. Canonical fieldOver_algType := AlgType K_F L_F fieldOver_scaleAr. Canonical fieldOver_unitAlgType := [unitAlgType K_F of L_F]. +Canonical fieldOver_comAlgType := [comAlgType K_F of L_F]. +Canonical fieldOver_comUnitAlgType := [comUnitAlgType K_F of L_F]. Fact fieldOver_vectMixin : Vector.mixin_of fieldOver_lmodType. Proof. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 30bef47..9a2bdfd 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -370,6 +370,8 @@ Definition lmodType := @Lmodule.Pack F phF cT xclass. Definition lalgType := @Lalgebra.Pack F phF cT xclass. Definition algType := @Algebra.Pack F phF cT xclass. Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass. +Definition comAlgType := @ComAlgebra.Pack F phF cT xclass. +Definition comUnitAlgType := @ComUnitAlgebra.Pack F phF cT xclass. Definition vectType := @Vector.Pack F phF cT xclass. Definition FalgType := @Falgebra.Pack F phF cT xclass. Definition fieldExtType := @FieldExt.Pack F phF cT xclass. @@ -405,8 +407,12 @@ 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. +Coercion comUnitAlgType : type >-> ComUnitAlgebra.type. +Canonical comUnitAlgType. Coercion vectType : type >-> Vector.type. Canonical vectType. Coercion FalgType : type >-> Falgebra.type. -- cgit v1.2.3