-- Choice-free lifting of compatible operations to quotient sets.
-- 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.Relation.QuotientOperations
import Quotient
import Algebra.Ring.Core
import Set.Function

predicate CompatibleBinary (A r op : Set) :=
  ∀ x ∈ A, ∀ y ∈ A, ∀ u ∈ A, ∀ v ∈ A,
    relates(r, x, y) → relates(r, u, v) → relates(r, op(x, u), op(y, v))
predicate CompatibleUnary (A r op : Set) :=
  ∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(r, op(x), op(y))

theorem quotient.representative (A r X : Set)
  requires member : X ∈ (A ⧸ r)
  shows ∃ x ∈ A, X = ⟦x⟧[A, r]
proof
  have data := quotient.membership.forward with member
  exact data.right

-- The canonical quotient map exists without selecting representatives.
defgraph quotientProjection (A r : Set) (x ∈ A) : (A ⧸ r) := ⟦x⟧[A, r]
requires equivalence : Equivalence(A, r)
proof
  exact quotient.contains_class with *

theorem quotientProjection.surjective (A r : Set)
  requires equivalence : Equivalence(A, r)
  shows SurjectiveBetween(quotientProjection(A, r), A, (A ⧸ r))
proof
  have function := quotientProjection.function at A, r with *
  unfold SurjectiveBetween
  refine ⟨function, ?_⟩
  intros X hX
  obtain ⟨x, hx, shape⟩ := quotient.representative with hX
  have value := quotientProjection.value at A, r, x with *
  have edge := FunctionBetween.relates_apply with *
  refine ⟨x, hx, ?_⟩
  rwa [shape, ← value]

defunique quotientBinaryValue (A r op p : Set) (Z ∈ (A ⧸ r)) :=
  ∃ x ∈ A, ∃ y ∈ A, p = (⟦x⟧[A, r], ⟦y⟧[A, r]) ∧ Z = ⟦op(x, y)⟧[A, r]
requires equivalence : Equivalence(A, r)
requires closed : IsMagma(A, op)
requires compatible : CompatibleBinary(A, r, op)
requires pair : p ∈ (A ⧸ r) × (A ⧸ r)
proof
  obtain ⟨bounded, X, hX, Y, hY, shape⟩ := product.membership.forward with pair
  obtain ⟨x, hx, xClass⟩ := quotient.representative with hX
  obtain ⟨y, hy, yClass⟩ := quotient.representative with hY
  have valueIn := quotient.contains_class at A, r, op(x, y) with *
  have input : p = (⟦x⟧[A, r], ⟦y⟧[A, r]) by cc
  refine ⟨⟦op(x, y)⟧[A, r], valueIn, x, hx, y, hy, input, rfl⟩
uniqueness
  intros Z hZ propertyZ W hW propertyW
  obtain ⟨x, hx, y, hy, inputZ, outputZ⟩ := propertyZ
  obtain ⟨u, hu, v, hv, inputW, outputW⟩ := propertyW
  have inputs : (⟦x⟧[A, r], ⟦y⟧[A, r]) = (⟦u⟧[A, r], ⟦v⟧[A, r]) by cc
  have coordinates := orderedPair.injective with inputs
  have xu := equivalenceClass.related_of_eq with equivalence, hx, hu, coordinates.left
  have yv := equivalenceClass.related_of_eq with equivalence, hy, hv, coordinates.right
  have outputs := compatible with x, hx, u, hu, y, hy, v, hv, xu, yv
  have equal := equivalenceClass.eq at A, r, op(x, y), op(u, v) with *
  cc

defgraph quotientBinary (A r op : Set) (p ∈ (A ⧸ r) × (A ⧸ r)) : (A ⧸ r) := quotientBinaryValue(A, r, op, p)
requires equivalence : Equivalence(A, r)
requires closed : IsMagma(A, op)
requires compatible : CompatibleBinary(A, r, op)
proof
  have selected := quotientBinaryValue.selected at A, r, op, p with *
  exact selected.left

