-- Coordinate projections of a product: the first and second coordinate
-- of a pair as functions on A × B, bijective when the other factor is a
-- point
-- 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.Set.Function.Projection
import Image

-- Coordinates of a pair, as functions on the product.
defunique firstOf (A B p : Set) (x ∈ A) := ∃ y ∈ B, p = (x, y)
requires pair : p ∈ A × B
proof
  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with pair
  refine ⟨x, hx, y, hy, shape⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨b, hb, shapeU⟩ := first
  obtain ⟨d, hd, shapeV⟩ := second
  have equal : (u, b) = (v, d) by cc
  have coordinates := orderedPair.injective with equal
  exact coordinates.left

defunique secondOf (A B p : Set) (y ∈ B) := ∃ x ∈ A, p = (x, y)
requires pair : p ∈ A × B
proof
  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with pair
  refine ⟨y, hy, x, hx, shape⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨a, ha, shapeU⟩ := first
  obtain ⟨c, hc, shapeV⟩ := second
  have equal : (a, u) = (c, v) by cc
  have coordinates := orderedPair.injective with equal
  exact coordinates.right

defgraph firstProjection (A B : Set) (p ∈ A × B) : A := firstOf(A, B, p)
proof
  have selected := firstOf.selected with member
  exact selected.left

defgraph secondProjection (A B : Set) (p ∈ A × B) : B := secondOf(A, B, p)
proof
  have selected := secondOf.selected with member
  exact selected.left

theorem firstProjection.pair (A B x y : Set)
  requires hx : x ∈ A
  requires hy : y ∈ B
  shows firstProjection(A, B)((x, y)) = x
proof
  have pair := product.pair at x, y, A, B with *
  have selected := firstOf.selected with pair
  obtain ⟨b, hb, shape⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := firstProjection.value with pair
  cc

theorem secondProjection.pair (A B x y : Set)
  requires hx : x ∈ A
  requires hy : y ∈ B
  shows secondProjection(A, B)((x, y)) = y
proof
  have pair := product.pair at x, y, A, B with *
  have selected := secondOf.selected with pair
  obtain ⟨a, ha, shape⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := secondProjection.value with pair
  cc

-- Over a single point in the other factor, a projection is a bijection.
theorem firstProjection.bijective_singleton (A b : Set)
  shows BijectiveBetween(firstProjection(A, {b}), A × {b}, A)
proof
  have function := firstProjection.function at A, {b}
  have self : b ∈ {b} by simp [singleton.membership]
  constructor
  . constructor
    . exact function
    . intros p hp q hq z hz hpz hqz
      have valueP := FunctionBetween.apply_value with function, hp, hpz
      have valueQ := FunctionBetween.apply_value with function, hq, hqz
      obtain ⟨boundP, x, hx, y, hy, shapeP⟩ := product.membership.forward with hp
      obtain ⟨boundQ, u, hu, v, hv, shapeQ⟩ := product.membership.forward with hq
      have sameY := singleton.membership.forward with hy
      have sameV := singleton.membership.forward with hv
      rw shapeP at valueP
      rw shapeQ at valueQ
      have pairP := firstProjection.pair with hx, hy
      have pairQ := firstProjection.pair with hu, hv
      rw [shapeP, shapeQ, sameY, sameV]
      have equal : x = u by cc
      rw equal
      rfl
  . constructor
    . exact function
    . intros x hx
      have pair := product.pair with hx, self
      refine ⟨(x, b), pair, ?_⟩
      have value := firstProjection.pair with hx, self
      have related := FunctionBetween.relates_apply with function, pair
      rwa value at related

theorem secondProjection.bijective_singleton (a B : Set)
  shows BijectiveBetween(secondProjection({a}, B), {a} × B, B)
proof
  have function := secondProjection.function at {a}, B
  have self : a ∈ {a} by simp [singleton.membership]
  constructor
  . constructor
    . exact function
    . intros p hp q hq z hz hpz hqz
      have valueP := FunctionBetween.apply_value with function, hp, hpz
      have valueQ := FunctionBetween.apply_value with function, hq, hqz
      obtain ⟨boundP, x, hx, y, hy, shapeP⟩ := product.membership.forward with hp
      obtain ⟨boundQ, u, hu, v, hv, shapeQ⟩ := product.membership.forward with hq
      have sameX := singleton.membership.forward with hx
      have sameU := singleton.membership.forward with hu
      rw shapeP at valueP
      rw shapeQ at valueQ
      have pairP := secondProjection.pair with hx, hy
      have pairQ := secondProjection.pair with hu, hv
      rw [shapeP, shapeQ, sameX, sameU]
      have equal : y = v by cc
      rw equal
      rfl
  . constructor
    . exact function
    . intros y hy
      have pair := product.pair with self, hy
      refine ⟨(a, y), pair, ?_⟩
      have value := secondProjection.pair with self, hy
      have related := FunctionBetween.relates_apply with function, pair
      rwa value at related