-- A homomorphism separating denominators from a nonzero kernel element obstructs localization.
-- 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.Field.LocalizationObstruction
import Localization
import Powers
import Set.OrderTransport

section Maps
variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e g h D : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
notation ring U := (C, sum, o, inverse, product, e)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis residue : IsCommRing(U)
hypothesis embedding : IsRingHom(g, R, S)
hypothesis injective : InjectiveBetween(g, R, S)
hypothesis evaluation : IsRingHom(h, R, U)
hypothesis bounded : D ⊆ R
hypothesis avoids : ∀ d ∈ D, h(d) ≠ U[0]

theorem localizationWithin.excludes_kernel_inverse (p y : Set)
  requires member : p ∈ R
  requires vanishes : h(p) = U[0]
  requires inverseP : IsInverse(B, times, unit, g(p), y)
  shows ¬(y ∈ localizationWithin(S, functionImage(g, R, S), functionImage(g, D, S)))
proof
  have ordinary := IsCommRing.ring with source
  have imageP := IsRingHom.closed with embedding, member
  have data := inverseP
  have inY := data.right.left
  have cancels := data.right.right.left
  intro localized
  obtain ⟨inB, d, hd, numerator⟩ := localizationWithin.membership.forward with localized
  obtain ⟨inD, a, ha, valueD⟩ := functionImage.membership.forward with hd
  obtain ⟨inProduct, q, hq, valueQ⟩ := functionImage.membership.forward with numerator
  have aIn : a ∈ R by simp [Subset]
  have qpIn := IsRing.mul_closed with ordinary, hq, member
  have mapped := IsRingHom.mul with embedding, hq, member
  have equation : g(R[q * p]) = g(a)
    have rearrange : S[(d * y) * g(p)] = S[d * (y * g(p))] by ring
    rw cancels at rearrange
    have identity : S[d * 1] = d by ring
    cc
  have equal := Injective.apply_cancel with injective, qpIn, aIn, equation
  have evaluated := IsRingHom.mul with evaluation, hq, member
  have valueQin := IsRingHom.closed with evaluation, hq
  have zeroProduct : U[h(q) * 0] = U[0] by ring
  have zeroValue : h(a) = U[0] by cc
  have distinct := avoids with a, ha
  exact distinct with zeroValue

end Maps

section Nonfields
variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e g h D T : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
notation ring U := (C, sum, o, inverse, product, e)
notation ring L := S ↾ T
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis residue : IsCommRing(U)
hypothesis embedding : IsRingHom(g, R, S)
hypothesis injective : InjectiveBetween(g, R, S)
hypothesis evaluation : IsRingHom(h, R, U)
hypothesis bounded : D ⊆ R
hypothesis avoids : ∀ d ∈ D, h(d) ≠ U[0]
hypothesis denominatorOne : R[1] ∈ D
hypothesis carrier : T = localizationWithin(S, functionImage(g, R, S), functionImage(g, D, S))

theorem localizationWithin.not_field_of_kernel (p : Set)
  requires member : p ∈ R
  requires nonzero : p ≠ R[0]
  requires vanishes : h(p) = U[0]
  shows ¬IsField(L)
proof
  have ordinary := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have zeroValue := IsRingHom.zero with embedding
  have oneValue := IsRingHom.one with embedding
  have image := IsRingHom.closed with embedding, member
  have targetRing := IsCommRing.ring with target
  have monoid := IsRing.multiplicative with targetRing
  have oneIn := IsMonoid.unit_in_carrier with monoid
  have multiplication : IsMagma(B, times) by simp [IsMonoid, IsSemigroup]
  have subset : T ⊆ S
    rw carrier
    exact localizationWithin.subset
  have imageNonzero : g(p) ≠ S[0]
    intro equal
    have mapped : g(p) = g(R[0]) by cc
    have impossible := Injective.apply_cancel with injective, member, zeroIn, mapped
    exact nonzero with impossible
  have function := IsRingHom.function with embedding
  have numerator := functionImage.value with function, member
  have denominator : S[1] ∈ functionImage(g, D, B)
    apply functionImage.membership.backward
    refine ⟨oneIn, R[1], denominatorOne, ?_⟩
    cc
  have localized : g(p) ∈ T
    rw carrier
    apply localizationWithin.membership.backward
    refine ⟨image, S[1], denominator, ?_⟩
    have identity : S[1 * g(p)] = g(p) by ring
    rwa identity
  intro field
  obtain ⟨y, inverseP⟩ := IsField.inverse_exists with field, localized, imageNonzero
  unfold IsInverse at inverseP
  have inY := inverseP.right.left
  have ambientY : y ∈ S by simp [Subset]
  have leftValue := restrictBinary.value_on_subset at B, T, times, y, g(p) with *
  have rightValue := restrictBinary.value_on_subset at B, T, times, g(p), y with *
  have leftInverse : S[y * g(p)] = S[1] by cc
  have rightInverse : S[g(p) * y] = S[1] by cc
  have ambientInverse : IsInverse(B, times, unit, g(p), y) by simp [IsInverse]
  have excluded := localizationWithin.excludes_kernel_inverse with source, target, residue, embedding, injective, evaluation, bounded, avoids, member, vanishes, ambientInverse
  rw carrier at inY
  exact excluded with inY

end Nonfields

section Fields
variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e g h D : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
notation ring U := (C, sum, o, inverse, product, e)
hypothesis source : IsCommRing(R)
hypothesis field : IsField(S)
hypothesis residue : IsCommRing(U)
hypothesis embedding : IsRingHom(g, R, S)
hypothesis injective : InjectiveBetween(g, R, S)
hypothesis evaluation : IsRingHom(h, R, U)
hypothesis bounded : D ⊆ R
hypothesis avoids : ∀ d ∈ D, h(d) ≠ U[0]

theorem localizationWithin.proper_of_kernel (p : Set)
  requires member : p ∈ R
  requires nonzero : p ≠ R[0]
  requires vanishes : h(p) = U[0]
  shows localizationWithin(S, functionImage(g, R, S), functionImage(g, D, S)) ≠ S
proof
  have target := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have zeroValue := IsRingHom.zero with embedding
  have image := IsRingHom.closed with embedding, member
  have imageNonzero : g(p) ≠ S[0]
    intro zero
    have equal : g(p) = g(R[0]) by cc
    have impossible := Injective.apply_cancel with injective, member, zeroIn, equal
    exact nonzero with impossible
  obtain ⟨y, inverseP⟩ := IsField.inverse_exists with field, imageNonzero
  have excluded := localizationWithin.excludes_kernel_inverse with source, target, residue, embedding, injective, evaluation, bounded, avoids, member, vanishes, inverseP
  have inY : y ∈ S by simp [IsInverse]
  intro equal
  have included : y ∈ localizationWithin(S, functionImage(g, R, S), functionImage(g, D, S)) by rwa equal
  exact excluded with included

end Fields