-- Ideal images, inverse images, and correspondence under surjections.
-- 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.Correspondence
import Image

def idealComap (f A J : Set) : Set := {x ∈ A | f(x) ∈ J}
def idealMap (f B I : Set) : Set := functionImage(f, I, B)

theorem idealMap.membership (f B I y : Set)
  shows y ∈ idealMap(f, B, I) ↔ y ∈ B ∧ ∃ x ∈ I, y = f(x)
proof
  simpa [idealMap] using functionImage.membership at f, I, B, y

theorem idealMap.value (f A B I x : Set)
  requires function : f : A → B
  requires hx : x ∈ A
  requires member : x ∈ I
  shows f(x) ∈ idealMap(f, B, I)
proof
  have valueIn := FunctionBetween.apply_closed with function, hx
  exact idealMap.membership.backward with ⟨valueIn, x, member, rfl⟩

theorem idealComap.monotone (f A I J : Set)
  requires subset : I ⊆ J
  shows idealComap(f, A, I) ⊆ idealComap(f, A, J)
proof
  intros x hx
  have data := idealComap.membership.forward with hx
  have mapped := subset with f(x), data.right
  exact idealComap.membership.backward with ⟨data.left, mapped⟩

theorem idealMap.monotone (f B I J : Set)
  requires subset : I ⊆ J
  shows idealMap(f, B, I) ⊆ idealMap(f, B, J)
proof
  intros y hy
  obtain ⟨yIn, x, hx, shape⟩ := idealMap.membership.forward with hy
  have xIn := subset with x, hx
  exact idealMap.membership.backward with ⟨yIn, x, xIn, shape⟩

theorem idealMap.galois (f A B I J : Set)
  requires function : f : A → B
  requires bounded : I ⊆ A
  shows idealMap(f, B, I) ⊆ J ↔ I ⊆ idealComap(f, A, J)
proof
  constructor
  . intros mapped x hx
    have xIn := bounded with x, hx
    have image := idealMap.value with function, xIn, hx
    have output := mapped with f(x), image
    exact idealComap.membership.backward with ⟨xIn, output⟩
  . intros included y hy
    obtain ⟨yIn, u, hu, shape⟩ := idealMap.membership.forward with hy
    have preimage := included with u, hu
    have data := idealComap.membership.forward with preimage
    rw shape
    exact data.right

theorem idealMap.comap_eq (f A B J : Set)
  requires onto : SurjectiveBetween(f, A, B)
  requires bounded : J ⊆ B
  shows idealMap(f, B, idealComap(f, A, J)) = J
proof
  have function := Surjective.function with onto
  ext y
  constructor
  . intro hy
    obtain ⟨yIn, x, hx, shape⟩ := idealMap.membership.forward with hy
    have data := idealComap.membership.forward with hx
    rw shape
    exact data.right
  . intro hy
    have yIn := bounded with y, hy
    obtain ⟨u, hu, edge⟩ := onto.right with y, yIn
    have value := FunctionBetween.apply_value with *
    have preimage : u ∈ idealComap(f, A, J)
      apply idealComap.membership.backward
      refine ⟨hu, ?_⟩
      rwa value
    apply idealMap.membership.backward
    refine ⟨yIn, u, preimage, ?_⟩
    cc

section RingMaps
variable (f A add zero neg mul one B plus z minus times unit : Set)
hypothesis source : IsCommRing(A, add, zero, neg, mul, one)
hypothesis target : IsCommRing(B, plus, z, minus, times, unit)
hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)

theorem IsRingHom.comap_ideal (J : Set)
  requires ideal : IsIdeal(B, plus, z, minus, times, J)
  shows IsIdeal(A, add, zero, neg, mul, idealComap(f, A, J))
