Constructible comm_semiring.lean

import topology.basic

open set topological_space


variables {X : Type*} [topological_space X]

def locally_closed (C : set X) :=
∃ U V : set X, is_open U ∧ is_closed V ∧ C = U ∩ V

lemma locally_closed_of_open {U : set X} : is_open U → locally_closed U :=
λ op, ⟨U, univ, op, is_closed_univ, (inter_univ _).symm⟩

lemma locally_closed_of_closed {V : set X} : is_open Vᶜ → locally_closed V :=
λ cl, ⟨univ, V, is_open_univ, cl, (univ_inter _).symm⟩

lemma locally_closed_of_int {U V : set X} :
  locally_closed U → locally_closed V → locally_closed (U ∩ V):=
begin
  rintros ⟨Uo, Uc, hUo, hUc, rfl⟩ ⟨Vo, Vc, hVo, hVc, rfl⟩,
  refine ⟨Uo ∩ Vo, Uc ∩ Vc, is_open_inter hUo hVo, is_closed_inter hUc hVc, ext (λ _,
     ⟨(λ ⟨⟨_, _⟩, _, _⟩, ⟨⟨‹_›, ‹_›⟩, ⟨‹_›, ‹_›⟩⟩), λ ⟨⟨_, _⟩, _, _⟩, ⟨⟨‹_›, ‹_›⟩, ⟨‹_›, ‹_›⟩⟩⟩)⟩,
end

inductive is_constructible : set X → Prop
| lc : ∀ {C : set X}, locally_closed C → is_constructible C
| union : ∀ {C D : set X}, is_constructible C → is_constructible D → is_constructible (C ∪ D)

-- it prints awfully, but seems to work
@[ext] class const (X : Type*) [topological_space X] :=
( cs   : set X)
( cons : is_constructible cs )

namespace const

lemma is_locally_closed_empty : locally_closed (∅ : set X) := locally_closed_of_open is_open_empty

lemma is_locally_closed_univ : locally_closed (univ : set X) := locally_closed_of_open is_open_univ

lemma is_constructible_of_is_locally_closed {U : set X} : locally_closed U → is_constructible U :=
λ lc, is_constructible.lc lc

lemma constructible_open {U : set X} : is_open U → is_constructible U :=
λ _, is_constructible_of_is_locally_closed (locally_closed_of_open ‹_›)

lemma constructible_closed {V : set X} : is_open Vᶜ → is_constructible V :=
λ _, is_constructible_of_is_locally_closed (locally_closed_of_closed ‹_›)

lemma is_constructible_union {C D : set X} :
  is_constructible C → is_constructible D → is_constructible (C ∪ D) :=
λ cC cD, is_constructible.union cC cD

lemma is_constructible_int_locally_closed {C D : set X} :
  is_constructible C → locally_closed D → is_constructible (C ∩ D) :=
begin
  intros cC cD,
  induction cC with E cE E F cE cF cED cFD,
  { exact is_constructible_of_is_locally_closed (locally_closed_of_int cE cD) },
  rw union_inter_distrib_right,
  exact is_constructible_union cED cFD,
end

lemma locally_closed_int_is_constructible {C D : set X} :
  locally_closed C → is_constructible D → is_constructible (C ∩ D) :=
begin
  intros cC cD,
  rw inter_comm,
  exact is_constructible_int_locally_closed cD cC,
end

lemma is_constructible_int {C D : set X} :
  is_constructible C → is_constructible D → is_constructible (C ∩ D) :=
begin
  intros cC cD,
  induction cC with E lcE E F cE cF cED cFD,
  { exact locally_closed_int_is_constructible lcE cD },
  rw union_inter_distrib_right,
  apply is_constructible_union cED cFD,
end

lemma is_constructible_empty : is_constructible (∅ : set X) :=
is_constructible_of_is_locally_closed is_locally_closed_empty

lemma is_constructible_univ : is_constructible (univ : set X) :=
is_constructible_of_is_locally_closed is_locally_closed_univ

lemma is_constructible_complement {C : set X} (hC : is_constructible C) :
  is_constructible Cᶜ :=
begin
  induction hC with D lcD D E cD cE cDc cEc,
  { rcases lcD with ⟨U, V, oU, cV, rfl⟩,
    rw compl_inter,
    apply is_constructible_union (constructible_closed _) (constructible_open cV),
    rw compl_compl',
    exact oU },
  { rw compl_union,
    exact is_constructible_int cDc cEc },
end

def cadd (C D : const X) : const X :=
⟨C.1 ∪ D.1, is_constructible_union C.2 D.2⟩

def czero (X : Type*) [topological_space X] : const X := ⟨(∅ : set X), is_constructible_empty⟩

def cmul (C D : const X) : const X :=
⟨C.1 ∩ D.1, is_constructible_int C.2 D.2⟩

def cone : const X := ⟨univ, is_constructible_univ⟩

def const_compl (C : const X) : const X :=
⟨(C.1)ᶜ, is_constructible_complement C.2⟩

lemma is_constructible_union_complement (C : const X) :
  C.1 ∪ (const_compl C).1 = univ :=
union_compl_self C.1

lemma is_constructible_complement_union (C : const X) :
  (const_compl C).1 ∪ C.1 = univ :=
begin
  rw union_comm,
  exact (union_compl_self (C.1)),
end

-- I do not know how to get instances to work
instance [has_add (const X)] : has_add (const X) :=
⟨λ U V, cadd U V⟩

instance [has_zero (const X)] : has_zero (const X) :=
⟨⟨(∅ : set X), is_constructible_empty⟩⟩

