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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(* General results about arbitrary integer implementations. *)
Require
MathClasses.theory.nat_distance.
From Coq Require Import Ring.
Require Import
MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers.
Require Export
MathClasses.interfaces.integers.
(* Any two integer implementations are trivially isomorphic because of their initiality,
but it's nice to have this stated in terms of integers_to_ring being self-inverse: *)
Lemma to_ring_involutive `{Integers Z} Z2 `{Integers Z2} x :
integers_to_ring Z2 Z (integers_to_ring Z Z2 x) = x.
Proof.
rapply (proj2 (@categories.initials_unique' _ _ _ _ _ _ (rings.object Z) (rings.object Z2) _
integers_initial _ integers_initial) tt x).
Qed.
Lemma to_ring_unique `{Integers Z} `{Ring R} (f: Z → R) {h: SemiRing_Morphism f} x :
f x = integers_to_ring Z R x.
Proof.
symmetry.
pose proof (rings.encode_morphism_and_ops (f:=f)).
set (@varieties.arrow rings.theory _ _ _ (rings.encode_variety_and_ops _) _ _ _ (rings.encode_variety_and_ops _) (λ _, f) _).
exact (integers_initial _ a tt x).
Qed.
Lemma to_ring_unique_alt `{Integers Z} `{Ring R} (f g: Z → R) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x :
f x = g x.
Proof. now rewrite (to_ring_unique f), (to_ring_unique g). Qed.
Lemma morphisms_involutive `{Integers Z} `{Integers Z2} (f: Z → Z2) (g: Z2 → Z)
`{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x : f (g x) = x.
Proof. now apply (to_ring_unique_alt (f ∘ g) id). Qed.
Lemma to_ring_twice `{Integers Z} `{Ring R1} `{Ring R2} (f : R1 → R2) (g : Z → R1) (h : Z → R2)
`{!SemiRing_Morphism f} `{!SemiRing_Morphism g} `{!SemiRing_Morphism h} x :
f (g x) = h x.
Proof. now apply (to_ring_unique_alt (f ∘ g) h). Qed.
Lemma to_ring_self `{Integers Z} (f : Z → Z) `{!SemiRing_Morphism f} x : f x = x.
Proof. now apply (to_ring_unique_alt f id). Qed.
(* A ring morphism from integers to another ring is injective if there's an injection in the other direction: *)
Lemma to_ring_injective `{Integers Z} `{Ring R} (f: R → Z) (g: Z → R) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} :
Injective g.
Proof.
repeat (split; try apply _). intros x y E.
rewrite <-(to_ring_self (f ∘ g) x), <-(to_ring_self (f ∘ g) y).
unfold compose. now rewrite E.
Qed.
#[global]
Instance integers_to_integers_injective `{Integers Z} `{Integers Z2} (f: Z → Z2) `{!SemiRing_Morphism f} :
Injective f.
Proof. apply (to_ring_injective (integers_to_ring Z2 Z) _). Qed.
#[global]
Instance naturals_to_integers_injective `{Integers Z} `{Naturals N} (f: N → Z) `{!SemiRing_Morphism f} :
Injective f.
Proof.
split; try apply _. intros x y E.
apply (injective (cast N (SRpair N))).
now rewrite <-2!(naturals.to_semiring_twice (integers_to_ring Z (SRpair N)) f (cast N (SRpair N))), E.
Qed.
Section retract_is_int.
Context `{Integers Z} `{Ring Z2}.
Context (f : Z → Z2) `{!Inverse f} `{!Surjective f} `{!SemiRing_Morphism f} `{!SemiRing_Morphism (f⁻¹)}.
(* If we make this an instance, then instance resolution will often loop *)
Definition retract_is_int_to_ring : IntegersToRing Z2 := λ Z2 _ _ _ _ _, integers_to_ring Z Z2 ∘ f⁻¹.
Section for_another_ring.
Context `{Ring R}.
Instance: SemiRing_Morphism (integers_to_ring Z R ∘ f⁻¹) := {}.
Context (h : Z2 → R) `{!SemiRing_Morphism h}.
Lemma same_morphism: integers_to_ring Z R ∘ f⁻¹ = h.
Proof with auto.
intros x y F. rewrite <-F.
transitivity ((h ∘ (f ∘ f⁻¹)) x).
symmetry. unfold compose. apply (to_ring_unique (h ∘ f)).
unfold compose. now rewrite jections.surjective_applied.
Qed.
End for_another_ring.
(* If we make this an instance, then instance resolution will often loop *)
Program Instance retract_is_int: Integers Z2 (U:=retract_is_int_to_ring).
Next Obligation. unfold integers_to_ring, retract_is_int_to_ring. apply _. Qed.
Next Obligation. apply integer_initial. intros. now apply same_morphism. Qed.
End retract_is_int.
Section contents.
Context `{Integers Z}.
Global Program Instance: ∀ x y: Z, Decision (x = y) | 10 := λ x y,
match decide (integers_to_ring Z (SRpair nat) x = integers_to_ring Z (SRpair nat) y) with
| left E => left _
| right E => right _
end.
Next Obligation. now apply (injective (integers_to_ring Z (SRpair nat))). Qed.
Global Program Instance slow_int_abs `{Naturals N} : IntAbs Z N | 10 := λ x,
match int_abs_sig (SRpair N) N (integers_to_ring Z (SRpair N) x) with
| inl (n↾E) => inl n
| inr (n↾E) => inr n
end.
Next Obligation.
apply (injective (integers_to_ring Z (SRpair N))).
rewrite <-E. apply (naturals.to_semiring_twice _ _ _).
Qed.
Next Obligation.
apply (injective (integers_to_ring Z (SRpair N))).
rewrite rings.preserves_negate, <-E.
now apply (naturals.to_semiring_twice _ _ _).
Qed.
Instance: PropHolds ((1:Z) ≠ 0).
Proof.
intros E.
apply (rings.is_ne_0 1).
apply (injective (naturals_to_semiring nat Z)).
now rewrite rings.preserves_0, rings.preserves_1.
Qed.
Global Instance: ZeroProduct Z.
Proof.
intros x y E.
destruct (zero_product (integers_to_ring Z (SRpair nat) x) (integers_to_ring Z (SRpair nat) y)).
now rewrite <-rings.preserves_mult, E, rings.preserves_0.
left. apply (injective (integers_to_ring Z (SRpair nat))). now rewrite rings.preserves_0.
right. apply (injective (integers_to_ring Z (SRpair nat))). now rewrite rings.preserves_0.
Qed.
Global Instance: IntegralDomain Z := {}.
End contents.
|
