Skip to content

Commit 5cb5e8a

Browse files
CohenCyrilgares
CohenCyril
authored and
gares
committed
moving category theory to theories
1 parent f49142f commit 5cb5e8a

File tree

2 files changed

+120
-109
lines changed

2 files changed

+120
-109
lines changed

‎theories/algebra.v‎

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
Require Import ssreflect ssrfun.
2+
From HB Require Import structures cat.
3+
4+
Set Implicit Arguments.
5+
Unset Strict Implicit.
6+
Unset Printing Implicit Defensive.
7+
Add Search Blacklist "__canonical__".
8+
9+
Local Open Scope algebra_scope.
10+
Local Open Scope cat_scope.
11+
12+
HB.mixin Record IsRing A := {
13+
zero : A;
14+
one : A;
15+
add : A -> A -> A;
16+
opp : A -> A;
17+
mul : A -> A -> A;
18+
addrA : associative add;
19+
addrC : commutative add;
20+
add0r : left_id zero add;
21+
addNr : left_inverse zero opp add;
22+
mulrA : associative mul;
23+
mul1r : left_id one mul;
24+
mulr1 : right_id one mul;
25+
mulrDl : left_distributive mul add;
26+
mulrDr : right_distributive mul add;
27+
}.
28+
29+
#[short(type="ring")]
30+
HB.structure Definition Ring := { A of IsRing A }.
31+
32+
Bind Scope algebra_scope with Ring.sort.
33+
Notation "0" := zero : algebra_scope.
34+
Notation "1" := one : algebra_scope.
35+
Infix "+" := (@add _) : algebra_scope.
36+
Notation "- x" := (@opp _ x) : algebra_scope.
37+
Infix "*" := (@mul _) : algebra_scope.
38+
Notation "x - y" := (x + - y) : algebra_scope.
39+
40+
Lemma addr0 (R : ring) : right_id (@zero R) add.
41+
Proof. by move=> x; rewrite addrC add0r. Qed.
42+
43+
Lemma addrN (R : ring) : right_inverse (@zero R) opp add.
44+
Proof. by move=> x; rewrite addrC addNr. Qed.
45+
46+
Lemma addKr (R : ring) (x : R) : cancel (add x) (add (- x)).
47+
Proof. by move=> y; rewrite addrA addNr add0r. Qed.
48+
49+
Lemma addrI (R : ring) (x : R) : injective (add x).
50+
Proof. exact: can_inj (addKr _). Qed.
51+
52+
Lemma opprK (R : ring) : involutive (@opp R).
53+
Proof. by move=> x; apply: (@addrI _ (- x)); rewrite addNr addrN. Qed.
54+
55+
HB.mixin Record IsRingHom (A B : ring) (f : A -> B) := {
56+
hom1_subproof : f 1%A = 1%A;
57+
homB_subproof : {morph f : x y / x - y};
58+
homM_subproof : {morph f : x y / (x * y)%A};
59+
}.
60+
61+
HB.structure Definition RingHom A B := { f of IsRingHom A B f }.
62+
63+
Lemma id_IsRingHom A : IsRingHom A A idfun. Proof. by []. Defined.
64+
HB.instance Definition _ A := id_IsRingHom A.
65+
66+
Lemma comp_IsRingHom (A B C : ring)
67+
(f : RingHom.type A B) (g : RingHom.type B C) :
68+
IsRingHom A C (f \; g :> U).
69+
Proof.
70+
by constructor => [|x y|x y];
71+
rewrite /comp/= ?hom1_subproof ?homB_subproof ?homM_subproof.
72+
Qed.
73+
HB.instance Definition _ A B C f g := @comp_IsRingHom A B C f g.
74+
75+
HB.instance Definition _ := IsQuiver.Build ring RingHom.type.
76+
HB.instance Definition _ :=
77+
Quiver_IsPreCat.Build ring (fun _ => idfun) (fun _ _ _ f g => f \; g :> U).
78+
HB.instance Definition _ := Quiver_IsPreConcrete.Build ring (fun _ _ => id).
79+
Lemma ring_precat : PreConcrete_IsConcrete ring.
80+
Proof.
81+
constructor => A B [f cf] [g cg]//=; rewrite -[_ = _]/(f = g) => fg.
82+
case: _ / fg in cg *; congr {|RingHom.sort := _ ; RingHom.class := _|}.
83+
case: cf cg => [[? ? ?]] [[? ? ?]].
84+
by congr RingHom.Class; congr IsRingHom.phant_Build => //=; apply: Prop_irrelevance.
85+
Qed.
86+
HB.instance Definition _ := ring_precat.
87+
88+
Lemma ring_IsCat : PreCat_IsCat ring.
89+
Proof.
90+
by constructor=> [A B f|A B f|A B C D f g h]; exact: concrete_fun_inj.
91+
Qed.
92+
HB.instance Definition _ := ring_IsCat.
93+
94+
Lemma hom1 (R S : ring) (f : R ~> S) : f 1%A = 1%A.
95+
Proof. exact: hom1_subproof. Qed.
96+
Lemma homB (R S : ring) (f : R ~> S) : {morph f : x y / x - y}.
97+
Proof. exact: homB_subproof. Qed.
98+
Lemma homM (R S : ring) (f : R ~> S) : {morph f : x y / (x * y)%A}.
99+
Proof. exact: homM_subproof. Qed.
100+
Lemma hom0 (R S : ring) (f : R ~> S) : f 0%A = 0%A.
101+
Proof. by rewrite -(addrN 1%A) homB addrN. Qed.
102+
Lemma homN (R S : ring) (f : R ~> S) : {morph f : x / - x}.
103+
Proof. by move=> x; rewrite -[- x]add0r homB hom0 add0r. Qed.
104+
Lemma homD (R S : ring) (f : R ~> S) : {morph f : x y / x + y}.
105+
Proof. by move=> x y; rewrite -[y]opprK !homB !homN. Qed.
106+
107+
HB.mixin Record IsIdeal (R : ring) (I : R -> Prop) := {
108+
ideal0 : I 0;
109+
idealD : forall x y, I x -> I y -> I (x + y);
110+
idealM : forall x y, I y -> I (x * y)%A;
111+
}.
112+
HB.structure Definition Ideal (R : ring) := { I of IsIdeal R I }.
113+
114+
HB.mixin Record Ideal_IsPrime (R : ring) (I : R -> Prop) of IsIdeal R I := {
115+
ideal_prime : forall x y : R, I (x * y)%A -> I x \/ I y
116+
}.
117+
#[short(type="spectrum")]
118+
HB.structure Definition PrimeIdeal (R : ring) :=
119+
{ I of Ideal_IsPrime R I & Ideal R I }.
120+

