## Stream: new members

### Topic: Encoding Field as Abelian Group

#### Mukesh Tiwari (Mar 23 2020 at 01:09):

Hi Everyone, I am going through this pdf (https://people.maths.ox.ac.uk/flynn/genus2/sheets0405/grfnotes1011.pdf) and wrote some Lean code to encode these structures. The definition of Field (in the page 13) has two definitions: 1) a commutative ring with identity and all the non zero elements in the field has a inverse, 2) it is a abelian group with respect to addition, and it is a abelian group with respect to multiplication (except zero). I have encode the first one and type-checker is happy, but I am struggling to encode the second one, mainly how to exclude zero from set A. I have encoded it as a sigma type(?) {x : A | x ≠ zero} , but the type checker is not happy.

/- How write the second definition-/
class field {A : Type*} (zero one : A)
(Fadd Fsub Fmult Fdiv : A → A → A) (Fopp Finv : A → A)
[Hdec : decidable_eq A] :=
(Hnz : zero ≠ one)
(Hmulabel : @abelian_group {x : A | x ≠ zero} one Fmult Finv Hdec)
(Field_sub_def : forall x y, Fsub x y = Fadd x (Fopp y))
(Field_div_def : forall x y, Fdiv x y = Fmult x (Finv y))
(Field_distr : forall x y z, Fmult x (Fadd y z) = Fadd (Fmult x y) (Fmult x z))


Complete source code.

namespace AlgStructures

class monoid {A : Type*} (e : A) (f : A → A → A) [decidable_eq A]:=
(Hassoc : ∀ a b c : A, f a (f b c) = f (f a b) c)
(Hidl : ∀ a : A, f e a = a)
(Hidr : ∀ a : A, f a e = a)

class group {A : Type*} (e : A) (f : A → A → A)
(inv : A → A) [Hdec : decidable_eq A] :=
(Hmon : @monoid A e f Hdec)
(Hinvl : ∀ x, f (inv x) x = e)
(Hinvr : ∀ x, f x (inv x) = e)

class abelian_group {A : Type*} (e : A) (f : A → A → A)
(inv : A → A) [Hdec : decidable_eq A] :=
(Hg : @group A e f inv Hdec)
(Hcomm : ∀ x y : A, f x y = f y x)

/- assuming a ring with identity -/
class ring {A : Type*} (zero one : A)
(Radd Rsub Rmult : A → A → A) (Ropp : A → A)
[Hdec : decidable_eq A] :=
(Habel : @abelian_group A zero Radd Ropp Hdec)
(Hmon : @monoid A one Rmult Hdec)
(Ring_distr_l : forall x y z, Rmult (Radd x y) z = Radd (Rmult x z) (Rmult y z))
(Ring_distr_r : forall x y z, Rmult z (Radd x y) = Radd (Rmult z x) (Rmult z y))
(Ring_sub_def : forall x y, Rsub x y = Radd x (Ropp y))

class commutative_ring {A : Type*} (zero one : A)
(Radd Rsub Rmult : A → A → A) (Ropp : A → A)
[Hdec : decidable_eq A] :=
(Hring : @ring A zero one Radd Rsub Rmult Ropp Hdec)
(Hinv : forall x y : A, Rmult x y = Rmult y x)

/- commutative Ring with inverse -/
class field {A : Type*} (zero one : A)
(Fadd Fsub Fmult Fdiv : A → A → A) (Fopp Finv : A → A)
[Hdec : decidable_eq A] :=
(Hcring : @commutative_ring A zero one Fadd Fsub Fmult
Fopp Hdec)
(Hfinvl : forall x : A, x ≠ zero -> Fmult (Finv x) x = one)
(Hfinvr : forall x : A, x ≠ zero -> Fmult x (Finv x) = one)

/- How write the second definition ? -/
class field {A : Type*} (zero one : A)
(Fadd Fsub Fmult Fdiv : A → A → A) (Fopp Finv : A → A)
[Hdec : decidable_eq A] :=
(Hnz : zero ≠ one)
(Hmulabel : @abelian_group {x : A | x ≠ zero} one Fmult Finv Hdec)
(Field_sub_def : forall x y, Fsub x y = Fadd x (Fopp y))
(Field_div_def : forall x y, Fdiv x y = Fmult x (Finv y))
(Field_distr : forall x y z, Fmult x (Fadd y z) = Fadd (Fmult x y) (Fmult x z))

end AlgStructures


#### Alex J. Best (Mar 23 2020 at 01:27):

So fields are already in lean core if you just want to use them you needn't define them yourself, and you can see how it is done there.
The issue here is that in the line  @abelian_group {x : A | x ≠ zero} one Fmult Finv Hdec the terms one and Fmult Finv Fdec are not terms of or functions on the type {x : A | x ≠ zero}  so you'll need to add some things like one ≠ zero and that Fmult takes a nonzero element and a nonzero element to a nonzero element as extra terms.

Thanks Alex.

#### Johan Commelin (Mar 23 2020 at 08:02):

@Mukesh Tiwari That second definition is a bit sloppy (it doesn't say anything about distributivity).

#### Kevin Buzzard (Mar 23 2020 at 08:27):

I think that asserting that multiplication makes the non-zero elements an abelian group will be problematic to use in practice, because what you want to know is that multiplication is commutative and associative on the whole field, and your set-up doesn't show a*(0*b)=(a*0)*b for example.

#### Kevin Buzzard (Mar 23 2020 at 08:28):

The power of notation in Lean means that you can set up these notations in a far more beautiful way. See for example the definition of a group in the group theory game

#### Mukesh Tiwari (Apr 12 2020 at 12:51):

Johan Commelin said:

Mukesh Tiwari That second definition is a bit sloppy (it doesn't say anything about distributivity).

You mean this one? "it is a abelian group with respect to addition, and it is a abelian group with respect to multiplication (except zero)."

Yup, that one

#### Kevin Buzzard (Apr 12 2020 at 13:59):

@Mukesh Tiwari if you're still thinking about this, why not switch over to the standard Lean way of doing things where you can use notation instead of having to write all this Fmult (Finv x) x = one stuff?

#### Kevin Buzzard (Apr 12 2020 at 14:05):

class ring' (A : Type) extends add_comm_group A, monoid A :=
(add_mul : ∀ x y z : A, (x + y) * z = x * z + y * z)
(mul_add : ∀ x y z : A, z * (x + y) = z * x + z * y)


#### Mukesh Tiwari (Apr 12 2020 at 22:21):

@Kevin Buzzard @Johan Commelin Thank you very much.

#### Mukesh Tiwari (Apr 13 2020 at 00:27):

I looked at the pdf again, and It says, "the distributive laws hold." (page 13). I was sloppy when writing the axioms. Thanks for the catch.

Last updated: May 12 2021 at 03:23 UTC