theorem quotientBinary.classes (A r op x y : Set)
  requires equivalence : Equivalence(A, r)
  requires closed : IsMagma(A, op)
  requires compatible : CompatibleBinary(A, r, op)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows (quotientBinary(A, r, op))(⟦x⟧[A, r], ⟦y⟧[A, r]) = ⟦op(x, y)⟧[A, r]
proof
  have xIn := quotient.contains_class at A, r, x with *
  have yIn := quotient.contains_class at A, r, y with *
  have pair := product.pair at ⟦x⟧[A, r], ⟦y⟧[A, r], (A ⧸ r), (A ⧸ r) with *
  have evaluated := quotientBinary.value at A, r, op, (⟦x⟧[A, r], ⟦y⟧[A, r]) with *
  have selected := quotientBinaryValue.selected at A, r, op, (⟦x⟧[A, r], ⟦y⟧[A, r]) with *
  obtain ⟨member, u, hu, v, hv, input, output⟩ := selected
  have coordinates := orderedPair.injective with input
  have xu := equivalenceClass.related_of_eq with equivalence, hx, hu, coordinates.left
  have yv := equivalenceClass.related_of_eq with equivalence, hy, hv, coordinates.right
  have related := compatible with x, hx, u, hu, y, hy, v, hv, xu, yv
  have equal := equivalenceClass.eq at A, r, op(x, y), op(u, v) with *
  have called : (quotientBinary(A, r, op))(⟦x⟧[A, r], ⟦y⟧[A, r]) = quotientBinaryValue(A, r, op, (⟦x⟧[A, r], ⟦y⟧[A, r]))
    unfold call2
    cc
  cc

defunique quotientUnaryValue (A r op X : Set) (Z ∈ (A ⧸ r)) :=
  ∃ x ∈ A, X = ⟦x⟧[A, r] ∧ Z = ⟦op(x)⟧[A, r]
requires equivalence : Equivalence(A, r)
requires closed : op : A → A
requires compatible : CompatibleUnary(A, r, op)
requires member : X ∈ (A ⧸ r)
proof
  obtain ⟨x, hx, shape⟩ := quotient.representative with member
  have valueInA : op(x) ∈ A
    exact FunctionBetween.apply_closed at op, A, A, x with *
  have valueIn := quotient.contains_class at A, r, op(x) with *
  refine ⟨⟦op(x)⟧[A, r], valueIn, x, hx, shape, rfl⟩
uniqueness
  intros Z hZ propertyZ W hW propertyW
  obtain ⟨x, hx, inputZ, outputZ⟩ := propertyZ
  obtain ⟨y, hy, inputW, outputW⟩ := propertyW
  have same : ⟦x⟧[A, r] = ⟦y⟧[A, r] by cc
  have xy := equivalenceClass.related_of_eq at A, r, x, y with *
  have outputs := compatible with x, hx, y, hy, xy
  have leftClosed : op(x) ∈ A
    exact FunctionBetween.apply_closed at op, A, A, x with *
  have rightClosed : op(y) ∈ A
    exact FunctionBetween.apply_closed at op, A, A, y with *
  have equal := equivalenceClass.eq at A, r, op(x), op(y) with *
  cc

defgraph quotientUnary (A r op : Set) (X ∈ (A ⧸ r)) : (A ⧸ r) := quotientUnaryValue(A, r, op, X)
requires equivalence : Equivalence(A, r)
requires closed : op : A → A
requires compatible : CompatibleUnary(A, r, op)
proof
  have selected := quotientUnaryValue.selected at A, r, op, X with *
  exact selected.left

theorem quotientUnary.classes (A r op x : Set)
  requires equivalence : Equivalence(A, r)
  requires closed : op : A → A
  requires compatible : CompatibleUnary(A, r, op)
  requires hx : x ∈ A
  shows (quotientUnary(A, r, op))(⟦x⟧[A, r]) = ⟦op(x)⟧[A, r]
