boolean_subalgebra.lean

/-
Copyright (c) 2021 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/
import order.boolean_algebra

/-! # Boolean subalgebras

Let `B` be a boolean algebra.  Given a predicate `B \to Prop`, we construct
the smallest boolean subalgebra of `B` containing the elements implied by
the predicate.
-/
open set

section bool

variables {B : Type*} [boolean_algebra B] {fil : B → Prop}

/-- Let `B` be a boolean algebra.  Given a predicate `fil : B → Prop` on `B`,
the predicate `is_bool_subalgebra fil` is the predicate on `B` that contains
all the elements of `fil` and is closed under taking finite unions and
complements.  It is implemented with pairwise unions and, for this reason, we
include `⊥` in `is_bool_subalgebra fil`.
Similar inductive Types could contain one among `{⊥, ⊤}` and one among `{⊔, ⊓}`,
delegating lemmas to prove the others. -/
inductive is_bool_subalgebra (fil : B → Prop) : B → Prop
| bsa_bot : is_bool_subalgebra ⊥
| bsa_fil   : ∀ {f}, fil f → is_bool_subalgebra f
| bsa_sup : ∀ {C D}, is_bool_subalgebra C → is_bool_subalgebra D → is_bool_subalgebra (C ⊔ D)
| bsa_compl : ∀ {C}, is_bool_subalgebra C → is_bool_subalgebra Cᶜ

open is_bool_subalgebra

lemma bsa_inf {a b : B} (ba : is_bool_subalgebra fil a) (bb : is_bool_subalgebra fil b) :
  is_bool_subalgebra fil (a ⊓ b) :=
