-- The Banach–Schröder–Bernstein theorem for equidecomposability: a set
-- equidecomposable with a subset of a second set, which is in turn
-- equidecomposable with a subset of the first, is equidecomposable with
-- the second. Equidecomposability is realised by a piecewise-moved
-- bijection and conversely; the back-and-forth chain of the
-- Cantor–Schröder–Bernstein construction splits both sets into two
-- parts, each decomposed onto its image by restricting a 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.SchroederBernstein
import Algebra.Group.Paradox.PieceMaps
import Cardinal.Dominance

-- A embeds in B when A is equidecomposable with a subset of B.
predicate Embeds (act G X A B : Set) :=
  ∃ C, C ⊆ B ∧ Equidecomposable(act, G, X, A, C)

-- f moves A piecewise: finitely many disjoint pieces cover A, and on each
-- piece f agrees with one group element.
predicate PiecewiseMoved (act G X A f : Set) :=
  ∃ F, Finite(F) ∧ F ⊆ 𝒫(X) × Group.carrier(G) ∧ Pieces(A, F) ∧
    (∀ p ∈ F, ∀ x ∈ fst(p), f(x) = act(snd(p), x))

-- The complement of the chain is the image under g of the complement of
-- the image of the chain under f.
theorem chain.complement (f g A B : Set)
  requires fFunction : f : A → B
  requires gInjective : InjectiveBetween(g, B, A)
  shows functionImage(g, B ∖ functionImage(f, chain(f, g, A, B), B), A) =
    A ∖ chain(f, g, A, B)
proof
  have gFunction := Injective.function with gInjective
  ext x
  constructor
  . intro hx
    obtain ⟨xIn, y, hy, xEq⟩ := functionImage.membership.forward with hx
    obtain ⟨yIn, outside⟩ := difference.membership.forward with hy
    apply difference.membership.backward
    refine ⟨xIn, ?_⟩
    intro inChain
    rw xEq at inChain
    obtain ⟨z, hz, zEq⟩ :=
      chain.preimage with fFunction, gInjective, yIn, inChain
    apply outside
    have zIn : z ∈ A := chain.subset at f, g, A, B with z, hz
    have inB := FunctionBetween.apply_closed with fFunction, zIn
    rw zEq at inB
    symm at zEq
    exact functionImage.membership.backward with ⟨inB, z, hz, zEq⟩
  . intro hx
    obtain ⟨xIn, outside⟩ := difference.membership.forward with hx
    have inImage := chain.off_in_image with xIn, outside
    obtain ⟨xIn2, y, hy, xEq⟩ := functionImage.membership.forward with inImage
    apply functionImage.membership.backward
    refine ⟨xIn, y, ?_, xEq⟩
    apply difference.membership.backward
    refine ⟨hy, ?_⟩
    intro inImageF
    obtain ⟨yIn, z, hz, yEq⟩ := functionImage.membership.forward with inImageF
    have closed := chain.closed with fFunction, gFunction, hz
    rw [← yEq, ← xEq] at closed
    exact outside with closed

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

theorem Embeds.of_subset (A B : Set)
  requires bounded : A ⊆ X
  requires subset : A ⊆ B
  shows Embeds(act, G, X, A, B)
proof
  have same := Equidecomposable.reflexive with action, bounded
  witness A
  exact ⟨subset, same⟩

theorem Embeds.of_equidecomposable (A B C : Set)
  requires subset : C ⊆ B
  requires equidecomposable : Equidecomposable(act, G, X, A, C)
  shows Embeds(act, G, X, A, B)
proof
  witness C
  exact ⟨subset, equidecomposable⟩

-- Equidecomposability is realised by a piecewise-moved bijection.
theorem Equidecomposable.bijection (A B : Set)
  requires equidecomposable : Equidecomposable(act, G, X, A, B)
  shows ∃ f, BijectiveBetween(f, A, B) ∧ PiecewiseMoved(act, G, X, A, f)
proof
  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := equidecomposable
  have bijective := pieceMap.bijective with action, bounded, pieces, movedPieces
  witness pieceMap(act, X, F)
  constructor
  . exact bijective
  . witness F
    refine ⟨finite, bounded, pieces, ?_⟩
    intros p hp x hx
    exact pieceMap.apply with action, bounded, pieces, hp, hx

-- Conversely, a piecewise-moved bijection onto B decomposes A onto B.
theorem Equidecomposable.of_bijection (A B f : Set)
  requires bijective : BijectiveBetween(f, A, B)
  requires piecewise : PiecewiseMoved(act, G, X, A, f)
  shows Equidecomposable(act, G, X, A, B)
