-- Bases of a topology: every open set is a union of basis sets, the
-- topology generated by a family satisfying the basis axioms, closure,
-- interior, and continuity tested on a basis, bases of subspaces and
-- products, and the open balls as a basis of the real line
-- 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.Basis
import Separation
import Real

predicate Basis (X T B : Set) :=
  B ⊆ T ∧ (∀ U ∈ T, ∀ x ∈ U, ∃ W ∈ B, x ∈ W ∧ W ⊆ U)

theorem Basis.subset (X T B : Set)
  requires basis : Basis(X, T, B)
  shows B ⊆ T
proof
  exact basis.left

theorem Basis.refine (X T B U x : Set)
  requires basis : Basis(X, T, B)
  requires hU : U ∈ T
  requires hx : x ∈ U
  shows ∃ W ∈ B, x ∈ W ∧ W ⊆ U
proof
  exact basis.right with U, hU, x, hx

theorem Basis.self (X T : Set)
  shows Basis(X, T, T)
proof
  constructor
  . exact Subset.reflexive at T
  . intros U hU x hx
    exact ⟨U, hU, hx, (Subset.reflexive at U)⟩

-- The basis sets inside U.

def basisBelow (B U : Set) : Set := { W ∈ B | W ⊆ U }

theorem basisBelow.union (B U : Set)
  requires refines : ∀ x ∈ U, ∃ W ∈ B, x ∈ W ∧ W ⊆ U
  shows U = ⋃(basisBelow(B, U))
proof
  apply Subset.antisymmetric
  . intros x hx
    obtain ⟨W, hW, hxW, below⟩ := refines with x, hx
    have found : W ∈ basisBelow(B, U) := basisBelow.membership.backward with ⟨hW, below⟩
    exact union.contains with found, hxW
  . apply union.subset
    intros W hW
    have parts := basisBelow.membership.forward with hW
    exact parts.right

theorem basisBelow.open (X T B U : Set)
  requires topology : IsTopology(X, T)
  requires inside : B ⊆ T
  shows ⋃(basisBelow(B, U)) ∈ T
proof
  apply IsTopology.union with topology
  intros W hW
  have parts := basisBelow.membership.forward with hW
  exact inside with W, parts.left

-- Every open set is the union of the basis sets inside it.
theorem Basis.open_union (X T B U : Set)
  requires basis : Basis(X, T, B)
  requires hU : U ∈ T
  shows U = ⋃(basisBelow(B, U))
proof
  apply basisBelow.union
  intros x hx
  exact basis.right with U, hU, x, hx

