Grace/Cumulus/Algebra/Ring/IdealAdjoin.g17

Open in Workbench Download source

Imports

IdealCore

Declarations

Source

1-- Adjoining an element to an ideal in a commutative ring (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.Ring.IdealAdjoin8import IdealCore910-- I + (x): finite algebra, with no choice of generators or representatives.11def idealAdjoin (A add mul I x : Set) : Set :=12  {z ∈ A | ∃ i ∈ I, ∃ a ∈ A, z = call2(add, i, call2(mul, a, x))}1314theorem idealAdjoin.contains (A add zero neg mul one I x : Set)15  requires ring : IsCommRing(A, add, zero, neg, mul, one)16  requires ideal : IsIdeal(A, add, zero, neg, mul, I)17  requires hx : x ∈ A18  shows I ⊆ idealAdjoin(A, add, mul, I, x)19proof20  have ordinary := IsCommRing.ring with ring21  have zeroInA := IsRing.zero_in_carrier with ordinary22  have bounded := IsIdeal.subset_carrier with ideal23  intros i hi24  have iInA := bounded with i, hi25  have equation : i = call2(add, i, call2(mul, zero, x)) by ring26  exact idealAdjoin.membership.backward with ⟨iInA, i, hi, zero, zeroInA, equation⟩2728theorem idealAdjoin.generator (A add zero neg mul one I x : Set)29  requires ring : IsCommRing(A, add, zero, neg, mul, one)30  requires ideal : IsIdeal(A, add, zero, neg, mul, I)31  requires hx : x ∈ A32  shows x ∈ idealAdjoin(A, add, mul, I, x)33proof34  have ordinary := IsCommRing.ring with ring35  have monoid := IsRing.multiplicative with ordinary36  have oneInA := IsMonoid.unit_in_carrier with monoid37  have zeroIn := IsIdeal.zero_closed with ideal38  have equation : x = call2(add, zero, call2(mul, one, x)) by ring39  exact idealAdjoin.membership.backward with ⟨hx, zero, zeroIn, one, oneInA, equation⟩4041theorem idealAdjoin.ideal (A add zero neg mul one I x : Set)42  requires ring : IsCommRing(A, add, zero, neg, mul, one)43  requires ideal : IsIdeal(A, add, zero, neg, mul, I)44  requires hx : x ∈ A45  shows IsIdeal(A, add, zero, neg, mul, idealAdjoin(A, add, mul, I, x))46proof47  have ordinary := IsCommRing.ring with ring48  have boundedI := IsIdeal.subset_carrier with ideal49  have contains := idealAdjoin.contains with *50  have zeroInI := IsIdeal.zero_closed with ideal51  have zeroIn := contains with zero, zeroInI52  unfold IsIdeal53  refine ⟨?_, ⟨zeroIn, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩54    intros z hz55    have data := idealAdjoin.membership.forward with hz56    exact data.left57  . intros z hz w hw58    obtain ⟨zInA, i, hi, a, ha, zValue⟩ := idealAdjoin.membership.forward with hz59    obtain ⟨wInA, j, hj, b, hb, wValue⟩ := idealAdjoin.membership.forward with hw60    have iInA := boundedI with i, hi61    have jInA := boundedI with j, hj62    have sumInA := IsRing.add_closed at A, add, zero, neg, mul, one, z, w with *63    have sumInI := IsIdeal.add_closed with hi, hj64    have coefficientInA := IsRing.add_closed with ha, hb65    have equation : call2(add, z, w) = call2(add, call2(add, i, j), call2(mul, call2(add, a, b), x))66      rw [zValue, wValue]67      ring68    exact idealAdjoin.membership.backward with ⟨sumInA, call2(add, i, j), sumInI, call2(add, a, b), coefficientInA, equation⟩69  . intros z hz70    obtain ⟨zInA, n, hn, d, hd, value⟩ := idealAdjoin.membership.forward with hz71    have jInA := boundedI with n, hn72    have negInA := IsRing.neg_closed at A, add, zero, neg, mul, one, z with *73    have negInI := IsIdeal.neg_closed with hn74    have coefficientInA := IsRing.neg_closed with hd75    have equation : neg(z) = call2(add, neg(n), call2(mul, neg(d), x))76      rw value77      ring78    exact idealAdjoin.membership.backward with ⟨negInA, neg(n), negInI, neg(d), coefficientInA, equation⟩79  . intros t ht z hz80    obtain ⟨zInA, k, hk, c, hc, value⟩ := idealAdjoin.membership.forward with hz81    have kInA := boundedI with k, hk82    have leftInA := IsRing.mul_closed at A, add, zero, neg, mul, one, t,83      z with *84    have rightInA := IsRing.mul_closed at A, add, zero, neg, mul, one, z,85      t with *86    have productInI := IsIdeal.mul_left_closed with ht, hk87    have coefficientInA := IsRing.mul_closed with ht, hc88    have equation : call2(mul, t, z) = call2(add, call2(mul, t, k), call2(mul, call2(mul, t, c), x))89      rw value90      ring91    have reverse := IsCommRing.mul_comm at A, add, zero, neg, mul, one, z, t with *92    constructor93    . apply idealAdjoin.membership.backward at94      A, add, mul, I, x, call2(mul, t, z)95      refine ⟨leftInA, call2(mul, t, k), productInI, call2(mul, t, c), coefficientInA, equation⟩96    . rw reverse97      exact idealAdjoin.membership.backward with ⟨leftInA, call2(mul, t, k), productInI, call2(mul, t, c), coefficientInA, equation⟩9899theorem idealAdjoin.least (A add zero neg mul I x J : Set)100  requires idealJ : IsIdeal(A, add, zero, neg, mul, J)101  requires contains : I ⊆ J102  requires generator : x ∈ J103  shows idealAdjoin(A, add, mul, I, x) ⊆ J104proof105  intros z hz106  obtain ⟨zInA, i, hi, a, ha, value⟩ := idealAdjoin.membership.forward with hz107  have iInJ := contains with i, hi108  have product := IsIdeal.mul_left_closed at A, add, zero, neg, mul, J, a, x with *109  have sum := IsIdeal.add_closed at A, add, zero, neg, mul, J, i, call2(mul, a, x) with *110  rwa value111112theorem IsMaximalIdeal.bezout (A add zero neg mul one I x : Set)113  requires ring : IsCommRing(A, add, zero, neg, mul, one)114  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)115  requires hx : x ∈ A116  requires outside : ¬(x ∈ I)117  shows ∃ i ∈ I, ∃ a ∈ A, one = call2(add, i, call2(mul, a, x))118proof119  have ideal : IsIdeal(A, add, zero, neg, mul, I) by simp [IsMaximalIdeal, IsProperIdeal]120  have ordinary := IsCommRing.ring with ring121  have monoid := IsRing.multiplicative with ordinary122  have oneInA := IsMonoid.unit_in_carrier with monoid123  have adjoinIdeal := idealAdjoin.ideal at A, add, zero, neg, mul, one, I, x with *124  have contains := idealAdjoin.contains at A, add, zero, neg, mul, one, I, x with *125  have generator := idealAdjoin.generator at A, add, zero, neg, mul, one, I, x with *126  have alternatives := IsMaximalIdeal.eq_or_whole with *127  cases alternatives with same | whole128  . rw same at generator129    exfalso130    exact outside with generator131  . have oneIn : one ∈ idealAdjoin(A, add, mul, I, x)132      rwa whole133    have data := idealAdjoin.membership.forward with oneIn134    exact data.right135