-- Continuous maps: constant maps, inclusions, restrictions and
-- corestrictions, closed sets of a closed subspace, the pasting lemma,
-- open and closed maps, homeomorphisms as an equivalence, and a
-- continuous bijection from a compact space onto a Hausdorff space as a
-- homeomorphism
-- 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.Maps
import CompactMore
import CompactImage

-- Constant maps and inclusions are continuous.

theorem ContinuousMap.constant (X T Y S y : Set)
  requires topology : IsTopology(X, T)
  requires hy : y ∈ Y
  shows ContinuousMap(constantFunction(X, Y, y), X, T, Y, S)
proof
  have function := constantFunction.function at X, Y, y with hy
  constructor
  . exact function
  . intros V hV
    have split : y ∈ V ∨ ¬y ∈ V by tauto
    cases split with inV | outside
    . have equal : functionPreimage(constantFunction(X, Y, y), X, V) = X
        apply Subset.antisymmetric
        . exact functionPreimage.subset at constantFunction(X, Y, y), X, V
        . intros x hx
          have value := constantFunction.apply with hx, hy
          apply functionPreimage.membership.backward
          rw value
          exact ⟨hx, inV⟩
      rw equal
      exact IsTopology.whole with topology
    . have equal : functionPreimage(constantFunction(X, Y, y), X, V) = ∅
        apply Subset.empty_iff.forward
        intros x hx
        have parts := functionPreimage.membership.forward with hx
        have value := constantFunction.apply with parts.left, hy
        rw value at parts
        exfalso
        exact outside with parts.right
      rw equal
      exact IsTopology.empty with topology

theorem ContinuousMap.inclusion (X T A : Set)
  requires topology : IsTopology(X, T)
  requires hA : A ⊆ X
  shows ContinuousMap(inclusionMap(A, X), A, subspaceTopology(T, A), X, T)
proof
  have function := inclusionMap.function at A, X with hA
  constructor
  . exact function
  . intros V hV
    have equal : functionPreimage(inclusionMap(A, X), A, V) = V ∩ A
      ext x
      constructor
      . intro hx
        have parts := functionPreimage.membership.forward with hx
        have value := inclusionMap.value at A, X, x with hA, parts.left
        rw value at parts
        exact intersection.membership.backward with ⟨parts.right, parts.left⟩
      . intro hx
        have parts := intersection.membership.forward with hx
        have value := inclusionMap.value at A, X, x with hA, parts.right
        apply functionPreimage.membership.backward
        rw value
        exact ⟨parts.right, parts.left⟩
    rw equal
    exact subspaceTopology.membership.backward with ⟨V, hV, rfl⟩

-- Restriction to a subspace and corestriction to a subspace of the
-- codomain.

theorem restrict.preimage (f X Y A V : Set)
  requires function : f : X → Y
  requires hA : A ⊆ X
  shows functionPreimage(restrict(f, A), A, V) = functionPreimage(f, X, V) ∩ A
proof
  ext x
  constructor
  . intro hx
    have parts := functionPreimage.membership.forward with hx
    have value := restrict.domain_apply with function, hA, parts.left
    rw value at parts
    have hxX := hA with x, parts.left
    exact intersection.membership.backward with ⟨(functionPreimage.membership.backward with ⟨hxX, parts.right⟩), parts.left⟩
  . intro hx
    have parts := intersection.membership.forward with hx
    have inner := functionPreimage.membership.forward with parts.left
    have value := restrict.domain_apply with function, hA, parts.right
    apply functionPreimage.membership.backward
    rw value
    exact ⟨parts.right, inner.right⟩

theorem ContinuousMap.restrict (f X T Y S A : Set)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  requires hA : A ⊆ X
  shows ContinuousMap(restrict(f, A), A, subspaceTopology(T, A), Y, S)
proof
  have function := continuous.left
  constructor
  . exact restrict.domain_function with function, hA
  . intros V hV
    have equal := restrict.preimage at f, X, Y, A, V with function, hA
    rw equal
    have isOpen := continuous.right with V, hV
    exact subspaceTopology.membership.backward with ⟨functionPreimage(f, X, V), isOpen, rfl⟩

theorem ContinuousMap.corestrict (f X T Y S B : Set)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  requires hB : B ⊆ Y
  requires values : ∀ x ∈ X, f(x) ∈ B
  shows ContinuousMap(f, X, T, B, subspaceTopology(S, B))
