Grace/Cumulus/Algebra/Ring/PrimeIdealCore.g17

Open in Workbench Download source

Imports

IdealCore

Declarations

Source

1-- Prime ideals over separate pieces: the engine under PrimeIdeal, with2-- the colon ideals of a commutative ring, all in ZF3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Ring.PrimeIdealCore9import IdealCore1011-- IsPrimeIdeal(A, add, zero, neg, mul, one, I) is the prime ideal over12-- separate pieces; the bundled PrimeIdeal(R, I) is defined in PrimeIdeal13-- and bridged to this form.14predicate IsPrimeIdeal (A add zero neg mul one I : Set) :=15  IsProperIdeal(A, add, zero, neg, mul, one, I) ∧16  (∀ x ∈ A, ∀ y ∈ A, call2(mul, x, y) ∈ I → x ∈ I ∨ y ∈ I)1718notation scoped IsPrimeIdeal(R, I) => IsPrimeIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, I)1920-- The colon ideal (I : y), with its ambient carrier explicit.21def colonIdeal (A mul I y : Set) : Set := {x ∈ A | call2(mul, x, y) ∈ I}2223theorem colonIdeal.contains (A add zero neg mul I y : Set)24  requires ideal : IsIdeal(A, add, zero, neg, mul, I)25  requires hy : y ∈ A26  shows I ⊆ colonIdeal(A, mul, I, y)27proof28  rcases ideal with ⟨bounded, zeroIn, sums, negatives, products⟩29  intros x hx30  have xInA := bounded with x, hx31  obtain ⟨leftProduct, rightProduct⟩ := products with y, hy, x, hx32  exact colonIdeal.membership.backward with ⟨xInA, rightProduct⟩3334theorem colonIdeal.ideal (A add zero neg mul one I y : Set)35  requires commRing : IsCommRing(A, add, zero, neg, mul, one)36  requires ideal : IsIdeal(A, add, zero, neg, mul, I)37  requires hy : y ∈ A38  shows IsIdeal(A, add, zero, neg, mul, colonIdeal(A, mul, I, y))39proof40  have ring := IsCommRing.ring with commRing41  rcases ideal with ⟨boundedI, zeroIn, sums, negatives, products⟩42  constructor43  . settle with Subset, colonIdeal.membership44  . constructor45    . have zeroInA := IsRing.zero_in_carrier with ring46      have zeroProduct := IsRing.zero_mul at A, add, zero, neg, mul, one,47        y with *48      apply colonIdeal.membership.backward49      constructor50      . exact zeroInA51      . rw zeroProduct52        exact zeroIn53    . constructor54      . intros x hx z hz55        have xData := colonIdeal.membership.forward with hx56        have zData := colonIdeal.membership.forward with hz57        rcases xData with ⟨xInA, xyIn⟩58        rcases zData with ⟨zInA, zyIn⟩59        have sumInA := IsRing.add_closed at A, add, zero, neg, mul, one, x, z with *60        have sumIn := sums with call2(mul, x, y), xyIn, call2(mul, z, y), zyIn61        have distribute := IsCommRing.add_mul at A, add, zero, neg, mul, one, x, z, y with *62        apply colonIdeal.membership.backward63        constructor64        . exact sumInA65        . rw distribute66          exact sumIn67      . constructor68        . intros x hx69          obtain ⟨xInA, xyIn⟩ := colonIdeal.membership.forward with hx70          have negInA := IsRing.neg_closed with ring, xInA71          have negIn := negatives with call2(mul, x, y), xyIn72          have distribute := IsRing.neg_mul at A, add, zero, neg, mul, one, x, y with *73          apply colonIdeal.membership.backward74          constructor75          . exact negInA76          . rw distribute77            exact negIn78        . intros a ha x hx79          obtain ⟨xInA, xyIn⟩ := colonIdeal.membership.forward with hx80          have axInA := IsRing.mul_closed at A, add, zero, neg, mul, one, a, x with *81          have xaInA := IsRing.mul_closed at A, add, zero, neg, mul, one, x, a with *82          obtain ⟨leftProduct, rightProduct⟩ := products with a, ha, call2(mul, x, y), xyIn83          have associate := IsCommRing.mul_assoc at A, add, zero, neg, mul, one, a, x, y with *84          have commute := IsCommRing.mul_comm at A, add, zero, neg, mul, one, x, a with *85          constructor86          . apply colonIdeal.membership.backward at87            A, mul, I, y, call2(mul, a, x)88            constructor89            . exact axInA90            . rw associate91              exact leftProduct92          . apply colonIdeal.membership.backward at93            A, mul, I, y, call2(mul, x, a)94            constructor95            . exact xaInA96            . rw [commute, associate]97              exact leftProduct9899theorem colonIdeal.proper (A add zero neg mul one I y : Set)100  requires commRing : IsCommRing(A, add, zero, neg, mul, one)101  requires ideal : IsIdeal(A, add, zero, neg, mul, I)102  requires hy : y ∈ A103  requires absent : ¬(y ∈ I)104  shows IsProperIdeal(A, add, zero, neg, mul, one, colonIdeal(A, mul, I, y))105proof106  have colon := colonIdeal.ideal with *107  have identity := IsCommRing.one_left with *108  constructor109  . exact colon110  . intro member111    obtain ⟨oneInA, productIn⟩ := colonIdeal.membership.forward with member112    rw identity at productIn113    exact absent with productIn114115theorem IsMaximalIdeal.is_prime (A add zero neg mul one M : Set)116  requires commRing : IsCommRing(A, add, zero, neg, mul, one)117  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, M)118  shows IsPrimeIdeal(A, add, zero, neg, mul, one, M)119proof120  rcases maximal with ⟨proper, largest⟩121  have ideal : IsIdeal(A, add, zero, neg, mul, M) by simp [IsProperIdeal]122  constructor123  . exact proper124  . intros x hx y hy productIn125    have alternatives : y ∈ M ∨ ¬(y ∈ M) by tauto126    cases alternatives with yIn | yOut127    . right128      exact yIn129    . left130      have colonProper := colonIdeal.proper with *131      have contains := colonIdeal.contains with ideal, hy132      have equal := largest with colonIdeal(A, mul, M, y), colonProper, contains133      have xInColon : x ∈ colonIdeal(A, mul, M, y) := colonIdeal.membership.backward with ⟨hx, productIn⟩134      rwa equal at xInColon135136theorem IsPrimeIdeal.proper (A add zero neg mul one I : Set)137  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, I)138  shows IsProperIdeal(A, add, zero, neg, mul, one, I)139proof140  simp [IsPrimeIdeal]141142theorem IsPrimeIdeal.ideal (A add zero neg mul one I : Set)143  requires h : IsPrimeIdeal(A, add, zero, neg, mul, one, I)144  shows IsIdeal(A, add, zero, neg, mul, I)145proof146  have proper := IsPrimeIdeal.proper with h147  exact proper.left148149theorem IsPrimeIdeal.left_of_mul (A add zero neg mul one I x y : Set)150  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, I)151  requires hx : x ∈ A152  requires hy : y ∈ A153  requires productIn : call2(mul, x, y) ∈ I154  requires absent : ¬(y ∈ I)155  shows x ∈ I156proof157  rcases prime with ⟨proper, factors⟩158  have alternatives := factors with x, hx, y, hy, productIn159  cases alternatives with xIn | yIn160  . exact xIn161  . exfalso162    exact absent with yIn163164theorem IsPrimeIdeal.colon_eq (A add zero neg mul one I y : Set)165  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, I)166  requires hy : y ∈ A167  requires absent : ¬(y ∈ I)168  shows colonIdeal(A, mul, I, y) = I169proof170  obtain ⟨ideal, oneOut⟩ := IsPrimeIdeal.proper with prime171  have contains := colonIdeal.contains with *172  apply Subset.antisymmetric173    intros x hx174    obtain ⟨xInA, productIn⟩ := colonIdeal.membership.forward with hx175    exact IsPrimeIdeal.left_of_mul with *176  . exact contains177178theorem IsIntegralDomain.zero_prime (A add zero neg mul one : Set)179  requires domain : IsIntegralDomain(A, add, zero, neg, mul, one)180  shows IsPrimeIdeal(A, add, zero, neg, mul, one, {zero})181proof182  have commRing := IsIntegralDomain.comm_ring with domain183  have ring := IsCommRing.ring with commRing184  have nontrivial := IsIntegralDomain.nontrivial with domain185  have noZeroDivisors := IsIntegralDomain.no_zero_divisors with domain186  have proper := IsProperIdeal.zero_ideal with *187  constructor188  . exact proper189  . intros x hx y hy productIn190    have zeroProduct := singleton.membership.forward with productIn191    have alternatives := noZeroDivisors with x, hx, y, hy, zeroProduct192    cases alternatives with xZero | yZero193    . left194      exact singleton.membership.backward with xZero195    . right196      exact singleton.membership.backward with yZero197198theorem IsPrimeIdeal.zero_iff_domain (A add zero neg mul one : Set)199  requires commRing : IsCommRing(A, add, zero, neg, mul, one)200  shows IsPrimeIdeal(A, add, zero, neg, mul, one, {zero}) ↔201    IsIntegralDomain(A, add, zero, neg, mul, one)202proof203  constructor204  . intro prime205    have ring := IsCommRing.ring with commRing206    have zeroInA := IsRing.zero_in_carrier with ring207    have monoid := IsRing.multiplicative with ring208    have oneInA := IsMonoid.unit_in_carrier with monoid209    rcases prime with ⟨proper, factors⟩210    rcases proper with ⟨ideal, oneOut⟩211    have distinct : zero ≠ one212      intro equal213      apply oneOut214      apply singleton.membership.backward215      symm216      exact equal217    have nontrivial : Nontrivial(A, zero, one)218      unfold Nontrivial219      refine ⟨zeroInA, oneInA, distinct⟩220    have noZeroDivisors : NoZeroDivisors(A, mul, zero)221      intros x hx y hy productZero222      have productIn := singleton.membership.backward with productZero223      have alternatives := factors with x, hx, y, hy, productIn224      cases alternatives with xIn | yIn225      . left226        exact singleton.membership.forward with xIn227      . right228        exact singleton.membership.forward with yIn229    unfold IsIntegralDomain230    refine ⟨commRing, nontrivial, noZeroDivisors⟩231  . intro domain232    exact IsIntegralDomain.zero_prime with domain233