interfaces.abstract_algebra

Require
 Equivalence.
Require Export
 Morphisms Setoid Program
 canonical_names util workarounds setoid_tactics.


Class Setoid A {e: Equiv A} : Prop := setoid_eq:> Equivalence (@equiv A e).

Class StrongSetoid A {e: Equiv A} `{ap : Apart A} : Prop :=
  { strong_setoid_irreflexive :> Irreflexive (⪥)
  ; strong_setoid_symmetric :> Symmetric (⪥)
  ; strong_setoid_cotrans :> CoTransitive (⪥)
  ; tight_apart : x y, ¬x y x = y }.

Section setoid_morphisms.
  Context {A B : Type} {Ae: Equiv A} {Aap: Apart A} {Be: Equiv B} {Bap : Apart B} (f: A B).

  Class Setoid_Morphism :=
    { setoidmor_a: Setoid A
    ; setoidmor_b: Setoid B
    ; sm_proper:> Proper ((=) ==> (=)) f }.

  Class StrongSetoid_Morphism :=
    { strong_setoidmor_a: StrongSetoid A
    ; strong_setoidmor_b: StrongSetoid B
    ; strong_extensionality : x y, f x f y x y }.
End setoid_morphisms.

Implicit Arguments sm_proper [[A] [B] [Ae] [Be] [f] [Setoid_Morphism]].

Section setoid_binary_morphisms.
  Context {A B C : Type} {Ae: Equiv A} {Aap: Apart A}
    {Be: Equiv B} {Bap : Apart B} {Ce: Equiv C} {Cap : Apart C} (f: A B C).

  Class StrongSetoid_BinaryMorphism :=
    { strong_binary_setoidmor_a: StrongSetoid A
    ; strong_binary_setoidmor_b: StrongSetoid B
    ; strong_binary_setoidmor_c: StrongSetoid C
    ; strong_binary_extensionality : x₁ y₁ x₂ y₂, f x₁ y₁ f x₂ y₂ x₁ x₂ y₁ y₂ }.
End setoid_binary_morphisms.

Section upper_classes.
  Context A {e: Equiv A}.

  Class SemiGroup {op: SemiGroupOp A}: Prop :=
    { sg_setoid:> Setoid A
    ; sg_ass:> Associative (&)
    ; sg_op_proper:> Proper ((=) ==> (=) ==> (=)) (&) }.

  Class Monoid {op: SemiGroupOp A} {unit: MonoidUnit A}: Prop :=
    { monoid_semigroup:> SemiGroup
    ; monoid_left_id:> LeftIdentity (&) mon_unit
    ; monoid_right_id:> RightIdentity (&) mon_unit }.

  Class CommutativeMonoid {op unit}: Prop :=
    { commonoid_mon:> @Monoid op unit
    ; commonoid_commutative:> Commutative (&) }.

  Class Group {op unit} {inv: GroupInv A}: Prop :=
    { group_monoid:> @Monoid op unit
    ; inv_proper:> Setoid_Morphism (-)
    ; ginv_l:> LeftInverse (&) (-) mon_unit
    ; ginv_r:> RightInverse (&) (-) mon_unit }.

  Class AbGroup {op unit inv}: Prop :=
    { abgroup_group:> @Group op unit inv
    ; abgroup_commutative:> Commutative (&) }.

  Context {plus: RingPlus A} {mult: RingMult A} {zero: RingZero A} {one: RingOne A}.

  Class SemiRing: Prop :=
    { semiring_mult_monoid:> @CommutativeMonoid ringmult_is_semigroupop ringone_is_monoidunit
    ; semiring_plus_monoid:> @CommutativeMonoid ringplus_is_semigroupop ringzero_is_monoidunit
    ; semiring_distr:> Distribute (.*.) (+)
    ; semiring_left_absorb:> LeftAbsorb (.*.) 0 }.

  Context {inv: GroupInv A}.

  Class Ring: Prop :=
    { ring_group:> @AbGroup ringplus_is_semigroupop ringzero_is_monoidunit _
    ; ring_monoid:> @CommutativeMonoid ringmult_is_semigroupop ringone_is_monoidunit
    ; ring_dist:> Distribute (.*.) (+) }.


  Class IntegralDomain: Prop :=
    { intdom_ring: Ring
    ; intdom_nontrivial: PropHolds (1 0)
    ; intdom_nozeroes:> NoZeroDivisors A }.

  Class Field {ap: Apart A} {mult_inv: MultInv A} : Prop :=
    { field_ring:> Ring
    ; field_strongsetoid:> StrongSetoid A
    ; field_plus_ext:> StrongSetoid_BinaryMorphism (+)
    ; field_mult_ext:> StrongSetoid_BinaryMorphism (.*.)
    ; field_nontrivial: PropHolds (1 0)
    ; mult_inv_proper:> Setoid_Morphism (//)
    ; mult_inverse: x, `x // x = 1 }.

  Class DecField {dec_mult_inv: DecMultInv A}: Prop :=
    { decfield_ring:> Ring
    ; decfield_nontrivial: PropHolds (1 0)
    ; dec_mult_inv_proper:> Setoid_Morphism (/)
    ; dec_mult_inv_0: /0 = 0
    ; dec_mult_inverse: x, x 0 x / x = 1 }.
