-
Notifications
You must be signed in to change notification settings - Fork 51
/
Copy pathAlgebra_facts.v
115 lines (106 loc) · 3.63 KB
/
Algebra_facts.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
(* This program is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* This program is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this program; if not, write to the Free *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)
Set Automatic Coercions Import.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Algebra.
Require Export Ring_util.
Section Lemmas.
Variable R : CRING.
Variable A : algebra R.
Lemma ALGEBRA_comp :
forall x x' y y' : A,
Equal x x' -> Equal y y' -> Equal (algebra_mult x y) (algebra_mult x' y').
intros x x' y y' H' H'0; try assumption.
unfold algebra_mult in |- *.
apply Ap_comp.
auto with algebra.
apply
(Ap_comp (B:=Hom_module (algebra_carrier A) (algebra_carrier A))
(f:=algebra_bilinear_map (algebra_on_def A))
(g:=algebra_bilinear_map (algebra_on_def A)) H').
auto with algebra.
Qed.
Lemma ALGEBRA_lin_right :
forall x y z : A,
Equal (algebra_mult x (sgroup_law A y z))
(sgroup_law A (algebra_mult x y) (algebra_mult x z)).
intros x y z; try assumption.
unfold algebra_mult in |- *.
auto with algebra.
Qed.
Parameter
ALGEBRA_lin_left :
forall x y z : A,
Equal (algebra_mult (sgroup_law A x y) z)
(sgroup_law A (algebra_mult x z) (algebra_mult y z)).
Lemma ALGEBRA_mult_lin_right :
forall (x y : A) (a : R),
Equal (algebra_mult x (module_mult a y)) (module_mult a (algebra_mult x y)).
intros x y a; try assumption.
unfold algebra_mult in |- *.
auto with algebra.
Qed.
Parameter
ALGEBRA_mult_lin_left :
forall (x y : A) (a : R),
Equal (algebra_mult (module_mult a x) y)
(module_mult a (algebra_mult x y)).
End Lemmas.
Hint Resolve ALGEBRA_comp ALGEBRA_lin_right ALGEBRA_lin_left
ALGEBRA_mult_lin_right ALGEBRA_mult_lin_left: algebra.
Section Lemmas2.
Variable R : CRING.
Variable A : ring_algebra R.
Lemma RING_ALGEBRA_assoc :
forall x y z : A,
Equal (algebra_mult (algebra_mult x y) z)
(algebra_mult x (algebra_mult y z)).
exact (ring_algebra_assoc A).
Qed.
Lemma RING_ALGEBRA_unit_l :
forall x : A, Equal (algebra_mult (ring_algebra_unit A) x) x.
exact (ring_algebra_unit_l A).
Qed.
Lemma RING_ALGEBRA_unit_r :
forall x : A, Equal (algebra_mult x (ring_algebra_unit A)) x.
exact (ring_algebra_unit_r A).
Qed.
End Lemmas2.
Hint Resolve RING_ALGEBRA_assoc RING_ALGEBRA_unit_l RING_ALGEBRA_unit_r:
algebra.
Section Ring_algebra_as_ring.
Variable R : CRING.
Variable A : ring_algebra R.
Definition ring_algebra_ring : ring.
apply
(BUILD_RING (E:=A) (ringplus:=sgroup_law A)
(ringmult:=algebra_mult (R:=R) (A:=A)) (zero:=monoid_unit A)
(un:=ring_algebra_unit A) (ringopp:=group_inverse A)).
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
auto with algebra.
Defined.
End Ring_algebra_as_ring.
Coercion ring_algebra_ring : ring_algebra >-> ring.