Zulip Chat Archive

Stream: new members

Topic: Denoting element of a group


view this post on Zulip 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]cgyr[a, b]c in G such that the binary operation obeys the left gyroassociative law: a(bc)=(ab)gyr[a,b]ca{\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]:GGgyr[a, b]:G → G given by cgyr[a,b]cc → gyr[a, b]c is an automorphism of the groupoid (G,)(G, {\displaystyle \oplus }\oplus ). That is gyr[a,b]gyr[a, b] is a member of Aut(G,)Aut(G, {\displaystyle \oplus }\oplus ) and the automorphism gyr[a,b]gyr[a, b] of G is called the gyroautomorphism of G generated by a, b in G. The operation gyr:G×GAut(G,)gyr:G × G → Aut(G, {\displaystyle \oplus }\oplus ) is called the gyrator of G.
  5. The gyroautomorphism gyr[a,b]gyr[a, b] has the left loop property gyr[a,b]=gyr[ab,b]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)Aut((G,)) 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?

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Aug 09 2020 at 17:39):

Aut is not a set.

view this post on Zulip 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

view this post on Zulip James Arthur (Aug 09 2020 at 17:47):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 17:48):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 17:48):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 17:48):

or something like that

view this post on Zulip Mario Carneiro (Aug 09 2020 at 17:49):

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

view this post on Zulip 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

view this post on Zulip 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