proof
  have member := quotient.contains_class at A, r, x with *
  have evaluated := quotientUnary.value at A, r, op, ⟦x⟧[A, r] with *
  have selected := quotientUnaryValue.selected at A, r, op, ⟦x⟧[A, r] with *
  obtain ⟨bounded, y, hy, shape, output⟩ := selected
  have xy := equivalenceClass.related_of_eq at A, r, x, y with *
  have related := compatible with x, hx, y, hy, xy
  have leftClosed : op(x) ∈ A
    exact FunctionBetween.apply_closed at op, A, A, x with *
  have rightClosed : op(y) ∈ A
    exact FunctionBetween.apply_closed at op, A, A, y with *
  have equal := equivalenceClass.eq at A, r, op(x), op(y) with *
  have called : (quotientUnary(A, r, op))(⟦x⟧[A, r]) = quotientUnaryValue(A, r, op, ⟦x⟧[A, r])
    cc
  cc


theorem quotientBinary.magma (A r op : Set)
  requires equivalence : Equivalence(A, r)
  requires closed : IsMagma(A, op)
  requires compatible : CompatibleBinary(A, r, op)
  shows IsMagma((A ⧸ r), quotientBinary(A, r, op))
proof
  unfold IsMagma
  exact quotientBinary.function at A, r, op with *

theorem quotientBinary.associative (A r op : Set)
  requires equivalence : Equivalence(A, r)
  requires closed : IsMagma(A, op)
  requires compatible : CompatibleBinary(A, r, op)
  requires law : Associative(A, op)
  shows Associative((A ⧸ r), quotientBinary(A, r, op))
proof
  intros X hX Y hY Z hZ
  obtain ⟨x, hx, xShape⟩ := quotient.representative with hX
  obtain ⟨y, hy, yShape⟩ := quotient.representative with hY
  obtain ⟨z, hz, zShape⟩ := quotient.representative with hZ
  rw [xShape, yShape, zShape]
  have xy := quotientBinary.classes at A, r, op, x, y with *
  have yz := quotientBinary.classes at A, r, op, y, z with *
  have lhs := quotientBinary.classes at A, r, op, op(x, y), z with *
  have rhs := quotientBinary.classes at A, r, op, x, op(y, z) with *
  have ordinary := law with x, hx, y, hy, z, hz
  cc

theorem quotientBinary.commutative (A r op : Set)
  requires equivalence : Equivalence(A, r)
  requires closed : IsMagma(A, op)
  requires compatible : CompatibleBinary(A, r, op)
  requires law : Commutative(A, op)
  shows Commutative((A ⧸ r), quotientBinary(A, r, op))
proof
  intros X hX Y hY
  obtain ⟨x, hx, xShape⟩ := quotient.representative with hX
  obtain ⟨y, hy, yShape⟩ := quotient.representative with hY
  rw [xShape, yShape]
  have xy := quotientBinary.classes with hx, hy
  have yx := quotientBinary.classes with hy, hx
  have ordinary := law with x, hx, y, hy
  cc

theorem quotientBinary.identity (A r op unit : Set)
  requires equivalence : Equivalence(A, r)
  requires closed : IsMagma(A, op)
  requires compatible : CompatibleBinary(A, r, op)
  requires law : Identity(A, op, unit)
  shows Identity((A ⧸ r), quotientBinary(A, r, op), ⟦unit⟧[A, r])
proof
  have unitIn := quotient.contains_class with equivalence, law.left
  unfold Identity
  refine ⟨unitIn, ?_⟩
  intros X hX
  obtain ⟨x, hx, shape⟩ := quotient.representative with hX
  rw shape
  have left := quotientBinary.classes with equivalence, closed, compatible, law.left, hx
  have right := quotientBinary.classes with equivalence, closed, compatible, hx, law.left
  have ordinary := law.right with x, hx
  have leftLaw := ordinary.left
  have rightLaw := ordinary.right
  constructor
  . cc
  . cc

theorem quotientUnary.inverse (A r op unit inv : Set)
  requires equivalence : Equivalence(A, r)
  requires closed : IsMagma(A, op)
  requires compatible : CompatibleBinary(A, r, op)
  requires invCompatible : CompatibleUnary(A, r, inv)
  requires law : Inverse(A, op, unit, inv)
  shows Inverse((A ⧸ r), quotientBinary(A, r, op), ⟦unit⟧[A, r], quotientUnary(A, r, inv))
