theory.ua_homomorphisms

Require Import
  abstract_algebra universal_algebra.

Section contents.
  Variable : Signature.

  Typeclasses Transparent Equiv.
  Notation OpType := (OpType (sorts )).

  Section homo.

  Context (A B: sorts Type)
    `{A_equiv : a, Equiv (A a)} `{B_equiv : a, Equiv (B a)}
    `{A_ops : AlgebraOps A} `{B_ops : AlgebraOps B}.

  Section with_f.
    Context (f : a, A a B a).

    Implicit Arguments f [[a]].

    Fixpoint Preservation {n : OpType}: op_type A n op_type B n Prop :=
      match n with
      | ne_list.one d => λ oA oB, f oA = oB
      | ne_list.cons x y => λ oA oB, x, Preservation (oA x) (oB (f x))
      end.

    Class HomoMorphism: Prop :=
      { homo_proper:> a, Setoid_Morphism (@f a)
      ; preserves: (o: ), Preservation (A_ops o) (B_ops o)
      ; homo_source_algebra: Algebra A
      ; homo_target_algebra: Algebra B }.

    Context `{ a, Setoid (A a)} `{ b, Setoid (B b)} `{ a, Setoid_Morphism (@f a)}.

    Global Instance Preservation_proper n:
      Proper (op_type_equiv _ _ _ ==> op_type_equiv _ B n ==> iff) (@Preservation n).

    Global Instance Preservation_proper'' n:
      Proper (eq ==> (=) ==> iff) (@Preservation n).

  End with_f.

  Lemma Preservation_proper' (f g: a, A a B a)
   `{ a, Setoid (A a)} `{ b, Setoid (B b)} `{ a, Setoid_Morphism (@f a)}:
    ( a (x: A a), f a x = g a x) (n: OpType) x y, Proper (=) x Proper (=) y
      @Preservation f n x y
      @Preservation g n x y.

    Lemma HomoMorphism_Proper: Proper ((λ f g, a x, f a x = g a x) ==> iff) HomoMorphism.

  End homo.

  Global Instance id_homomorphism A
    `{ a, Equiv (A a)} {ao: AlgebraOps A} `{!Algebra A}: HomoMorphism _ _ (λ _, id).

  Global Instance compose_homomorphisms A B C f g
    `{ a, Equiv (A a)} `{ a, Equiv (B a)} `{ a, Equiv (C a)}
    {ao: AlgebraOps A} {bo: AlgebraOps B} {co: AlgebraOps C}
    {gh: HomoMorphism A B g} {fh: HomoMorphism B C f}: HomoMorphism A C (λ a, f a g a).

  Lemma invert_homomorphism A B f
    `{ a, Equiv (A a)} `{ a, Equiv (B a)}
    {ao: AlgebraOps A} {bo: AlgebraOps B}
    {fh: HomoMorphism A B f}
    `{inv: a, Inverse (f a)}:
    ( a, Bijective (f a))
    HomoMorphism A B f HomoMorphism B A inv.


End contents.