proof
  have function := IsRingHom.function with hom
  have ring := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier with ring
  have zeroValue := IsRingHom.zero with hom
  have zeroMember := IsIdeal.zero_closed with ideal
  unfold IsIdeal
  refine ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩
  . settle with Subset, idealComap.membership
  . apply idealComap.membership.backward at f, A, J, zero
    refine ⟨zeroIn, ?_⟩
    rwa zeroValue
  . intros x hx y hy
    have dx := idealComap.membership.forward with hx
    have dy := idealComap.membership.forward with hy
    have closed := IsRing.add_closed with ring, dx.left, dy.left
    have mapped := IsRingHom.add with hom, dx.left, dy.left
    have member := IsIdeal.add_closed with ideal, dx.right, dy.right
    apply idealComap.membership.backward
    refine ⟨closed, ?_⟩
    rwa mapped
  . intros x hx
    have data := idealComap.membership.forward with hx
    have closed := IsRing.neg_closed with ring, data.left
    have mapped := IsRingHom.neg with hom, data.left
    have member := IsIdeal.neg_closed with ideal, data.right
    apply idealComap.membership.backward
    refine ⟨closed, ?_⟩
    rwa mapped
  . intros a ha x hx
    have data := idealComap.membership.forward with hx
    have fa := IsRingHom.closed with hom, ha
    have leftClosed := IsRing.mul_closed with ring, ha, data.left
    have rightClosed := IsRing.mul_closed with ring, data.left, ha
    have leftValue := IsRingHom.mul with hom, ha, data.left
    have rightValue := IsRingHom.mul with hom, data.left, ha
    have leftMember := IsIdeal.mul_left_closed with ideal, data.right
    have rightMember := IsIdeal.mul_right_closed with ideal, data.right
    constructor
    . apply idealComap.membership.backward at f, A, J, call2(mul, a, x)
      refine ⟨leftClosed, ?_⟩
      rwa leftValue
    . apply idealComap.membership.backward at f, A, J, call2(mul, x, a)
      refine ⟨rightClosed, ?_⟩
      rwa rightValue

theorem IsRingHom.kernel_subset_comap (J : Set)
  requires ideal : IsIdeal(B, plus, z, minus, times, J)
  shows ringKernel(f, A, z) ⊆ idealComap(f, A, J)
proof
  have zeroMember := IsIdeal.zero_closed with ideal
  intros x hx
  have data := ringKernel.membership.forward with hx
  apply idealComap.membership.backward
  refine ⟨data.left, ?_⟩
  rwa data.right

theorem IsRingHom.comap_map_eq (I : Set)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires contains : ringKernel(f, A, z) ⊆ I
  shows idealComap(f, A, idealMap(f, B, I)) = I
proof
  have function := IsRingHom.function with hom
  have bounded := IsIdeal.subset_carrier with ideal
  have included := contains
  ext x
  constructor
  . intro hx
    obtain ⟨xIn, imageMember⟩ := idealComap.membership.forward with hx
    obtain ⟨fxIn, y, hy, images⟩ := idealMap.membership.forward with imageMember
    have yIn := bounded with y, hy
    have congruent := IsRingHom.kernel_congruent.backward with source, target, hom, xIn, yIn, images
    have difference := included with call2(add, x, neg(y)), congruent
    have sum := IsIdeal.add_closed with ideal, difference, hy
    ring_nf at sum
    exact sum
  . intro hx
    have xIn := bounded with x, hx
    have image := idealMap.value with function, xIn, hx
    exact idealComap.membership.backward with ⟨xIn, image⟩

section Surjections
hypothesis onto : SurjectiveBetween(f, A, B)