instance [has_mul (const X)] : has_mul (const X) :=
⟨λ U V, ⟨U.1 ∩ V.1, is_constructible_int U.2 V.2⟩⟩

instance [has_one (const X)] : has_one (const X) :=
⟨⟨(univ : set X), is_constructible_univ⟩⟩

variables a b : (const X)

lemma cadd_assoc : ∀ (a b c : const X), cadd (cadd a b) c = cadd a (cadd b c) :=
begin
  intros _ _ _,
  ext,
  refine ⟨λ h, _, λ h, _⟩,
  { rcases h with ⟨h1 | h1⟩ | h1,
    exact or.inl h1,
    exact or.inr (or.inl h1),
    exact or.inr (or.inr h1) },
  { rcases h with h1 | ⟨h1 | h1⟩,
    { exact or.inl (or.inl h1) },
    { exact (or.inl (or.inr h1)) },
    { exact or.inr h1 }, },
end

lemma czero_cadd : ∀ (a : const X), cadd (czero X) a = a :=
begin
  intros _,
  ext1,
  ext,
  refine ⟨λ a , _, λ a, or.inr a⟩,
  { cases a with a a,
    { exact false.dcases_on _ a},
    { exact a } },
end

lemma cadd_czero : ∀ (a : const X), cadd a (czero X) = a :=
begin
  intros _,
  ext1,
  ext,
  refine ⟨λ a , _, λ a, or.inl a⟩,
  rcases a with a | a,
  { exact a },
  { exact false.dcases_on _ a},
end

lemma cadd_comm : ∀ (a b : const X), cadd a b = cadd b a :=
λ _ _, ext _ _ (set.ext (λ _, ⟨λ a, or.swap a, λ a, or.swap a⟩))

lemma cmul_assoc : ∀ (a b c : const X), cmul (cmul a b) c = cmul a (cmul b c) :=
λ _ _ _, ext _ _ (set.ext (λ _, ⟨λ ⟨⟨a1,a2⟩, a3⟩, ⟨a1, ⟨a2, a3⟩⟩, λ ⟨a1,⟨a2, a3⟩⟩, ⟨⟨a1, a2⟩, a3⟩⟩))

lemma cone_mul : ∀ (a : const X), cmul cone a = a :=
λ _, ext _ _ (set.ext (λ _, ⟨λ ⟨a1, a2⟩, a2, λ a, ⟨⟨⟩, a⟩⟩))

lemma mul_cone : ∀ (a : const X), cmul a cone = a :=
λ _, ext _ _ (set.ext (λ (x : X), ⟨λ ⟨a, b⟩, a, λ a, ⟨a, ⟨⟩⟩⟩))

lemma czero_cmul : ∀ (a : const X), cmul (czero X) a = (czero X) :=
λ _, ext _ _ (set.ext (λ _, ⟨λ ⟨a, b⟩, a, λ a, false.rec _ a⟩))

lemma cmul_czero : ∀ (a : const X), cmul a (czero X) = (czero X) :=
λ _, ext _ _ (set.ext (λ _, ⟨λ ⟨a, b⟩, b, λ a, false.rec _ a⟩))

lemma cmul_cadd : ∀ (a b c : const X), cmul a (cadd b c) = cadd (cmul a b) (cmul a c) :=
λ _ _ _, ext _ _
begin
  refine set.ext (λ _, ⟨λ a, _, λ a, _⟩),
  { rcases a with ⟨a, b | c⟩,
    { exact or.inl ⟨a, b⟩ },
    { exact or.inr ⟨a, c⟩ } },
  { rcases a with ⟨a, b⟩ | ⟨c, d⟩,
    { exact ⟨a, or.inl b⟩ },
    { exact ⟨c, or.inr d⟩ } },
end

lemma cadd_cmul : ∀ (a b c : const X), cmul (cadd a b) c = cadd (cmul a c) (cmul b c) :=
λ _ _ _, ext _ _
begin
  refine set.ext (λ _, ⟨λ a, _, λ a, _⟩),
  { rcases a with ⟨a | b, c⟩,
    { exact or.inl ⟨a, c⟩ },
    { exact or.inr ⟨b, c⟩ } },
  { rcases a with ⟨a, b⟩ | ⟨c, d⟩,
    { exact ⟨or.inl a, b⟩ },
    { exact ⟨or.inr c, d⟩ } },
end

lemma cmul_comm : ∀ (a b : const X), cmul a b = cmul b a :=
λ _ _, ext _ _ (set.ext (λ _, ⟨λ a, and.symm a, λ a, and.symm a⟩))

def secon (X : Type*) [topological_space X] : comm_semiring (const X) :=
begin
  refine ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _⟩,
  --addition: union
  { exact cadd },
  --add_assoc
  { exact cadd_assoc },
  --unit of addition: empty
  { exact ⟨∅, is_constructible_empty⟩ },
  --zero_add
  { exact czero_cadd },
  --add_zero
  { exact cadd_czero },
  --add_comm
  { exact cadd_comm },
  --has_mul: intersection
  { exact cmul },
  --mul_assoc
  { exact cmul_assoc },
  --unit of multiplication: univ
  { exact cone },
  --one_mul
  { exact cone_mul },
    --mul_one
  { exact mul_cone },
  --zero_mul
  { exact czero_cmul },
  --mul_zero
  { exact cmul_czero },
  --mul_add
  { exact cmul_cadd },
  --add_mul
  { exact cadd_cmul },
  --mul_comm
  { exact cmul_comm },
end

end const