IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Field_ZF imports Ring_ZF

begin

This theory covers basic facts about fields.

Definition and basic properties

In this section we define what is a field and list the basic properties of fields.

Field is a notrivial commutative ring such that all non-zero elements have an inverse. We define the notion of being a field as a statement about three sets. The first set, denoted K is the carrier of the field. The second set, denoted A represents the additive operation on K (recall that in ZF set theory functions are sets). The third set M represents the multiplicative operation on K.

definition

\( \text{IsAfield}(K,A,M) \equiv \) \( ( \text{IsAring}(K,A,M) \wedge (M \text{ is commutative on } K) \wedge \) \( \text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge \) \( (\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow \) \( (\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M)))) \)

The field0 context extends the ring0 context adding field-related assumptions and notation related to the multiplicative inverse.

locale field0 = ring0 K A M +

assumes mult_commute: \( M \text{ is commutative on } K \)

assumes not_triv: \( 0 \neq 1 \)

assumes inv_exists: \( \forall x\in K.\ x\neq 0 \longrightarrow (\exists y\in K.\ x\cdot y = 1 ) \)

defines \( K_0 \equiv K-\{ 0 \} \)

defines \( a^{-1} \equiv \text{GroupInv}(K_0,\text{restrict}(M,K_0\times K_0))(a) \)

The next lemma assures us that we are talking fields in the field0 context.

lemma (in field0) Field_ZF_1_L1:

shows \( \text{IsAfield}(K,A,M) \) using ringAssum, mult_commute, not_triv, inv_exists, IsAfield_def

We can use theorems proven in the field0 context whenever we talk about a field.

lemma field_field0:

assumes \( \text{IsAfield}(K,A,M) \)

shows \( field0(K,A,M) \) using assms, IsAfield_def, field0_axioms.intro, ring0_def, field0_def

Let's have an explicit statement that the multiplication in fields is commutative.

lemma (in field0) field_mult_comm:

assumes \( a\in K \), \( b\in K \)

shows \( a\cdot b = b\cdot a \) using mult_commute, assms, IsCommutative_def

Fields do not have zero divisors.

lemma (in field0) field_has_no_zero_divs:

shows \( \text{HasNoZeroDivs}(K,A,M) \)proof

{

fix \( a \) \( b \)

assume A1: \( a\in K \), \( b\in K \) and A2: \( a\cdot b = 0 \) and A3: \( b\neq 0 \)

from inv_exists, A1, A3 obtain \( c \) where I: \( c\in K \) and II: \( b\cdot c = 1 \)

from A2 have \( a\cdot b\cdot c = 0 \cdot c \)

with A1, I have \( a\cdot (b\cdot c) = 0 \) using Ring_ZF_1_L11, Ring_ZF_1_L6

with A1, II have \( a= 0 \) using Ring_ZF_1_L3

}

then have \( \forall a\in K.\ \forall b\in K.\ a\cdot b = 0 \longrightarrow a= 0 \vee b= 0 \)

then show \( thesis \) using HasNoZeroDivs_def

qed

