Grace/Cumulus/Algebra/Field/Core.g17

Open in Workbench Download source

Imports

Defs · Ring.Core

Declarations

Source

1-- Core field theory2-- 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.Core8import Defs9import Ring.Core1011-- Division is multiplication by the inverse.  Packaging that familiar12-- operation as a function graph lets notation select it through the same13-- instance machinery as addition and multiplication.14def fieldDiv (A mul inv : Set) : Set :=15  { p ∈ ((A × A) × A) |16    ∃ x ∈ A, ∃ y ∈ A,17      p = ((x, y) ↦ call2(mul, x, inv(y))) }1819theorem fieldDiv.relates (A mul inv x y : Set)20  requires mulFunction : mul : A × A → A21  requires invFunction : inv : A → A22  requires xInA : x ∈ A23  requires yInA : y ∈ A24  shows relates(fieldDiv(A, mul, inv), (x, y),25    call2(mul, x, inv(y)))26proof27  have inverseInA : inv(y) ∈ A28    exact FunctionBetween.apply_closed with invFunction, yInA29  have inputInProduct := product.pair with xInA, inverseInA30  have quotientInA : call2(mul, x, inv(y)) ∈ A31    unfold call232    exact FunctionBetween.apply_closed with mulFunction, inputInProduct33  unfold relates34  apply fieldDiv.membership.backward35  constructor36  . apply product.pair at (x, y), call2(mul, x, inv(y)), A × A, A37    . exact product.pair with xInA, yInA38    . exact quotientInA39  . refine ⟨x, xInA, y, yInA, rfl⟩4041theorem fieldDiv.factors (A mul inv input output : Set)42  requires mapped : relates(fieldDiv(A, mul, inv), input, output)43  shows ∃ x ∈ A, ∃ y ∈ A,44    input = (x, y) ∧ output = call2(mul, x, inv(y))45proof46  unfold relates at mapped47  simp [fieldDiv.membership] at mapped48  rcases mapped with ⟨bounded, x, xInA, y, yInA, shape⟩49  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape50  refine ⟨x, xInA, y, yInA, inputShape, outputShape⟩5152theorem fieldDiv.total (A mul inv : Set)53  requires mulFunction : mul : A × A → A54  requires invFunction : inv : A → A55  shows TotalBetween(fieldDiv(A, mul, inv), A × A, A)56proof57  intros input inputInProduct58  obtain ⟨bounded, x, xInA, y, yInA, inputShape⟩ := product.membership.forward with inputInProduct59  have inverseInA : inv(y) ∈ A60    exact FunctionBetween.apply_closed with invFunction, yInA61  have mulInput := product.pair with xInA, inverseInA62  have quotientInA : call2(mul, x, inv(y)) ∈ A63    unfold call264    exact FunctionBetween.apply_closed with mulFunction, mulInput65  witness call2(mul, x, inv(y))66  constructor67  . exact quotientInA68  . rw inputShape69    exact fieldDiv.relates with mulFunction, invFunction, xInA, yInA7071theorem fieldDiv.functional (A mul inv : Set)72  shows Functional(fieldDiv(A, mul, inv))73proof74  intros input first inputFirst second inputSecond75  obtain ⟨x, xInA, y, yInA, firstInput, firstOutput⟩ := fieldDiv.factors with inputFirst76  obtain ⟨u, uInA, v, vInA, secondInput, secondOutput⟩ := fieldDiv.factors with inputSecond77  rw firstInput at secondInput78  obtain ⟨sameLeft, sameRight⟩ := orderedPair.injective with secondInput79  rw [firstOutput, secondOutput, sameLeft, sameRight]80  rfl8182theorem fieldDiv.function (A mul inv : Set)83  requires mulFunction : mul : A × A → A84  requires invFunction : inv : A → A85  shows fieldDiv(A, mul, inv) : A × A → A86proof87  constructor88    intros p hp89    simp [fieldDiv.membership] at hp90    rcases hp with ⟨bounded, witnesses⟩91    exact bounded92  . have functional := fieldDiv.functional at A, mul, inv93    refine ⟨functional, _⟩94    exact fieldDiv.total with mulFunction, invFunction9596theorem DivisionSemiring.semiring (A add zero mul one inv : Set)97  requires h : DivisionSemiring(A, add, zero, mul, one, inv)98  shows IsSemiring(A, add, zero, mul, one)99proof100  simp [DivisionSemiring]101102theorem Semifield.comm_semiring (A add zero mul one inv : Set)103  requires h : Semifield(A, add, zero, mul, one, inv)104  shows CommSemiring(A, add, zero, mul, one)105proof106  simp [Semifield]107108theorem DivisionRing.ring (A add zero neg mul one inv : Set)109  requires h : DivisionRing(A, add, zero, neg, mul, one, inv)110  shows IsRing(A, add, zero, neg, mul, one)111proof112  simp [DivisionRing]113114theorem DivisionRing.nontrivial (A add zero neg mul one inv : Set)115  requires h : DivisionRing(A, add, zero, neg, mul, one, inv)116  shows Nontrivial(A, zero, one)117proof118  simp [DivisionRing]119120theorem DivisionRing.inverse (A add zero neg mul one inv : Set)121  requires h : DivisionRing(A, add, zero, neg, mul, one, inv)122  shows MultiplicativeInverse(A, mul, zero, one, inv)123proof124  simp [DivisionRing]125126theorem IsFieldWithInverse.comm_ring (A add zero neg mul one inv : Set)127  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)128  shows IsCommRing(A, add, zero, neg, mul, one)129proof130  simp [IsFieldWithInverse]131132theorem IsFieldWithInverse.nontrivial (A add zero neg mul one inv : Set)133  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)134  shows Nontrivial(A, zero, one)135proof136  simp [IsFieldWithInverse]137138theorem IsFieldWithInverse.inverse (A add zero neg mul one inv : Set)139  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)140  shows MultiplicativeInverse(A, mul, zero, one, inv)141proof142  simp [IsFieldWithInverse]143144theorem IsFieldWithInverse.one_in_carrier (A add zero neg mul one inv : Set)145  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)146  shows one ∈ A147proof148  have commRing := IsFieldWithInverse.comm_ring with field149  have ring := IsCommRing.ring with commRing150  have monoid := IsRing.multiplicative with ring151  exact IsMonoid.unit_in_carrier with monoid152153theorem IsFieldWithInverse.inverse_closed (A add zero neg mul one inv x : Set)154  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)155  requires xInA : x ∈ A156  shows inv(x) ∈ A157proof158  obtain ⟨function, laws⟩ := IsFieldWithInverse.inverse with field159  exact FunctionBetween.apply_closed with function, xInA160161theorem IsFieldWithInverse.inverse_left (A add zero neg mul one inv x : Set)162  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)163  requires xInA : x ∈ A164  requires nonzero : x ≠ zero165  shows call2(mul, inv(x), x) = one166proof167  obtain ⟨function, laws⟩ := IsFieldWithInverse.inverse with field168  obtain ⟨left, right⟩ := laws with x, xInA, nonzero169  exact left170171theorem IsFieldWithInverse.inverse_right (A add zero neg mul one inv x : Set)172  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)173  requires xInA : x ∈ A174  requires nonzero : x ≠ zero175  shows call2(mul, x, inv(x)) = one176proof177  obtain ⟨function, laws⟩ := IsFieldWithInverse.inverse with field178  obtain ⟨left, right⟩ := laws with x, xInA, nonzero179  exact right180181theorem IsFieldWithInverse.division_ring (A add zero neg mul one inv : Set)182  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)183  shows DivisionRing(A, add, zero, neg, mul, one, inv)184proof185  rcases h with ⟨commRing, division⟩186  rcases commRing with ⟨ring, commutative⟩187  refine ⟨ring, division⟩188189theorem IsFieldWithInverse.integral_domain (A add zero neg mul one inv : Set)190  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)191  requires noZero : NoZeroDivisors(A, mul, zero)192  shows IsIntegralDomain(A, add, zero, neg, mul, one)193proof194  rcases h with ⟨commRing, nontrivial, inverse⟩195  refine ⟨commRing, nontrivial, noZero⟩196