symbolic-dynamics/Action.v -rw-r--r-- 1.3 KiB
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.
```