-- Piece maps: the function a decomposition realises, carrying each point
-- of a piece by the element of that piece. It is an injection of the
-- decomposed set whose image is the union of the moved pieces, and
-- cutting the pieces down to a subset decomposes the subset onto its
-- image under the piece map
-- 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.Group.Paradox.PieceMaps
import Algebra.Group.Paradox

-- The piece map of a family F: x is carried to act(g, x) when x lies in
-- the piece of (S, g).
def pieceMap (act X F : Set) : Set :=
  { q ∈ X × X | ∃ p ∈ F, fst(q) ∈ fst(p) ∧ snd(q) = act(snd(p), fst(q)) }

-- Every piece cut down to C, carried by the same element.
defgraph cutPair (X G C : Set) (p ∈ 𝒫(X) × Group.carrier(G)) :
    𝒫(X) × Group.carrier(G) :=
  (fst(p) ∩ C, snd(p))
proof
  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with member
  have subset := powerset.membership_iff.forward with hS
  have cut : S ∩ C ⊆ X :=
    Subset.transitive with (intersection.subset_left at S, C), subset
  have cutIn := powerset.membership_iff.backward with cut
  rw [shape, fst.pair, snd.pair]
  exact product.pair with cutIn, hg

theorem pieceMap.relates (act X F x y : Set)
  shows relates(pieceMap(act, X, F), x, y) ↔
    (x, y) ∈ X × X ∧ ∃ p ∈ F, x ∈ fst(p) ∧ y = act(snd(p), x)
proof
  unfold relates
  constructor
  . intro h
    obtain ⟨pair, p, hp, inP, equal⟩ := pieceMap.membership.forward with h
    rw fst.pair at inP
    rw [fst.pair, snd.pair] at equal
    exact ⟨pair, p, hp, inP, equal⟩
  . intro h
    obtain ⟨pair, p, hp, inP, equal⟩ := h
    apply pieceMap.membership.backward
    refine ⟨pair, p, hp, ?_, ?_⟩
    . rw fst.pair
      exact inP
    . rw [fst.pair, snd.pair]
      exact equal

-- The two coordinates of a piece: a subset of X and a group element.
theorem piece.parts (G X p : Set)
  requires hp : p ∈ 𝒫(X) × Group.carrier(G)
  shows fst(p) ⊆ X ∧ snd(p) ∈ Group.carrier(G)
proof
  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with hp
  have subset := powerset.membership_iff.forward with hS
  rw [shape, fst.pair, snd.pair]
  exact ⟨subset, hg⟩

theorem cutPair.shape (act G X C p : Set)
  requires hp : p ∈ 𝒫(X) × Group.carrier(G)
  shows fst(cutPair(X, G, C)(p)) = fst(p) ∩ C ∧
    moved(act, X, cutPair(X, G, C)(p)) = translate(act, X, snd(p), fst(p) ∩ C)
proof
  have value := cutPair.value at X, G, C, p with hp
  rw [value, fst.pair, moved.value]
  exact ⟨rfl, rfl⟩

section PieceMaps
variable (act G X : Set)
hypothesis action : act : G ↷ X

theorem pieceMap.relates_of (F p x : Set)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires hp : p ∈ F
  requires hx : x ∈ fst(p)
  shows relates(pieceMap(act, X, F), x, act(snd(p), x))
proof
  obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)
  have xIn := subset with x, hx
  have moved : snd(p) ·ₐ x ∈ X := Action.act_mem with action, gIn, xIn
  have pair := product.pair with xIn, moved
  exact pieceMap.relates.backward with ⟨pair, p, hp, hx, rfl⟩

-- The piece map is a function on the decomposed set.
theorem pieceMap.function (A F : Set)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires pieces : Pieces(A, F)
  shows pieceMap(act, X, F) : A → X
proof
  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces
  refine ⟨?_, ?_, ?_⟩
  . intros q hq
    obtain ⟨qIn, p, hp, inPiece, equal⟩ := pieceMap.membership.forward with hq
    obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with qIn
    rw [shape, fst.pair] at inPiece
    have xIn := piecesBounded with p, hp, x, inPiece
    rw shape
    exact product.pair with xIn, hy
  . intros x y hxy z hxz
    obtain ⟨pairY, p, hp, inP, yEq⟩ := pieceMap.relates.forward with hxy
    obtain ⟨pairZ, q, hq, inQ, zEq⟩ := pieceMap.relates.forward with hxz
    have split : p = q ∨ p ≠ q by tauto
    cases split with same | apart
    . rw [yEq, zEq, same]
      rfl
    . exfalso
      have disjoint := piecesDisjoint with p, hp, q, hq, apart
      have absent := Disjoint.iff.forward with disjoint
      exact absent with x, inP, inQ
  . intros x hx
    obtain ⟨p, hp, inP⟩ := piecesCover with x, hx
    obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)
    have xIn := subset with x, inP
    have moved : snd(p) ·ₐ x ∈ X := Action.act_mem with action, gIn, xIn
    have related := pieceMap.relates_of with action, bounded, hp, inP
    witness act(snd(p), x)
    exact ⟨moved, related⟩

