Defining Group Structure question

Stream: new members

[Luna]

Hey all. I've been working my way through MIL and got to section 7. I wanted to try creating my own algebraic hierarchy just to experiment with how different definitions play with the class instances.

I tried the following but immediately ran into a problem:

structure Group (α : Type _) (op : α → α → α) where
    has_ident : ∃ (ident : α), op ident a = a
    has_inv : ∀ (a : α), ∃ (a_inv : α), (op a a_inv = has_ident.1)  -- note *.1 is the only notation that I know to get access to the first term
    op_assoc : ∀ (a b c : α), op a (op b c) = op (op a b) c

Lean reports the error:

invalid projection, the expression
  has_ident
is a proposition and has type
  ∃ ident, op ident ?m.40 = ?m.40
but the projected value is not, it has type
  α

The goal is to extract the term ident from has_ident and use it to define the has_inv prop. Is this possible within Lean? I know that theident term cannot be extracted and used outside of a Prop type (because of proof irrelevance) but I didn't think it would be a problem here.

Note : I would like to avoid adding an ident field or parameterizing Group with ident since it should ideally be inferred by the operation op.

[Eric Wieser]

I recommend you add set_option autoImplicit false, and fix the resulting error

[Eric Wieser]

I don't think you're quantifying over a correctly in has_ident

[Luna]

I added set_option autoImplicit false and below is the full .lean file.

section

    set_option autoImplicit false

    structure Group (α : Type _) (op : α → α → α) where
        has_ident : ∃ (ident : α), ∀ (a : α), op ident a = a
        has_inv : ∀ (a : α), ∃ (a_inv : α), (op a a_inv = has_ident.1)   -- <<< error is here
        op_assoc : ∀ (a b c : α), op a (op b c) = op (op a b) c

end

I'm still getting (almost) the same error, though I don't know why the meta-variables are no longer in the error message:

invalid projection, the expression
  has_ident
is a proposition and has type
  ∃ ident, ∀ (a : α), op ident a = a
but the projected value is not, it has type
  α

[Luna]

I double checked and I get the same error message whether or not set_option autoImplicit false is present or not. I don't know why the error message previously showed meta-variables

[Kevin Buzzard]

Mathematically you can't do this because at this point there could be several idents which work.

[Kevin Buzzard]

This is a not uncommon error in the literature (asserting existence of an identity in the identity axiom and then implicitly assuming its uniqueness in the inverse axiom). In mathlib we avoid this by making ident data. Another attempt to justify the bad approach is to prove that identities are unique later and say that the definition now makes sense so it was ok all along but this is circular.

[Kevin Buzzard]

The error says exactly what you know, that you can't turn a prop into data. You could use the type theory axiom of choice to get around it and then ultimately prove that ident is unique, but it will make the theory much harder to set up.

[Kevin Buzzard]

You're better off setting it up mathlib's way in the definition, proving that identities are unique and then making a new constructor for groups which eats a multiplication and a proof that there's an e satisfying both the identity and inverse axioms and spits out a group

[Alex Mobius]

Here's an approach that avoids data and choice axioms, but is more cumbersome:

import Mathlib.Logic.ExistsUnique

def IsIdent {α: Type _} (op: α → α → α) (ident: α) := ∀ a: α, op ident a = a

structure Group (α : Type _) (op : α → α → α) where
    has_ident : ∃! (ident : α), IsIdent op ident
    has_inv : ∀ (a : α), ∃ (a_inv : α), IsIdent op $ op a a_inv
    op_assoc : ∀ (a b c : α), op a (op b c) = op (op a b) c

To my understanding, you either need to assert uniqueness, OR you need to define your identity as being both left and right. https://math.stackexchange.com/questions/537572/any-set-with-associativity-left-identity-left-inverse-is-a-group gives a third construction, for which you define an inverse for each possible left identity. If you don't do one of those, then fun _ y => y satisfies all the axioms, with all elements being the identity :)

[Ruben Van de Velde]

But then you need choice to write 1

[Luna]

@Alex Mobius It turns out that asserting uniqueness is not required. I implemented a working version and created a new conversation about it here: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Group.20Hierarchy.20and.20Type.20Classes

It has the nice benefit that data is not inside a type class and non-definitional equality is implicitly handled.

[Luna]

And in case someone looks back at this, I took inspiration from Kevin Buzzard's reply and used Classical.choose to solve the problem I was having. I think I can use DecidableProp to not have to use the axiom of choice in all scenarios but as a proof of concept Classical.choose works.