proof
  obtain ⟨injective, surjective⟩ := bijective
  have function := Injective.function with injective
  obtain ⟨F, finite, bounded, pieces, values⟩ := piecewise
  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces
  have moves : ∀ p ∈ F, moved(act, X, p) = functionImage(f, fst(p), B)
    intros p hp
    obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)
    rw moved.unfold
    ext y
    constructor
    . intro hy
      obtain ⟨yIn, x, hx, yEq⟩ := translate.membership.forward with hy
      have value := values with p, hp, x, hx
      have xIn := piecesBounded with p, hp, x, hx
      have inB := FunctionBetween.apply_closed with function, xIn
      rw ← value at yEq
      rw yEq
      exact functionImage.membership.backward with ⟨inB, x, hx, rfl⟩
    . intro hy
      obtain ⟨inB, x, hx, yEq⟩ := functionImage.membership.forward with hy
      have value := values with p, hp, x, hx
      have member : snd(p) ·ₐ x ∈ translate(act, X, snd(p), fst(p)) :=
        translate.act_mem with action, subset, hx
      rw [yEq, value]
      exact member
  witness F
  refine ⟨finite, bounded, pieces, ?_⟩
  refine ⟨?_, ?_, ?_⟩
  . intros p hp
    have move := moves with p, hp
    rw move
    exact functionImage.subset at f, fst(p), B
  . intros y hy
    obtain ⟨x, hx, related⟩ := surjective.right with y, hy
    have value := FunctionBetween.apply_value with function, hx, related
    obtain ⟨p, hp, inP⟩ := piecesCover with x, hx
    have move := moves with p, hp
    symm at value
    have member : y ∈ functionImage(f, fst(p), B) :=
      functionImage.membership.backward with ⟨hy, x, inP, value⟩
    witness p
    rw move
    exact ⟨hp, member⟩
  . intros p hp q hq different
    have moveP := moves with p, hp
    have moveQ := moves with q, hq
    rw [moveP, moveQ]
    apply Disjoint.iff.backward
    intros y hyP hyQ
    obtain ⟨inB, x, hx, yEqX⟩ := functionImage.membership.forward with hyP
    obtain ⟨inB2, x2, hx2, yEqX2⟩ := functionImage.membership.forward with hyQ
    have xIn := piecesBounded with p, hp, x, hx
    have x2In := piecesBounded with q, hq, x2, hx2
    have same : f(x) = f(x2) by cc
    have equal := Injective.apply_cancel with injective, xIn, x2In, same
    rw ← equal at hx2
    have disjoint := piecesDisjoint with p, hp, q, hq, different
    have absent := Disjoint.iff.forward with disjoint
    exact absent with x, hx, hx2

-- The Schröder–Bernstein engine: injections f : A → B and g : B → A that
-- decompose every subset onto its image decompose A onto B, by splitting
-- A at the chain and B at the image of the chain.
theorem Equidecomposable.of_injections (A B f g : Set)
  requires fFunction : f : A → B
  requires gInjective : InjectiveBetween(g, B, A)
  requires first : ∀ C, C ⊆ A →
    Equidecomposable(act, G, X, C, functionImage(f, C, B))
  requires second : ∀ D, D ⊆ B →
    Equidecomposable(act, G, X, D, functionImage(g, D, A))
  shows Equidecomposable(act, G, X, A, B)
proof
  have chainSubset := chain.subset at f, g, A, B
  have imageSubset := functionImage.subset at f, chain(f, g, A, B), B
  have restSubset :=
    difference.subset_left at B, functionImage(f, chain(f, g, A, B), B)
  have firstPart := first with chain(f, g, A, B), chainSubset
  have secondPart :=
    second with B ∖ functionImage(f, chain(f, g, A, B), B), restSubset
  have complement := chain.complement with fFunction, gInjective
  rw complement at secondPart
  have backPart := Equidecomposable.symmetric with action, secondPart
  have disjointSource := Disjoint.difference_right at A, chain(f, g, A, B)
  have disjointTarget :=
    Disjoint.difference_right at B, functionImage(f, chain(f, g, A, B), B)
  have union := Equidecomposable.disjoint_union with action, firstPart,
    backPart, disjointSource, disjointTarget
  have coverA := difference.union2_of_subset with chainSubset
  have coverB := difference.union2_of_subset with imageSubset
  rw [coverA, coverB] at union
  exact union

-- The Banach–Schröder–Bernstein theorem.
theorem Equidecomposable.of_embeddings (A B : Set)
  requires boundedA : A ⊆ X
  requires boundedB : B ⊆ X
  requires forward : Embeds(act, G, X, A, B)
  requires backward : Embeds(act, G, X, B, A)
  shows Equidecomposable(act, G, X, A, B)
proof
  obtain ⟨B1, subsetB1, firstPieces⟩ := forward
  obtain ⟨A1, subsetA1, secondPieces⟩ := backward
  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := firstPieces
  obtain ⟨F2, finite2, bounded2, pieces2, movedPieces2⟩ := secondPieces
  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces
  obtain ⟨movedBounded2, movedCover2, movedDisjoint2⟩ := movedPieces2
  have movedB : ∀ p ∈ F, moved(act, X, p) ⊆ B
    intros p hp
    exact Subset.transitive with (movedBounded with p, hp), subsetB1
  have movedA : ∀ p ∈ F2, moved(act, X, p) ⊆ A
    intros p hp
    exact Subset.transitive with (movedBounded2 with p, hp), subsetA1
  have fInjective := pieceMap.injective with action, bounded, pieces, movedB,
    movedDisjoint
  have gInjective := pieceMap.injective with action, bounded2, pieces2, movedA,
    movedDisjoint2
  have fFunction := Injective.function with fInjective
  have first : ∀ C, C ⊆ A →
      Equidecomposable(act, G, X, C, functionImage(pieceMap(act, X, F), C, B))
    intros C hC
    exact Equidecomposable.restrict with action, finite, bounded, pieces,
      movedB, movedDisjoint, hC
  have second : ∀ D, D ⊆ B →
      Equidecomposable(act, G, X, D, functionImage(pieceMap(act, X, F2), D, A))
    intros D hD
    exact Equidecomposable.restrict with action, finite2, bounded2, pieces2,
      movedA, movedDisjoint2, hD
  exact Equidecomposable.of_injections with action, fFunction, gInjective,
    first, second

end SchroederBernstein