\(K_0\) (the set of nonzero field elements is closed with respect to multiplication.

lemma (in field0) Field_ZF_1_L2:

shows \( K_0 \text{ is closed under } M \) using Ring_ZF_1_L4, field_has_no_zero_divs, Ring_ZF_1_L12, IsOpClosed_def

Any nonzero element has a right inverse that is nonzero.

lemma (in field0) Field_ZF_1_L3:

assumes A1: \( a\in K_0 \)

shows \( \exists b\in K_0.\ a\cdot b = 1 \)proof

from inv_exists, A1 obtain \( b \) where \( b\in K \) and \( a\cdot b = 1 \)

with not_triv, A1 show \( \exists b\in K_0.\ a\cdot b = 1 \) using Ring_ZF_1_L6

qed

If we remove zero, the field with multiplication becomes a group and we can use all theorems proven in group0 context.

theorem (in field0) Field_ZF_1_L4:

shows \( \text{IsAgroup}(K_0,\text{restrict}(M,K_0\times K_0)) \), \( group0(K_0,\text{restrict}(M,K_0\times K_0)) \), \( 1 = \text{ TheNeutralElement}(K_0,\text{restrict}(M,K_0\times K_0)) \)proof

let \( f = \text{restrict}(M,K_0\times K_0) \)

have \( M \text{ is associative on } K \), \( K_0 \subseteq K \), \( K_0 \text{ is closed under } M \) using Field_ZF_1_L1, IsAfield_def, IsAring_def, IsAgroup_def, IsAmonoid_def, Field_ZF_1_L2

then have \( f \text{ is associative on } K_0 \) using func_ZF_4_L3

moreover

from not_triv have I: \( 1 \in K_0 \wedge (\forall a\in K_0.\ f\langle 1 ,a\rangle = a \wedge f\langle a,1 \rangle = a) \) using Ring_ZF_1_L2, Ring_ZF_1_L3

then have \( \exists n\in K_0.\ \forall a\in K_0.\ f\langle n,a\rangle = a \wedge f\langle a,n\rangle = a \)

ultimately have II: \( \text{IsAmonoid}(K_0,f) \) using IsAmonoid_def

then have \( monoid0(K_0,f) \) using monoid0_def

moreover

note I

ultimately show \( 1 = \text{ TheNeutralElement}(K_0,f) \) by (rule group0_1_L4 )

then have \( \forall a\in K_0.\ \exists b\in K_0.\ f\langle a,b\rangle = \text{ TheNeutralElement}(K_0,f) \) using Field_ZF_1_L3

with II show \( \text{IsAgroup}(K_0,f) \) by (rule definition_of_group )

then show \( group0(K_0,f) \) using group0_def

qed

The inverse of a nonzero field element is nonzero.

lemma (in field0) Field_ZF_1_L5:

assumes A1: \( a\in K \), \( a\neq 0 \)

shows \( a^{-1} \in K_0 \), \( (a^{-1})^2 \in K_0 \), \( a^{-1} \in K \), \( a^{-1} \neq 0 \)proof

from A1 have \( a \in K_0 \)

then show \( a^{-1} \in K_0 \) using Field_ZF_1_L4, inverse_in_group

then show \( (a^{-1})^2 \in K_0 \), \( a^{-1} \in K \), \( a^{-1} \neq 0 \) using Field_ZF_1_L2, IsOpClosed_def

qed

The inverse is really the inverse.

lemma (in field0) Field_ZF_1_L6:

assumes A1: \( a\in K \), \( a\neq 0 \)

shows \( a\cdot a^{-1} = 1 \), \( a^{-1}\cdot a = 1 \)proof

let \( f = \text{restrict}(M,K_0\times K_0) \)

from A1 have \( group0(K_0,f) \), \( a \in K_0 \) using Field_ZF_1_L4

then have \( f\langle a, \text{GroupInv}(K_0, f)(a)\rangle = \text{ TheNeutralElement}(K_0,f) \wedge \) \( f\langle \text{GroupInv}(K_0,f)(a),a\rangle = \text{ TheNeutralElement}(K_0, f) \) by (rule group0_2_L6 )

with A1 show \( a\cdot a^{-1} = 1 \), \( a^{-1}\cdot a = 1 \) using Field_ZF_1_L5, Field_ZF_1_L4

qed

A lemma with two field elements and cancelling.

lemma (in field0) Field_ZF_1_L7:

assumes \( a\in K \), \( b\in K \), \( b\neq 0 \)

shows \( a\cdot b\cdot b^{-1} = a \), \( a\cdot b^{-1}\cdot b = a \) using assms, Field_ZF_1_L5, Ring_ZF_1_L11, Field_ZF_1_L6, Ring_ZF_1_L3

Equations and identities

This section deals with more specialized identities that are true in fields.

\(a/(a^2) = 1/a \) .

lemma (in field0) Field_ZF_2_L1:

assumes A1: \( a\in K \), \( a\neq 0 \)

shows \( a\cdot (a^{-1})^2 = a^{-1} \)proof

have \( a\cdot (a^{-1})^2 = a\cdot (a^{-1}\cdot a^{-1}) \)

also

from A1 have \( \ldots = (a\cdot a^{-1})\cdot a^{-1} \) using Field_ZF_1_L5, Ring_ZF_1_L11

also

from A1 have \( \ldots = a^{-1} \) using Field_ZF_1_L6, Field_ZF_1_L5, Ring_ZF_1_L3

finally show \( a\cdot (a^{-1})^2 = a^{-1} \)

qed

If we multiply two different numbers by a nonzero number, the results will be different.

lemma (in field0) Field_ZF_2_L2:

assumes \( a\in K \), \( b\in K \), \( c\in K \), \( a\neq b \), \( c\neq 0 \)

shows \( a\cdot c^{-1} \neq b\cdot c^{-1} \) using assms, field_has_no_zero_divs, Field_ZF_1_L5, Ring_ZF_1_L12B

We can put a nonzero factor on the other side of non-identity (is this the best way to call it?) changing it to the inverse.

lemma (in field0) Field_ZF_2_L3:

assumes A1: \( a\in K \), \( b\in K \), \( b\neq 0 \), \( c\in K \) and A2: \( a\cdot b \neq c \)

shows \( a \neq c\cdot b^{-1} \)proof

from A1, A2 have \( a\cdot b\cdot b^{-1} \neq c\cdot b^{-1} \) using Ring_ZF_1_L4, Field_ZF_2_L2

with A1 show \( a \neq c\cdot b^{-1} \) using Field_ZF_1_L7

qed

If if the inverse of \(b\) is different than \(a\), then the inverse of \(a\) is different than \(b\).

lemma (in field0) Field_ZF_2_L4:

assumes \( a\in K \), \( a\neq 0 \) and \( b^{-1} \neq a \)

shows \( a^{-1} \neq b \) using assms, Field_ZF_1_L4, group0_2_L11B

An identity with two field elements, one and an inverse.

lemma (in field0) Field_ZF_2_L5:

assumes \( a\in K \), \( b\in K \), \( b\neq 0 \)

shows \( (1 + a\cdot b)\cdot b^{-1} = a + b^{-1} \) using assms, Ring_ZF_1_L4, Field_ZF_1_L5, Ring_ZF_1_L2, ring_oper_distr, Field_ZF_1_L7, Ring_ZF_1_L3

An identity with three field elements, inverse and cancelling.

lemma (in field0) Field_ZF_2_L6:

assumes A1: \( a\in K \), \( b\in K \), \( b\neq 0 \), \( c\in K \)

shows \( a\cdot b\cdot (c\cdot b^{-1}) = a\cdot c \)proof

from A1 have T: \( a\cdot b \in K \), \( b^{-1} \in K \) using Ring_ZF_1_L4, Field_ZF_1_L5

with mult_commute, A1 have \( a\cdot b\cdot (c\cdot b^{-1}) = a\cdot b\cdot (b^{-1}\cdot c) \) using IsCommutative_def

moreover

from A1, T have \( a\cdot b \in K \), \( b^{-1} \in K \), \( c\in K \)

then have \( a\cdot b\cdot b^{-1}\cdot c = a\cdot b\cdot (b^{-1}\cdot c) \) by (rule Ring_ZF_1_L11 )

ultimately have \( a\cdot b\cdot (c\cdot b^{-1}) = a\cdot b\cdot b^{-1}\cdot c \)

with A1 show \( a\cdot b\cdot (c\cdot b^{-1}) = a\cdot c \) using Field_ZF_1_L7

qed

1/0=0

In ZF if \(f: X\rightarrow Y\) and \(x\notin X\) we have \(f(x)=\emptyset\). Since \(\emptyset\) (the empty set) in ZF is the same as zero of natural numbers we can claim that \(1/0=0\) in certain sense. In this section we prove a theorem that makes makes it explicit.

The next locale extends the field0 locale to introduce notation for division operation.

locale fieldd = field0 +

defines \( division \equiv \{\langle p,\text{fst}(p)\cdot \text{snd}(p)^{-1}\rangle .\ p\in K\times K_0\} \)

defines \( x / y \equiv division\langle x,y\rangle \)

Division is a function on \(K\times K_0\) with values in \(K\).

lemma (in fieldd) div_fun:

shows \( division: K\times K_0 \rightarrow K \)proof

have \( \forall p \in K\times K_0.\ \text{fst}(p)\cdot \text{snd}(p)^{-1} \in K \)proof

fix \( p \)

assume \( p \in K\times K_0 \)

hence \( \text{fst}(p) \in K \) and \( \text{snd}(p) \in K_0 \)

then show \( \text{fst}(p)\cdot \text{snd}(p)^{-1} \in K \) using Ring_ZF_1_L4, Field_ZF_1_L5

qed

then have \( \{\langle p,\text{fst}(p)\cdot \text{snd}(p)^{-1}\rangle .\ p\in K\times K_0\}: K\times K_0 \rightarrow K \) by (rule ZF_fun_from_total )

thus \( thesis \)

qed

So, really \(1/0=0\). The essential lemma is apply_0 from standard Isabelle's func.thy.

theorem (in fieldd) one_over_zero:

shows \( 1 / 0 = 0 \)proof

have \( domain(division) = K\times K_0 \) using div_fun, func1_1_L1

hence \( \langle 1 , 0 \rangle \notin domain(division) \)

then show \( thesis \) using apply_0

qed

end

Definition of IsAfield: \( \text{IsAfield}(K,A,M) \equiv \) \( ( \text{IsAring}(K,A,M) \wedge (M \text{ is commutative on } K) \wedge \) \( \text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge \) \( (\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow \) \( (\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M)))) \)

