-- Centralizers and bicommutants in a ring: the elements commuting with a
-- set S form a subring, the bicommutant of a commuting set is a commutative
-- subring containing it, and bicommutantRing(T, S) is that commutative
-- ring; everything here is ZF
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Ring.Bicommutant
import Subring

-- The centralizer of S in T, the bicommutant, and the ring on the latter
-- with the operations of T restricted.
def ringCentralizer (T S : Set) : Set :=
  { z ∈ Ring.carrier(T) |
    ∀ x ∈ S, call2(Ring.mul(T), z, x) = call2(Ring.mul(T), x, z) }
def bicommutant (T S : Set) : Set := ringCentralizer(T, ringCentralizer(T, S))
def bicommutantRing (T S : Set) : Set := subringRing(T, bicommutant(T, S))

theorem bicommutantRing.carrierOf (T S : Set)
  shows Ring.carrier(bicommutantRing(T, S)) = bicommutant(T, S)
proof
  simp [bicommutantRing, subringRing, Ring.mk.carrier]

theorem bicommutantRing.addOf (T S : Set)
  shows Ring.add(bicommutantRing(T, S)) =
    restrict(Ring.add(T), bicommutant(T, S) × bicommutant(T, S))
proof
  simp [bicommutantRing, subringRing, Ring.mk.add]

theorem bicommutantRing.zeroOf (T S : Set)
  shows Ring.zero(bicommutantRing(T, S)) = Ring.zero(T)
proof
  simp [bicommutantRing, subringRing, Ring.mk.zero]

theorem bicommutantRing.negOf (T S : Set)
  shows Ring.neg(bicommutantRing(T, S)) = restrict(Ring.neg(T), bicommutant(T, S))
proof
  simp [bicommutantRing, subringRing, Ring.mk.neg]

theorem bicommutantRing.mulOf (T S : Set)
  shows Ring.mul(bicommutantRing(T, S)) =
    restrict(Ring.mul(T), bicommutant(T, S) × bicommutant(T, S))
proof
  simp [bicommutantRing, subringRing, Ring.mk.mul]

theorem bicommutantRing.oneOf (T S : Set)
  shows Ring.one(bicommutantRing(T, S)) = Ring.one(T)
proof
  simp [bicommutantRing, subringRing, Ring.mk.one]