theorem pieceMap.apply (A F p x : Set)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires pieces : Pieces(A, F)
  requires hp : p ∈ F
  requires hx : x ∈ fst(p)
  shows pieceMap(act, X, F)(x) = snd(p) ·ₐ x
proof
  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces
  have function := pieceMap.function with action, bounded, pieces
  have xIn := piecesBounded with p, hp, x, hx
  have related := pieceMap.relates_of with action, bounded, hp, hx
  exact FunctionBetween.apply_value with function, xIn, related

-- The value at a point of a piece lies in the moved piece.
theorem pieceMap.apply_mem (A F p x : Set)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires pieces : Pieces(A, F)
  requires hp : p ∈ F
  requires hx : x ∈ fst(p)
  shows pieceMap(act, X, F)(x) ∈ moved(act, X, p)
proof
  obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)
  have value := pieceMap.apply with action, bounded, pieces, hp, hx
  have member : snd(p) ·ₐ x ∈ translate(act, X, snd(p), fst(p)) :=
    translate.act_mem with action, subset, hx
  rw [value, moved.unfold]
  exact member

-- With the moved pieces inside B, the piece map lands in B.
theorem pieceMap.codomain (A B F : Set)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires pieces : Pieces(A, F)
  requires movedBounded : ∀ p ∈ F, moved(act, X, p) ⊆ B
  shows pieceMap(act, X, F) : A → B
proof
  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces
  have function := pieceMap.function with action, bounded, pieces
  apply FunctionBetween.codomain_of_values with function
  intros x hx
  obtain ⟨p, hp, inP⟩ := piecesCover with x, hx
  have member := pieceMap.apply_mem with action, bounded, pieces, hp, inP
  exact movedBounded with p, hp, pieceMap(act, X, F)(x), member

-- Disjoint moved pieces make the piece map injective.
theorem pieceMap.injective (A B F : Set)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires pieces : Pieces(A, F)
  requires movedBounded : ∀ p ∈ F, moved(act, X, p) ⊆ B
  requires movedDisjoint : ∀ p q ∈ F, p ≠ q →
    Disjoint(moved(act, X, p), moved(act, X, q))
  shows InjectiveBetween(pieceMap(act, X, F), A, B)
proof
  have group := Action.group with action
  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces
  have function := pieceMap.codomain with action, bounded, pieces, movedBounded
  apply Injective.of_pointwise with function
  intros x hx y hy same
  obtain ⟨p, hp, inP⟩ := piecesCover with x, hx
  obtain ⟨q, hq, inQ⟩ := piecesCover with y, hy
  have memberX := pieceMap.apply_mem with action, bounded, pieces, hp, inP
  have memberY := pieceMap.apply_mem with action, bounded, pieces, hq, inQ
  have valueX := pieceMap.apply with action, bounded, pieces, hp, inP
  have valueY := pieceMap.apply with action, bounded, pieces, hq, inQ
  have split : p = q ∨ p ≠ q by tauto
  cases split with equal | apart
  . obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)
    have xIn := subset with x, inP
    rw ← equal at inQ
    have yIn := subset with y, inQ
    rw [valueX, valueY] at same
    rw ← equal at same
    have backX : snd(p)⁻¹ ·ₐ snd(p) ·ₐ x = x := inv_act_cancel with *
    have backY : snd(p)⁻¹ ·ₐ snd(p) ·ₐ y = y := inv_act_cancel with *
    have step : snd(p)⁻¹ ·ₐ snd(p) ·ₐ x = snd(p)⁻¹ ·ₐ snd(p) ·ₐ y
      rw same
      rfl
    rw [backX, backY] at step
    exact step
  . exfalso
    have disjoint := movedDisjoint with p, hp, q, hq, apart
    have absent := Disjoint.iff.forward with disjoint
    rw same at memberX
    exact absent with pieceMap(act, X, F)(y), memberX, memberY

-- Moved pieces covering B make the piece map onto B.
theorem pieceMap.surjective (A B F : Set)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires pieces : Pieces(A, F)
  requires movedPieces : MovedPieces(act, X, B, F)
  shows SurjectiveBetween(pieceMap(act, X, F), A, B)
proof
  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces
  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces
  have function := pieceMap.codomain with action, bounded, pieces, movedBounded
  constructor
  . exact function
  . intros y hy
    obtain ⟨p, hp, member⟩ := movedCover with y, hy
    rw moved.unfold at member
    obtain ⟨yIn, x, hx, yEq⟩ := translate.membership.forward with member
    have xIn := piecesBounded with p, hp, x, hx
    have related := pieceMap.relates_of with action, bounded, hp, hx
    witness x
    rw yEq
    exact ⟨xIn, related⟩

