Grace/Cumulus/Algebra/Ring/Bicommutant.g17

Open in Workbench Download source

Imports

Subring

Declarations

Source

1-- Centralizers and bicommutants in a ring: the elements commuting with a2-- set S form a subring, the bicommutant of a commuting set is a commutative3-- subring containing it, and bicommutantRing(T, S) is that commutative4-- ring; everything here is ZF5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Ring.Bicommutant11import Subring1213-- The centralizer of S in T, the bicommutant, and the ring on the latter14-- with the operations of T restricted.15def ringCentralizer (T S : Set) : Set :=16  { z ∈ Ring.carrier(T) |17    ∀ x ∈ S, call2(Ring.mul(T), z, x) = call2(Ring.mul(T), x, z) }18def bicommutant (T S : Set) : Set := ringCentralizer(T, ringCentralizer(T, S))19def bicommutantRing (T S : Set) : Set := subringRing(T, bicommutant(T, S))2021theorem bicommutantRing.carrierOf (T S : Set)22  shows Ring.carrier(bicommutantRing(T, S)) = bicommutant(T, S)23proof24  simp [bicommutantRing, subringRing, Ring.mk.carrier]2526theorem bicommutantRing.addOf (T S : Set)27  shows Ring.add(bicommutantRing(T, S)) =28    restrict(Ring.add(T), bicommutant(T, S) × bicommutant(T, S))29proof30  simp [bicommutantRing, subringRing, Ring.mk.add]3132theorem bicommutantRing.zeroOf (T S : Set)33  shows Ring.zero(bicommutantRing(T, S)) = Ring.zero(T)34proof35  simp [bicommutantRing, subringRing, Ring.mk.zero]3637theorem bicommutantRing.negOf (T S : Set)38  shows Ring.neg(bicommutantRing(T, S)) = restrict(Ring.neg(T), bicommutant(T, S))39proof40  simp [bicommutantRing, subringRing, Ring.mk.neg]4142theorem bicommutantRing.mulOf (T S : Set)43  shows Ring.mul(bicommutantRing(T, S)) =44    restrict(Ring.mul(T), bicommutant(T, S) × bicommutant(T, S))45proof46  simp [bicommutantRing, subringRing, Ring.mk.mul]4748theorem bicommutantRing.oneOf (T S : Set)49  shows Ring.one(bicommutantRing(T, S)) = Ring.one(T)50proof51  simp [bicommutantRing, subringRing, Ring.mk.one]5253-- Multiplication by a negation in a ring that need not commute.54theorem IsRing.mul_neg (A add zero neg mul one x y : Set)55  requires ring : IsRing(A, add, zero, neg, mul, one)56  requires xInA : x ∈ A57  requires yInA : y ∈ A58  shows call2(mul, x, neg(y)) = neg(call2(mul, x, y))59proof60  have additive := IsRing.additive with ring61  have group := IsAbelianGroup.group with additive62  have monoid := IsGroup.monoid with group63  have distributive := IsRing.distributive with ring64  have negIn := IsRing.neg_closed with ring, yInA65  have product := IsRing.mul_closed with ring, xInA, yInA66  have negProduct := IsRing.mul_closed with ring, xInA, negIn67  have inverseIn := IsRing.neg_closed with ring, product68  have zeroIn := IsRing.zero_in_carrier with ring69  have rightLaw := distributive with x, xInA, y, yInA, neg(y), negIn70  have leftLaw := distributive with x, xInA, neg(y), negIn, y, yInA71  have cancelRight := IsRing.add_inverse_right with ring, yInA72  have cancelLeft := IsRing.add_inverse_left with ring, yInA73  have vanish := IsRing.mul_zero with ring, xInA74  have first : IsInverse(A, add, zero, call2(mul, x, y), call2(mul, x, neg(y)))75    have sumRight := rightLaw.left76    have sumLeft := leftLaw.left77    rw cancelRight at sumRight78    rw cancelLeft at sumLeft79    unfold IsInverse80    refine ⟨product, negProduct, ?_, ?_⟩81    . cc82    . cc83  have second : IsInverse(A, add, zero, call2(mul, x, y), neg(call2(mul, x, y)))84    have left := IsRing.add_inverse_left with ring, product85    have right := IsRing.add_inverse_right with ring, product86    unfold IsInverse87    exact ⟨product, inverseIn, left, right⟩88  exact IsInverse.unique with monoid, first, second8990theorem restrictBinary.commutative_on (A S op : Set)91  requires function : IsMagma(A, op)92  requires subset : S ⊆ A93  requires closed : ClosedBinary(S, op)94  requires law : Commutative(S, op)95  shows Commutative(S, restrict(op, S × S))96proof97  intros x hx y hy98  have first := restrictBinary.value with hx, hy99  have second := restrictBinary.value with hy, hx100  have original := law with x, hx, y, hy101  cc102103-- A subring on which the multiplication commutes is a commutative ring104-- under the restricted operations, whether or not the ambient ring is.105theorem IsSubring.comm_ring_of_commutative (A add zero neg mul one S : Set)106  requires ring : IsRing(A, add, zero, neg, mul, one)107  requires subring : IsSubring(A, add, zero, neg, mul, one, S)108  requires commutative : Commutative(S, mul)109  shows IsCommRing(S, restrict(add, S × S), zero, restrict(neg, S),110    restrict(mul, S × S), one)111proof112  have subset := IsSubring.subset_carrier with subring113  have zeroIn := IsSubring.zero_closed with subring114  have oneIn := IsSubring.one_closed with subring115  have addClosed := IsSubring.add_closed with subring116  have mulClosed := IsSubring.mul_closed with subring117  have negClosed := IsSubring.neg_closed with subring118  have addition : IsMagma(A, add) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]119  have multiplication : IsMagma(A, mul) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]120  have addAssoc : Associative(A, add) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]121  have mulAssoc : Associative(A, mul) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]122  have addComm : Commutative(A, add) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]123  have addUnit : Identity(A, add, zero) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]124  have mulUnit : Identity(A, mul, one) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]125  have inverse : Inverse(A, add, zero, neg) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]126  have distribute : Distributive(A, add, mul) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]127  have negation : neg : A → A by simp [Inverse]128  have addFunction := restrictBinary.function at A, S, add with *129  have mulFunction := restrictBinary.function at A, S, mul with *130  have restrictedAdd : IsMagma(S, restrict(add, S × S)) by exact addFunction131  have restrictedMul : IsMagma(S, restrict(mul, S × S)) by exact mulFunction132  have rAddAssoc := restrictBinary.associative at A, S, add with *133  have rMulAssoc := restrictBinary.associative at A, S, mul with *134  have rAddComm := restrictBinary.commutative at A, S, add with *135  have rMulComm := restrictBinary.commutative_on at A, S, mul with *136  have rAddUnit := restrictBinary.identity at A, S, add, zero with *137  have rMulUnit := restrictBinary.identity at A, S, mul, one with *138  have rInverse := restrictUnary.inverse with *139  have rDistribute := restrictBinary.distributive with *140  simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]141142section Centralizers143variable (T S : Set)144hypothesis ring : Ring(T)145hypothesis bounded : S ⊆ Ring.carrier(T)146147theorem ringCentralizer.subset148  shows ringCentralizer(T, S) ⊆ Ring.carrier(T)149proof150  intros z hz151  have member := ringCentralizer.membership.forward with hz152  exact member.left153154theorem ringCentralizer.commutes (z x : Set)155  requires central : z ∈ ringCentralizer(T, S)156  requires element : x ∈ S157  shows call2(Ring.mul(T), z, x) = call2(Ring.mul(T), x, z)158proof159  have member := ringCentralizer.membership.forward with central160  exact member.right with x, element161162theorem ringCentralizer.mem (z : Set)163  requires element : z ∈ Ring.carrier(T)164  requires commutes : ∀ x ∈ S, call2(Ring.mul(T), z, x) = call2(Ring.mul(T), x, z)165  shows z ∈ ringCentralizer(T, S)166proof167  exact ringCentralizer.membership.backward with ⟨element, commutes⟩168169theorem ringCentralizer.subring170  shows IsSubring(Ring.carrier(T), Ring.add(T), Ring.zero(T), Ring.neg(T),171    Ring.mul(T), Ring.one(T), ringCentralizer(T, S))172proof173  have parts := Ring.parts with ring174  have subset := ringCentralizer.subset at T, S with *175  have monoid := IsRing.multiplicative with parts176  have assoc := IsMonoid.associative with monoid177  have distributive := IsRing.distributive with parts178  have zeroIn : Ring.zero(T) ∈ ringCentralizer(T, S)179    have zeroCarrier := IsRing.zero_in_carrier with parts180    have commutes : ∀ x ∈ S, call2(Ring.mul(T), Ring.zero(T), x) = call2(Ring.mul(T), x, Ring.zero(T))181      intros x hx182      have xIn := bounded with x, hx183      have left := IsRing.zero_mul with parts, xIn184      have right := IsRing.mul_zero with parts, xIn185      cc186    exact ringCentralizer.mem with *187  have oneIn : Ring.one(T) ∈ ringCentralizer(T, S)188    have oneCarrier := IsMonoid.unit_in_carrier with monoid189    have commutes : ∀ x ∈ S, call2(Ring.mul(T), Ring.one(T), x) = call2(Ring.mul(T), x, Ring.one(T))190      intros x hx191      have xIn := bounded with x, hx192      have left := IsMonoid.left_identity with monoid, xIn193      have right := IsMonoid.right_identity with monoid, xIn194      cc195    exact ringCentralizer.mem with *196  have negClosed : ClosedUnary(ringCentralizer(T, S), Ring.neg(T))197    intros z hz198    have zIn := subset with z, hz199    have negIn := IsRing.neg_closed with parts, zIn200    have commutes : ∀ x ∈ S, call2(Ring.mul(T), Ring.neg(T)(z), x) = call2(Ring.mul(T), x, Ring.neg(T)(z))201      intros x hx202      have xIn := bounded with x, hx203      have swap := ringCentralizer.commutes at T, S, z, x with *204      have left := IsRing.neg_mul with parts, zIn, xIn205      have right := IsRing.mul_neg with parts, xIn, zIn206      cc207    exact ringCentralizer.mem with *208  have addClosed : ClosedBinary(ringCentralizer(T, S), Ring.add(T))209    intros z hz w hw210    have zIn := subset with z, hz211    have wIn := subset with w, hw212    have sumIn := IsRing.add_closed with parts, zIn, wIn213    have commutes : ∀ x ∈ S, call2(Ring.mul(T), call2(Ring.add(T), z, w), x) = call2(Ring.mul(T), x, call2(Ring.add(T), z, w))214      intros x hx215      have xIn := bounded with x, hx216      have swapZ := ringCentralizer.commutes at T, S, z, x with *217      have swapW := ringCentralizer.commutes at T, S, w, x with *218      have left := distributive with z, zIn, w, wIn, x, xIn219      have right := distributive with x, xIn, z, zIn, w, wIn220      have expandLeft := left.right221      have expandRight := right.left222      cc223    exact ringCentralizer.mem with *224  have mulClosed : ClosedBinary(ringCentralizer(T, S), Ring.mul(T))225    intros z hz w hw226    have zIn := subset with z, hz227    have wIn := subset with w, hw228    have productIn := IsRing.mul_closed with parts, zIn, wIn229    have commutes : ∀ x ∈ S, call2(Ring.mul(T), call2(Ring.mul(T), z, w), x) = call2(Ring.mul(T), x, call2(Ring.mul(T), z, w))230      intros x hx231      have xIn := bounded with x, hx232      have swapZ := ringCentralizer.commutes at T, S, z, x with *233      have swapW := ringCentralizer.commutes at T, S, w, x with *234      have first := assoc with z, zIn, w, wIn, x, xIn235      have second := assoc with z, zIn, x, xIn, w, wIn236      have third := assoc with x, xIn, z, zIn, w, wIn237      cc238    exact ringCentralizer.mem with *239  unfold IsSubring240  exact ⟨subset, zeroIn, oneIn, negClosed, addClosed, mulClosed⟩241242theorem bicommutant.subset243  shows bicommutant(T, S) ⊆ Ring.carrier(T)244proof245  have central := ringCentralizer.subset at T, S with *246  unfold bicommutant247  exact ringCentralizer.subset at T, ringCentralizer(T, S) with *248249theorem bicommutant.contains250  shows S ⊆ bicommutant(T, S)251proof252  intros s hs253  have sIn := bounded with s, hs254  have central := ringCentralizer.subset at T, S with *255  have commutes : ∀ c ∈ ringCentralizer(T, S), call2(Ring.mul(T), s, c) = call2(Ring.mul(T), c, s)256    intros c hc257    have swap := ringCentralizer.commutes at T, S, c, s with *258    cc259  unfold bicommutant260  exact ringCentralizer.mem at T, ringCentralizer(T, S), s with *261262theorem bicommutant.subring263  shows IsSubring(Ring.carrier(T), Ring.add(T), Ring.zero(T), Ring.neg(T),264    Ring.mul(T), Ring.one(T), bicommutant(T, S))265proof266  have central := ringCentralizer.subset at T, S with *267  unfold bicommutant268  exact ringCentralizer.subring at T, ringCentralizer(T, S) with *269270-- When the generators commute with each other, the bicommutant commutes.271theorem bicommutant.commutative272  requires commuting : S ⊆ ringCentralizer(T, S)273  shows Commutative(bicommutant(T, S), Ring.mul(T))274proof275  have central := ringCentralizer.subset at T, S with *276  have double := bicommutant.subset at T, S with *277  intros b hb c hc278  have cIn := double with c, hc279  unfold bicommutant at hb280  unfold bicommutant at hc281  have cCentral : c ∈ ringCentralizer(T, S)282    have commutes : ∀ s ∈ S, call2(Ring.mul(T), c, s) = call2(Ring.mul(T), s, c)283      intros s hs284      have sCentral := commuting with s, hs285      exact ringCentralizer.commutes at T, ringCentralizer(T, S), c, s with *286    exact ringCentralizer.mem at T, S, c with *287  exact ringCentralizer.commutes at T, ringCentralizer(T, S), b, c with *288289theorem bicommutantRing.comm_ring290  requires commuting : S ⊆ ringCentralizer(T, S)291  shows CommRing(bicommutantRing(T, S))292proof293  have parts := Ring.parts with ring294  have subring := bicommutant.subring at T, S with *295  have commutative := bicommutant.commutative at T, S with *296  have engine := IsSubring.comm_ring_of_commutative with parts, subring, commutative297  unfold bicommutantRing298  unfold subringRing299  exact CommRing.of_parts with engine300301-- A single element commutes with itself, so its bicommutant is a302-- commutative ring containing it.303theorem bicommutant.singleton_commuting (a : Set)304  requires element : a ∈ Ring.carrier(T)305  shows {a} ⊆ ringCentralizer(T, {a})306proof307  intros s hs308  have equal := singleton.membership.forward with hs309  rw equal310  have commutes : ∀ x ∈ {a}, call2(Ring.mul(T), a, x) = call2(Ring.mul(T), x, a)311    intros x hx312    have same := singleton.membership.forward with hx313    rw same314    rfl315  exact ringCentralizer.mem at T, {a}, a with *316317end Centralizers318