End upper_classes.

Hint Extern 4 (PropHolds (1 0)) => eapply @intdom_nontrivial : typeclass_instances.
Hint Extern 5 (PropHolds (1 0)) => eapply @field_nontrivial : typeclass_instances.
Hint Extern 5 (PropHolds (1 0)) => eapply @decfield_nontrivial : typeclass_instances.

Hint Extern 10 (Ring _) => apply @intdom_ring : typeclass_instances.

Implicit Arguments tight_apart [[A] [e] [ap] [StrongSetoid]].
Implicit Arguments mult_inverse [[A] [e] [plus] [mult] [zero] [one] [inv] [ap] [mult_inv0] [Field]].
Implicit Arguments dec_mult_inverse [[A] [e] [plus] [mult] [zero] [one] [inv] [dec_mult_inv0] [DecField]].
Implicit Arguments dec_mult_inv_0 [[A] [e] [plus] [mult] [zero] [one] [inv] [dec_mult_inv0] [DecField]].
Implicit Arguments sg_op_proper [[A] [e] [op] [SemiGroup]].

Section cancellation.
  Context `{e : Equiv A} `{ap : Apart A} (op : A A A) (z : A).

  Class LeftCancellation := left_cancellation : `(op z x = op z y x = y).
  Class RightCancellation := right_cancellation : `(op x z = op y z x = y).

  Class StrongLeftCancellation := strong_left_cancellation : `(x y op z x op z y).
  Class StrongRightCancellation := strong_right_cancellation : `(x y op x z op y z).
End cancellation.

Class Category O `{!Arrows O} `{ x y: O, Equiv (x y)} `{!CatId O} `{!CatComp O}: Prop :=
  { arrow_equiv:> x y, Setoid (x y)
  ; comp_proper:> x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z)
  ; comp_assoc :> ArrowsAssociative O
  ; id_l :> `(LeftIdentity (comp x y y) cat_id)
  ; id_r :> `(RightIdentity (comp x x y) cat_id) }.


Implicit Arguments comp_assoc [[O] [Arrows0] [H] [CatId0] [CatComp0] [Category] [w] [x] [y] [z]].

Section morphism_classes.
  Context {A B : Type} {Ae: Equiv A} {Be: Equiv B}.

  Class SemiGroup_Morphism {Aop Bop} (f: A B) :=
    { sgmor_a: @SemiGroup A Ae Aop
    ; sgmor_b: @SemiGroup B Be Bop
    ; sgmor_setmor:> Setoid_Morphism f
    ; preserves_sg_op: `(f (a & a') = f a & f a') }.

  Class Monoid_Morphism {Aunit Bunit Amult Bmult} (f: A B) :=
    { monmor_a: @Monoid A Ae Amult Aunit
    ; monmor_b: @Monoid B Be Bmult Bunit
    ; monmor_sgmor:> SemiGroup_Morphism f
    ; preserves_mon_unit: f mon_unit = mon_unit }.

  Class SemiRing_Morphism {Aplus Amult Azero Aone Bplus Bmult Bzero Bone} (f: A B) :=
    { semiringmor_a: @SemiRing A Ae Aplus Amult Azero Aone
    ; semiringmor_b: @SemiRing B Be Bplus Bmult Bzero Bone
    ; semiringmor_plus_mor:> @Monoid_Morphism ringzero_is_monoidunit ringzero_is_monoidunit
            ringplus_is_semigroupop ringplus_is_semigroupop f
    ; semiringmor_mult_mor:> @Monoid_Morphism ringone_is_monoidunit ringone_is_monoidunit
            ringmult_is_semigroupop ringmult_is_semigroupop f }.

  Context {Aap: Apart A} {Bap: Apart B}.
  Class StrongSemiRing_Morphism {Aplus Amult Azero Aone Bplus Bmult Bzero Bone} (f: A B) :=
    { strong_semiringmor_sr_mor:> @SemiRing_Morphism Aplus Amult Azero Aone Bplus Bmult Bzero Bone f
    ; strong_semiringmor_strong_mor:> StrongSetoid_Morphism f }.
End morphism_classes.

Implicit Arguments monmor_a [[A] [B] [Ae] [Be] [Aunit] [Bunit] [Amult] [Bmult] [Monoid_Morphism]].
Implicit Arguments monmor_b [[A] [B] [Ae] [Be] [Aunit] [Bunit] [Amult] [Bmult] [Monoid_Morphism]].


Section jections.
  Context {A B : Type} {Ae: Equiv A} {Aap: Apart A}
    {Be: Equiv B} {Bap : Apart B} (f: A B) `{inv: !Inverse f}.

  Class StrongInjective: Prop :=
    { strong_injective: x y, x y f x f y
    ; strong_injective_mor: StrongSetoid_Morphism f }.

  Class Injective: Prop :=
    { injective: x y, f x = f y x = y
    ; injective_mor: Setoid_Morphism f }.

  Class Surjective: Prop :=
    { surjective: f (f ⁻¹) = id
    ; surjective_mor: Setoid_Morphism f }.

  Class Bijective: Prop :=
    { bijective_injective:> Injective
    ; bijective_surjective:> Surjective }.
End jections.