‎examples/cat/cat.v‎ renamed to ‎theories/cat.v‎

Lines changed: 0 additions & 109 deletions
Original file line numberDiff line numberDiff line change
@@ -881,113 +881,4 @@ HB.structure Definition Monoidal : Set :=
881881
{ C of PreMonoidal_IsMonoidal C & PreMonoidal C }.
882882
Set Universe Checking.
883883

884-
HB.mixin Record IsRing A := {
885-
zero : A;
886-
one : A;
887-
add : A -> A -> A;
888-
opp : A -> A;
889-
mul : A -> A -> A;
890-
addrA : associative add;
891-
addrC : commutative add;
892-
add0r : left_id zero add;
893-
addNr : left_inverse zero opp add;
894-
mulrA : associative mul;
895-
mul1r : left_id one mul;
896-
mulr1 : right_id one mul;
897-
mulrDl : left_distributive mul add;
898-
mulrDr : right_distributive mul add;
899-
}.
900-
901-
#[short(type="ring")]
902-
HB.structure Definition Ring := { A of IsRing A }.
903-
904-
Bind Scope algebra_scope with Ring.sort.
905-
Notation "0" := zero : algebra_scope.
906-
Notation "1" := one : algebra_scope.
907-
Infix "+" := (@add _) : algebra_scope.
908-
Notation "- x" := (@opp _ x) : algebra_scope.
909-
Infix "*" := (@mul _) : algebra_scope.
910-
Notation "x - y" := (x + - y) : algebra_scope.
911-
912-
Lemma addr0 (R : ring) : right_id (@zero R) add.
913-
Proof. by move=> x; rewrite addrC add0r. Qed.
914-
915-
Lemma addrN (R : ring) : right_inverse (@zero R) opp add.
916-
Proof. by move=> x; rewrite addrC addNr. Qed.
917-
918-
Lemma addKr (R : ring) (x : R) : cancel (add x) (add (- x)).
919-
Proof. by move=> y; rewrite addrA addNr add0r. Qed.
920-
921-
Lemma addrI (R : ring) (x : R) : injective (add x).
922-
Proof. exact: can_inj (addKr _). Qed.
923-
924-
Lemma opprK (R : ring) : involutive (@opp R).
925-
Proof. by move=> x; apply: (@addrI _ (- x)); rewrite addNr addrN. Qed.
926-
927-
HB.mixin Record IsRingHom (A B : ring) (f : A -> B) := {
928-
hom1_subproof : f 1%A = 1%A;
929-
homB_subproof : {morph f : x y / x - y};
930-
homM_subproof : {morph f : x y / (x * y)%A};
931-
}.
932-
933-
HB.structure Definition RingHom A B := { f of IsRingHom A B f }.
934-
935-
Lemma id_IsRingHom A : IsRingHom A A idfun. Proof. by []. Defined.
936-
HB.instance Definition _ A := id_IsRingHom A.
937-
938-
Lemma comp_IsRingHom (A B C : ring)
939-
(f : RingHom.type A B) (g : RingHom.type B C) :
940-
IsRingHom A C (f \; g :> U).
941-
Proof.
942-
by constructor => [|x y|x y];
943-
rewrite /comp/= ?hom1_subproof ?homB_subproof ?homM_subproof.
944-
Qed.
945-
HB.instance Definition _ A B C f g := @comp_IsRingHom A B C f g.
946-
947-
HB.instance Definition _ := IsQuiver.Build ring RingHom.type.
948-
HB.instance Definition _ :=
949-
Quiver_IsPreCat.Build ring (fun _ => idfun) (fun _ _ _ f g => f \; g :> U).
950-
HB.instance Definition _ := Quiver_IsPreConcrete.Build ring (fun _ _ => id).
951-
Lemma ring_precat : PreConcrete_IsConcrete ring.
952-
Proof.
953-
constructor => A B [f cf] [g cg]//=; rewrite -[_ = _]/(f = g) => fg.
954-
case: _ / fg in cg *; congr {|RingHom.sort := _ ; RingHom.class := _|}.
955-
case: cf cg => [[? ? ?]] [[? ? ?]].
956-
by congr RingHom.Class; congr IsRingHom.phant_Build => //=; apply: Prop_irrelevance.
957-
Qed.
958-
HB.instance Definition _ := ring_precat.
959-
960-
Lemma ring_IsCat : PreCat_IsCat ring.
961-
Proof.
962-
by constructor=> [A B f|A B f|A B C D f g h]; exact: concrete_fun_inj.
963-
Qed.
964-
HB.instance Definition _ := ring_IsCat.
965-
966-
Lemma hom1 (R S : ring) (f : R ~> S) : f 1%A = 1%A.
967-
Proof. exact: hom1_subproof. Qed.
968-
Lemma homB (R S : ring) (f : R ~> S) : {morph f : x y / x - y}.
969-
Proof. exact: homB_subproof. Qed.
970-
Lemma homM (R S : ring) (f : R ~> S) : {morph f : x y / (x * y)%A}.
971-
Proof. exact: homM_subproof. Qed.
972-
Lemma hom0 (R S : ring) (f : R ~> S) : f 0%A = 0%A.
973-
Proof. by rewrite -(addrN 1%A) homB addrN. Qed.
974-
Lemma homN (R S : ring) (f : R ~> S) : {morph f : x / - x}.
975-
Proof. by move=> x; rewrite -[- x]add0r homB hom0 add0r. Qed.
976-
Lemma homD (R S : ring) (f : R ~> S) : {morph f : x y / x + y}.
977-
Proof. by move=> x y; rewrite -[y]opprK !homB !homN. Qed.
978-
979-
HB.mixin Record IsIdeal (R : ring) (I : R -> Prop) := {
980-
ideal0 : I 0;
981-
idealD : forall x y, I x -> I y -> I (x + y);
982-
idealM : forall x y, I y -> I (x * y)%A;
983-
}.
984-
HB.structure Definition Ideal (R : ring) := { I of IsIdeal R I }.
985-
986-
HB.mixin Record Ideal_IsPrime (R : ring) (I : R -> Prop) of IsIdeal R I := {
987-
ideal_prime : forall x y : R, I (x * y)%A -> I x \/ I y
988-
}.
989-
#[short(type="spectrum")]
990-
HB.structure Definition PrimeIdeal (R : ring) :=
991-
{ I of Ideal_IsPrime R I & Ideal R I }.
992-
993884

0 commit comments

Comments
 (0)