## 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:

1. In G there is at least one element e called a left identity with e * a = a for all a ∈ G.
2. For each a ∈ G there is an element a⁻¹ in G called a left inverse of a with a⁻¹ * a = e.
3. 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\oplus }\oplus (b\oplus }\oplus c) = (a\oplus }\oplus b)\oplus }\oplus gyr[a, b]$
4. The map $gyr[a, b]:G → G$ given by $c → gyr[a, b]c$ is an automorphism of the groupoid $(G, \oplus }\oplus$. That is $gyr[a, b]$ is a member of $Aut(G, \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, \oplus }\oplus$ is called the gyrator of G.
5. The gyroautomorphism $gyr[a, b]$ has the left loop property $gyr[a, b] = gyr[a\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_neg : has_neg G,
to_has_zero : has_zero G,
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