theorem Basis.open_iff (X T B U : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  shows U ∈ T ↔ U ⊆ X ∧ (∀ x ∈ U, ∃ W ∈ B, x ∈ W ∧ W ⊆ U)
proof
  constructor
  . intro hU
    constructor
    . exact IsTopology.subset with topology, hU
    . intros x hx
      exact basis.right with U, hU, x, hx
  . intro h
    obtain ⟨inside, refines⟩ := h
    have equal := basisBelow.union with refines
    rw equal
    exact basisBelow.open with topology, basis.left

theorem Basis.covers (X T B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  shows ⋃(B) = X
proof
  apply Subset.antisymmetric
  . apply union.subset
    intros W hW
    exact IsTopology.subset with topology, (basis.left with W, hW)
  . intros x hx
    obtain ⟨W, hW, hxW, inside⟩ := basis.right with X, (IsTopology.whole with topology), x, hx
    exact union.contains with hW, hxW

theorem Basis.meet (X T B W1 W2 x : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires hW1 : W1 ∈ B
  requires hW2 : W2 ∈ B
  requires hx : x ∈ W1 ∩ W2
  shows ∃ W ∈ B, x ∈ W ∧ W ⊆ W1 ∩ W2
proof
  have openMeet := IsTopology.intersection2 with topology, (basis.left with W1, hW1), (basis.left with W2, hW2)
  exact basis.right with W1 ∩ W2, openMeet, x, hx

-- The basis axioms: a family of subsets of X that covers X and refines
-- pairwise intersections; such a family generates a topology.

predicate BasisAxioms (X B : Set) :=
  B ⊆ 𝒫(X) ∧ (∀ x ∈ X, ∃ W ∈ B, x ∈ W) ∧
  (∀ W1 ∈ B, ∀ W2 ∈ B, ∀ x ∈ W1 ∩ W2, ∃ W ∈ B, x ∈ W ∧ W ⊆ W1 ∩ W2)

theorem Basis.axioms (X T B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  shows BasisAxioms(X, B)
proof
  refine ⟨?_, ?_, ?_⟩
  . intros W hW
    apply powerset.membership_iff.backward
    exact IsTopology.subset with topology, (basis.left with W, hW)
  . intros x hx
    obtain ⟨W, hW, hxW, inside⟩ := basis.right with X, (IsTopology.whole with topology), x, hx
    exact ⟨W, hW, hxW⟩
  . intros W1 hW1 W2 hW2 x hx
    exact Basis.meet with topology, basis, hW1, hW2, hx

def generatedTopology (X B : Set) : Set :=
  { U ∈ 𝒫(X) | ∀ x ∈ U, ∃ W ∈ B, x ∈ W ∧ W ⊆ U }

theorem generatedTopology.contains (X B : Set)
  requires axioms : BasisAxioms(X, B)
  shows B ⊆ generatedTopology(X, B)
proof
  intros W hW
  apply generatedTopology.membership.backward
  refine ⟨(axioms.left with W, hW), ?_⟩
  intros x hx
  exact ⟨W, hW, hx, (Subset.reflexive at W)⟩

theorem generatedTopology.topology (X B : Set)
  requires axioms : BasisAxioms(X, B)
  shows IsTopology(X, generatedTopology(X, B))
proof
  obtain ⟨inside, covers, meets⟩ := axioms
  refine ⟨?_, ?_, ?_, ?_⟩
  . intros U hU
    have parts := generatedTopology.membership.forward with hU
    exact parts.left
  . apply generatedTopology.membership.backward
    refine ⟨(powerset.self at X), ?_⟩
    intros x hx
    obtain ⟨W, hW, hxW⟩ := covers with x, hx
    have below := powerset.membership_iff.forward with (inside with W, hW)
    exact ⟨W, hW, hxW, below⟩
  . intros S hS
    apply generatedTopology.membership.backward
    constructor
    . apply powerset.membership_iff.backward
      apply union.subset
      intros U hU
      have parts := generatedTopology.membership.forward with (hS with U, hU)
      exact powerset.membership_iff.forward with parts.left
    . intros x hx
      obtain ⟨U, hU, hxU⟩ := union.membership.forward with hx
      have parts := generatedTopology.membership.forward with (hS with U, hU)
      obtain ⟨W, hW, hxW, below⟩ := parts.right with x, hxU
      refine ⟨W, hW, hxW, ?_⟩
      exact Subset.transitive with below, (union.subset_of_member with hU)
  . intros U hU V hV
    have partsU := generatedTopology.membership.forward with hU
    have partsV := generatedTopology.membership.forward with hV
    apply generatedTopology.membership.backward
    constructor
    . apply powerset.membership_iff.backward
      have insideU := powerset.membership_iff.forward with partsU.left
      exact Subset.transitive with (intersection.subset_left at U, V), insideU
    . intros x hx
      have both := intersection.membership.forward with hx
      obtain ⟨W1, hW1, hxW1, belowU⟩ := partsU.right with x, both.left
      obtain ⟨W2, hW2, hxW2, belowV⟩ := partsV.right with x, both.right
      have inMeet : x ∈ W1 ∩ W2 := intersection.membership.backward with ⟨hxW1, hxW2⟩
      obtain ⟨W, hW, hxW, below⟩ := meets with W1, hW1, W2, hW2, x, inMeet
      refine ⟨W, hW, hxW, ?_⟩
      exact Subset.transitive with below, (intersection.monotone with belowU, belowV)

theorem generatedTopology.basis (X B : Set)
  requires axioms : BasisAxioms(X, B)
  shows Basis(X, generatedTopology(X, B), B)
proof
  constructor
  . exact generatedTopology.contains with axioms
  . intros U hU x hx
    have parts := generatedTopology.membership.forward with hU
    exact parts.right with x, hx

-- The generated topology is the coarsest topology containing B.
theorem generatedTopology.coarsest (X T B : Set)
  requires topology : IsTopology(X, T)
  requires inside : B ⊆ T
  shows generatedTopology(X, B) ⊆ T
proof
  intros U hU
  have parts := generatedTopology.membership.forward with hU
  have equal := basisBelow.union with parts.right
  rw equal
  exact basisBelow.open with topology, inside

theorem Basis.generated (X T B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  shows T = generatedTopology(X, B)
proof
  apply Subset.antisymmetric
  . intros U hU
    apply generatedTopology.membership.backward
    constructor
    . exact powerset.membership_iff.backward with (IsTopology.subset with topology, hU)
    . intros x hx
      exact basis.right with U, hU, x, hx
  . exact generatedTopology.coarsest with topology, basis.left

-- Two bases of the same space determine each other's topology.
theorem Basis.unique_topology (X T T2 B : Set)
  requires topology : IsTopology(X, T)
  requires topology2 : IsTopology(X, T2)
  requires basis : Basis(X, T, B)
  requires basis2 : Basis(X, T2, B)
  shows T = T2
proof
  have first := Basis.generated with topology, basis
  have second := Basis.generated with topology2, basis2
  rw [first, second]
  rfl

-- Closure, interior, and continuity are tested on a basis.

theorem Basis.closure_membership (X T B A x : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires hA : A ⊆ X
  shows x ∈ closure(X, T, A) ↔ x ∈ X ∧ (∀ W ∈ B, x ∈ W → Nonempty(W ∩ A))
proof
  have characterization := closure.membership at X, T, A, x with topology, hA
  constructor
  . intro hx
    have parts := characterization.forward with hx
    refine ⟨parts.left, ?_⟩
    intros W hW hxW
    exact parts.right with W, (basis.left with W, hW), hxW
  . intro h
    obtain ⟨hxX, meets⟩ := h
    apply characterization.backward
    refine ⟨hxX, ?_⟩
    intros U hU hxU
    obtain ⟨W, hW, hxW, below⟩ := basis.right with U, hU, x, hxU
    obtain ⟨a, ha⟩ := meets with W, hW, hxW
    have inner := intersection.membership.forward with ha
    witness a
    exact intersection.membership.backward with ⟨(below with a, inner.left), inner.right⟩

theorem Basis.interior_membership (X T B A x : Set)
  requires basis : Basis(X, T, B)
  shows x ∈ interiorIn(T, A) ↔ ∃ W ∈ B, x ∈ W ∧ W ⊆ A
proof
  have characterization := interiorIn.membership at T, A, x
  constructor
  . intro hx
    obtain ⟨U, hU, hxU, below⟩ := characterization.forward with hx
    obtain ⟨W, hW, hxW, belowU⟩ := basis.right with U, hU, x, hxU
    exact ⟨W, hW, hxW, (Subset.transitive with belowU, below)⟩
  . intro h
    obtain ⟨W, hW, hxW, below⟩ := h
    apply characterization.backward
    exact ⟨W, (basis.left with W, hW), hxW, below⟩

theorem ContinuousMap.of_basis (f X T Y S B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(Y, S, B)
  requires function : f : X → Y
  requires pulledOpen : ∀ W ∈ B, functionPreimage(f, X, W) ∈ T
  shows ContinuousMap(f, X, T, Y, S)
proof
  constructor
  . exact function
  . intros V hV
    have equal : functionPreimage(f, X, V) = ⋃(preimages(f, X, basisBelow(B, V)))
      ext x
      constructor
      . intro hx
        have parts := functionPreimage.membership.forward with hx
        obtain ⟨W, hW, inW, below⟩ := basis.right with V, hV, f(x), parts.right
        have found : W ∈ basisBelow(B, V) := basisBelow.membership.backward with ⟨hW, below⟩
        have pulled : functionPreimage(f, X, W) ∈ preimages(f, X, basisBelow(B, V)) := preimages.membership.backward with ⟨W, found, rfl⟩
        have inPreimage : x ∈ functionPreimage(f, X, W) := functionPreimage.membership.backward with ⟨parts.left, inW⟩
        exact union.contains with pulled, inPreimage
      . intro hx
        obtain ⟨P, hP, hxP⟩ := union.membership.forward with hx
        obtain ⟨W, hW, shape⟩ := preimages.membership.forward with hP
        rw ← shape at hxP
        have parts := functionPreimage.membership.forward with hxP
        have belowParts := basisBelow.membership.forward with hW
        apply functionPreimage.membership.backward
        exact ⟨parts.left, (belowParts.right with f(x), parts.right)⟩
    rw equal
    apply IsTopology.union with topology
    intros P hP
    obtain ⟨W, hW, shape⟩ := preimages.membership.forward with hP
    rw ← shape
    have belowParts := basisBelow.membership.forward with hW
    exact pulledOpen with W, belowParts.left

-- Bases of subspaces and products.

theorem Basis.subspace (X T B A : Set)
  requires basis : Basis(X, T, B)
  requires hA : A ⊆ X
  shows Basis(A, subspaceTopology(T, A), subspaceTopology(B, A))
proof
  constructor
  . intros W hW
    obtain ⟨W0, hW0, shape⟩ := subspaceTopology.membership.forward with hW
    apply subspaceTopology.membership.backward
    exact ⟨W0, (basis.left with W0, hW0), shape⟩
  . intros V hV x hx
    obtain ⟨U, hU, shape⟩ := subspaceTopology.membership.forward with hV
    rw ← shape at hx
    have parts := intersection.membership.forward with hx
    obtain ⟨W, hW, hxW, below⟩ := basis.right with U, hU, x, parts.left
    have traced : W ∩ A ∈ subspaceTopology(B, A) := subspaceTopology.membership.backward with ⟨W, hW, rfl⟩
    refine ⟨W ∩ A, traced, (intersection.membership.backward with ⟨hxW, parts.right⟩), ?_⟩
    rw ← shape
    exact intersection.monotone_left with below

def boxes (X T Y S : Set) : Set :=
  { W ∈ 𝒫(X × Y) | ∃ U ∈ T, ∃ V ∈ S, W = U × V }

theorem Basis.product (X T Y S : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  shows Basis(X × Y, productTopology(X, T, Y, S), boxes(X, T, Y, S))
proof
  constructor
  . intros W hW
    have parts := boxes.membership.forward with hW
    obtain ⟨U, hU, V, hV, shape⟩ := parts.right
    rw shape
    exact productTopology.box with topologyX, topologyY, hU, hV
  . intros W hW p hp
    have parts := productTopology.membership.forward with hW
    obtain ⟨U, hU, V, hV, inBox, below⟩ := parts.right with p, hp
    have inside := product.monotone with (IsTopology.subset with topologyX, hU), (IsTopology.subset with topologyY, hV)
    have found : U × V ∈ boxes(X, T, Y, S)
      apply boxes.membership.backward
      exact ⟨(powerset.membership_iff.backward with inside), U, hU, V, hV, rfl⟩
    exact ⟨U × V, found, inBox, below⟩

-- The open balls form a basis of the real line.

def openBalls : Set :=
  { W ∈ 𝒫(ℝ) | ∃ C ∈ ℝ, ∃ E ∈ ℝ, 0 < E ∧ W = openBall(C, E) }

theorem openBall.member_balls (C E : Real)
  requires positive : 0 < E
  shows openBall(C, E) ∈ openBalls
proof
  have realC : C ∈ ℝ by typecheck
  have realE : E ∈ ℝ by typecheck
  apply openBalls.membership.backward
  exact ⟨(powerset.membership_iff.backward with (openBall.subset_reals at C, E)), C, realC, E, realE, positive, rfl⟩

theorem realTopology.basis
  shows Basis(ℝ, realTopology, openBalls)
proof
  constructor
  . intros W hW
    have parts := openBalls.membership.forward with hW
    obtain ⟨C, hC, E, hE, positive, shape⟩ := parts.right
    rw shape
    exact openBall.open at C, E
  . intros U hU x hx
    have parts := realTopology.membership.forward with hU
    have inside := powerset.membership_iff.forward with parts.left
    have hxR := inside with x, hx
    obtain ⟨E, hE, positive, below⟩ := parts.right with x, hx
    have center := openBall.center at x, E with positive
    have found := openBall.member_balls at x, E with positive
    exact ⟨openBall(x, E), found, center, below⟩