-- The product of two topological spaces: a set is open when every point
-- has an open box inside it. The coordinate projections are continuous,
-- and open boxes are open
-- 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.Topology.Product
import Subspace

-- The product topology.
def productTopology (X T Y S : Set) : Set :=
  { W ∈ 𝒫(X × Y) | ∀ p ∈ W, ∃ U ∈ T, ∃ V ∈ S, p ∈ U × V ∧ U × V ⊆ W }

theorem productTopology.box (X T Y S U V : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  requires hU : U ∈ T
  requires hV : V ∈ S
  shows U × V ∈ productTopology(X, T, Y, S)
proof
  apply productTopology.membership.backward
  have inside := product.monotone with (IsTopology.subset with topologyX, hU), (IsTopology.subset with topologyY, hV)
  refine ⟨(powerset.membership_iff.backward with inside), ?_⟩
  intros p hp
  refine ⟨U, hU, V, hV, hp, (Subset.reflexive at U × V)⟩

theorem productTopology.topology (X T Y S : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  shows IsTopology(X × Y, productTopology(X, T, Y, S))
proof
  constructor
  . intros W hW
    have parts := productTopology.membership.forward with hW
    exact parts.left
  . constructor
    . exact productTopology.box with topologyX, topologyY, (IsTopology.whole with topologyX), (IsTopology.whole with topologyY)
    . constructor
      . intros F hF
        apply productTopology.membership.backward
        constructor
        . apply powerset.membership_iff.backward
          apply union.subset
          intros W hW
          have parts := productTopology.membership.forward with (hF with W, hW)
          exact powerset.membership_iff.forward with parts.left
        . intros p hp
          obtain ⟨W, hW, hpW⟩ := union.membership.forward with hp
          have parts := productTopology.membership.forward with (hF with W, hW)
          obtain ⟨U, hU, V, hV, inBox, boxInside⟩ := parts.right with p, hpW
          refine ⟨U, hU, V, hV, inBox, ?_⟩
          exact Subset.transitive with boxInside, (union.subset_of_member with hW)
      . intros W1 hW1 W2 hW2
        have parts1 := productTopology.membership.forward with hW1
        have parts2 := productTopology.membership.forward with hW2
        have inside1 := powerset.membership_iff.forward with parts1.left
        apply productTopology.membership.backward
        constructor
        . apply powerset.membership_iff.backward
          exact Subset.transitive with (intersection.subset_left at W1, W2), inside1
        . intros p hp
          have both := intersection.membership.forward with hp
          obtain ⟨U1, hU1, V1, hV1, inBox1, boxInside1⟩ := parts1.right with p, both.left
          obtain ⟨U2, hU2, V2, hV2, inBox2, boxInside2⟩ := parts2.right with p, both.right
          have boxes := product.intersection at U1, U2, V1, V2
          refine ⟨U1 ∩ U2, (IsTopology.intersection2 with topologyX, hU1, hU2), V1 ∩ V2, (IsTopology.intersection2 with topologyY, hV1, hV2), ?_, ?_⟩
          . rw boxes
            exact intersection.membership.backward with ⟨inBox1, inBox2⟩
          . rw boxes
            exact intersection.monotone with boxInside1, boxInside2

-- Projections are continuous: the preimage of U is the box U × Y.
theorem firstProjection.continuous (X T Y S : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  shows ContinuousMap(firstProjection(X, Y), X × Y, productTopology(X, T, Y, S), X, T)
proof
  have function := firstProjection.function at X, Y
  constructor
  . exact function
  . intros U hU
    have inside := IsTopology.subset with topologyX, hU
    have same : functionPreimage(firstProjection(X, Y), X × Y, U) = U × Y
      ext p
      constructor
      . intro hp
        have parts := functionPreimage.membership.forward with hp
        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with parts.left
        have value := firstProjection.pair with hx, hy
        rw [shape, value] at parts
        rw shape
        exact product.pair with parts.right, hy
      . intro hp
        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp
        have hxX := inside with x, hx
        have value := firstProjection.pair with hxX, hy
        apply functionPreimage.membership.backward
        rw [shape, value]
        exact ⟨(product.pair with hxX, hy), hx⟩
    rw same
    exact productTopology.box with topologyX, topologyY, hU, (IsTopology.whole with topologyY)

theorem secondProjection.continuous (X T Y S : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  shows ContinuousMap(secondProjection(X, Y), X × Y, productTopology(X, T, Y, S), Y, S)
proof
  have function := secondProjection.function at X, Y
  constructor
  . exact function
  . intros V hV
    have inside := IsTopology.subset with topologyY, hV
    have same : functionPreimage(secondProjection(X, Y), X × Y, V) = X × V
      ext p
      constructor
      . intro hp
        have parts := functionPreimage.membership.forward with hp
        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with parts.left
        have value := secondProjection.pair with hx, hy
        rw [shape, value] at parts
        rw shape
        exact product.pair with hx, parts.right
      . intro hp
        obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp
        have hyY := inside with y, hy
        have value := secondProjection.pair with hx, hyY
        apply functionPreimage.membership.backward
        rw [shape, value]
        exact ⟨(product.pair with hx, hyY), hy⟩
    rw same
    exact productTopology.box with topologyX, topologyY, (IsTopology.whole with topologyX), hV