Definition is_algid e U :=
-
[/\ e \in U, e != 0
& {in U, ∀ u,
e × u = u ∧ u × e = u}].
+
[/\ e \in U, e != 0
& {in U, ∀ u,
e × u = u ∧ u × e = u}].
-
Fact algid_decidable U :
decidable (
∃ e, is_algid e U).
+
Fact algid_decidable U :
decidable (
∃ e, is_algid e U).
-
Definition has_algid :
pred {vspace aT} :=
algid_decidable.
+
Definition has_algid :
pred {vspace aT} :=
algid_decidable.
-
Lemma has_algidP {
U} :
reflect (
∃ e, is_algid e U) (
has_algid U).
+
Lemma has_algidP {
U} :
reflect (
∃ e, is_algid e U) (
has_algid U).
-
Lemma has_algid1 U : 1
\in U → has_algid U.
+
Lemma has_algid1 U : 1
\in U → has_algid U.
-
Definition is_aspace U :=
has_algid U && (
U × U ≤ U)%
VS.
-
Structure aspace :=
ASpace {
asval :>
{vspace aT};
_ :
is_aspace asval}.
-
Definition aspace_of of phant aT :=
aspace.
+
Definition is_aspace U :=
has_algid U && (
U × U ≤ U)%
VS.
+
Structure aspace :=
ASpace {
asval :>
{vspace aT};
_ :
is_aspace asval}.
+
Definition aspace_of of phant aT :=
aspace.
-
Canonical aspace_subType :=
Eval hnf in [subType for asval].
-
Definition aspace_eqMixin :=
[eqMixin of aspace by <:].
+
Canonical aspace_subType :=
Eval hnf in [subType for asval].
+
Definition aspace_eqMixin :=
[eqMixin of aspace by <:].
Canonical aspace_eqType :=
Eval hnf in EqType aspace aspace_eqMixin.
-
Definition aspace_choiceMixin :=
[choiceMixin of aspace by <:].
+
Definition aspace_choiceMixin :=
[choiceMixin of aspace by <:].
Canonical aspace_choiceType :=
Eval hnf in ChoiceType aspace aspace_choiceMixin.
-
Canonical aspace_of_subType :=
Eval hnf in [subType of {aspace aT}].
-
Canonical aspace_of_eqType :=
Eval hnf in [eqType of {aspace aT}].
-
Canonical aspace_of_choiceType :=
Eval hnf in [choiceType of {aspace aT}].
+
Canonical aspace_of_subType :=
Eval hnf in [subType of {aspace aT}].
+
Canonical aspace_of_eqType :=
Eval hnf in [eqType of {aspace aT}].
+
Canonical aspace_of_choiceType :=
Eval hnf in [choiceType of {aspace aT}].
-
Definition clone_aspace U (
A :
{aspace aT}) :=
-
fun algU &
phant_id algU (
valP A) ⇒ @
ASpace U algU : {aspace aT}.
+
Definition clone_aspace U (
A :
{aspace aT}) :=
+
fun algU &
phant_id algU (
valP A) ⇒ @
ASpace U algU : {aspace aT}.
Fact aspace1_subproof :
is_aspace 1.
-
Canonical aspace1 :
{aspace aT} :=
ASpace aspace1_subproof.
+
Canonical aspace1 :
{aspace aT} :=
ASpace aspace1_subproof.
Lemma aspacef_subproof :
is_aspace fullv.
-
Canonical aspacef :
{aspace aT} :=
ASpace aspacef_subproof.
+
Canonical aspacef :
{aspace aT} :=
ASpace aspacef_subproof.
Lemma polyOver1P p :
-
reflect (
∃ q, p = map_poly (
in_alg aT)
q) (
p \is a polyOver 1%
VS).
+
reflect (
∃ q, p = map_poly (
in_alg aT)
q) (
p \is a polyOver 1%
VS).
End FalgebraTheory.
@@ -586,23 +585,23 @@
Delimit Scope aspace_scope with AS.
-
Notation "{ 'aspace' T }" := (
aspace_of (
Phant T)) :
type_scope.
-
Notation "A * B" := (
prodv A B) :
vspace_scope.
-
Notation "A ^+ n" := (
expv A n) :
vspace_scope.
-
Notation "'C [ u ]" := (
centraliser1_vspace u) :
vspace_scope.
-
Notation "'C_ U [ v ]" := (
capv U 'C[v]) :
vspace_scope.
-
Notation "'C_ ( U ) [ v ]" := (
capv U 'C[v]) (
only parsing) :
vspace_scope.
-
Notation "'C ( V )" := (
centraliser_vspace V) :
vspace_scope.
-
Notation "'C_ U ( V )" := (
capv U 'C(V)) :
vspace_scope.
-
Notation "'C_ ( U ) ( V )" := (
capv U 'C(V)) (
only parsing) :
vspace_scope.
-
Notation "'Z ( V )" := (
center_vspace V) :
vspace_scope.
+
Notation "{ 'aspace' T }" := (
aspace_of (
Phant T)) :
type_scope.
+
Notation "A * B" := (
prodv A B) :
vspace_scope.
+
Notation "A ^+ n" := (
expv A n) :
vspace_scope.
+
Notation "'C [ u ]" := (
centraliser1_vspace u) :
vspace_scope.
+
Notation "'C_ U [ v ]" := (
capv U 'C[v]) :
vspace_scope.
+
Notation "'C_ ( U ) [ v ]" := (
capv U 'C[v]) (
only parsing) :
vspace_scope.
+
Notation "'C ( V )" := (
centraliser_vspace V) :
vspace_scope.
+
Notation "'C_ U ( V )" := (
capv U 'C(V)) :
vspace_scope.
+
Notation "'C_ ( U ) ( V )" := (
capv U 'C(V)) (
only parsing) :
vspace_scope.
+
Notation "'Z ( V )" := (
center_vspace V) :
vspace_scope.
-
Notation "1" := (
aspace1 _) :
aspace_scope.
-
Notation "{ : aT }" := (
aspacef aT) :
aspace_scope.
-
Notation "[ 'aspace' 'of' U ]" := (@
clone_aspace _ _ U _ _ id)
+
Notation "1" := (
aspace1 _) :
aspace_scope.
+
Notation "{ : aT }" := (
aspacef aT) :
aspace_scope.
+
Notation "[ 'aspace' 'of' U ]" := (@
clone_aspace _ _ U _ _ id)
(
at level 0,
format "[ 'aspace' 'of' U ]") :
form_scope.
-
Notation "[ 'aspace' 'of' U 'for' A ]" := (@
clone_aspace _ _ U A _ idfun)
+
Notation "[ 'aspace' 'of' U 'for' A ]" := (@
clone_aspace _ _ U A _ idfun)
(
at level 0,
format "[ 'aspace' 'of' U 'for' A ]") :
form_scope.
@@ -612,97 +611,97 @@
Variables (
K :
fieldType) (
aT :
FalgType K).
-
Implicit Types (
u v e :
aT) (
U V :
{vspace aT}) (
A B :
{aspace aT}).
+
Implicit Types (
u v e :
aT) (
U V :
{vspace aT}) (
A B :
{aspace aT}).
Import FalgLfun.
Lemma algid_subproof U :
-
{e | e \in U
-
& has_algid U ==> (
U ≤ lker (
amull e - 1)
:&: lker (
amulr e - 1))%
VS}.
+
{e | e \in U
+
& has_algid U ==> (
U ≤ lker (
amull e - 1)
:&: lker (
amulr e - 1))%
VS}.
Definition algid U :=
s2val (
algid_subproof U).
-
Lemma memv_algid U :
algid U \in U.
+
Lemma memv_algid U :
algid U \in U.
-
Lemma algidl A :
{in A, left_id (
algid A)
*%R}.
+
Lemma algidl A :
{in A, left_id (
algid A)
*%R}.
-
Lemma algidr A :
{in A, right_id (
algid A)
*%R}.
+
Lemma algidr A :
{in A, right_id (
algid A)
*%R}.
-
Lemma unitr_algid1 A u :
u \in A → u \is a GRing.unit → algid A = 1.
+
Lemma unitr_algid1 A u :
u \in A → u \is a GRing.unit → algid A = 1.
-
Lemma algid_eq1 A :
(algid A == 1
) = (1
\in A).
+
Lemma algid_eq1 A :
(algid A == 1
) = (1
\in A).
-
Lemma algid_neq0 A :
algid A != 0.
+
Lemma algid_neq0 A :
algid A != 0.
-
Lemma dim_algid A :
\dim <[algid A]> = 1%
N.
+
Lemma dim_algid A :
\dim <[algid A]> = 1%
N.
-
Lemma adim_gt0 A : (0
< \dim A)%
N.
+
Lemma adim_gt0 A : (0
< \dim A)%
N.
-
Lemma not_asubv0 A :
~~ (
A ≤ 0)%
VS.
+
Lemma not_asubv0 A :
~~ (
A ≤ 0)%
VS.
-
Lemma adim1P {
A} :
reflect (
A = <[algid A]>%
VS :> {vspace aT}) (
\dim A == 1%
N).
+
Lemma adim1P {
A} :
reflect (
A = <[algid A]>%
VS :> {vspace aT}) (
\dim A == 1%
N).
-
Lemma asubv A : (
A × A ≤ A)%
VS.
+
Lemma asubv A : (
A × A ≤ A)%
VS.
-
Lemma memvM A :
{in A &, ∀ u v,
u × v \in A}.
+
Lemma memvM A :
{in A &, ∀ u v,
u × v \in A}.
-
Lemma prodv_id A : (
A × A)%
VS = A.
+
Lemma prodv_id A : (
A × A)%
VS = A.
-
Lemma prodv_sub U V A : (
U ≤ A → V ≤ A → U × V ≤ A)%
VS.
+
Lemma prodv_sub U V A : (
U ≤ A → V ≤ A → U × V ≤ A)%
VS.
-
Lemma expv_id A n : (
A ^+ n.+1)%
VS = A.
+
Lemma expv_id A n : (
A ^+ n.+1)%
VS = A.
-
Lemma limg_amulr U v : (
amulr v @: U = U × <[v]>)%
VS.
+
Lemma limg_amulr U v : (
amulr v @: U = U × <[v]>)%
VS.
Lemma memv_cosetP {
U v w} :
-
reflect (
exists2 u, u\in U & w = u × v) (
w \in U × <[v]>)%
VS.
+
reflect (
exists2 u, u\in U & w = u × v) (
w \in U × <[v]>)%
VS.
-
Lemma dim_cosetv_unit V u :
u \is a GRing.unit → \dim (V × <[u]>) = \dim V.
+
Lemma dim_cosetv_unit V u :
u \is a GRing.unit → \dim (V × <[u]>) = \dim V.
-
Lemma memvV A u :
(u^-1 \in A) = (u \in A).
+
Lemma memvV A u :
(u^-1 \in A) = (u \in A).
-
Fact aspace_cap_subproof A B :
algid A \in B → is_aspace (
A :&: B).
+
Fact aspace_cap_subproof A B :
algid A \in B → is_aspace (
A :&: B).
Definition aspace_cap A B BeA :=
ASpace (@
aspace_cap_subproof A B BeA).
-
Fact centraliser1_is_aspace u :
is_aspace 'C[u].
+
Fact centraliser1_is_aspace u :
is_aspace 'C[u].
Canonical centraliser1_aspace u :=
ASpace (
centraliser1_is_aspace u).
-
Fact centraliser_is_aspace V :
is_aspace 'C(V).
+
Fact centraliser_is_aspace V :
is_aspace 'C(V).
Canonical centraliser_aspace V :=
ASpace (
centraliser_is_aspace V).
-
Lemma centv_algid A :
algid A \in 'C(A)%
VS.
-
Canonical center_aspace A :=
[aspace of 'Z(A) for aspace_cap (
centv_algid A)
].
+
Lemma centv_algid A :
algid A \in 'C(A)%
VS.
+
Canonical center_aspace A :=
[aspace of 'Z(A) for aspace_cap (
centv_algid A)
].
-
Lemma algid_center A :
algid 'Z(A) = algid A.
+
Lemma algid_center A :
algid 'Z(A) = algid A.
Lemma Falgebra_FieldMixin :
-
GRing.IntegralDomain.axiom aT → GRing.Field.mixin_of aT.
+
GRing.IntegralDomain.axiom aT → GRing.Field.mixin_of aT.
Section SkewField.
@@ -711,18 +710,18 @@
Hypothesis fieldT :
GRing.Field.mixin_of aT.
-
Lemma skew_field_algid1 A :
algid A = 1.
+
Lemma skew_field_algid1 A :
algid A = 1.
Lemma skew_field_module_semisimple A M :
-
let sumA X := (
\sum_(x <- X) A × <[x]>)%
VS in
- (
A × M ≤ M)%
VS → {X | [/\ sumA X = M, directv (
sumA X)
& 0
\notin X]}.
+
let sumA X := (
\sum_(x <- X) A × <[x]>)%
VS in
+ (
A × M ≤ M)%
VS → {X | [/\ sumA X = M, directv (
sumA X)
& 0
\notin X]}.
-
Lemma skew_field_module_dimS A M : (
A × M ≤ M)%
VS → \dim A %| \dim M.
+
Lemma skew_field_module_dimS A M : (
A × M ≤ M)%
VS → \dim A %| \dim M.
-
Lemma skew_field_dimS A B : (
A ≤ B)%
VS → \dim A %| \dim B.
+
Lemma skew_field_dimS A B : (
A ≤ B)%
VS → \dim A %| \dim B.
End SkewField.
@@ -737,9 +736,9 @@
Note that local centraliser might not be proper sub-algebras.