minimal working examples of spa issues

minimal_spa.lean

import tactic.interactive

universes u v w -- to keep us orientated

definition is_valuation {R : Type u} {Γ : Type v} [preorder Γ] (f : R → Γ) : Prop := sorry

structure valuation (R : Type u) (Γ : Type v) [preorder Γ] :=
(f : R → Γ)
(h : is_valuation f)

instance (R : Type u) (Γ : Type v) [preorder Γ] : has_coe_to_fun (valuation R Γ) :=
{ F := λ _, R → Γ, coe := λ v, v.f}

definition valuation.is_continuous {R : Type u} {Γ : Type v} [preorder Γ] (v : valuation R Γ) : Prop := sorry

definition valuation_equiv {R : Type u} {Γ1 : Type v} [preorder Γ1] {Γ2 : Type w} [preorder Γ2] 
(v1 : valuation R Γ1) (v2 : valuation R Γ2) :=
∀ r s : R, v1.f r ≤ v1.f s ↔ v2.f r ≤ v2.f s

theorem cts_iff_equiv_cts {R : Type u} {Γ1 : Type v} [preorder Γ1] {Γ2 : Type w} [preorder Γ2] 
(v1 : valuation R Γ1) (v2 : valuation R Γ2) :
valuation_equiv v1 v2 → (valuation.is_continuous v1 ↔ valuation.is_continuous v2) := sorry

/-- Kind of horrible -/
definition Spv1 (R : Type u) := 
{ineq : R → R → Prop // ∃ (Γ : Type u) [preorder Γ],
  by exactI ∃ (v : valuation R Γ), ∀ r s : R, ineq r s ↔ v r ≤ v s}

definition Spv1.is_continuous {R : Type u} (vs : Spv1 R) := ∃ (Γ : Type u) [preorder Γ],
  by exactI ∃ (v : valuation R Γ), (∀ r s : R, vs.val r s ↔ v r ≤ v s) ∧ valuation.is_continuous v 

definition Spa1 (R : Type u) :=
{vs : Spv1 R // Spv1.is_continuous vs}

-- Should we just jettison Spv?? I'm not convinced it plays an essential role.

-- the below definition does not read well in Lean

/-- basic open corresponding to r, s is v : v(r) <= v(s) and v(s) isn't <= v(0) ) -/
definition basic_open1 (R : Type u) [has_zero R] (r s : R) : set (Spa1 R) := 
{vs | vs.val.val r s ∧ ¬ vs.val.val s 0}

-- those .val.vals are horrible.

definition Spa2 (R : Type u) :=
{ ineq : R → R → Prop // ∃ (Γ : Type u) [preorder Γ],
  by exactI ∃ (v : valuation R Γ), valuation.is_continuous v ∧ ∀ r s : R, ineq r s ↔ v r ≤ v s}

/-- Still pretty awful -/
definition basic_open2 (R : Type u) [has_zero R] (r s : R) : set (Spa2 R) := 
{vs | vs.val r s ∧ ¬ vs.val s 0}

-- Johan's approach

structure Valuation (R : Type u) :=
(Γ : Type u)
[HΓ : preorder Γ]
(f : R → Γ)
(h : is_valuation f)

-- how does this work?
-- definition Spa3 (R : Type u) := quotient.mk '' {v : Valuation R | v.is_continuous}