IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

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 a\in K.\ a\neq 0 \longrightarrow (\exists b\in K.\ a\cdot b = 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 \)
lemma (in ring0) Ring_ZF_1_L12B:

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

shows \( a\cdot c \neq b\cdot c \)
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} \)
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 \)
lemma (in group0) group0_2_L11B:

assumes \( a\in G \) and \( b^{-1} \neq a \)

shows \( a^{-1} \neq b \)
lemma (in ring0) ring_oper_distr:

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

shows \( a\cdot (b + c) = a\cdot b + a\cdot c \), \( (b + c)\cdot a = b\cdot a + c\cdot a \)
lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)
lemma (in fieldd) div_fun: shows \( division: K\times K_0 \rightarrow K \)
lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \)
51
66
12
12