Encoding Field as Abelian Group

Stream: new members

[Mukesh Tiwari]

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)
 (Haddabel : @abelian_group A zero Fadd Fopp Hdec)
 (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)
 (Haddabel : @abelian_group A zero Fadd Fopp Hdec)
 (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]

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.

[Mukesh Tiwari]

Thanks Alex.

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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)."

[Johan Commelin]

Yup, that one

[Kevin Buzzard]

@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]

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]

@Kevin Buzzard @Johan Commelin Thank you very much.

[Mukesh Tiwari]

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.