proof
  have function := continuous.left
  constructor
  . exact FunctionBetween.codomain_of_values with function, values
  . intros W hW
    obtain ⟨V, hV, shape⟩ := subspaceTopology.membership.forward with hW
    have equal : functionPreimage(f, X, W) = functionPreimage(f, X, V)
      ext x
      constructor
      . intro hx
        have parts := functionPreimage.membership.forward with hx
        rw ← shape at parts
        have inner := intersection.membership.forward with parts.right
        exact functionPreimage.membership.backward with ⟨parts.left, inner.left⟩
      . intro hx
        have parts := functionPreimage.membership.forward with hx
        apply functionPreimage.membership.backward
        refine ⟨parts.left, ?_⟩
        rw ← shape
        exact intersection.membership.backward with ⟨parts.right, (values with x, parts.left)⟩
    rw equal
    exact continuous.right with V, hV

theorem ContinuousMap.into_image (f X T Y S : Set)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  shows ContinuousMap(f, X, T, functionImage(f, X, Y), subspaceTopology(S, functionImage(f, X, Y)))
proof
  have function := continuous.left
  apply ContinuousMap.corestrict with continuous, (functionImage.subset at f, X, Y)
  intros x hx
  exact functionImage.value with function, hx

-- Closed sets of a subspace: traces of closed sets, and closed sets of a
-- closed subspace are closed in the whole space.

theorem IsClosed.subspace_trace (X T A C : Set)
  requires topology : IsTopology(X, T)
  requires hA : A ⊆ X
  requires closed : IsClosed(X, T, C)
  shows IsClosed(A, subspaceTopology(T, A), C ∩ A)
proof
  constructor
  . exact intersection.subset_right at C, A
  . have equal : complement(A, C ∩ A) = complement(X, C) ∩ A
      ext x
      constructor
      . intro hx
        have parts := complement.membership.forward with hx
        have hxX := hA with x, parts.left
        apply intersection.membership.backward
        refine ⟨?_, parts.left⟩
        apply complement.membership.backward
        refine ⟨hxX, ?_⟩
        intro inC
        apply parts.right
        exact intersection.membership.backward with ⟨inC, parts.left⟩
      . intro hx
        have parts := intersection.membership.forward with hx
        have away := complement.membership.forward with parts.left
        apply complement.membership.backward
        refine ⟨parts.right, ?_⟩
        intro inBoth
        have inner := intersection.membership.forward with inBoth
        exact away.right with inner.left
    rw equal
    exact subspaceTopology.membership.backward with ⟨complement(X, C), closed.right, rfl⟩

theorem IsClosed.of_closed_subspace (X T A C : Set)
  requires topology : IsTopology(X, T)
  requires closedA : IsClosed(X, T, A)
  requires closed : IsClosed(A, subspaceTopology(T, A), C)
  shows IsClosed(X, T, C)
proof
  have hA := closedA.left
  have hCA := closed.left
  obtain ⟨U, hU, shape⟩ := subspaceTopology.membership.forward with closed.right
  have equal : C = A ∩ complement(X, U)
    ext x
    constructor
    . intro hx
      have hxA := hCA with x, hx
      apply intersection.membership.backward
      refine ⟨hxA, ?_⟩
      apply complement.membership.backward
      refine ⟨(hA with x, hxA), ?_⟩
      intro inU
      have inTrace : x ∈ U ∩ A := intersection.membership.backward with ⟨inU, hxA⟩
      rw shape at inTrace
      have away := complement.membership.forward with inTrace
      exact away.right with hx
    . intro hx
      have parts := intersection.membership.forward with hx
      have away := complement.membership.forward with parts.right
      by_contra outside
      have inComplement : x ∈ complement(A, C) := complement.membership.backward with ⟨parts.left, outside⟩
      rw ← shape at inComplement
      have inner := intersection.membership.forward with inComplement
      exact away.right with inner.left
  rw equal
  exact IsClosed.intersection2 with topology, closedA, (Open.complement_closed with topology, hU)