theorem pieceMap.bijective (A B F : Set)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires pieces : Pieces(A, F)
  requires movedPieces : MovedPieces(act, X, B, F)
  shows BijectiveBetween(pieceMap(act, X, F), A, B)
proof
  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces
  constructor
  . exact pieceMap.injective with action, bounded, pieces, movedBounded,
      movedDisjoint
  . exact pieceMap.surjective with action, bounded, pieces, movedPieces

-- Restriction: cutting the pieces down to C ⊆ A decomposes C onto its
-- image under the piece map.
theorem Equidecomposable.restrict (A B C F : Set)
  requires finite : Finite(F)
  requires bounded : F ⊆ 𝒫(X) × G.carrier
  requires pieces : Pieces(A, F)
  requires movedBounded : ∀ p ∈ F, moved(act, X, p) ⊆ B
  requires movedDisjoint : ∀ p q ∈ F, p ≠ q →
    Disjoint(moved(act, X, p), moved(act, X, q))
  requires subset : C ⊆ A
  shows Equidecomposable(act, G, X, C, functionImage(pieceMap(act, X, F), C, B))
proof
  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces
  have cutFunction := cutPair.function at X, G, C
  have cuts : ∀ p ∈ F, fst(cutPair(X, G, C)(p)) = fst(p) ∩ C ∧
      moved(act, X, cutPair(X, G, C)(p)) = translate(act, X, snd(p), fst(p) ∩ C)
    intros p hp
    exact cutPair.shape at act, G, X, C, p with (bounded with p, hp)
  have movedCut : ∀ p ∈ F, moved(act, X, cutPair(X, G, C)(p)) ⊆ moved(act, X, p)
    intros p hp
    obtain ⟨first, second⟩ := cuts with p, hp
    have inner := intersection.subset_left at fst(p), C
    rw [second, moved.unfold]
    exact translate.monotone at act, X, snd(p), fst(p) ∩ C, fst(p) with inner
  apply Equidecomposable.of_reindex with cutFunction, finite, bounded
  . intros p hp
    obtain ⟨first, second⟩ := cuts with p, hp
    rw first
    exact intersection.subset_right at fst(p), C
  . intros x hx
    obtain ⟨p, hp, inP⟩ := piecesCover with x, (subset with x, hx)
    obtain ⟨first, second⟩ := cuts with p, hp
    have both := intersection.membership.backward at fst(p), C, x with ⟨inP, hx⟩
    witness p
    rw first
    exact ⟨hp, both⟩
  . intros p hp q hq different
    obtain ⟨firstP, secondP⟩ := cuts with p, hp
    obtain ⟨firstQ, secondQ⟩ := cuts with q, hq
    have disjoint := piecesDisjoint with p, hp, q, hq, different
    have innerP := intersection.subset_left at fst(p), C
    have innerQ := intersection.subset_left at fst(q), C
    have step := Disjoint.of_subset_left with disjoint, innerP
    rw [firstP, firstQ]
    exact Disjoint.of_subset_right with step, innerQ
  . intros p hp
    obtain ⟨first, second⟩ := cuts with p, hp
    rw second
    intros y hy
    obtain ⟨yIn, x, hx, yEq⟩ := translate.membership.forward with hy
    obtain ⟨inP, inC⟩ := intersection.membership.forward with hx
    have value := pieceMap.apply with action, bounded, pieces, hp, inP
    have member := pieceMap.apply_mem with action, bounded, pieces, hp, inP
    rw [value, ← yEq] at member
    have inB := movedBounded with p, hp, y, member
    apply functionImage.membership.backward
    refine ⟨inB, x, inC, ?_⟩
    rw [value, yEq]
    rfl
  . intros y hy
    obtain ⟨inB, x, hx, yEq⟩ := functionImage.membership.forward with hy
    obtain ⟨p, hp, inP⟩ := piecesCover with x, (subset with x, hx)
    obtain ⟨first, second⟩ := cuts with p, hp
    obtain ⟨subsetP, gIn⟩ := piece.parts with (bounded with p, hp)
    have value := pieceMap.apply with action, bounded, pieces, hp, inP
    have inner := intersection.subset_left at fst(p), C
    have cutBounded : fst(p) ∩ C ⊆ X := Subset.transitive with inner, subsetP
    have both := intersection.membership.backward at fst(p), C, x with ⟨inP, hx⟩
    have member : snd(p) ·ₐ x ∈ translate(act, X, snd(p), fst(p) ∩ C) :=
      translate.act_mem with action, cutBounded, both
    witness p
    rw [second, yEq, value]
    exact ⟨hp, member⟩
  . intros p hp q hq different
    have disjoint := movedDisjoint with p, hp, q, hq, different
    have step := Disjoint.of_subset_left with disjoint, (movedCut with p, hp)
    exact Disjoint.of_subset_right with step, (movedCut with q, hq)

end PieceMaps