# Zulip Chat Archive

## Stream: new members

### Topic: Denoting element of a group

#### James Arthur (Aug 09 2020 at 17:05):

I'm trying to set up a magma with the following axioms, its called a gyrovectorspace:

- In G there is at least one element e called a left identity with e * a = a for all a ∈ G.
- For each a ∈ G there is an element a⁻¹ in G called a left inverse of a with a⁻¹ * a = e.
- For any a, b, c in G there exists a unique element $gyr[a, b]c$ in G such that the binary operation obeys the left gyroassociative law: $a{\displaystyle \oplus }\oplus (b{\displaystyle \oplus }\oplus c) = (a{\displaystyle \oplus }\oplus b){\displaystyle \oplus }\oplus gyr[a, b]c$
- The map $gyr[a, b]:G → G$ given by $c → gyr[a, b]c$ is an automorphism of the groupoid $(G, {\displaystyle \oplus }\oplus )$. That is $gyr[a, b]$ is a member of $Aut(G, {\displaystyle \oplus }\oplus )$ and the automorphism $gyr[a, b]$ of G is called the gyroautomorphism of G generated by a, b in G. The operation $gyr:G × G → Aut(G, {\displaystyle \oplus }\oplus )$ is called the gyrator of G.
- The gyroautomorphism $gyr[a, b]$ has the left loop property $gyr[a, b] = gyr[a{\displaystyle \oplus }\oplus b, b]$.

The first pair of axioms are like the group axioms. The last pair present the gyrator axioms and the middle axiom links the two pairs. I have got thus far with some help, but I have come stuck with defining that $gyr(a, b) \in Aut((G, \oplus))$. Here is my code this far:

```
import data.real.basic category_theory.endomorphism
open category_theory
class gyrogroup (G : Type) extends has_add G, has_neg G, has_zero G :=
-- axiom 1: 0 ⊕ a = a
(zero_add : ∀ (a : G), 0 + a = a)
-- axiom 2: ⊖a⊕a = 0
(add_left_neg : ∀ (a : G), -a + a = 0)
(gyr : G → G → G → G) -- gyr a b c is gyr[a, b]c in the notation from the Wiki
-- axiom 3: ∀ a b c ∈ G, a + (b + c) = (a + b) + gyr a b c
(add_gyr_assoc : ∀ a b c, a + (b + c) = (a + b) + gyr a b c)
(add_gyr_assoc' : ∀ a b c d, a + (b + c) = (a + b) + d → d = gyr a b c) -- uniqueness
-- axiom 4: gyr a b ∈ Aut(G, ⊕)
-- (gyr_autom : ∀ (a:G) (b:G), gyr a b ∈ Aut G) <- This line is the problem, more specifically the $$ \in $$
-- axiom 5: gyr a b = gyr (a + b) b
(gyr_loop : ∀ a b, gyr a b = gyr (a + b) b)
```

Heres the error

```
failed to synthesize type class instance for
G : Type,
to_has_add : has_add G,
to_has_neg : has_neg G,
to_has_zero : has_zero G,
add : (λ {α : Type} (c : has_add α), α → α → α) to_has_add := has_add.add,
neg : (λ {α : Type} (c : has_neg α), α → α) to_has_neg := has_neg.neg,
zero : (λ {α : Type} (c : has_zero α), α) to_has_zero := 0,
zero_add : ∀ (a : G), 0 + a = a,
add_left_neg : ∀ (a : G), -a + a = 0,
gyr : G → G → G → G,
add_gyr_assoc : ∀ (a b c : G), a + (b + c) = a + b + gyr a b c,
add_gyr_assoc' : ∀ (a b c d : G), a + (b + c) = a + b + d → d = gyr a b c,
a b : G
⊢ has_mem (G → G) Type
```

Is this a quirk of lean or just me being stupid and overlooking a detail?

#### Yury G. Kudryashov (Aug 09 2020 at 17:39):

You should state separate axioms `gyr a b 0 = 0`

and `gyr a b (c + d) = gyr a b c + gyr a b d`

#### Yury G. Kudryashov (Aug 09 2020 at 17:39):

`Aut`

is not a set.

#### Mario Carneiro (Aug 09 2020 at 17:46):

Alternatively, you could have `gyr`

be a function into the automorphism group if you want to more closely match the wiki version. But I think Yury's suggestion is better

#### James Arthur (Aug 09 2020 at 17:47):

So, Yurys suggestion is just the same as having a function into the automorphism group?

#### Mario Carneiro (Aug 09 2020 at 17:48):

You would construct the actual function after the fact, using Yury's axioms

#### Mario Carneiro (Aug 09 2020 at 17:48):

you would get `gyr' : G -> G -> Aut G`

#### Mario Carneiro (Aug 09 2020 at 17:48):

or something like that

#### Mario Carneiro (Aug 09 2020 at 17:49):

such that `\u (gyr' a b) c = gyr a b c`

#### Mario Carneiro (Aug 09 2020 at 17:50):

My alternative is suggesting putting `gyr'`

in the structure, and then not having the function `gyr`

at all except via the coercion

#### James Arthur (Aug 09 2020 at 17:52):

State seperate, sorry I misread that. So I want to just do something like this?

```
import data.real.basic category_theory.endomorphism
open category_theory
class gyrogroup (G : Type) extends has_add G, has_neg G, has_zero G :=
-- axiom 1: 0 ⊕ a = a
(zero_add : ∀ (a : G), 0 + a = a)
-- axiom 2: ⊖a⊕a = 0
(add_left_neg : ∀ (a : G), -a + a = 0)
(gyr : G → G → G → G) -- gyr a b c is gyr[a, b]c in the notation from the Wiki
-- axiom 3: ∀ a b c ∈ G, a + (b + c) = (a + b) + gyr a b c
(add_gyr_assoc : ∀ a b c, a + (b + c) = (a + b) + gyr a b c)
(add_gyr_assoc' : ∀ a b c d, a + (b + c) = (a + b) + d → d = gyr a b c) -- uniqueness
-- axiom 4: gyr a b ∈ Aut(G, ⊕)
(gyr_zero (a b : G) : gyr a b 0 = 0)
(gyr_distrib (a b c d : G) : gyr a b (c + d) = gyr a b c + gyr a b d)
--(gyr_autom : ∀ (a:G) (b:G), gyr a b ∈ Aut G)
-- axiom 5: gyr a b = gyr (a + b) b
(gyr_loop : ∀ a b, gyr a b = gyr (a + b) b)
variables (G : Type) [gyrogroup G]
variables (a b c : G)
def gyr := G -> G -> Aut G
lemma gyr_zero (a b : G): gyr a b 0 = 0 :=
begin
sorry
end
```

Last updated: May 13 2021 at 17:42 UTC