217 lines
7.3 KiB
Text
217 lines
7.3 KiB
Text
/-
|
|
Copyright (c) 2016 Johannes Hölzl. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Author: Johannes Hölzl
|
|
|
|
Galois connections - order theoretic adjoints.
|
|
-/
|
|
import standard
|
|
open classical eq.ops algebra set function complete_lattice
|
|
|
|
/- Move to set? -/
|
|
definition kern_image {X Y : Type} (f : X → Y) (S : set X) : set Y := {y | ∀x, f x = y → x ∈ S }
|
|
|
|
/- Order theoretic definitions -/
|
|
|
|
/- TODO: move to order? -/
|
|
section order
|
|
variables {A B : Type} {S : set A} {a a' : A} {b b' : B} {f : A → B} [weak_order A] [weak_order B]
|
|
|
|
definition increasing (f : A → A) := ∀⦃a⦄, a ≤ f a
|
|
definition decreasing (f : A → A) := ∀⦃a⦄, f a ≤ a
|
|
|
|
definition upper_bounds (S : set A) : set A := { x | ∀₀ s ∈ S, s ≤ x }
|
|
definition lower_bounds (S : set A) : set A := { x | ∀₀ s ∈ S, x ≤ s }
|
|
definition is_least (S : set A) (a : A) := a ∈ S ∧ a ∈ lower_bounds S
|
|
definition is_greatest (S : set A) (a : A) := a ∈ S ∧ a ∈ upper_bounds S
|
|
|
|
definition monotone (f : A → B) := ∀⦃a b⦄, a ≤ b → f a ≤ f b
|
|
|
|
lemma eq_of_is_least_of_is_least (Ha : is_least S a) (Hb : is_least S a') : a = a' :=
|
|
le.antisymm
|
|
begin apply (and.elim_right Ha), apply (and.elim_left Hb) end
|
|
begin apply (and.elim_right Hb), apply (and.elim_left Ha) end
|
|
|
|
lemma is_least_iff_eq_of_is_least (Ha : is_least S a) : is_least S a' ↔ a = a' :=
|
|
iff.intro (eq_of_is_least_of_is_least Ha) begin intro H, cases H, apply Ha end
|
|
|
|
lemma eq_of_is_greatest_of_is_greatest (Ha : is_greatest S a) (Hb : is_greatest S a') : a = a' :=
|
|
le.antisymm
|
|
begin apply (and.elim_right Hb), apply (and.elim_left Ha) end
|
|
begin apply (and.elim_right Ha), apply (and.elim_left Hb) end
|
|
|
|
lemma is_greatest_iff_eq_of_is_greatest (Ha : is_greatest S a) : is_greatest S a' ↔ a = a' :=
|
|
iff.intro (eq_of_is_greatest_of_is_greatest Ha) begin intro H, cases H, apply Ha end
|
|
|
|
definition is_lub (S : set A) := is_least (upper_bounds S)
|
|
definition is_glb (S : set A) := is_greatest (lower_bounds S)
|
|
|
|
lemma eq_of_is_lub_of_is_lub : is_lub S a → is_lub S a' → a = a' :=
|
|
!eq_of_is_least_of_is_least
|
|
|
|
lemma is_lub_iff_eq_of_is_lub : is_lub S a → (is_lub S a' ↔ a = a') :=
|
|
!is_least_iff_eq_of_is_least
|
|
|
|
lemma eq_of_is_glb_of_is_glb : is_glb S a → is_glb S a' → a = a' :=
|
|
!eq_of_is_greatest_of_is_greatest
|
|
|
|
lemma is_glb_iff_eq_of_is_glb : is_glb S a → (is_glb S a' ↔ a = a') :=
|
|
!is_greatest_iff_eq_of_is_greatest
|
|
|
|
lemma mem_upper_bounds_image (Hf : monotone f) (Ha : a ∈ upper_bounds S) : f a ∈ upper_bounds (f ' S) :=
|
|
bounded_forall_image_of_bounded_forall (take x H, Hf (Ha `x ∈ S`))
|
|
|
|
lemma mem_lower_bounds_image (Hf : monotone f) (Ha : a ∈ lower_bounds S) : f a ∈ lower_bounds (f ' S) :=
|
|
bounded_forall_image_of_bounded_forall (take x H, Hf (Ha `x ∈ S`))
|
|
|
|
end order
|
|
|
|
definition galois_connection {A B : Type} [weak_order A] [weak_order B] (l : A → B) (u : B → A) :=
|
|
∀{a b}, l a ≤ b ↔ a ≤ u b
|
|
|
|
namespace galois_connection
|
|
|
|
section
|
|
parameters {A B : Type} [weak_order A] [weak_order B] (l : A → B) (u : B → A)
|
|
|
|
lemma monotone_intro (Mu : monotone u) (Ml : monotone l)
|
|
(Iul : increasing (u ∘ l)) (Dlu : decreasing (l ∘ u)) : galois_connection l u :=
|
|
begin
|
|
intros a b,
|
|
apply iff.intro,
|
|
{ intro H, apply le.trans, apply Iul, apply Mu, assumption },
|
|
{ intro H, apply le.trans, apply Ml, assumption, apply Dlu }
|
|
end
|
|
|
|
parameter (gc : galois_connection l u)
|
|
include gc
|
|
|
|
lemma l_le {a : A} {b : B} : a ≤ u b → l a ≤ b :=
|
|
and.elim_right !gc
|
|
|
|
lemma le_u {a : A} {b : B} : l a ≤ b → a ≤ u b :=
|
|
and.elim_left !gc
|
|
|
|
lemma increasing_u_l : increasing (u ∘ l) :=
|
|
take a, le_u !le.refl
|
|
|
|
lemma decreasing_l_u : decreasing (l ∘ u) :=
|
|
take a, l_le !le.refl
|
|
|
|
lemma monotone_u : monotone u :=
|
|
take a b H, le_u (le.trans !decreasing_l_u H)
|
|
|
|
lemma monotone_l : monotone l :=
|
|
take a b H, l_le (le.trans H !increasing_u_l)
|
|
|
|
lemma u_l_u_eq_u : u ∘ l ∘ u = u :=
|
|
funext (take x, le.antisymm (monotone_u !decreasing_l_u) !increasing_u_l)
|
|
|
|
lemma l_u_l_eq_l : l ∘ u ∘ l = l :=
|
|
funext (take x, le.antisymm !decreasing_l_u (monotone_l !increasing_u_l))
|
|
|
|
lemma u_mem_upper_bounds {S : set A} {b : B} (H : b ∈ upper_bounds (l ' S)) : u b ∈ upper_bounds S :=
|
|
take c, suppose c ∈ S, le_u (H (!mem_image_of_mem `c ∈ S`))
|
|
|
|
lemma l_mem_lower_bounds {S : set B} {a : A} (H : a ∈ lower_bounds (u ' S)) : l a ∈ lower_bounds S :=
|
|
take c, suppose c ∈ S, l_le (H (!mem_image_of_mem `c ∈ S`))
|
|
|
|
lemma is_lub_l_image {S : set A} {a : A} (H : is_lub S a) : is_lub (l ' S) (l a) :=
|
|
and.intro
|
|
(mem_upper_bounds_image monotone_l (and.elim_left `is_lub S a`))
|
|
(take b Hb, l_le (and.elim_right `is_lub S a` _ (u_mem_upper_bounds Hb)))
|
|
|
|
lemma is_glb_u_image {S : set B} {b : B} (H : is_glb S b) : is_glb (u ' S) (u b) :=
|
|
and.intro
|
|
(mem_lower_bounds_image monotone_u (and.elim_left `is_glb S b`))
|
|
(take a Ha, le_u (and.elim_right `is_glb S b` _ (l_mem_lower_bounds Ha)))
|
|
|
|
lemma is_glb_l {a : A} : is_glb { b | a ≤ u b } (l a) :=
|
|
begin
|
|
apply and.intro,
|
|
{ intro b, apply l_le },
|
|
{ intro b H, apply H, apply increasing_u_l }
|
|
end
|
|
|
|
lemma is_lub_u {b : B} : is_lub { a | l a ≤ b } (u b) :=
|
|
begin
|
|
apply and.intro,
|
|
{ intro a, apply le_u },
|
|
{ intro a H, apply H, apply decreasing_l_u }
|
|
end
|
|
|
|
end
|
|
|
|
/- Constructing Galois connections -/
|
|
|
|
protected lemma id {A : Type} [weak_order A] : @galois_connection A A _ _ id id :=
|
|
take a b, iff.intro (λx, x) (λx, x)
|
|
|
|
protected lemma dual {A B : Type} [woA : weak_order A] [woB : weak_order B]
|
|
(l : A → B) (u : B → A) (gc : galois_connection l u) :
|
|
@galois_connection B A (weak_order_dual woB) (weak_order_dual woA) u l :=
|
|
take a b,
|
|
begin
|
|
apply iff.symm,
|
|
rewrite le_dual_eq_le,
|
|
rewrite le_dual_eq_le,
|
|
exact gc,
|
|
end
|
|
|
|
protected lemma compose {A B C : Type} [weak_order A] [weak_order B] [weak_order C]
|
|
(l1 : A → B) (u1 : B → A) (l2 : B → C) (u2 : C → B)
|
|
(gc1 : galois_connection l1 u1) (gc2 : galois_connection l2 u2) :
|
|
galois_connection (l2 ∘ l1) (u1 ∘ u2) :=
|
|
by intros; rewrite gc2; rewrite gc1
|
|
|
|
section
|
|
variables {A B : Type} {f : A → B}
|
|
|
|
protected lemma image_preimage : galois_connection (image f) (preimage f) :=
|
|
@image_subset_iff A B f
|
|
|
|
protected lemma preimage_kern_image : galois_connection (preimage f) (kern_image f) :=
|
|
begin
|
|
intros X Y, apply iff.intro, all_goals (intro H x Hx),
|
|
{ intro x' eq, apply H, cases eq, exact Hx },
|
|
{ apply H,
|
|
esimp [preimage, mem, set_of] at Hx, exact Hx, -- TODO: why is esimp necessary?
|
|
exact rfl }
|
|
end
|
|
end
|
|
|
|
end galois_connection
|
|
|
|
/- Bounds on complete lattices -/
|
|
/- TODO: move to complete lattices? -/
|
|
|
|
section
|
|
variables {A : Type} (S : set A) {a b : A} [complete_lattice A]
|
|
|
|
lemma is_lub_sup : is_lub '{a, b} (sup a b) :=
|
|
and.intro
|
|
begin
|
|
xrewrite [+bounded_forall_insert_iff, bounded_forall_empty_iff, and_true],
|
|
exact (and.intro !le_sup_left !le_sup_right)
|
|
end
|
|
begin
|
|
intro x Hx,
|
|
xrewrite [+bounded_forall_insert_iff at Hx, bounded_forall_empty_iff at Hx, and_true at Hx],
|
|
apply sup_le,
|
|
apply (and.elim_left Hx),
|
|
apply (and.elim_right Hx),
|
|
end
|
|
|
|
lemma is_lub_Sup : is_lub S (⨆S) :=
|
|
and.intro (take x, le_Sup) (take x, Sup_le)
|
|
|
|
lemma is_lub_iff_Sup_eq {a : A} : is_lub S a ↔ (⨆S) = a :=
|
|
!is_lub_iff_eq_of_is_lub !is_lub_Sup
|
|
|
|
lemma is_glb_Inf : is_glb S (⨅S) :=
|
|
and.intro (take a, Inf_le) (take a, le_Inf)
|
|
|
|
lemma is_glb_iff_Inf_eq : is_glb S a ↔ (⨅S) = a :=
|
|
!is_glb_iff_eq_of_is_glb !is_glb_Inf
|
|
|
|
end
|