Definition of IsCommutative: \( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)

lemma (in ring0) Ring_ZF_1_L11:

assumes \( a\in R \), \( b\in R \), \( c\in R \)

shows \( a + b + c = a + (b + c) \), \( a\cdot b\cdot c = a\cdot (b\cdot c) \)

lemma (in ring0) Ring_ZF_1_L6:

assumes \( x\in R \)

shows \( 0 \cdot x = 0 \), \( x\cdot 0 = 0 \)

lemma (in ring0) Ring_ZF_1_L3:

assumes \( a\in R \)

shows \( ( - a) \in R \), \( ( - ( - a)) = a \), \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \), \( 2 \cdot a = a + a \), \( ( - a) + a = 0 \)

Definition of HasNoZeroDivs: \( \text{HasNoZeroDivs}(R,A,M) \equiv (\forall a\in R.\ \forall b\in R.\ \) \( M\langle a,b\rangle = \text{ TheNeutralElement}(R,A) \longrightarrow \) \( a = \text{ TheNeutralElement}(R,A) \vee b = \text{ TheNeutralElement}(R,A)) \)

lemma (in ring0) Ring_ZF_1_L4:

assumes \( a\in R \), \( b\in R \)

shows \( a + b \in R \), \( a - b \in R \), \( a\cdot b \in R \), \( a + b = b + a \)

