Challenge.lean

/-
Copyright (c) 2026  Lars Warren Ericson.  All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lars Warren Ericson.
-/
import Mathlib.Order.CompleteLattice.Basic
import Mathlib.Order.UpperLower.Basic
import Mathlib.Order.Directed
import Mathlib.Order.BourbakiWitt
import Mathlib.Topology.Order.ScottTopology
import Mathlib.Topology.Homeomorph.Defs

/-!
# Scott 1972, Theorem 4.4 (Palomar statement of record)

Ground truth for the wording is
`sources/ScottContinLatt1972.md`. Theorem 4.4 there is:

> The inverse limit \(D_\infty\) of the recursively defined sequence
> \(\langle D_n, j_n \rangle_{n=0}^{\infty}\) of function spaces is not only a
> continuous lattice, but it is also homeomorphic to its own function space
> \([D_\infty \to D_\infty]\).

The sequence is the one defined just above that theorem: \(D = D_0\) a given
continuous lattice; \(D_1 = [D_0 \to D_0]\) with a chosen projection pair
\(i_0, j_0\) (Proposition 3.13); then recursively
\(D_{n+1} = [D_n \to D_n]\) and \(j_{n+1} = [j_n \to j_n]\) by Proposition 3.7.
Definition 3.1: \([X \to Y]\) is the space of continuous functions with the
product topology (pointwise convergence). The inverse limit has the subspace
topology induced from the product of the \(D_n\). Theorem 3.3 and Proposition
4.1 identify these source topologies with the corresponding lattice Scott
topologies, but the theorem below names the source topologies explicitly.

The lattice and tower data used by the theorem are concrete below:
`ScottMap.instCompleteLattice` is generated by pointwise order and pointwise
arbitrary suprema; `instCompleteLattice` on the inverse limit is generated by
coordinatewise order and coordinatewise arbitrary infima; and `towerProj`
recurses by the Proposition 3.7 formulas `f ↦ i ∘ f ∘ j` and
`g ↦ j ∘ g ∘ i`. Comparator checks these definition bodies, while the named
proof obligations alone are left open in this Challenge.

This file imports only Mathlib. The proofs live in `Scott1972/ContinuousLattice/*`
and are compared against this file by Comparator via `Solution.lean`.

## How to read this file

The definitions below are the vocabulary of the claim. A reader who wants to
check *what* has been proved should read this file and need not read the proof
development. `Solution.lean` imports the sorry-free library.
-/

namespace Scott1972.ContinuousLattice

open Set Topology

universe u v

variable {D : Type u} {D' : Type v} [CompleteLattice D] [CompleteLattice D']

/-- **Scott 1972, §2.** `U` is *Scott-open* when it is an upper set and is
inaccessible by suprema of non-empty directed sets. -/
def ScottOpen (U : Set D) : Prop :=
  letI : LE D :=
    (CompleteLattice.toCompleteSemilatticeInf (α := D)).toPartialOrder.toPreorder.toLE
  letI : SupSet D :=
    (CompleteLattice.toCompleteSemilatticeSup (α := D)).toSupSet
  IsUpperSet U ∧
    ∀ ⦃S : Set D⦄, S.Nonempty → DirectedOn (· ≤ ·) S → sSup S ∈ U → (S ∩ U).Nonempty

/-- **Scott 1972, §2.** The *way-below* relation: `x ≪ y` iff `y` lies in the
interior of the principal up-set `Set.Ici x` for the induced topology. -/
def WayBelow (x y : D) : Prop :=
  letI : LE D :=
    (CompleteLattice.toCompleteSemilatticeInf (α := D)).toPartialOrder.toPreorder.toLE
  letI : Preorder D :=
    (CompleteLattice.toCompleteSemilatticeInf (α := D)).toPartialOrder.toPreorder
  ∃ U : Set D, ScottOpen U ∧ y ∈ U ∧ U ⊆ Set.Ici x

@[inherit_doc] scoped infix:50 " ≪ " => WayBelow

/-- **Scott 1972, Definition 2.3.** A complete lattice is a *continuous lattice*
when every element is the supremum of the elements way below it. -/
def IsContinuousLattice (D : Type u) [CompleteLattice D] : Prop :=
  letI : LE D :=
    (CompleteLattice.toCompleteSemilatticeInf (α := D)).toPartialOrder.toPreorder.toLE
  ∀ y : D, IsLUB {x | x ≪ y} y