begin
  rw [← @compl_compl' _ (a ⊓ b), compl_inf],
  exact bsa_compl (bsa_sup (bsa_compl ba) (bsa_compl bb)),
end

/--- `bsa_type` is the SubType of `B` consisting of the elements
spelled out by `is_bsubalgebra fil`. -/
def bsa_type (fil : B → Prop) : Type* := {s : B // is_bool_subalgebra fil s}

namespace bas_type

instance inhabited : inhabited (bsa_type fil) :=
⟨⟨_, bsa_bot⟩⟩

instance has_sup : has_sup (bsa_type fil) :=
⟨λ a b, ⟨_, is_bool_subalgebra.bsa_sup a.2 b.2⟩⟩

instance has_le : has_le (bsa_type fil) :=
⟨λ a b, a.1 ≤ b.1⟩

lemma le_subtype {a b : bsa_type fil} : a ≤ b ↔ a.1 ≤ b.1 :=
by refl

@[simp] lemma sup_subtype {a b : bsa_type fil} : (a ⊔ b).1 = a.1 ⊔ b.1 := rfl

instance has_inf : has_inf (bsa_type fil) :=
⟨λ a b, ⟨_, bsa_inf a.2 b.2⟩⟩

@[simp] lemma inf_subtype {a b : bsa_type fil} : (a ⊓ b).1 = a.1 ⊓ b.1 := rfl

instance has_compl : has_compl (bsa_type fil) :=
⟨λ a, ⟨_, bsa_compl a.2⟩⟩

@[simp] lemma compl_subtype {a : bsa_type fil} : (aᶜ).1 = (a.1)ᶜ := rfl

instance has_top : has_top (bsa_type fil) :=
⟨⟨_, bsa_compl bsa_bot⟩⟩

instance has_bot : has_bot (bsa_type fil) :=
⟨⟨_, bsa_bot ⟩⟩

@[simp] lemma bot_subtype : (⊥ : bsa_type fil).1 = (⊥ : B) := rfl

@[simp] lemma top_subtype : (⊤ : bsa_type fil).1 = (⊤ : B) :=
begin
  rw [← compl_bot, ← bot_subtype, ← compl_subtype],
  refl,
end

instance has_sdiff : has_sdiff (bsa_type fil) :=
⟨λ a b, ⟨_, bsa_inf a.2 (bsa_compl b.2)⟩⟩

instance has_lt : has_lt (bsa_type fil) :=
⟨λ a b, a ≤ b ∧ ¬ b ≤ a⟩

lemma le_refl : ∀ a : bsa_type fil, a ≤ a :=
λ a, rfl.le

lemma le_trans : ∀ (a b c : bsa_type fil), a ≤ b → b ≤ c → a ≤ c :=
λ a b c, le_trans

lemma lt_iff_le_not_le : ∀ (a b : bsa_type fil), a < b ↔ a ≤ b ∧ ¬b ≤ a :=
λ _ _, iff.refl _

lemma le_antisymm : ∀ (a b : bsa_type fil), a ≤ b → b ≤ a → a = b :=
begin
  intros a b ab ba,
  cases a,
  cases b,
  exact subtype.mk_eq_mk.mpr (le_antisymm (subtype.mk_le_mk.mp ab) (subtype.mk_le_mk.mp ba)),
end

instance partial_order : partial_order (bsa_type fil) :=
{ le               := (≤),
  lt               := (<),
  le_refl          := le_refl,
  le_trans         := le_trans,
  lt_iff_le_not_le := lt_iff_le_not_le,
  le_antisymm      := le_antisymm }

lemma le_sup_left : ∀ a b : bsa_type fil, a ≤ (a ⊔ b) :=
λ a b, le_subtype.mpr le_sup_left

lemma le_sup_right : ∀ a b : bsa_type fil, b ≤ (a ⊔ b) :=
λ a b, le_subtype.mpr le_sup_right

lemma sup_le : ∀ (a b c : bsa_type fil), a ≤ c → b ≤ c → a ⊔ b ≤ c :=
λ a b c ac bc, @sup_le B _ _ _ _ (le_subtype.mpr ac) (le_subtype.mpr bc)

lemma inf_le_left : ∀ (a b : bsa_type fil), a ⊓ b ≤ a :=
λ a b, le_subtype.mpr inf_le_left

lemma inf_le_right : ∀ (a b : bsa_type fil), a ⊓ b ≤ b :=
λ a b, le_subtype.mpr inf_le_right

lemma le_inf : ∀ (a b c : bsa_type fil), a ≤ b → a ≤ c → a ≤ b ⊓ c :=
λ a b c ab ac, le_subtype.mpr $ le_inf (le_subtype.mp ab) (le_subtype.mp ac)

lemma le_sup_inf : ∀ (x y z : bsa_type fil), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z :=
λ a b c, le_subtype.mpr le_sup_inf

lemma le_top : ∀ (a : bsa_type fil), a ≤ ⊤ :=
λ a, le_subtype.mpr $ by rw top_subtype; exact le_top

lemma bot_le : ∀ (a : bsa_type fil), ⊥ ≤ a :=
λ a, le_subtype.mpr bot_le

@[simp] lemma inf_compl_self_eq_bot {x : bsa_type fil} : x ⊓ xᶜ = ⊥ :=
by { ext, unfold_coes, simp }

lemma inf_compl_le_bot : ∀ (x : bsa_type fil), x ⊓ xᶜ ≤ ⊥ :=
λ x, le_of_eq inf_compl_self_eq_bot

@[simp] lemma sup_compl_self_eq_top {x : bsa_type fil} : x ⊔ xᶜ = ⊤ :=
by { ext, unfold_coes, simp }

lemma top_le_sup_compl : ∀ (x : bsa_type fil), ⊤ ≤ x ⊔ xᶜ :=
λ a, le_of_eq sup_compl_self_eq_top.symm

lemma sdiff_eq : ∀ (x y : bsa_type fil), x \ y = x ⊓ yᶜ :=
λ _ _, rfl

instance boolean_subalgebra (fil : B → Prop) : boolean_algebra (bsa_type fil) :=
{ sup := (⊔),
  le_sup_left := le_sup_left,
  le_sup_right := le_sup_right,
  sup_le := sup_le,
  inf := (⊓),
  inf_le_left := inf_le_left,
  inf_le_right := inf_le_right,
  le_inf := le_inf,
  le_sup_inf := le_sup_inf,
  top := ⊤,
  le_top := le_top,
  bot := ⊥,
  bot_le := bot_le,
  compl := has_compl.compl,
  sdiff := (\),
  inf_compl_le_bot := inf_compl_le_bot,
  top_le_sup_compl := top_le_sup_compl,
  sdiff_eq := sdiff_eq,
  ..bas_type.partial_order }

end bas_type

end bool