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
|
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories
MathClasses.categories.varieties.
Require
MathClasses.varieties.rings.
Section initial_maps.
Variable A : Type.
Class IntegersToRing :=
integers_to_ring: ∀ R `{Mult R} `{Plus R} `{One R} `{Zero R} `{Negate R}, A → R.
Context `{IntegersToRing} `{Ring A} `{∀ `{Ring B}, SemiRing_Morphism (integers_to_ring B)}.
Global Instance integer_initial_arrow: InitialArrow (rings.object A).
intro y.
exists (λ u, match u return A → y u with tt => integers_to_ring (y tt) end).
abstract (apply rings.encode_morphism_only; apply _).
Defined. (* for some reason [Program] isn't cooperating here. look into it *)
Lemma integer_initial (same_morphism : ∀ `{Ring B} {h : A → B} `{!SemiRing_Morphism h}, integers_to_ring B = h) :
Initial (rings.object A).
Proof.
intros y [x h] [] ?. simpl in *.
apply same_morphism.
apply rings.decode_variety_and_ops.
apply (@rings.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h).
reflexivity.
Qed.
End initial_maps.
#[global]
Instance: Params (@integers_to_ring) 8 := {}.
Class Integers A {e plus mult zero one negate} `{U : IntegersToRing A} :=
{ integers_ring:: @Ring A e plus mult zero one negate
; integers_to_ring_mor:: ∀ `{Ring B}, SemiRing_Morphism (integers_to_ring A B)
; integers_initial:: Initial (rings.object A) }.
Section specializable.
Context (Z N : Type) `{Integers Z} `{Naturals N}.
Class IntAbs := int_abs_sig : ∀ x,
{ n : N | naturals_to_semiring N Z n = x } + { n : N | naturals_to_semiring N Z n = -x }.
Definition int_abs `{ia : IntAbs} (x : Z) : N :=
match int_abs_sig x with
| inl (n↾_) => n
| inr (n↾_) => n
end.
Definition int_to_nat `{Zero N} `{ia : IntAbs} (x : Z) : N :=
match int_abs_sig x with
| inl (n↾_) => n
| inr (n↾_) => 0
end.
End specializable.
#[global]
Instance: Params (@int_abs) 10 := {}.
#[global]
Instance: Params (@int_abs_sig) 10 := {}.
#[global]
Instance: Params (@int_to_nat) 11 := {}.
|