-- The pasting lemma: a map continuous on each of two closed pieces
-- covering the space is continuous.
theorem ContinuousMap.pasting (f X T Y S C D : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  requires function : f : X → Y
  requires closedC : IsClosed(X, T, C)
  requires closedD : IsClosed(X, T, D)
  requires whole : C ∪ D = X
  requires onC : ContinuousMap(restrict(f, C), C, subspaceTopology(T, C), Y, S)
  requires onD : ContinuousMap(restrict(f, D), D, subspaceTopology(T, D), Y, S)
  shows ContinuousMap(f, X, T, Y, S)
proof
  have hC := closedC.left
  have hD := closedD.left
  apply ContinuousMap.of_closed_preimages with topologyX, topologyY, function
  intros K closedK
  have preimageC := ContinuousMap.closed_preimage with onC, closedK
  have preimageD := ContinuousMap.closed_preimage with onD, closedK
  have equalC := restrict.preimage at f, X, Y, C, K with function, hC
  have equalD := restrict.preimage at f, X, Y, D, K with function, hD
  rw equalC at preimageC
  rw equalD at preimageD
  have closedInC := IsClosed.of_closed_subspace with topologyX, closedC,
    preimageC
  have closedInD := IsClosed.of_closed_subspace with topologyX, closedD,
    preimageD
  have below := functionPreimage.subset at f, X, K
  have split : functionPreimage(f, X, K) = functionPreimage(f, X, K) ∩ C ∪ functionPreimage(f, X, K) ∩ D
    rw [← intersection.union2_distrib, whole]
    symm
    exact intersection.eq_left_of_subset with below
  rw split
  exact IsClosed.union2 with topologyX, closedInC, closedInD

-- Open maps, closed maps, and homeomorphisms.

predicate OpenMap (f X T Y S : Set) :=
  FunctionBetween(f, X, Y) ∧ (∀ U ∈ T, functionImage(f, U, Y) ∈ S)

predicate ClosedMap (f X T Y S : Set) :=
  FunctionBetween(f, X, Y) ∧
  (∀ C, IsClosed(X, T, C) → IsClosed(Y, S, functionImage(f, C, Y)))

-- Under a bijection the image of U is the preimage of U under the inverse.
theorem Bijective.image_eq_preimage (f X Y U : Set)
  requires bijective : BijectiveBetween(f, X, Y)
  requires hU : U ⊆ X
  shows functionImage(f, U, Y) = functionPreimage(converse(f, X, Y), Y, U)
proof
  ext y
  constructor
  . intro hy
    have parts := functionImage.membership.forward with hy
    obtain ⟨hyY, x, hx, shape⟩ := parts
    have back := Bijective.inverse_apply with bijective, (hU with x, hx)
    have back2 : converse(f, X, Y)(y) = x
      rw shape
      exact back
    apply functionPreimage.membership.backward
    rw back2
    exact ⟨hyY, hx⟩
  . intro hy
    have parts := functionPreimage.membership.forward with hy
    have forward := Bijective.apply_inverse with bijective, parts.left
    apply functionImage.membership.backward
    refine ⟨parts.left, converse(f, X, Y)(y), parts.right, ?_⟩
    rw forward
    rfl

theorem IsHomeomorphism.open_map (f X T Y S : Set)
  requires topology : IsTopology(X, T)
  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)
  shows OpenMap(f, X, T, Y, S)
proof
  obtain ⟨bijective, continuous, inverse⟩ := homeomorphism
  constructor
  . exact continuous.left
  . intros U hU
    have equal := Bijective.image_eq_preimage with bijective, (IsTopology.subset with topology, hU)
    rw equal
    exact inverse.right with U, hU

theorem IsHomeomorphism.closed_map (f X T Y S : Set)
  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)
  shows ClosedMap(f, X, T, Y, S)
proof
  obtain ⟨bijective, continuous, inverse⟩ := homeomorphism
  constructor
  . exact continuous.left
  . intros C closed
    have equal := Bijective.image_eq_preimage with bijective, closed.left
    rw equal
    exact ContinuousMap.closed_preimage with inverse, closed

theorem IsHomeomorphism.of_open_bijection (f X T Y S : Set)
  requires topology : IsTopology(X, T)
  requires bijective : BijectiveBetween(f, X, Y)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  requires openMap : OpenMap(f, X, T, Y, S)
  shows IsHomeomorphism(f, X, T, Y, S)
proof
  refine ⟨bijective, continuous, ?_⟩
  constructor
  . exact converse.function_of_bijective with bijective
  . intros U hU
    have equal := Bijective.image_eq_preimage with bijective, (IsTopology.subset with topology, hU)
    rw ← equal
    exact openMap.right with U, hU