/-- Scott's induced topology on a complete lattice. -/
@[reducible] noncomputable def scottTopologicalSpace : TopologicalSpace D :=
  Topology.scott D univ

/-- **Scott 1972, Definition 3.1.** `[X → Y]` is the space of continuous functions
\(f : X \to Y\). On continuous lattices, Theorem 3.3 identifies the lattice
topology with the product topology of 3.1; we take continuity for the induced
(lattice) topology. -/
def ScottMap (D : Type u) (D' : Type v) [CompleteLattice D] [CompleteLattice D'] : Type _ :=
  { f : D → D' // @Continuous D D' scottTopologicalSpace scottTopologicalSpace f }

namespace ScottMap

instance : CoeFun (ScottMap D D') (fun _ => D → D') where
  coe f := f.1

/-- Extensional equality of Scott maps. -/
theorem ext {f g : ScottMap D D'} (h : ∀ x, f x = g x) : f = g :=
  Subtype.ext (funext h)

/-- Pointwise order on Scott-continuous maps. -/
def le (f g : ScottMap D D') : Prop :=
  letI : LE D' :=
    (ChainCompletePartialOrder.instOfCompleteLattice
      (α := D')).toPartialOrder.toPreorder.toLE
  ∀ x, f x ≤ g x

/-- Reflexivity of the pointwise order. -/
theorem le_refl' (f : ScottMap D D') : le f f := by
  sorry

/-- Transitivity of the pointwise order. -/
theorem le_trans' (f g h : ScottMap D D') (hfg : le f g) (hgh : le g h) :
    le f h := by
  sorry

/-- Antisymmetry of the pointwise order. -/
theorem le_antisymm' (f g : ScottMap D D') (hfg : le f g) (hgf : le g f) :
    f = g := by
  sorry

/-- Strict pointwise order induced by `ScottMap.le`. -/
def lt (f g : ScottMap D D') : Prop :=
  le f g ∧ ¬ le g f

/-- The chosen strict pointwise order is `≤ ∧ ¬ ≥`. -/
theorem lt_iff_le_not_ge' (f g : ScottMap D D') :
    lt f g ↔ le f g ∧ ¬ le g f := by
  sorry

instance instPartialOrder : PartialOrder (ScottMap D D') where
  le := le
  lt := lt
  le_refl := le_refl'
  le_trans := le_trans'
  lt_iff_le_not_ge := lt_iff_le_not_ge'
  le_antisymm := le_antisymm'

/-- The pointwise supremum function is Scott-continuous. This is the proof
obligation supplied by Theorem 3.3. -/
theorem sSupMaps_continuous (F : Set (ScottMap D D')) :
    @Continuous D D' scottTopologicalSpace scottTopologicalSpace
      (fun x => sSup (Set.image (fun f : ScottMap D D' => (f : D → D') x) F)) := by
  sorry

/-- The pointwise supremum of any family of Scott-continuous maps. -/
noncomputable def sSupMaps (F : Set (ScottMap D D')) : ScottMap D D' :=
  ⟨fun x => sSup (Set.image (fun f : ScottMap D D' => (f : D → D') x) F),
    sSupMaps_continuous F⟩

noncomputable instance instSupSet : SupSet (ScottMap D D') := ⟨sSupMaps⟩

/-- The explicitly pointwise `sSupMaps` is a least upper bound. -/
theorem isLUB_sSup (F : Set (ScottMap D D')) : IsLUB F (sSup F) := by
  sorry

/-- **Scott 1972, Theorem 3.3.** `[D → D']` has the complete lattice uniquely
determined by pointwise order and pointwise arbitrary suprema. Its infima are
derived by `completeLatticeOfSup`; they are not asserted to be pointwise. -/
noncomputable instance instCompleteLattice {D : Type u} {D' : Type v}
    [CompleteLattice D] [CompleteLattice D'] : CompleteLattice (ScottMap D D') :=
  completeLatticeOfSup (ScottMap D D') isLUB_sSup

end ScottMap

/-- **Scott 1972, Definition 3.1 (on lattices).** The literal Pi topology on
all functions `D → D'`, restricted along the underlying-function map of
`ScottMap`. -/
@[reducible] noncomputable def scottMapInducedPiTopology (D : Type u) (D' : Type v)
    [CompleteLattice D] [CompleteLattice D'] : TopologicalSpace (ScottMap D D') :=
  TopologicalSpace.induced (fun f : ScottMap D D' => (f : D → D'))
    (@Pi.topologicalSpace D (fun _ => D') (fun _ => scottTopologicalSpace))

/-- **Scott 1972, Definition 3.6.** A *retraction* of continuous lattices. -/
structure IsContinuousLatticeRetraction (D : Type u) (D' : Type v)
    [CompleteLattice D] [CompleteLattice D'] where
  incl : ScottMap D D'
  retr : ScottMap D' D
  retr_incl : ∀ d, retr (incl d) = d

/-- **Scott 1972, Definition 3.6.** A *projection* of continuous lattices: a retract with
`i ∘ j ⊑ id`. -/
structure IsContinuousLatticeProjection (D : Type u) (D' : Type v)
    [CompleteLattice D] [CompleteLattice D']
    extends IsContinuousLatticeRetraction D D' where
  incl_retr_le : ∀ d,
    @LE.le D'
      (ChainCompletePartialOrder.instOfCompleteLattice (α := D')).toPartialOrder.toPreorder.toLE
      (incl (retr d)) d

/-- Continuity of the inner map `i ∘ f ∘ j`. -/
theorem functionSpaceInclFun_continuous {D D' : Type u}
    [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') (f : ScottMap D D) :
    @Continuous D' D' scottTopologicalSpace scottTopologicalSpace
      (fun x => P.incl (f (P.retr x))) := by
  sorry

/-- The inclusion part of `[P → P]`, with its underlying function explicit. -/
def functionSpaceInclFun {D D' : Type u} [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') (f : ScottMap D D) : ScottMap D' D' :=
  ⟨fun x => P.incl (f (P.retr x)), functionSpaceInclFun_continuous P f⟩

/-- Continuity, for the lattice Scott topologies on the function spaces, of
`f ↦ i ∘ f ∘ j`. -/
theorem functionSpaceInclFun_outer_continuous {D D' : Type u}
    [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') :
    @Continuous (ScottMap D D) (ScottMap D' D')
      scottTopologicalSpace scottTopologicalSpace (functionSpaceInclFun P) := by
  sorry

/-- Continuity of the inner map `j ∘ g ∘ i`. -/
theorem functionSpaceRetrFun_continuous {D D' : Type u}
    [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') (g : ScottMap D' D') :
    @Continuous D D scottTopologicalSpace scottTopologicalSpace
      (fun x => P.retr (g (P.incl x))) := by
  sorry

/-- The retraction part of `[P → P]`, with its underlying function explicit. -/
def functionSpaceRetrFun {D D' : Type u} [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') (g : ScottMap D' D') : ScottMap D D :=
  ⟨fun x => P.retr (g (P.incl x)), functionSpaceRetrFun_continuous P g⟩

/-- Continuity, for the lattice Scott topologies on the function spaces, of
`g ↦ j ∘ g ∘ i`. -/
theorem functionSpaceRetrFun_outer_continuous {D D' : Type u}
    [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') :
    @Continuous (ScottMap D' D') (ScottMap D D)
      scottTopologicalSpace scottTopologicalSpace (functionSpaceRetrFun P) := by
  sorry

/-- Retraction law for the diagonal Proposition 3.7 construction. -/
theorem functionSpaceRetrIncl {D D' : Type u} [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') :
    ∀ f, functionSpaceRetrFun P (functionSpaceInclFun P f) = f := by
  sorry

/-- Projection inequality for the diagonal Proposition 3.7 construction. -/
theorem functionSpaceInclRetrLe {D D' : Type u} [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') :
    ∀ g, functionSpaceInclFun P (functionSpaceRetrFun P g) ≤ g := by
  sorry

/-- Scott's Proposition 3.7 construction specialized diagonally. The underlying
maps are fixed here; only continuity and projection laws are proof obligations. -/
noncomputable def functionSpaceProjection
    {D D' : Type u} [CompleteLattice D] [CompleteLattice D']
    (P : IsContinuousLatticeProjection D D') :
    IsContinuousLatticeProjection (ScottMap D D) (ScottMap D' D') where
  incl := ⟨functionSpaceInclFun P, functionSpaceInclFun_outer_continuous P⟩
  retr := ⟨functionSpaceRetrFun P, functionSpaceRetrFun_outer_continuous P⟩
  retr_incl := functionSpaceRetrIncl P
  incl_retr_le := functionSpaceInclRetrLe P

/-- A complete lattice bundled with its instance, used to define the function-space tower by
recursion on `ℕ`. -/
structure CLat : Type (u + 1) where
  carrier : Type u
  [str : CompleteLattice carrier]

attribute [instance] CLat.str

/-- The tower `D₀, [D₀→D₀], [[D₀→D₀]→[D₀→D₀]], …` as bundled complete lattices. -/
noncomputable def towerCLat (D₀ : CLat.{u}) : ℕ → CLat.{u}
  | 0 => D₀
  | (n + 1) => ⟨ScottMap (towerCLat D₀ n).carrier (towerCLat D₀ n).carrier⟩

/-- The carrier `Dₙ` of the function-space tower. -/
def towerType (D₀ : CLat.{u}) (n : ℕ) : Type u := (towerCLat D₀ n).carrier

noncomputable instance towerCompleteLattice (D₀ : CLat.{u}) (n : ℕ) :
    CompleteLattice (towerType D₀ n) := (towerCLat D₀ n).str

/-- The projection tower `j_{n+1} = [j_n → j_n]`, anchored at a chosen base
projection `j₀ : [D₀ → D₀] → D₀`. This is the concrete recursion from
Proposition 3.7, not an arbitrary supplied tower. -/
noncomputable def towerProj (D₀ : CLat.{u})
    (j₀ : IsContinuousLatticeProjection D₀.carrier (ScottMap D₀.carrier D₀.carrier)) :
    ∀ n, IsContinuousLatticeProjection (towerType D₀ n) (towerType D₀ (n + 1))
  | 0 => j₀
  | n + 1 => functionSpaceProjection (towerProj D₀ j₀ n)

section InverseLimit

variable (D : ℕ → Type u) [∀ n, CompleteLattice (D n)]
variable (P : ∀ n, IsContinuousLatticeProjection (D n) (D (n + 1)))

/-- **Scott 1972, §4.** The inverse-limit compatibility condition
\(j_n(x_{n+1}) = x_n\). -/
def Compatible (x : ∀ n, D n) : Prop := ∀ n, (P n).retr (x (n + 1)) = x n

/-- **Scott 1972, §4.** The inverse limit is the subspace of the product consisting
of those sequences \(x = \langle x_n \rangle_{n=0}^{\infty}\) with
\(j_n(x_{n+1}) = x_n\). -/
abbrev InverseLimit : Type u := {x : ∀ n, D n // Compatible D P x}

/-- Coordinatewise order on compatible sequences. Kept reducible so existing
subtype-order lemmas see the underlying pointwise relation definitionally. -/
abbrev inverseLimitLE (x y : InverseLimit D P) : Prop :=
  ∀ n,
    @LE.le (D n)
      (ChainCompletePartialOrder.instOfCompleteLattice
        (α := D n)).toPartialOrder.toPreorder.toLE
      (x.1 n) (y.1 n)

/-- Strict coordinatewise order induced by `inverseLimitLE`. -/
abbrev inverseLimitLT (x y : InverseLimit D P) : Prop :=
  inverseLimitLE D P x y ∧ ¬ inverseLimitLE D P y x

/-- Reflexivity of the coordinatewise inverse-limit order. -/
theorem inverseLimitLE_refl (x : InverseLimit D P) :
    inverseLimitLE D P x x := by
  sorry

/-- Transitivity of the coordinatewise inverse-limit order. -/
theorem inverseLimitLE_trans (x y z : InverseLimit D P)
    (hxy : inverseLimitLE D P x y) (hyz : inverseLimitLE D P y z) :
    inverseLimitLE D P x z := by
  sorry

/-- Antisymmetry of the coordinatewise inverse-limit order. -/
theorem inverseLimitLE_antisymm (x y : InverseLimit D P)
    (hxy : inverseLimitLE D P x y) (hyx : inverseLimitLE D P y x) :
    x = y := by
  sorry

/-- The chosen strict inverse-limit order is `≤ ∧ ¬ ≥`. -/
theorem inverseLimitLT_iff_LE_not_GE (x y : InverseLimit D P) :
    inverseLimitLT D P x y ↔
      inverseLimitLE D P x y ∧ ¬ inverseLimitLE D P y x := by
  sorry

/-- The inverse limit carries the coordinatewise order inherited from its
ambient product. This declaration makes that order explicit instead of
leaving typeclass search to choose an equivalent route. -/
instance inverseLimitPartialOrder : PartialOrder (InverseLimit D P) where
  le := inverseLimitLE D P
  lt := inverseLimitLT D P
  le_refl := inverseLimitLE_refl D P
  le_trans := inverseLimitLE_trans D P
  lt_iff_le_not_ge := inverseLimitLT_iff_LE_not_GE D P
  le_antisymm := inverseLimitLE_antisymm D P

/-- The coordinatewise infimum of a family of compatible sequences, before
packaging the compatibility proof. -/
noncomputable def inverseLimitSInfCoe (S : Set (InverseLimit D P)) : ∀ n, D n :=
  fun n => sInf ((fun x : InverseLimit D P => x.1 n) '' S)

/-- The pointwise infimum of compatible sequences is compatible, because each
projection is a right adjoint and hence preserves arbitrary infima. -/
theorem compatible_sInf (S : Set (InverseLimit D P)) :
    Compatible D P (inverseLimitSInfCoe D P S) := by
  sorry

/-- Coordinatewise infimum of compatible sequences. -/
noncomputable instance : InfSet (InverseLimit D P) :=
  ⟨fun S => ⟨inverseLimitSInfCoe D P S, compatible_sInf D P S⟩⟩

/-- The explicitly coordinatewise infimum is a greatest lower bound. -/
theorem isGLB_sInf' (S : Set (InverseLimit D P)) :
    @IsGLB (InverseLimit D P)
      (inverseLimitPartialOrder D P).toPreorder.toLE S (sInf S) := by
  sorry

/-- The inverse-limit complete lattice is concretely generated from
coordinatewise arbitrary infima. Its order is the subtype's coordinatewise
order; directed suprema are consequently coordinatewise as well. -/
noncomputable instance instCompleteLattice : CompleteLattice (InverseLimit D P) :=
  @completeLatticeOfInf (InverseLimit D P) (inverseLimitPartialOrder D P)
    inferInstance (isGLB_sInf' D P)

/-- **Scott 1972, §4.** The inverse-limit subspace topology induced by
`Subtype.val` from the Pi product of the stage Scott topologies. -/
@[reducible] noncomputable def inverseLimitTopology : TopologicalSpace (InverseLimit D P) :=
  TopologicalSpace.induced (Subtype.val : InverseLimit D P → ∀ n, D n)
    (@Pi.topologicalSpace ℕ D (fun _ => scottTopologicalSpace))

end InverseLimit

section LimitMaps

variable (D₀ : CLat.{u})
  (j₀ : IsContinuousLatticeProjection D₀.carrier (ScottMap D₀.carrier D₀.carrier))

/-- **Scott 1972, §4.** The inverse limit \(D_\infty\) of
\(\langle D_n, j_n \rangle_{n=0}^{\infty}\). -/
abbrev DInf : Type u := InverseLimit (towerType D₀) (towerProj D₀ j₀)

/-- **Scott 1972, Definition 3.1 / Theorem 4.4.** The function space
\([D_\infty \to D_\infty]\). -/
abbrev DInfFn : Type u := ScottMap (DInf D₀ j₀) (DInf D₀ j₀)

/-- **Scott 1972, Theorem 4.4** (`sources/ScottContinLatt1972.md`):
*The inverse limit \(D_\infty\) of the recursively defined sequence
\(\langle D_n, j_n \rangle_{n=0}^{\infty}\) of function spaces is not only a
continuous lattice, but it is also homeomorphic to its own function space
\([D_\infty \to D_\infty]\).* -/
theorem theorem_4_4 (h₀ : IsContinuousLattice D₀.carrier) :
    @IsContinuousLattice (DInf D₀ j₀) inferInstance ∧
      Nonempty
        (@Homeomorph (DInf D₀ j₀) (DInfFn D₀ j₀)
          (inverseLimitTopology (towerType D₀) (towerProj D₀ j₀))
          (scottMapInducedPiTopology (DInf D₀ j₀) (DInf D₀ j₀))) := by
  sorry

end LimitMaps

end Scott1972.ContinuousLattice