Grace/Cumulus/Algebra/Field/Construction.g17

Open in Workbench Download source

Imports

Core

Declarations

Source

1-- Fieldness as a property and a canonical inverse graph, constructed in ZF.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Field.Construction8import Core910predicate IsField (A add zero neg mul one : Set) :=11  IsCommRing(A, add, zero, neg, mul, one) ∧ Nontrivial(A, zero, one) ∧12  (∀ x ∈ A, x ≠ zero → ∃ y, IsInverse(A, mul, one, x, y))1314notation scoped IsField(R) => IsField(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)1516theorem IsField.comm_ring (A add zero neg mul one : Set)17  requires structure : IsField(A, add, zero, neg, mul, one)18  shows IsCommRing(A, add, zero, neg, mul, one)19proof20  simp [IsField]2122theorem IsField.nontrivial (A add zero neg mul one : Set)23  requires structure : IsField(A, add, zero, neg, mul, one)24  shows Nontrivial(A, zero, one)25proof26  simp [IsField]2728theorem IsField.inverse_exists (A add zero neg mul one x : Set)29  requires structure : IsField(A, add, zero, neg, mul, one)30  requires hx : x ∈ A31  requires nonzero : x ≠ zero32  shows ∃ y, IsInverse(A, mul, one, x, y)33proof34  exact structure.right.right with x, hx, nonzero3536-- The zero branch is normalized to zero. Away from zero, uniqueness37-- follows from the monoid inverse-uniqueness theorem.38defunique fieldInverseValue (A add zero neg mul one x : Set) (y ∈ A) :=39  (x = zero ∧ y = zero) ∨ (x ≠ zero ∧ IsInverse(A, mul, one, x, y))40requires structure : IsField(A, add, zero, neg, mul, one)41requires hx : x ∈ A42proof43  have nontrivial := IsField.nontrivial with structure44  have alternatives : x = zero ∨ x ≠ zero by tauto45  cases alternatives with isZero | nonzero46  . witness zero47    refine ⟨nontrivial.left, ?_⟩48    left49    refine ⟨isZero, rfl⟩50  . obtain ⟨y, inverse⟩ := IsField.inverse_exists at A, add, zero, neg, mul, one, x with *51    have yInA : y ∈ A by simp [IsInverse]52    witness y53    refine ⟨yInA, ?_⟩54    right55    refine ⟨nonzero, inverse⟩56uniqueness57  intros y hy propertyY z hz propertyZ58  cases propertyY with yZero | yInverse59  . cases propertyZ with zZero | zInverse60    . have yValue := yZero.right61      have zValue := zZero.right62      cc63    . exfalso64      exact zInverse.left with yZero.left65  . cases propertyZ with zZero | zInverse66    . exfalso67      exact yInverse.left with zZero.left68    . have ring := IsField.comm_ring with structure69      have ordinary := IsCommRing.ring with ring70      have monoid := IsRing.multiplicative with ordinary71      exact IsInverse.unique with monoid, yInverse.right, zInverse.right7273defgraph fieldInverse (A add zero neg mul one : Set) (x ∈ A) : A := fieldInverseValue(A, add, zero, neg, mul, one, x)74requires structure : IsField(A, add, zero, neg, mul, one)75proof76  have selected := fieldInverseValue.selected at A, add, zero, neg, mul, one, x with *77  exact selected.left7879theorem fieldInverse.inverse (A add zero neg mul one x : Set)80  requires structure : IsField(A, add, zero, neg, mul, one)81  requires hx : x ∈ A82  requires nonzero : x ≠ zero83  shows IsInverse(A, mul, one, x, (fieldInverse(A, add, zero, neg, mul, one))(x))84proof85  have selected := fieldInverseValue.selected at A, add, zero, neg, mul, one, x with *86  have inverse : IsInverse(A, mul, one, x, fieldInverseValue(A, add, zero, neg, mul, one, x)) by tauto87  have value := fieldInverse.value at A, add, zero, neg, mul, one, x with *88  rwa value8990theorem fieldInverse.zero (A add zero neg mul one : Set)91  requires structure : IsField(A, add, zero, neg, mul, one)92  shows (fieldInverse(A, add, zero, neg, mul, one))(zero) = zero93proof94  have nontrivial := IsField.nontrivial with structure95  have hz := nontrivial.left96  have selected := fieldInverseValue.selected at A, add, zero, neg, mul, one, zero with *97  have reflexive : zero = zero by rfl98  have chosen : fieldInverseValue(A, add, zero, neg, mul, one, zero) = zero by tauto99  have value := fieldInverse.value at A, add, zero, neg, mul, one, zero with *100  cc101102theorem IsField.field (A add zero neg mul one : Set)103  requires structure : IsField(A, add, zero, neg, mul, one)104  shows IsFieldWithInverse(A, add, zero, neg, mul, one, fieldInverse(A, add, zero, neg, mul, one))105proof106  have ring := IsField.comm_ring with structure107  have nontrivial := IsField.nontrivial with structure108  have function := fieldInverse.function at A, add, zero, neg, mul, one with *109  unfold IsFieldWithInverse110  refine ⟨ring, nontrivial, ?_⟩111  unfold MultiplicativeInverse112  refine ⟨function, ?_⟩113  intros x hx nonzero114  have inverse := fieldInverse.inverse with *115  exact inverse.right.right116117theorem IsFieldWithInverse.is_field (A add zero neg mul one inv : Set)118  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)119  shows IsField(A, add, zero, neg, mul, one)120proof121  have ring := IsFieldWithInverse.comm_ring with field122  have nontrivial := IsFieldWithInverse.nontrivial with field123  unfold IsField124  refine ⟨ring, nontrivial, ?_⟩125  intros x hx nonzero126  have closed := IsFieldWithInverse.inverse_closed with *127  have left := IsFieldWithInverse.inverse_left with *128  have right := IsFieldWithInverse.inverse_right with *129  witness inv(x)130  unfold IsInverse131  refine ⟨hx, closed, left, right⟩132133theorem IsField.iff_exists_inverse (A add zero neg mul one : Set)134  shows IsField(A, add, zero, neg, mul, one) ↔ ∃ inv, IsFieldWithInverse(A, add, zero, neg, mul, one, inv)135proof136  constructor137  . intro structure138    have field := IsField.field with structure139    refine ⟨fieldInverse(A, add, zero, neg, mul, one), field⟩140  . intro existence141    obtain ⟨inv, field⟩ := existence142    exact IsFieldWithInverse.is_field with field143144section Domains145variable (A add zero neg mul one : Set)146notation ring R := (A, add, zero, neg, mul, one)147hypothesis field : IsField(R)148149theorem IsField.no_zero_divisors150  shows NoZeroDivisors(A, mul, zero)151proof152  have ring := IsField.comm_ring with field153  have ordinary := IsCommRing.ring with ring154  intros x hx y hy equation155  have alternatives : x = zero ∨ x ≠ zero by tauto156  cases alternatives with isZero | nonzero157  . left158    exact isZero159  . obtain ⟨v, inverse⟩ := IsField.inverse_exists with field, hx, nonzero160    have inV := inverse.right.left161    have cancels := inverse.right.right.left162    right163    have associate : R[v * (x * y)] = R[(v * x) * y] by ring164    rw [equation, cancels] at associate165    have zeroProduct : R[v * 0] = zero by ring166    have oneProduct : R[1 * y] = y by ring167    cc168169theorem IsField.integral_domain170  shows IsIntegralDomain(A, add, zero, neg, mul, one)171proof172  have ring := IsField.comm_ring with field173  have nontrivial := IsField.nontrivial with field174  have noZero := IsField.no_zero_divisors with field175  unfold IsIntegralDomain176  refine ⟨ring, nontrivial, noZero⟩177178end Domains179