proof
  have invClosed := law.left
  have function := quotientUnary.function at A, r, inv with *
  unfold Inverse
  refine ⟨function, ?_⟩
  intros X hX
  obtain ⟨x, hx, shape⟩ := quotient.representative with hX
  rw shape
  have invIn : inv(x) ∈ A
    exact FunctionBetween.apply_closed with *
  have inverseValue := quotientUnary.classes with hx
  have left := quotientBinary.classes at A, r, op, inv(x), x with *
  have right := quotientBinary.classes at A, r, op, x, inv(x) with *
  have ordinary := law.right with x, hx
  have leftLaw := ordinary.left
  have rightLaw := ordinary.right
  constructor
  . cc
  . cc

theorem quotientBinary.distributive (A r add mul : Set)
  requires equivalence : Equivalence(A, r)
  requires addClosed : IsMagma(A, add)
  requires mulClosed : IsMagma(A, mul)
  requires addCompatible : CompatibleBinary(A, r, add)
  requires mulCompatible : CompatibleBinary(A, r, mul)
  requires law : Distributive(A, add, mul)
  shows Distributive((A ⧸ r), quotientBinary(A, r, add), quotientBinary(A, r, mul))
proof
  intros X hX Y hY Z hZ
  obtain ⟨x, hx, xShape⟩ := quotient.representative with hX
  obtain ⟨y, hy, yShape⟩ := quotient.representative with hY
  obtain ⟨z, hz, zShape⟩ := quotient.representative with hZ
  rw [xShape, yShape, zShape]
  have sumYZ := quotientBinary.classes at A, r, add, y, z with *
  have sumXY := quotientBinary.classes at A, r, add, x, y with *
  have prodXY := quotientBinary.classes at A, r, mul, x, y with *
  have prodXZ := quotientBinary.classes at A, r, mul, x, z with *
  have prodYZ := quotientBinary.classes at A, r, mul, y, z with *
  have leftL := quotientBinary.classes at A, r, mul, x, call2(add, y, z) with *
  have rightL := quotientBinary.classes at A, r, add, call2(mul, x, y), call2(mul, x, z) with *
  have leftR := quotientBinary.classes at A, r, mul, call2(add, x, y), z with *
  have rightR := quotientBinary.classes at A, r, add, call2(mul, x, z), call2(mul, y, z) with *
  have ordinary := law with x, hx, y, hy, z, hz
  have leftLaw := ordinary.left
  have rightLaw := ordinary.right
  constructor
  . cc
  . cc


theorem quotient.comm_ring (A r add zero neg mul one : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires equivalence : Equivalence(A, r)
  requires addCompatible : CompatibleBinary(A, r, add)
  requires mulCompatible : CompatibleBinary(A, r, mul)
  requires negCompatible : CompatibleUnary(A, r, neg)
  shows IsCommRing((A ⧸ r), quotientBinary(A, r, add), ⟦zero⟧[A, r],
    quotientUnary(A, r, neg), quotientBinary(A, r, mul), ⟦one⟧[A, r])
proof
  have addClosed : IsMagma(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have mulClosed : IsMagma(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have addAssoc : Associative(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have mulAssoc : Associative(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have addComm : Commutative(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have mulComm : Commutative(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have addUnit : Identity(A, add, zero) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have mulUnit : Identity(A, mul, one) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have inverse : Inverse(A, add, zero, neg) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have distribute : Distributive(A, add, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have qAdd := quotientBinary.magma at A, r, add with *
  have qMul := quotientBinary.magma at A, r, mul with *
  have qAddAssoc := quotientBinary.associative at A, r, add with *
  have qMulAssoc := quotientBinary.associative at A, r, mul with *
  have qAddComm := quotientBinary.commutative at A, r, add with *
  have qMulComm := quotientBinary.commutative at A, r, mul with *
  have qAddUnit := quotientBinary.identity at A, r, add, zero with *
  have qMulUnit := quotientBinary.identity at A, r, mul, one with *
  have qInverse := quotientUnary.inverse with *
  have qDistribute := quotientBinary.distributive with *
  simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]