-- The algebra of dominance and equipotence: products and disjoint sums
-- respect dominance, a factor embeds in a product, any two sets are
-- comparable under dominance, and the naturals square to themselves
-- 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.Cardinal.Algebra
import Set.Ordinal.OrderType
import Infinite
import CountableClosure

theorem Dominated.product (A B C D : Set)
  requires hAC : A ≼ C
  requires hBD : B ≼ D
  shows (A × B) ≼ (C × D)
proof
  obtain ⟨f, hf⟩ := hAC
  obtain ⟨g, hg⟩ := hBD
  witness productMap(f, g, A, B, C, D)
  exact productMap.injective with hf, hg

theorem Dominated.disjointSum (A B C D : Set)
  requires hAC : A ≼ C
  requires hBD : B ≼ D
  shows (A ⊎ B) ≼ (C ⊎ D)
proof
  obtain ⟨f, hf⟩ := hAC
  obtain ⟨g, hg⟩ := hBD
  witness sumMap(f, g, A, B, C, D)
  exact sumMap.injective with hf, hg

theorem Equipotent.product_commutative (A B : Set)
  shows (A × B) ≃ (B × A)
proof
  witness productSwap(A, B)
  exact productSwap.bijective

-- A factor embeds in the product once the other factor has a point.
defgraph pairWith (A B b : Set) (x ∈ A) : A × B := (x, b)
requires hb : b ∈ B
proof
  exact product.pair with hb

theorem pairWith.injective (A B b : Set)
  requires hb : b ∈ B
  shows InjectiveBetween(pairWith(A, B, b), A, A × B)
proof
  have function := pairWith.function at A, B, b with *
  constructor
  . exact function
  . intros x hx y hy z hz hxz hyz
    have valueX := FunctionBetween.apply_value with function, hx, hxz
    have valueY := FunctionBetween.apply_value with function, hy, hyz
    have stepX := pairWith.value at A, B, b, x with *
    have stepY := pairWith.value at A, B, b, y with *
    have same : (x, b) = (y, b) by cc
    have parts := orderedPair.injective with same
    exact parts.left

theorem Dominated.left_factor (A B : Set)
  requires inhabited : Nonempty(B)
  shows A ≼ A × B
proof
  obtain ⟨b, hb⟩ := inhabited
  witness pairWith(A, B, b)
  exact pairWith.injective with hb

theorem Dominated.right_factor (A B : Set)
  requires inhabited : Nonempty(B)
  shows A ≼ B × A
proof
  have left := Dominated.left_factor at A, B with inhabited
  have swap := Dominated.of_equipotent with (Equipotent.product_commutative at A, B)
  exact Dominated.transitive with left, swap

-- Any two sets are comparable: well-order both and compare the orders.
theorem Dominated.total (A B : Set)
  shows A ≼ B ∨ B ≼ A
proof
  obtain ⟨r, orderA⟩ := WellOrder.exists at A
  obtain ⟨s, orderB⟩ := WellOrder.exists at B
  have comparison := WellOrder.comparable with orderA, orderB
  cases comparison with intoB | intoA
  . obtain ⟨I, f, initial, iso⟩ := intoB
    left
    have hI := InitialSegment.subset with initial
    have injective := Bijective.injective with iso.left
    have toSegment := Dominated.of_injective with injective
    exact Dominated.transitive with toSegment, (Dominated.of_subset with hI)
  . obtain ⟨I, f, initial, iso⟩ := intoA
    right
    have hI := InitialSegment.subset with initial
    have injective := Bijective.injective with iso.left
    have toSegment := Dominated.of_injective with injective
    exact Dominated.transitive with toSegment, (Dominated.of_subset with hI)

theorem omega.square
  shows (ℕ × ℕ) ≃ ℕ
proof
  obtain ⟨f, hf⟩ := Countable.product with naturals.countable, naturals.countable
  have down := Dominated.of_injective with hf
  have zeroNat : Nat(0) by typecheck
  have hzero : 0 ∈ ℕ := nat.omega.forward with zeroNat
  have inhabited : Nonempty(ℕ) := ⟨0, hzero⟩
  have up := Dominated.left_factor at ℕ, ℕ with inhabited
  exact Dominated.antisymmetric with down, up