theorem IsRingHom.map_ideal (I : Set)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows IsIdeal(B, plus, z, minus, times, idealMap(f, B, I))
proof
  have function := IsRingHom.function with hom
  have ring := IsCommRing.ring with source
  have bounded := IsIdeal.subset_carrier with ideal
  have ontoLaw := onto
  have zeroMember := IsIdeal.zero_closed with ideal
  have zeroIn := bounded with zero, zeroMember
  have zeroImage := idealMap.value with function, zeroIn, zeroMember
  have zeroValue := IsRingHom.zero with hom
  unfold IsIdeal
  refine ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩
    intros y hy
    have data := idealMap.membership.forward with hy
    exact data.left
  . cc
  . intros y hy w hw
    obtain ⟨yIn, a, ha, sy⟩ := idealMap.membership.forward with hy
    obtain ⟨wIn, b, hb, sw⟩ := idealMap.membership.forward with hw
    have aIn := bounded with a, ha
    have bIn := bounded with b, hb
    have closed := IsRing.add_closed with ring, aIn, bIn
    have member := IsIdeal.add_closed with ideal, ha, hb
    have mapped := IsRingHom.add with hom, aIn, bIn
    have image := idealMap.value with function, closed, member
    cc
  . intros y hy
    obtain ⟨yIn, c, hc, shape⟩ := idealMap.membership.forward with hy
    have cIn := bounded with c, hc
    have closed := IsRing.neg_closed with ring, cIn
    have member := IsIdeal.neg_closed with ideal, hc
    have mapped := IsRingHom.neg with hom, cIn
    have image := idealMap.value with function, closed, member
    cc
  . intros b hb y hy
    obtain ⟨u, hu, edge⟩ := ontoLaw.right with b, hb
    have value := FunctionBetween.apply_value with *
    obtain ⟨yIn, x, hx, shape⟩ := idealMap.membership.forward with hy
    have xIn := bounded with x, hx
    have leftClosed := IsRing.mul_closed with ring, hu, xIn
    have rightClosed := IsRing.mul_closed with ring, xIn, hu
    have leftMember := IsIdeal.mul_left_closed with ideal, hu, hx
    have rightMember := IsIdeal.mul_right_closed with ideal, hu, hx
    have leftValue := IsRingHom.mul with hom, hu, xIn
    have rightValue := IsRingHom.mul with hom, xIn, hu
    have leftImage := idealMap.value with function, leftClosed, leftMember
    have rightImage := idealMap.value with function, rightClosed, rightMember
    constructor
    . cc
    . cc

-- The two assignments preserve ideals and are mutually inverse on their domains.
theorem IsRingHom.ideal_correspondence
  shows
    (∀ J, IsIdeal(B, plus, z, minus, times, J) →
      IsIdeal(A, add, zero, neg, mul, idealComap(f, A, J)) ∧
      ringKernel(f, A, z) ⊆ idealComap(f, A, J) ∧
      idealMap(f, B, idealComap(f, A, J)) = J) ∧
    (∀ I, IsIdeal(A, add, zero, neg, mul, I) → ringKernel(f, A, z) ⊆ I →
      IsIdeal(B, plus, z, minus, times, idealMap(f, B, I)) ∧
      idealComap(f, A, idealMap(f, B, I)) = I)
proof
  constructor
  . intros J ideal
    have preimage := IsRingHom.comap_ideal with source, target, hom, ideal
    have contains := IsRingHom.kernel_subset_comap with source, target, hom,
      ideal
    have bounded := IsIdeal.subset_carrier with ideal
    have roundtrip := idealMap.comap_eq with onto, bounded
    refine ⟨preimage, contains, roundtrip⟩
  . intros I ideal contains
    have image := IsRingHom.map_ideal with source, target, hom, onto, ideal
    have roundtrip := IsRingHom.comap_map_eq with source, target, hom, ideal, contains
    refine ⟨image, roundtrip⟩

end Surjections

end RingMaps
section QuotientIdeals
variable (A add zero neg mul one I : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)
hypothesis ideal : IsIdeal(A, add, zero, neg, mul, I)

theorem idealQuotient.kernel_eq
  shows ringKernel(quotientProjection(A, idealRelation(A, add, neg, I)), A, ⟦zero⟧[A, idealRelation(A, add, neg, I)]) = I
proof
  have bounded := IsIdeal.subset_carrier with ideal
  ext x
  constructor
  . intro hx
    have data := ringKernel.membership.forward with hx
    exact idealQuotient.projection_kernel.forward with ring, ideal, data.left, data.right
  . intro hx
    have xIn := bounded with x, hx
    have value := idealQuotient.projection_kernel.backward with ring, ideal, xIn, hx
    exact ringKernel.membership.backward with ⟨xIn, value⟩

theorem idealQuotient.comap_map_eq (J : Set)
  requires idealJ : IsIdeal(A, add, zero, neg, mul, J)
  requires contains : I ⊆ J
  shows idealComap(quotientProjection(A, idealRelation(A, add, neg, I)), A, idealMap(quotientProjection(A, idealRelation(A, add, neg, I)), (A ⧸ idealRelation(A, add, neg, I)), J)) = J
