varieties.rings

Require
categories.varieties theory.rings.
Require Import
Ring
abstract_algebra universal_algebra ua_homomorphisms workaround_tactics.

Inductive op := plus | mult | zero | one | opp.

Definition sig: Signature := single_sorted_signature
(λ o, match o with zero | one => O | opp => 1%nat | plus | mult => 2%nat end).

Section laws.
Global Instance: RingPlus (Term0 sig nat tt) :=
λ x, App sig _ _ _ (App sig _ _ _ (Op sig _ plus) x).
Global Instance: RingMult (Term0 sig nat tt) :=
λ x, App sig _ _ _ (App sig _ _ _ (Op sig _ mult) x).
Global Instance: RingZero (Term0 sig nat tt) := Op sig _ zero.
Global Instance: RingOne (Term0 sig nat tt) := Op sig _ one.
Global Instance: GroupInv (Term0 sig nat tt) := App sig _ _ _ (Op sig _ opp).

Local Notation x := (Var sig nat 0%nat tt).
Local Notation y := (Var sig nat 1%nat tt).
Local Notation z := (Var sig nat 2%nat tt).

Import notations.

Inductive Laws: EqEntailment sig Prop :=
|e_plus_assoc: Laws (x + (y + z) === (x + y) + z)
|e_plus_comm: Laws (x + y === y + x)
|e_plus_0_l: Laws (0 + x === x)
|e_mult_assoc: Laws (x * (y * z) === (x * y) * z)
|e_mult_comm: Laws (x * y === y * x)
|e_mult_1_l: Laws (1 * x === x)
|e_mult_0_l: Laws (0 * x === 0)
|e_distr: Laws (x * (y + z) === x * y + x * z)
|e_distr_l: Laws ((x + y) * z === x * z + y * z)
|e_plus_opp_r: Laws (x + - x === 0)
|e_plus_opp_l: Laws (- x + x === 0).
End laws.

Definition theory: EquationalTheory := Build_EquationalTheory sig Laws.
Definition Object := varieties.Object theory.

Section decode_operations.
Context `{AlgebraOps theory A}.
Global Instance: RingPlus (A tt) := algebra_op plus.
Global Instance: RingMult (A tt) := algebra_op mult.
Global Instance: RingZero (A tt) := algebra_op zero.
Global Instance: RingOne (A tt) := algebra_op one.
Global Instance: GroupInv (A tt) := algebra_op opp.
End decode_operations.

Section encode_with_ops.
Context A `{Ring A}.

Global Instance encode_operations: AlgebraOps sig (λ _, A) := λ o,
match o with plus => (+) | mult => (.*.) | zero => 0:A | one => 1:A | opp => (-) end.

Global Instance encode_algebra_and_ops: Algebra sig _.

Global Instance encode_variety_and_ops: InVariety theory (λ _, A).

Definition object: Object := varieties.object theory (λ _, A).
End encode_with_ops.

Lemma encode_algebra_only `{!AlgebraOps theory A} `{ u, Equiv (A u)} `{!Ring (A tt)}: Algebra sig A .

Instance decode_variety_and_ops `{InVariety theory A}: Ring (A tt).

Lemma encode_morphism_only
`{AlgebraOps theory A} `{ u, Equiv (A u)}
`{AlgebraOps theory B} `{ u, Equiv (B u)}
(f: u, A u B u) `{!Ring (A tt)} `{!Ring (B tt)} `{!SemiRing_Morphism (f tt)}: HomoMorphism sig A B f.

Lemma encode_morphism_and_ops `{Ring A} `{Ring B} {f : A B} `{!SemiRing_Morphism f}:
@HomoMorphism sig (λ _, A) (λ _, B) _ _ _ _ (λ _, f).

Lemma decode_morphism_and_ops
`{InVariety theory x} `{InVariety theory y} `{!HomoMorphism theory x y f}:
SemiRing_Morphism (f tt).