-- Infinite sets: closed upward, and holding two distinct points.
theorem Infinite.of_subset (A B : Set)
  requires infinite : Infinite(A)
  requires hAB : A ⊆ B
  shows Infinite(B)
proof
  unfold Infinite
  intro finite
  unfold Infinite at infinite
  apply infinite
  exact Finite.subset with finite, hAB

theorem Infinite.two_points (A : Set)
  requires infinite : Infinite(A)
  shows ∃ a ∈ A, ∃ b ∈ A, a ≠ b
proof
  obtain ⟨g, injective⟩ := Infinite.omega_dominated with infinite
  have function := Injective.function with injective
  have zeroNat : Nat(0) by typecheck
  have oneNat : Nat(1) by typecheck
  have hzero : 0 ∈ ℕ := nat.omega.forward with zeroNat
  have hone : 1 ∈ ℕ := nat.omega.forward with oneNat
  have closedZero := FunctionBetween.apply_closed with function, hzero
  have closedOne := FunctionBetween.apply_closed with function, hone
  refine ⟨g(0), closedZero, g(1), closedOne, ?_⟩
  intro equal
  have same := Injective.apply_cancel with injective, equal
  exact zero.ne_one with same

-- Two sets dominated by X, kept apart by two points of X, together sit
-- inside X × X: send one through (·, a) and the other through (·, b).
theorem Dominated.union_of_two_points (A B X a b : Set)
  requires hA : A ≼ X
  requires hB : B ≼ X
  requires ha : a ∈ X
  requires hb : b ∈ X
  requires distinct : a ≠ b
  requires disjoint : Disjoint(A, B)
  shows (A ∪ B) ≼ (X × X)
proof
  obtain ⟨f, hf⟩ := hA
  obtain ⟨g, hg⟩ := hB
  have fFunction := Injective.function with hf
  have gFunction := Injective.function with hg
  have pairA := pairWith.injective at X, X, a with ha
  have pairB := pairWith.injective at X, X, b with hb
  have pairAFunction := pairWith.function at X, X, a with ha
  have pairBFunction := pairWith.function at X, X, b with hb
  have leftInjective := compose.injective with hf, pairA
  have rightInjective := compose.injective with hg, pairB
  have leftCorestrict := Injective.corestrict with leftInjective
  have rightCorestrict := Injective.corestrict with rightInjective
  have imagesDisjoint : Disjoint(
      functionImage(compose(pairWith(X, X, a), f, A, X, X × X), A, X × X),
      functionImage(compose(pairWith(X, X, b), g, B, X, X × X), B, X × X))
    apply Disjoint.iff.backward
    intros p hp hp2
    simp [functionImage.membership] at hp
    simp [functionImage.membership] at hp2
    obtain ⟨pIn, x, hx, shapeX⟩ := hp
    obtain ⟨pIn2, y, hy, shapeY⟩ := hp2
    have stepX := compose.apply with fFunction, pairAFunction, hx
    have stepY := compose.apply with gFunction, pairBFunction, hy
    have closedX := FunctionBetween.apply_closed with fFunction, hx
    have closedY := FunctionBetween.apply_closed with gFunction, hy
    have valueX := pairWith.value with ha, closedX
    have valueY := pairWith.value with hb, closedY
    have same : (f(x), a) = (g(y), b) by cc
    have parts := orderedPair.injective with same
    exact distinct with parts.right
  have unionInjective := Injective.union_disjoint with leftCorestrict, rightCorestrict, disjoint, imagesDisjoint
  have dominated := Dominated.of_injective with unionInjective
  have leftInside := functionImage.subset at compose(pairWith(X, X, a), f, A, X, X × X), A, X × X
  have rightInside := functionImage.subset at compose(pairWith(X, X, b), g, B, X, X × X), B, X × X
  have inside := union2.subset with leftInside, rightInside
  exact Dominated.transitive with dominated, (Dominated.of_subset with inside)