[Luna]

@Ruben Van de Velde My main goal with this hierarchy is to avoid placing data inside a type class. So I have to remain high-level and use the term ident instead of the syntax 1, since 1 places an assumption about the type of group it is (e.g. a multiplicative group instead of a generic group).

[Luna]

Alex Mobius said:

Here's an approach that avoids data and choice axioms, but is more cumbersome:

import Mathlib.Logic.ExistsUnique

def IsIdent {α: Type _} (op: α → α → α) (ident: α) := ∀ a: α, op ident a = a

structure Group (α : Type _) (op : α → α → α) where
    has_ident : ∃! (ident : α), IsIdent op ident
    has_inv : ∀ (a : α), ∃ (a_inv : α), IsIdent op $ op a a_inv
    op_assoc : ∀ (a b c : α), op a (op b c) = op (op a b) c

To my understanding, you either need to assert uniqueness, OR you need to define your identity as being both left and right. https://math.stackexchange.com/questions/537572/any-set-with-associativity-left-identity-left-inverse-is-a-group gives a third construction, for which you define an inverse for each possible left identity. If you don't do one of those, then fun _ y => y satisfies all the axioms, with all elements being the identity :)

Ah I misread. In my revised version, I noticed I couldn't create a group with a left identity and right inverse. Thanks for pointing it out!

[Eric Wieser]

Luna said:

So I have to remain high-level and use the term ident instead of the syntax 1,

There is nothing stopping you from having ident be data, and using it directly rather than via syntax.

[Luna]

Eric Wieser said:

Luna said:

So I have to remain high-level and use the term ident instead of the syntax 1,

There is nothing stopping you from having ident be data, and using it directly rather than via syntax.

In this specific case that is correct, since Group is parameterized by an operation instead of the type α. But from my understanding, placing data in a type class adds the risk that the data isn't unique and hence implicitly enforces a singular interpretation of that class.

The main example I'm thinking about where this is a problem is in Mathlib's definition of a Group which is only parameterized by the type and not by the operation. This forces the operation to be supplied in the group instance and hence only allows a single interpretation of a Group on a given type. From my understanding, the way that Mathlib gets around this problem is by duplicating all of Group and its theorems to an identical copy called AddGroup, which seems inelegant.

So I've figured that a good rule of thumb to avoid those issues is to never include data in a type class and only include hypotheses (since all hypotheses are guaranteed to be unique by prop extensionality).

[Yakov Pechersky]

Kevin has remarked on how there really is an assymetry between addition and multiplication, when you start thinking about rings/modules, which appear naturally as structure on endomorphisms. So, given your group class, how would you define a ring?

[Luna]

Yakov Pechersky said:

Kevin has remarked on how there really is an assymetry between addition and multiplication, when you start thinking about rings/modules, which appear naturally as structure on endomorphisms. So, given your group class, how would you define a ring?

I haven't written the Group to be in terms of a monoid yet. I would probably have to mess around to make sure everything works as expected, but my initial go would be the following:

variable {α : Type _} (op : α → α → α)

local infix:70 (priority := high) " * " => op

class Semigroup where
    op_assoc : ∀ (a b c : α), a * (b * c) = (a * b) * c

class Group extends (Semigroup op) where
    has_ident_and_inv : ∃ (ident : α), ∃ (inv : α → α), ∀ (a : α), (a * ident = a) ∧ (a * (inv a) = ident)


class Monoid extends (Semigroup op) where
    has_ident : ∃ (ident : α), ∀ (a : α), op ident a = a


def Monoid.Ident {op : α → α → α} (M : Monoid op) := Classical.choose M.has_ident


class Group₂ extends (Monoid op) where
    has_inv : ∃ (inv : α → α), ∀ (a : α), op (inv a) a = toMonoid.Ident


class CommGroup extends (Group₂ op) where
    op_comm : ∀ (a b : α), a * b = b * a


class Ring (add_op mul_op : α → α → α) [CommGroup add_op] [Monoid mul_op] where
    left_distrib : ∀ (a b c : α), mul_op a (add_op b c) = add_op (mul_op a b) (mul_op a c)
    right_distrib : ∀ (a b c : α), mul_op (add_op b c) a = add_op (mul_op b a) (mul_op c a)

[Luna]

I would recommend checking out how I define just a group here: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Group.20Hierarchy.20and.20Type.20Classes

As it addresses a lot of the issues the come up when defining things this way.