Denoting element of a group

Stream: new members

[James Arthur]

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{\displaystyle \oplus }\oplus (b{\displaystyle \oplus }\oplus c) = (a{\displaystyle \oplus }\oplus b){\displaystyle \oplus }\oplus gyr[a, b]c$
4. 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.
5. 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]

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]

Aut is not a set.

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

or something like that

[Mario Carneiro]

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

[Mario Carneiro]

My alternative is suggesting putting gyr' in the structure, and then not having the function gyr at all except via the coercion

[James Arthur]

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