-- Localization inside an ambient commutative ring, with explicit denominators (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.Localization
import Ring.GeneratedSubring
import Field.Construction
import Cardinal.ListSupport

predicate Denominators (B times z unit T D : Set) :=
  D ⊆ T ∧ unit ∈ D ∧ ClosedBinary(D, times) ∧ (∀ d ∈ D, d ≠ z)

notation scoped Denominators(R, T, D) => Denominators(R.carrier, R.mul, R.zero, R.one, T, D)

def localizationWithin (B times T D : Set) : Set :=
  {x ∈ B | ∃ d ∈ D, times(d, x) ∈ T}

notation scoped localizationWithin(R, T, D) => localizationWithin(R.carrier, R.mul, T, D)

theorem localizationWithin.subset (B times T D : Set)
  shows localizationWithin(B, times, T, D) ⊆ B
proof
  simp

section Rings
variable (B plus z minus times unit T D : Set)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis ring : IsCommRing(S)
hypothesis subring : IsSubring(S, T)
hypothesis denominators : Denominators(S, T, D)

theorem Denominators.subset
  shows D ⊆ T
proof
  simp [Denominators]

theorem Denominators.one_mem
  shows S[1] ∈ D
proof
  simp [Denominators]

theorem Denominators.mul_closed
  shows ClosedBinary(D, times)
proof
  simp [Denominators]

theorem Denominators.nonzero (d : Set)
  requires member : d ∈ D
  shows d ≠ S[0]
proof
  exact denominators.right.right.right with d, member

theorem localizationWithin.contains
  shows T ⊆ localizationWithin(S, T, D)
proof
  have ordinary := IsCommRing.ring with ring
  have bounded := IsSubring.subset_carrier with subring
  have one := Denominators.one_mem with *
  intros x hx
  have inB : x ∈ S by simp [Subset]
  have equation : S[1 * x] = x by ring
  apply localizationWithin.membership.backward
  refine ⟨inB, unit, one, ?_⟩
  rwa equation

theorem localizationWithin.subring
  shows IsSubring(S, localizationWithin(S, T, D))
proof
  have ordinary := IsCommRing.ring with ring
  have bounded := IsSubring.subset_carrier with subring
  have denomBound := Denominators.subset with *
  have denomClosed := Denominators.mul_closed with *
  have denomAmbient := Subset.transitive with denomBound, bounded
  have contains := localizationWithin.contains with *
  have subset := localizationWithin.subset at B, times, T, D
  have zero := IsSubring.zero_closed with subring
  have one := IsSubring.one_closed with subring
  have zeroMem : S[0] ∈ localizationWithin(S, T, D) by simp [Subset]
  have oneMem : S[1] ∈ localizationWithin(S, T, D) by simp [Subset]
  have negClosed := IsSubring.neg_closed with subring
  have addClosed := IsSubring.add_closed with subring
  have mulClosed := IsSubring.mul_closed with subring
  have negative : ClosedUnary(localizationWithin(S, T, D), minus)
    intros x hx
    obtain ⟨inB, d, hd, cleared⟩ := localizationWithin.membership.forward with hx
    have dIn : d ∈ S by simp [Subset]
    have closed := IsRing.neg_closed with ordinary, inB
    have numerator := ClosedUnary.mem with negClosed, cleared
    have equation : S[d * (-x)] = S[-(d * x)] by ring
    apply localizationWithin.membership.backward
    refine ⟨closed, d, hd, ?_⟩
    rwa equation
  have addition : ClosedBinary(localizationWithin(S, T, D), plus)
    intros x hx y hy
    obtain ⟨inX, d, hd, numeratorX⟩ := localizationWithin.membership.forward with hx
    obtain ⟨inY, e, he, numeratorY⟩ := localizationWithin.membership.forward with hy
    have dIn : d ∈ S by simp [Subset]
    have eIn : e ∈ S by simp [Subset]
    have dInT : d ∈ T by simp [Subset]
    have eInT : e ∈ T by simp [Subset]
    have denominator := ClosedBinary.mem with denomClosed, hd, he
    have left := ClosedBinary.mem with mulClosed, eInT, numeratorX
    have right := ClosedBinary.mem with mulClosed, dInT, numeratorY
    have numerator := ClosedBinary.mem with addClosed, left, right
    have closed := IsRing.add_closed with ordinary, inX, inY
    have equation : S[(d * e) * (x + y)] = S[e * (d * x) + d * (e * y)] by ring
    apply localizationWithin.membership.backward
    refine ⟨closed, S[d * e], denominator, ?_⟩
    rwa equation
  have multiplication : ClosedBinary(localizationWithin(S, T, D), times)
    intros x hx y hy
    obtain ⟨inX, d, hd, numeratorX⟩ := localizationWithin.membership.forward with hx
    obtain ⟨inY, e, he, numeratorY⟩ := localizationWithin.membership.forward with hy
    have dIn : d ∈ S by simp [Subset]
    have eIn : e ∈ S by simp [Subset]
    have denominator := ClosedBinary.mem with denomClosed, hd, he
    have numerator := ClosedBinary.mem with mulClosed, numeratorX, numeratorY
    have closed := IsRing.mul_closed with ordinary, inX, inY
    have equation : S[(d * e) * (x * y)] = S[(d * x) * (e * y)] by ring
    apply localizationWithin.membership.backward
    refine ⟨closed, S[d * e], denominator, ?_⟩
    rwa equation
  unfold IsSubring
  refine ⟨subset, zeroMem, oneMem, negative, addition, multiplication⟩

theorem localizationWithin.inverse_mem (d y : Set)
  requires member : d ∈ D
  requires inverse : IsInverse(B, times, unit, d, y)
  shows y ∈ localizationWithin(S, T, D)
proof
  have one := IsSubring.one_closed with subring
  apply localizationWithin.membership.backward
  refine ⟨inverse.right.left, d, member, ?_⟩
  have cancels := inverse.right.right.right
  rwa cancels

theorem localizationWithin.least (V : Set)
  requires larger : IsSubring(S, V)
  requires included : T ⊆ V
  requires inverses : ∀ d ∈ D, ∃ y ∈ V, IsInverse(B, times, unit, d, y)
  shows localizationWithin(S, T, D) ⊆ V
proof
  have bound := IsSubring.subset_carrier with subring
  have denomBound := Denominators.subset with *
  have ambient := Subset.transitive with denomBound, bound
  have closure := IsSubring.mul_closed with larger
  intros x hx
  obtain ⟨inX, d, hd, numerator⟩ := localizationWithin.membership.forward with hx
  obtain ⟨y, hy, inverse⟩ := inverses with d, hd
  have dIn : d ∈ S by simp [Subset]
  have inV : S[d * x] ∈ V by simp [Subset]
  have inY := inverse.right.left
  have cancels := inverse.right.right.left
  have member := ClosedBinary.mem with closure, hy, inV
  have equation : S[y * (d * x)] = x
    have associate : S[y * (d * x)] = S[(y * d) * x] by ring
    rw [associate, cancels]
    ring
  rwa equation at member

end Rings