-- Multiplication by a negation in a ring that need not commute.
theorem IsRing.mul_neg (A add zero neg mul one x y : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows call2(mul, x, neg(y)) = neg(call2(mul, x, y))
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have monoid := IsGroup.monoid with group
  have distributive := IsRing.distributive with ring
  have negIn := IsRing.neg_closed with ring, yInA
  have product := IsRing.mul_closed with ring, xInA, yInA
  have negProduct := IsRing.mul_closed with ring, xInA, negIn
  have inverseIn := IsRing.neg_closed with ring, product
  have zeroIn := IsRing.zero_in_carrier with ring
  have rightLaw := distributive with x, xInA, y, yInA, neg(y), negIn
  have leftLaw := distributive with x, xInA, neg(y), negIn, y, yInA
  have cancelRight := IsRing.add_inverse_right with ring, yInA
  have cancelLeft := IsRing.add_inverse_left with ring, yInA
  have vanish := IsRing.mul_zero with ring, xInA
  have first : IsInverse(A, add, zero, call2(mul, x, y), call2(mul, x, neg(y)))
    have sumRight := rightLaw.left
    have sumLeft := leftLaw.left
    rw cancelRight at sumRight
    rw cancelLeft at sumLeft
    unfold IsInverse
    refine ⟨product, negProduct, ?_, ?_⟩
    . cc
    . cc
  have second : IsInverse(A, add, zero, call2(mul, x, y), neg(call2(mul, x, y)))
    have left := IsRing.add_inverse_left with ring, product
    have right := IsRing.add_inverse_right with ring, product
    unfold IsInverse
    exact ⟨product, inverseIn, left, right⟩
  exact IsInverse.unique with monoid, first, second

theorem restrictBinary.commutative_on (A S op : Set)
  requires function : IsMagma(A, op)
  requires subset : S ⊆ A
  requires closed : ClosedBinary(S, op)
  requires law : Commutative(S, op)
  shows Commutative(S, restrict(op, S × S))
proof
  intros x hx y hy
  have first := restrictBinary.value with hx, hy
  have second := restrictBinary.value with hy, hx
  have original := law with x, hx, y, hy
  cc

-- A subring on which the multiplication commutes is a commutative ring
-- under the restricted operations, whether or not the ambient ring is.
theorem IsSubring.comm_ring_of_commutative (A add zero neg mul one S : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires subring : IsSubring(A, add, zero, neg, mul, one, S)
  requires commutative : Commutative(S, mul)
  shows IsCommRing(S, restrict(add, S × S), zero, restrict(neg, S),
    restrict(mul, S × S), one)
proof
  have subset := IsSubring.subset_carrier with subring
  have zeroIn := IsSubring.zero_closed with subring
  have oneIn := IsSubring.one_closed with subring
  have addClosed := IsSubring.add_closed with subring
  have mulClosed := IsSubring.mul_closed with subring
  have negClosed := IsSubring.neg_closed with subring
  have addition : IsMagma(A, add) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have multiplication : IsMagma(A, mul) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have addAssoc : Associative(A, add) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have mulAssoc : Associative(A, mul) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have addComm : Commutative(A, add) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have addUnit : Identity(A, add, zero) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have mulUnit : Identity(A, mul, one) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have inverse : Inverse(A, add, zero, neg) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have distribute : Distributive(A, add, mul) by simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have negation : neg : A → A by simp [Inverse]
  have addFunction := restrictBinary.function at A, S, add with *
  have mulFunction := restrictBinary.function at A, S, mul with *
  have restrictedAdd : IsMagma(S, restrict(add, S × S)) by exact addFunction
  have restrictedMul : IsMagma(S, restrict(mul, S × S)) by exact mulFunction
  have rAddAssoc := restrictBinary.associative at A, S, add with *
  have rMulAssoc := restrictBinary.associative at A, S, mul with *
  have rAddComm := restrictBinary.commutative at A, S, add with *
  have rMulComm := restrictBinary.commutative_on at A, S, mul with *
  have rAddUnit := restrictBinary.identity at A, S, add, zero with *
  have rMulUnit := restrictBinary.identity at A, S, mul, one with *
  have rInverse := restrictUnary.inverse with *
  have rDistribute := restrictBinary.distributive with *
  simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]

section Centralizers
variable (T S : Set)
hypothesis ring : Ring(T)
hypothesis bounded : S ⊆ Ring.carrier(T)

theorem ringCentralizer.subset
  shows ringCentralizer(T, S) ⊆ Ring.carrier(T)
proof
  intros z hz
  have member := ringCentralizer.membership.forward with hz
  exact member.left

theorem ringCentralizer.commutes (z x : Set)
  requires central : z ∈ ringCentralizer(T, S)
  requires element : x ∈ S
  shows call2(Ring.mul(T), z, x) = call2(Ring.mul(T), x, z)
proof
  have member := ringCentralizer.membership.forward with central
  exact member.right with x, element

theorem ringCentralizer.mem (z : Set)
  requires element : z ∈ Ring.carrier(T)
  requires commutes : ∀ x ∈ S, call2(Ring.mul(T), z, x) = call2(Ring.mul(T), x, z)
  shows z ∈ ringCentralizer(T, S)
proof
  exact ringCentralizer.membership.backward with ⟨element, commutes⟩

theorem ringCentralizer.subring
  shows IsSubring(Ring.carrier(T), Ring.add(T), Ring.zero(T), Ring.neg(T),
    Ring.mul(T), Ring.one(T), ringCentralizer(T, S))
proof
  have parts := Ring.parts with ring
  have subset := ringCentralizer.subset at T, S with *
  have monoid := IsRing.multiplicative with parts
  have assoc := IsMonoid.associative with monoid
  have distributive := IsRing.distributive with parts
  have zeroIn : Ring.zero(T) ∈ ringCentralizer(T, S)
    have zeroCarrier := IsRing.zero_in_carrier with parts
    have commutes : ∀ x ∈ S, call2(Ring.mul(T), Ring.zero(T), x) = call2(Ring.mul(T), x, Ring.zero(T))
      intros x hx
      have xIn := bounded with x, hx
      have left := IsRing.zero_mul with parts, xIn
      have right := IsRing.mul_zero with parts, xIn
      cc
    exact ringCentralizer.mem with *
  have oneIn : Ring.one(T) ∈ ringCentralizer(T, S)
    have oneCarrier := IsMonoid.unit_in_carrier with monoid
    have commutes : ∀ x ∈ S, call2(Ring.mul(T), Ring.one(T), x) = call2(Ring.mul(T), x, Ring.one(T))
      intros x hx
      have xIn := bounded with x, hx
      have left := IsMonoid.left_identity with monoid, xIn
      have right := IsMonoid.right_identity with monoid, xIn
      cc
    exact ringCentralizer.mem with *
  have negClosed : ClosedUnary(ringCentralizer(T, S), Ring.neg(T))
    intros z hz
    have zIn := subset with z, hz
    have negIn := IsRing.neg_closed with parts, zIn
    have commutes : ∀ x ∈ S, call2(Ring.mul(T), Ring.neg(T)(z), x) = call2(Ring.mul(T), x, Ring.neg(T)(z))
      intros x hx
      have xIn := bounded with x, hx
      have swap := ringCentralizer.commutes at T, S, z, x with *
      have left := IsRing.neg_mul with parts, zIn, xIn
      have right := IsRing.mul_neg with parts, xIn, zIn
      cc
    exact ringCentralizer.mem with *
  have addClosed : ClosedBinary(ringCentralizer(T, S), Ring.add(T))
    intros z hz w hw
    have zIn := subset with z, hz
    have wIn := subset with w, hw
    have sumIn := IsRing.add_closed with parts, zIn, wIn
    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))
      intros x hx
      have xIn := bounded with x, hx
      have swapZ := ringCentralizer.commutes at T, S, z, x with *
      have swapW := ringCentralizer.commutes at T, S, w, x with *
      have left := distributive with z, zIn, w, wIn, x, xIn
      have right := distributive with x, xIn, z, zIn, w, wIn
      have expandLeft := left.right
      have expandRight := right.left
      cc
    exact ringCentralizer.mem with *
  have mulClosed : ClosedBinary(ringCentralizer(T, S), Ring.mul(T))
    intros z hz w hw
    have zIn := subset with z, hz
    have wIn := subset with w, hw
    have productIn := IsRing.mul_closed with parts, zIn, wIn
    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))
      intros x hx
      have xIn := bounded with x, hx
      have swapZ := ringCentralizer.commutes at T, S, z, x with *
      have swapW := ringCentralizer.commutes at T, S, w, x with *
      have first := assoc with z, zIn, w, wIn, x, xIn
      have second := assoc with z, zIn, x, xIn, w, wIn
      have third := assoc with x, xIn, z, zIn, w, wIn
      cc
    exact ringCentralizer.mem with *
  unfold IsSubring
  exact ⟨subset, zeroIn, oneIn, negClosed, addClosed, mulClosed⟩