lemma (in field0) field_has_no_zero_divs: shows \( \text{HasNoZeroDivs}(K,A,M) \)

lemma (in ring0) Ring_ZF_1_L12:

assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a\in R \), \( a\neq 0 \), \( b\in R \), \( b\neq 0 \)

shows \( a\cdot b\neq 0 \)

Definition of IsOpClosed: \( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)

lemma (in field0) Field_ZF_1_L1: shows \( \text{IsAfield}(K,A,M) \)

Definition of IsAring: \( \text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge \) \( \text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M) \)

Definition of IsAgroup: \( \text{IsAgroup}(G,f) \equiv \) \( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)

Definition of IsAmonoid: \( \text{IsAmonoid}(G,f) \equiv \) \( f \text{ is associative on } G \wedge \) \( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)

lemma (in field0) Field_ZF_1_L2: shows \( K_0 \text{ is closed under } M \)

lemma func_ZF_4_L3:

assumes \( f \text{ is associative on } X \) and \( A\subseteq X \) and \( A \text{ is closed under } f \)

shows \( \text{restrict}(f,A\times A) \text{ is associative on } A \)

lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \)

lemma (in monoid0) group0_1_L4:

assumes \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)

shows \( e = \text{ TheNeutralElement}(G,f) \)

lemma (in field0) Field_ZF_1_L3:

assumes \( a\in K_0 \)

shows \( \exists b\in K_0.\ a\cdot b = 1 \)

lemma definition_of_group:

assumes \( \text{IsAmonoid}(G,f) \) and \( \forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f) \)

shows \( \text{IsAgroup}(G,f) \)

theorem (in field0) Field_ZF_1_L4: shows \( \text{IsAgroup}(K_0,\text{restrict}(M,K_0\times K_0)) \), \( group0(K_0,\text{restrict}(M,K_0\times K_0)) \), \( 1 = \text{ TheNeutralElement}(K_0,\text{restrict}(M,K_0\times K_0)) \)

lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)

lemma (in group0) group0_2_L6:

assumes \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)

lemma (in field0) Field_ZF_1_L5:

assumes \( a\in K \), \( a\neq 0 \)

shows \( a^{-1} \in K_0 \), \( (a^{-1})^2 \in K_0 \), \( a^{-1} \in K \), \( a^{-1} \neq 0 \)

lemma (in field0) Field_ZF_1_L6:

assumes \( a\in K \), \( a\neq 0 \)

shows \( a\cdot a^{-1} = 1 \), \( a^{-1}\cdot a = 1 \)