theorem IsHomeomorphism.of_closed_bijection (f X T Y S : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  requires bijective : BijectiveBetween(f, X, Y)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  requires closedMap : ClosedMap(f, X, T, Y, S)
  shows IsHomeomorphism(f, X, T, Y, S)
proof
  refine ⟨bijective, continuous, ?_⟩
  have inverse := converse.function_of_bijective with bijective
  apply ContinuousMap.of_closed_preimages with topologyY, topologyX, inverse
  intros C closed
  have equal := Bijective.image_eq_preimage with bijective, closed.left
  rw ← equal
  exact closedMap.right with C, closed

theorem IsHomeomorphism.identity (X T : Set)
  requires topology : IsTopology(X, T)
  shows IsHomeomorphism(identity(X), X, T, X, T)
proof
  have openMap : OpenMap(identity(X), X, T, X, T)
    constructor
    . exact identity.function at X
    . intros U hU
      have equal := functionImage.identity_of_subset with (IsTopology.subset with topology, hU)
      rwa equal
  exact IsHomeomorphism.of_open_bijection with topology, (identity.bijective at X), (ContinuousMap.identity with topology), openMap

theorem OpenMap.compose (g f X T Y S Z R : Set)
  requires topology : IsTopology(X, T)
  requires first : OpenMap(f, X, T, Y, S)
  requires second : OpenMap(g, Y, S, Z, R)
  shows OpenMap(compose(g, f, X, Y, Z), X, T, Z, R)
proof
  have fFunction := first.left
  have gFunction := second.left
  constructor
  . exact compose.function with fFunction, gFunction
  . intros U hU
    have hUX := IsTopology.subset with topology, hU
    have equal := functionImage.compose with fFunction, gFunction, hUX
    rw equal
    exact second.right with functionImage(f, U, Y), (first.right with U, hU)

theorem ClosedMap.compose (g f X T Y S Z R : Set)
  requires first : ClosedMap(f, X, T, Y, S)
  requires second : ClosedMap(g, Y, S, Z, R)
  shows ClosedMap(compose(g, f, X, Y, Z), X, T, Z, R)
proof
  have fFunction := first.left
  have gFunction := second.left
  constructor
  . exact compose.function with fFunction, gFunction
  . intros C closed
    have equal := functionImage.compose with fFunction, gFunction, closed.left
    rw equal
    exact second.right with functionImage(f, C, Y), (first.right with C, closed)

theorem IsHomeomorphism.compose (g f X T Y S Z R : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  requires first : IsHomeomorphism(f, X, T, Y, S)
  requires second : IsHomeomorphism(g, Y, S, Z, R)
  shows IsHomeomorphism(compose(g, f, X, Y, Z), X, T, Z, R)
proof
  have openF := IsHomeomorphism.open_map with topologyX, first
  have openG := IsHomeomorphism.open_map with topologyY, second
  have openMap := OpenMap.compose with topologyX, openF, openG
  obtain ⟨bijectiveF, continuousF, inverseF⟩ := first
  obtain ⟨bijectiveG, continuousG, inverseG⟩ := second
  have bijective := compose.bijective with bijectiveF, bijectiveG
  have continuous := ContinuousMap.compose with continuousF, continuousG
  exact IsHomeomorphism.of_open_bijection with topologyX, bijective, continuous, openMap

-- A continuous map from a compact space to a Hausdorff space is closed,
-- so a continuous bijection between them is a homeomorphism.

theorem IsCompact.continuous_closed_map (f X T Y S : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  requires compact : IsCompact(X, T, X)
  requires hausdorff : IsHausdorff(Y, S)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  shows ClosedMap(f, X, T, Y, S)
proof
  constructor
  . exact continuous.left
  . intros C closed
    have compactC := IsCompact.closed_subset with topologyX, compact, closed, closed.left
    have compactImage := IsCompact.image with continuous, compactC
    exact IsCompact.hausdorff_closed with topologyY, hausdorff, compactImage

theorem IsHomeomorphism.compact_hausdorff (f X T Y S : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  requires compact : IsCompact(X, T, X)
  requires hausdorff : IsHausdorff(Y, S)
  requires bijective : BijectiveBetween(f, X, Y)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  shows IsHomeomorphism(f, X, T, Y, S)
proof
  have closedMap := IsCompact.continuous_closed_map with topologyX, topologyY, compact, hausdorff, continuous
  exact IsHomeomorphism.of_closed_bijection with topologyX, topologyY, bijective, continuous, closedMap

-- Topological properties carried along maps.

theorem IsCompact.of_surjection (f X T Y S : Set)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  requires surjective : SurjectiveBetween(f, X, Y)
  requires compact : IsCompact(X, T, X)
  shows IsCompact(Y, S, Y)
proof
  have function := continuous.left
  have image := IsCompact.image with continuous, compact
  have whole : functionImage(f, X, Y) = Y
    apply Subset.antisymmetric
    . exact functionImage.subset at f, X, Y
    . intros y hy
      obtain ⟨x, hx, edge⟩ := surjective.right with y, hy
      have value := FunctionBetween.apply_value with function, hx, edge
      rw ← value
      exact functionImage.value with function, hx
  rwa whole at image

theorem IsDense.image (f X T Y S A : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  requires surjective : SurjectiveBetween(f, X, Y)
  requires hA : A ⊆ X
  requires dense : IsDense(X, T, A)
  shows IsDense(Y, S, functionImage(f, A, Y))
proof
  have function := continuous.left
  have equal : closure(X, T, A) = X := dense
  have inclusion := ContinuousMap.image_closure with topologyX, topologyY, continuous, hA
  rw equal at inclusion
  have whole : functionImage(f, X, Y) = Y
    apply Subset.antisymmetric
    . exact functionImage.subset at f, X, Y
    . intros y hy
      obtain ⟨x, hx, edge⟩ := surjective.right with y, hy
      have value := FunctionBetween.apply_value with function, hx, edge
      rw ← value
      exact functionImage.value with function, hx
  rw whole at inclusion
  have inside := closure.subset with topologyY, (functionImage.subset at f, A, Y)
  exact Subset.antisymmetric with inside, inclusion

theorem IsHausdorff.of_homeomorphism (f X T Y S : Set)
  requires topologyX : IsTopology(X, T)
  requires topologyY : IsTopology(Y, S)
  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)
  requires hausdorff : IsHausdorff(X, T)
  shows IsHausdorff(Y, S)
proof
  have openMap := IsHomeomorphism.open_map with topologyX, homeomorphism
  obtain ⟨bijective, continuous, inverse⟩ := homeomorphism
  have injective := Bijective.injective with bijective
  have inverseFunction := converse.function_of_bijective with bijective
  intros y1 hy1 y2 hy2 distinct
  have hx1 := FunctionBetween.apply_closed with inverseFunction, hy1
  have hx2 := FunctionBetween.apply_closed with inverseFunction, hy2
  have forward1 := Bijective.apply_inverse with bijective, hy1
  have forward2 := Bijective.apply_inverse with bijective, hy2
  have distinctX : converse(f, X, Y)(y1) ≠ converse(f, X, Y)(y2)
    intro same
    apply distinct
    rw [← forward1, ← forward2, same]
    rfl
  obtain ⟨U, hU, V, hV, inU, inV, disjoint⟩ := hausdorff with converse(f, X, Y)(y1), hx1, converse(f, X, Y)(y2), hx2, distinctX
  have separated := Disjoint.iff.forward with disjoint
  have hUX := IsTopology.subset with topologyX, hU
  have hVX := IsTopology.subset with topologyX, hV
  refine ⟨functionImage(f, U, Y), (openMap.right with U, hU), functionImage(f, V, Y), (openMap.right with V, hV), ?_, ?_, ?_⟩
  . apply functionImage.membership.backward
    refine ⟨hy1, converse(f, X, Y)(y1), inU, ?_⟩
    rw forward1
    rfl
  . apply functionImage.membership.backward
    refine ⟨hy2, converse(f, X, Y)(y2), inV, ?_⟩
    rw forward2
    rfl
  . apply Disjoint.iff.backward
    intros z hzU hzV
    have partsU := functionImage.membership.forward with hzU
    have partsV := functionImage.membership.forward with hzV
    obtain ⟨hzY, a, ha, shapeA⟩ := partsU
    obtain ⟨hzY2, b, hb, shapeB⟩ := partsV
    have same : f(a) = f(b)
      rw [← shapeA, ← shapeB]
      rfl
    have equal := Injective.apply_cancel with injective, (hUX with a, ha), (hVX with b, hb), same
    rw equal at ha
    exact separated with b, ha, hb