theorem bicommutant.subset
  shows bicommutant(T, S) ⊆ Ring.carrier(T)
proof
  have central := ringCentralizer.subset at T, S with *
  unfold bicommutant
  exact ringCentralizer.subset at T, ringCentralizer(T, S) with *

theorem bicommutant.contains
  shows S ⊆ bicommutant(T, S)
proof
  intros s hs
  have sIn := bounded with s, hs
  have central := ringCentralizer.subset at T, S with *
  have commutes : ∀ c ∈ ringCentralizer(T, S), call2(Ring.mul(T), s, c) = call2(Ring.mul(T), c, s)
    intros c hc
    have swap := ringCentralizer.commutes at T, S, c, s with *
    cc
  unfold bicommutant
  exact ringCentralizer.mem at T, ringCentralizer(T, S), s with *

theorem bicommutant.subring
  shows IsSubring(Ring.carrier(T), Ring.add(T), Ring.zero(T), Ring.neg(T),
    Ring.mul(T), Ring.one(T), bicommutant(T, S))
proof
  have central := ringCentralizer.subset at T, S with *
  unfold bicommutant
  exact ringCentralizer.subring at T, ringCentralizer(T, S) with *

-- When the generators commute with each other, the bicommutant commutes.
theorem bicommutant.commutative
  requires commuting : S ⊆ ringCentralizer(T, S)
  shows Commutative(bicommutant(T, S), Ring.mul(T))
proof
  have central := ringCentralizer.subset at T, S with *
  have double := bicommutant.subset at T, S with *
  intros b hb c hc
  have cIn := double with c, hc
  unfold bicommutant at hb
  unfold bicommutant at hc
  have cCentral : c ∈ ringCentralizer(T, S)
    have commutes : ∀ s ∈ S, call2(Ring.mul(T), c, s) = call2(Ring.mul(T), s, c)
      intros s hs
      have sCentral := commuting with s, hs
      exact ringCentralizer.commutes at T, ringCentralizer(T, S), c, s with *
    exact ringCentralizer.mem at T, S, c with *
  exact ringCentralizer.commutes at T, ringCentralizer(T, S), b, c with *

theorem bicommutantRing.comm_ring
  requires commuting : S ⊆ ringCentralizer(T, S)
  shows CommRing(bicommutantRing(T, S))
proof
  have parts := Ring.parts with ring
  have subring := bicommutant.subring at T, S with *
  have commutative := bicommutant.commutative at T, S with *
  have engine := IsSubring.comm_ring_of_commutative with parts, subring, commutative
  unfold bicommutantRing
  unfold subringRing
  exact CommRing.of_parts with engine

-- A single element commutes with itself, so its bicommutant is a
-- commutative ring containing it.
theorem bicommutant.singleton_commuting (a : Set)
  requires element : a ∈ Ring.carrier(T)
  shows {a} ⊆ ringCentralizer(T, {a})
proof
  intros s hs
  have equal := singleton.membership.forward with hs
  rw equal
  have commutes : ∀ x ∈ {a}, call2(Ring.mul(T), a, x) = call2(Ring.mul(T), x, a)
    intros x hx
    have same := singleton.membership.forward with hx
    rw same
    rfl
  exact ringCentralizer.mem at T, {a}, a with *

end Centralizers