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

$ IsAfield(K,A,M) \equiv $ $ (IsAring(K,A,M) \wedge (M \text{ is commutative on } K) \wedge $ $ TheNeutralElement(K,A) \neq TheNeutralElement(K,M) \wedge $ $ (\forall a\in K.\ a\neq TheNeutralElement(K,A)\longrightarrow $ $ (\exists b\in K.\ M\langle a,b\rangle = 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 GroupInv(K_0,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 $ 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 $ 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 $ 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,restrict(M,K_0\times K_0)) $, $ group0(K_0,restrict(M,K_0\times K_0)) $, $ 1 = TheNeutralElement(K_0,restrict(M,K_0\times K_0)) $proof

let $ f = 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 = 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 = 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 = 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,GroupInv(K_0, f)(a)\rangle = TheNeutralElement(K_0,f) \wedge $ $ f\langle GroupInv(K_0,f)(a),a\rangle = 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) = 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

end

Definition of IsAfield: $ IsAfield(K,A,M) \equiv $ $ (IsAring(K,A,M) \wedge (M \text{ is commutative on } K) \wedge $ $ TheNeutralElement(K,A) \neq TheNeutralElement(K,M) \wedge $ $ (\forall a\in K.\ a\neq TheNeutralElement(K,A)\longrightarrow $ $ (\exists b\in K.\ M\langle a,b\rangle = 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: $ HasNoZeroDivs(R,A,M) \equiv (\forall a\in R.\ \forall b\in R.\ $ $ M\langle a,b\rangle = TheNeutralElement(R,A) \longrightarrow $ $ a = TheNeutralElement(R,A) \vee b = 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 $ HasNoZeroDivs(K,A,M) $

lemma (in ring0) Ring_ZF_1_L12: assumes $ 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 $ IsAfield(K,A,M) $

Definition of IsAring: $ IsAring(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge $ $ \text{IsAmonoid}(R,M) \wedge 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 = 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 $ 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 = 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 = TheNeutralElement(G,f) $ shows $ \text{IsAgroup}(G,f) $

theorem (in field0) Field_ZF_1_L4: shows $ \text{IsAgroup}(K_0,restrict(M,K_0\times K_0)) $, $ group0(K_0,restrict(M,K_0\times K_0)) $, $ 1 = TheNeutralElement(K_0,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 $ 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 $

This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License.