proof
  have quotientRing := idealQuotient.comm_ring with ring, ideal
  have projection := idealQuotient.projection_hom with ring, ideal
  have kernel := idealQuotient.kernel_eq with ring, ideal
  have containsKernel : ringKernel(quotientProjection(A, idealRelation(A, add, neg, I)), A, ⟦zero⟧[A, idealRelation(A, add, neg, I)]) ⊆ J
    rwa kernel
  exact IsRingHom.comap_map_eq with ring, quotientRing, projection, idealJ, containsKernel

end QuotientIdeals

-- The same results for bundled rings.
section BundledRingMaps
variable (f R S : Set)
hypothesis source : CommRing(R)
hypothesis target : CommRing(S)
hypothesis hom : f : R →+* S

theorem idealComap.ideal (J : Set)
  requires ideal : Ideal(S, J)
  shows Ideal(R, idealComap(f, R, J))
proof
  have sourceParts := CommRing.parts with source
  have targetParts := CommRing.parts with target
  have parts := RingHom.parts with hom
  have idealParts := Ideal.parts with ideal
  have engine := IsRingHom.comap_ideal with sourceParts, targetParts, parts,
    idealParts
  exact Ideal.of_projections with engine

theorem idealComap.kernel_subset (J : Set)
  requires ideal : Ideal(S, J)
  shows ker(f) ⊆ idealComap(f, R, J)
proof
  have sourceParts := CommRing.parts with source
  have targetParts := CommRing.parts with target
  have parts := RingHom.parts with hom
  have idealParts := Ideal.parts with ideal
  exact IsRingHom.kernel_subset_comap with sourceParts, targetParts, parts,
    idealParts

theorem idealComap.map_eq (I : Set)
  requires ideal : Ideal(R, I)
  requires contains : ker(f) ⊆ I
  shows idealComap(f, R, idealMap(f, S, I)) = I
proof
  have sourceParts := CommRing.parts with source
  have targetParts := CommRing.parts with target
  have parts := RingHom.parts with hom
  have idealParts := Ideal.parts with ideal
  exact IsRingHom.comap_map_eq with sourceParts, targetParts, parts, idealParts,
    contains

section BundledSurjections
hypothesis onto : SurjectiveBetween(f, R.carrier, S.carrier)

theorem idealMap.ideal (I : Set)
  requires ideal : Ideal(R, I)
  shows Ideal(S, idealMap(f, S, I))
proof
  have sourceParts := CommRing.parts with source
  have targetParts := CommRing.parts with target
  have parts := RingHom.parts with hom
  have idealParts := Ideal.parts with ideal
  have engine := IsRingHom.map_ideal with sourceParts, targetParts, parts, onto,
    idealParts
  exact Ideal.of_projections with engine

-- The ideals of S correspond to the ideals of R containing the kernel.
theorem RingHom.correspondence
  shows
    (∀ J, Ideal(S, J) →
      Ideal(R, idealComap(f, R, J)) ∧
      ker(f) ⊆ idealComap(f, R, J) ∧
      idealMap(f, S, idealComap(f, R, J)) = J) ∧
    (∀ I, Ideal(R, I) → ker(f) ⊆ I →
      Ideal(S, idealMap(f, S, I)) ∧
      idealComap(f, R, idealMap(f, S, I)) = I)
proof
  constructor
  . intros J ideal
    have preimage := idealComap.ideal with source, target, hom, ideal
    have contains := idealComap.kernel_subset with source, target, hom, ideal
    have bounded := Ideal.subset with ideal
    have roundtrip := idealMap.comap_eq with onto, bounded
    refine ⟨preimage, contains, roundtrip⟩
  . intros I ideal contains
    have image := idealMap.ideal with source, target, hom, onto, ideal
    have roundtrip := idealComap.map_eq with source, target, hom, ideal, contains
    refine ⟨image, roundtrip⟩

end BundledSurjections
end BundledRingMaps

section BundledQuotientIdeals
variable (R I : Set)
hypothesis comm : CommRing(R)
hypothesis ideal : Ideal(R, I)

theorem quotientRing.projection_kernel
  shows ringKernel(quotientProjection(R.carrier, quotientRelation(R, I)), R,
    Ring.zero(R ⧸ I)) = I
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  have engine := idealQuotient.kernel_eq with parts, idealParts
  rw [quotientRing.zeroOf, quotientRelation.value]
  exact engine

end BundledQuotientIdeals