~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Action.v -rw-r--r-- 1.3 KiB View raw
5857f238Andrew Miloradovsky .build.yml: continuous integration for SourceHut 7 months ago
                                                                                
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
Require Import Algebra.

Section Action.

  Let is_identity_map {X: Type} (f: X -> X) := forall x: X, f x = x.
  Let swap {X Y Z: Type} (f: X -> Y -> Z) := fun x y => f y x.
  Let Fixpoint power {X: Type} (f: X -> X) (n: nat) :=
    match n with O => (fun x => x)
            | S k => (fun x => f (power f k x)) end.

  Variables T S: Type.  (* T -- time, S -- space *)
  Variables (op: T -> T -> T) (neutral: T) (inverse: T -> T).
  Variables (left_action: T -> S -> S) (right_action: S -> T -> S).

  Hypothesis T_is_a_monoid: is_a_monoid T op neutral.

  (* associativity / transitivity *)
  Definition is_left_compatible := forall (g h: T) (x: S),
      left_action (op g h) x = left_action g (left_action h x).
  Definition is_right_compatible := forall (g h: T) (x: S),
      right_action x (op g h) = right_action (right_action x g) h.
  (* identity / reflexivity *)
  Definition is_left_identity :=
    is_identity_map (left_action neutral).
  Definition is_right_identity :=
    is_identity_map (swap right_action neutral).
  (* inverse / symmetry *)
  (* TODO: if T is a group, it is mapped to auto-morphisms *)

  Definition is_left_action :=
    is_left_compatible /\ is_left_identity.
  Definition is_right_action :=
    is_right_compatible /\ is_right_identity.

  Variable f g: S -> S.  (* an endo-functions *)

End Action.