Library UniMath.OrderTheory.DCPOs.AlternativeDefinitions.FixedPointTheorems
Fixed-point theorems on posets
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.Combinatorics.WellOrderedSets.
Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo.
Local Open Scope poset. Local Open Scope logic. Local Open Scope subtype.
The following are the main results of the file (stated for now with some black boxes, for concepts not yet defined).
In Section Check_Overview at the end of the file, we confirm that these statements have been proven.
Context (is_complete : Poset -> UU)
(is_directed_complete : Poset -> UU)
(is_chain_complete : Poset -> UU)
(Progressive_map : forall P:Poset, hsubtype (P -> P))
(Postfixedpoint : forall P:Poset, (P -> P) -> hsubtype P)
(Fixedpoint : forall P:Poset, (P -> P) -> hsubtype P).
Arguments Postfixedpoint {_} _.
Arguments Fixedpoint {_} _.
The master form of the Tarski/Knaster fixed-point theorems:
the fixed points of a monotone map on a complete poset
are themselves complete.
Definition Tarski_fixpoint_theorem_statement
:= forall (P:Poset) (P_complete : is_complete P) (f : posetmorphism P P),
is_complete (Fixedpoint f : Subposet P).
:= forall (P:Poset) (P_complete : is_complete P) (f : posetmorphism P P),
is_complete (Fixedpoint f : Subposet P).
A constructive fixed-point theorem, due to Pataraia.
Definition fixpoint_for_monotone_on_dcpo_statement
:= forall (P : Poset) (P_dir: is_directed_complete P)
(f : posetmorphism P P) (x : Postfixedpoint f),
∑ y : Fixedpoint f, pr1 x ≤ pr1 y.
:= forall (P : Poset) (P_dir: is_directed_complete P)
(f : posetmorphism P P) (x : Postfixedpoint f),
∑ y : Fixedpoint f, pr1 x ≤ pr1 y.
Classical theorem, usually attrib. Bourbaki (1949) and Witt (1951).
Definition Bourbaki_Witt_fixpoint_theorem_statement
:= LEM ->
forall (P : Poset) (_ : is_chain_complete P) (f : Progressive_map P),
Fixedpoint (pr1 f).
End Overview.
:= LEM ->
forall (P : Poset) (_ : is_chain_complete P) (f : Progressive_map P),
Fixedpoint (pr1 f).
End Overview.
Background material
Definition lt_to_nleq {P : Poset} {x y : P} : x < y ⇒ ¬ (y ≤ x).
Show proof.
Definition isrefl'_posetRelation {P : Poset} {x y : P} : x = y ⇒ x ≤ y.
Show proof.
Definition isaposetmorphism_hProp {P Q : Poset} (f : P -> Q) : hProp
:= ∀ x x' : P, x ≤ x' ⇒ f x ≤ f x'.
Definition posetmorphism_property {P Q} (f : posetmorphism P Q)
: isaposetmorphism f
:= pr2 f.
Lemma isaposetmorphism_idfun {P : Poset} : isaposetmorphism (idfun P).
Show proof.
intros ? ? ?; assumption.
Lemma isaposetmorphism_compose {P P' P'' : Poset}
{f : P -> P'} (f_monot : isaposetmorphism f)
{g : P' -> P''} (g_monot : isaposetmorphism g)
: isaposetmorphism (g ∘ f).
Show proof.
intros x y le_xy.
apply g_monot, f_monot, le_xy.
apply g_monot, f_monot, le_xy.
This order of arguments is often more convenient to use than the original hdisj_monot
This order of arguments is often more convenient to use than the original hconjtohdisj
Definition hconjtohdisj' {p q r} : (p ∨ q) ⇒ (p ⇒ r) ⇒ (q ⇒ r) ⇒ r.
Show proof.
Definition hdisj_comm {p q} : (p ∨ q) ⇒ (q ∨ p).
Show proof.
Definition exists_monotone {X:UU} (A B : X -> UU)
: (forall x, A x -> B x) -> (∃ x, A x) -> ∃ x, B x.
Show proof.
Show proof.
Definition hdisj_comm {p q} : (p ∨ q) ⇒ (q ∨ p).
Show proof.
Definition exists_monotone {X:UU} (A B : X -> UU)
: (forall x, A x -> B x) -> (∃ x, A x) -> ∃ x, B x.
Show proof.
Definition istrans_subtype_containment {X} {A B C : hsubtype X}
(leq_AB : A ⊆ B) (leq_BC : B ⊆ C)
: A ⊆ C.
Show proof.
cbn in *; auto.
Definition negexists_to_forallneg_restricted
{X:UU} {A B : hsubtype X}
: ¬ (∃ x, A x ∧ B x) ⇒ (∀ x, A x ⇒ ¬ B x).
Show proof.
Definition negforall_to_existsneg_restricted (H_LEM : LEM)
{X:UU} {A B : hsubtype X}
: ¬ (∀ x, A x ⇒ B x) ⇒ ∃ x, A x ∧ ¬ B x.
Show proof.
intros H_forall. apply (proof_by_contradiction H_LEM).
intros H_nex.
use H_forall. intros x A_x. apply (proof_by_contradiction H_LEM).
use (negexists_to_forallneg_restricted H_nex); assumption.
intros H_nex.
use H_forall. intros x A_x. apply (proof_by_contradiction H_LEM).
use (negexists_to_forallneg_restricted H_nex); assumption.
Definition subtype_binaryintersection {X} (A B : hsubtype X) : hsubtype X
:= fun x => A x ∧ B x.
Notation "A ∩ B" := (subtype_binaryintersection A B)
(at level 40, left associativity) : subtype.
Definition subtype_binaryintersection_leq1 {X} (A B : hsubtype X)
: A ∩ B ⊆ A
:= fun x => pr1.
Definition subtype_binaryintersection_leq2 {X} (A B : hsubtype X)
: A ∩ B ⊆ B
:= fun x => pr2.
Definition hconj_equiv {X:UU}
{A A' B B' : hsubtype X} (e_A : A ≡ A') (e_B : B ≡ B')
: (A ∩ B) ≡ (A' ∩ B').
Show proof.
intros x; split; intros [? ?]; split;
try apply e_A; try apply e_B; assumption.
try apply e_A; try apply e_B; assumption.
Definition subtype_binaryintersection_univ {X} (A B C : hsubtype X)
: C ⊆ A ∩ B <-> C ⊆ A ∧ C ⊆ B.
Show proof.
split.
- intros C_AB. split; apply (istrans_subtype_containment C_AB).
+ apply subtype_binaryintersection_leq1.
+ apply subtype_binaryintersection_leq2.
- cbn. intros [? ?]; split; auto.
- intros C_AB. split; apply (istrans_subtype_containment C_AB).
+ apply subtype_binaryintersection_leq1.
+ apply subtype_binaryintersection_leq2.
- cbn. intros [? ?]; split; auto.
Definition image {X Y : UU} (f : X -> Y) : hsubtype Y
:= fun y => ∥ hfiber f y ∥.
Definition value_in_image {X Y : UU} (f : X -> Y) (x : X) : image f (f x)
:= hinhpr (x ,, idpath _).
Definition to_image {X Y : UU} (f : X -> Y) (x : X) : image f
:= (f x,, value_in_image f x).
See image_univ below for a version that plays better with apply.
Definition image_univ
{X Y : UU} (f : X -> Y)
(A : hsubtype Y )
: (∀ x:X, A (f x)) <-> (image f ⊆ A).
Show proof.
{X Y : UU} (f : X -> Y)
(A : hsubtype Y )
: (∀ x:X, A (f x)) <-> (image f ⊆ A).
Show proof.
split.
- intros H_A y Hy.
refine (factor_through_squash_hProp _ _ Hy);
intros [x e_xy]; destruct e_xy.
use H_A.
- intros H_A x.
use H_A. apply value_in_image.
- intros H_A y Hy.
refine (factor_through_squash_hProp _ _ Hy);
intros [x e_xy]; destruct e_xy.
use H_A.
- intros H_A x.
use H_A. apply value_in_image.
Alias of image_univ using explicit “forall” instead of “⊆” or “∀”, for easier use with the apply tactic.
Definition image_univ'
{X Y : UU} (f : X -> Y)
(A : hsubtype Y )
: (forall x:X, A (f x)) <-> (forall y:Y, (image f y) -> A y).
Show proof.
Definition image_carrier_univ
{X Y : UU} (f : X -> Y)
(A : hsubtype Y )
: (∀ x:X, A (f x)) <-> (∀ y : image f, A (pr1 y)).
Show proof.
{X Y : UU} (f : X -> Y)
(A : hsubtype Y )
: (forall x:X, A (f x)) <-> (forall y:Y, (image f y) -> A y).
Show proof.
Definition image_carrier_univ
{X Y : UU} (f : X -> Y)
(A : hsubtype Y )
: (∀ x:X, A (f x)) <-> (∀ y : image f, A (pr1 y)).
Show proof.
split.
- intros H [y im_y]. eapply image_univ'; eassumption.
- intros H; cbn. apply image_univ'.
intros y im_y. exact (H (y,,im_y)).
- intros H [y im_y]. eapply image_univ'; eassumption.
- intros H; cbn. apply image_univ'.
intros y im_y. exact (H (y,,im_y)).
Like image_univ', alias using explicit “forall” instead of “∀”, for easier use with the apply tactic.
Definition image_carrier_univ'
{X Y : UU} (f : X -> Y)
(A : hsubtype Y )
: (forall x:X, A (f x)) <-> (forall y : image f, A (pr1 y)).
Show proof.
End Auxiliary.
Notation "A ∩ B" := (subtype_binaryintersection A B)
(at level 40, left associativity) : subtype.
Notation "A ∪ B" := (subtype_binaryunion A B)
(at level 40, left associativity) : subtype.
{X Y : UU} (f : X -> Y)
(A : hsubtype Y )
: (forall x:X, A (f x)) <-> (forall y : image f, A (pr1 y)).
Show proof.
End Auxiliary.
Notation "A ∩ B" := (subtype_binaryintersection A B)
(at level 40, left associativity) : subtype.
Notation "A ∪ B" := (subtype_binaryunion A B)
(at level 40, left associativity) : subtype.
Completeness properties
Section LowerBounds.
Context {P : Poset}.
Definition islowerbound {I} (p : I -> P) (x : P) : hProp
:= ∀ i : I, x ≤ p i.
Definition islowerbound_subtype (A : hsubtype P) (x : P) : hProp
:= islowerbound (pr1carrier A) x.
Definition islowerbound_subtype_equiv {A B : hsubtype P}
: (A ≡ B)
-> islowerbound_subtype A ≡ islowerbound_subtype B.
Show proof.
Definition is_lower_bound_subfamily {I} (f : I -> P) {J} (g : J -> P)
(ff : forall j, (image f) (g j))
{x} (x_lb : islowerbound f x)
: islowerbound g x.
Show proof.
Definition image_same_lower_bounds {I} (f : I -> P) {x : P}
: islowerbound f x
<-> islowerbound_subtype (image f) x.
Show proof.
End LowerBounds.
Section UpperBounds.
Context {P : Poset}.
Definition isupperbound_hprop {I} (p : I -> P) (x:P) : hProp
:= make_hProp _ (isaprop_isupperbound p x).
Definition isupperbound_subtype (A : hsubtype P) (x : P) : hProp
:= isupperbound_hprop (pr1carrier A) x.
Definition isupperbound_subtype_equiv {A B : hsubtype P}
: (A ≡ B)
-> isupperbound_subtype A ≡ isupperbound_subtype B.
Show proof.
Definition is_upper_bound_subfamily {I} (f : I -> P) {J} (g : J -> P)
(ff : forall j, (image f) (g j))
{x} (x_ub : isupperbound f x)
: isupperbound g x.
Show proof.
Definition image_same_upper_bounds {I} (f : I -> P) {x : P}
: isupperbound f x
<-> isupperbound_subtype (image f) x.
Show proof.
End UpperBounds.
Section Least.
Context {P : Poset}.
Definition least_of_family {I} (p : I -> P)
:= ∑ i : I, islowerbound p (p i).
Definition least_of_family_index {I} {p : I -> P}
: least_of_family p -> I
:= pr1.
Coercion realise_least_of_family {I} (p : I -> P)
: least_of_family p -> P
:= fun ih => p (pr1 ih).
Definition least_is_least {I} (p : I -> P) (x : least_of_family p)
: islowerbound p x
:= pr2 x.
Definition least_suchthat (A : P -> UU) : UU
:= least_of_family (pr1 : (∑ x:P, A x) -> P).
Identity Coercion id_least_suchthat : least_suchthat >-> least_of_family.
Definition least_suchthat_satisfies {A : P -> UU} (x : least_suchthat A)
: A x
:= pr2 (least_of_family_index x).
Definition least_suchthat_is_least {A : P -> UU} (x : least_suchthat A)
: ∏ y, A y -> x ≤ y.
Show proof.
It’s useful to define least_suchthat as above, for interaction with least_of_family, etc; but also helpful to have a standalone predicate version.
Definition is_least_suchthat (A : P -> hProp) (x : P) : hProp
:= (A x) ∧ (islowerbound_subtype A x).
Definition least_suchthat_property {A : P -> hProp} (x : least_suchthat A)
: is_least_suchthat A x.
Show proof.
Definition make_least_suchthat {A : P -> hProp}
(x : P) (x_least : is_least_suchthat A x)
: least_suchthat A.
Show proof.
End Least.
Section Greatest.
Context {P : Poset}.
Definition greatest_of_family {I} (p : I -> P)
:= ∑ i : I, isupperbound p (p i).
Definition greatest_of_family_index {I} {p : I -> P}
: greatest_of_family p -> I
:= pr1.
Coercion realise_greatest_of_family {I} (p : I -> P)
: greatest_of_family p -> P
:= fun ih => p (pr1 ih).
Definition greatest_is_greatest {I} (p : I -> P) (x : greatest_of_family p)
: isupperbound p x
:= pr2 x.
Definition greatest_suchthat (A : P -> UU) : UU
:= greatest_of_family (pr1 : (∑ x:P, A x) -> P).
Identity Coercion id_greatest_suchthat : greatest_suchthat >-> greatest_of_family.
Definition greatest_suchthat_satisfies {A : P -> UU} (x : greatest_suchthat A)
: A x
:= pr2 (greatest_of_family_index x).
Definition greatest_suchthat_is_greatest {A : P -> UU} (x : greatest_suchthat A)
: ∏ y, A y -> y ≤ x.
Show proof.
:= (A x) ∧ (islowerbound_subtype A x).
Definition least_suchthat_property {A : P -> hProp} (x : least_suchthat A)
: is_least_suchthat A x.
Show proof.
Definition make_least_suchthat {A : P -> hProp}
(x : P) (x_least : is_least_suchthat A x)
: least_suchthat A.
Show proof.
End Least.
Section Greatest.
Context {P : Poset}.
Definition greatest_of_family {I} (p : I -> P)
:= ∑ i : I, isupperbound p (p i).
Definition greatest_of_family_index {I} {p : I -> P}
: greatest_of_family p -> I
:= pr1.
Coercion realise_greatest_of_family {I} (p : I -> P)
: greatest_of_family p -> P
:= fun ih => p (pr1 ih).
Definition greatest_is_greatest {I} (p : I -> P) (x : greatest_of_family p)
: isupperbound p x
:= pr2 x.
Definition greatest_suchthat (A : P -> UU) : UU
:= greatest_of_family (pr1 : (∑ x:P, A x) -> P).
Identity Coercion id_greatest_suchthat : greatest_suchthat >-> greatest_of_family.
Definition greatest_suchthat_satisfies {A : P -> UU} (x : greatest_suchthat A)
: A x
:= pr2 (greatest_of_family_index x).
Definition greatest_suchthat_is_greatest {A : P -> UU} (x : greatest_suchthat A)
: ∏ y, A y -> y ≤ x.
Show proof.
It’s useful to define greatest_suchthat as above, for interaction with greatest_of_family, etc; but also helpful to have a standalone predicate version.
Definition is_greatest_suchthat (A : P -> hProp) (x : P) : hProp
:= (A x) ∧ (isupperbound_subtype A x).
Definition greatest_suchthat_property {A : P -> hProp} (x : greatest_suchthat A)
: is_greatest_suchthat A x.
Show proof.
Definition make_greatest_suchthat {A : P -> hProp}
(x : P) (x_greatest : is_greatest_suchthat A x)
: greatest_suchthat A.
Show proof.
End Greatest.
Section LeastUpperBounds.
Context {P : Poset}.
Definition least_upper_bound {I} (p : I -> P)
:= least_suchthat (isupperbound_hprop p).
Identity Coercion id_least_upper_bound : least_upper_bound >-> least_suchthat.
Definition least_upper_bound_is_upper_bound {I} {p : I -> P}
(x : least_upper_bound p)
: isupperbound p x
:= least_suchthat_satisfies x.
:= (A x) ∧ (isupperbound_subtype A x).
Definition greatest_suchthat_property {A : P -> hProp} (x : greatest_suchthat A)
: is_greatest_suchthat A x.
Show proof.
Definition make_greatest_suchthat {A : P -> hProp}
(x : P) (x_greatest : is_greatest_suchthat A x)
: greatest_suchthat A.
Show proof.
End Greatest.
Section LeastUpperBounds.
Context {P : Poset}.
Definition least_upper_bound {I} (p : I -> P)
:= least_suchthat (isupperbound_hprop p).
Identity Coercion id_least_upper_bound : least_upper_bound >-> least_suchthat.
Definition least_upper_bound_is_upper_bound {I} {p : I -> P}
(x : least_upper_bound p)
: isupperbound p x
:= least_suchthat_satisfies x.
It’s useful to define least_upper_bound as above, for interaction with upper_bound, etc; but also helpful to have a standalone predicate version.
Definition is_least_upper_bound {I} (p : I -> P) (x : P) : hProp
:= is_least_suchthat (isupperbound_hprop p) x.
Definition make_least_upper_bound {I} {p : I -> P}
(x:P) (x_lub : is_least_upper_bound p x)
: least_upper_bound p
:= make_least_suchthat x x_lub.
Definition least_upper_bound_property {I} {p : I -> P}
(x : least_upper_bound p)
: is_least_upper_bound p x
:= least_suchthat_property x.
:= is_least_suchthat (isupperbound_hprop p) x.
Definition make_least_upper_bound {I} {p : I -> P}
(x:P) (x_lub : is_least_upper_bound p x)
: least_upper_bound p
:= make_least_suchthat x x_lub.
Definition least_upper_bound_property {I} {p : I -> P}
(x : least_upper_bound p)
: is_least_upper_bound p x
:= least_suchthat_property x.
The universal property of the least upper bound
Definition least_upper_bound_univ {I} {p : I -> P}
(x : least_upper_bound p) (x' : P)
: x ≤ x' <-> isupperbound p x'.
Show proof.
(x : least_upper_bound p) (x' : P)
: x ≤ x' <-> isupperbound p x'.
Show proof.
split.
- intros xx' i.
eapply istrans_posetRelation; try eassumption.
apply least_upper_bound_is_upper_bound.
- intros H. refine (least_is_least _ x (_,,H)).
- intros xx' i.
eapply istrans_posetRelation; try eassumption.
apply least_upper_bound_is_upper_bound.
- intros H. refine (least_is_least _ x (_,,H)).
Specialisation of the above functions to least upper bounds of subtypes
— a common use-case, and the functions are often easier to use in this form.
Definition is_least_upper_bound_subtype (A : hsubtype P) (x : P) : hProp
:= is_least_upper_bound (pr1carrier A) x.
Definition least_upper_bound_subtype (A : hsubtype P) : UU
:= least_upper_bound (pr1carrier A).
Identity Coercion id_least_upper_bound_subtype
: least_upper_bound_subtype >-> least_upper_bound.
Definition least_upper_bound_subtype_is_upper_bound {A : hsubtype P}
(x : least_upper_bound_subtype A) {y : P} (A_y : A y)
: y ≤ x
:= least_upper_bound_is_upper_bound x (y,,A_y).
Definition least_upper_bound_subtype_univ {A : hsubtype P}
(x : least_upper_bound (pr1carrier A)) (x' : P)
: x ≤ x' <-> (forall y, A y -> y ≤ x').
Show proof.
:= is_least_upper_bound (pr1carrier A) x.
Definition least_upper_bound_subtype (A : hsubtype P) : UU
:= least_upper_bound (pr1carrier A).
Identity Coercion id_least_upper_bound_subtype
: least_upper_bound_subtype >-> least_upper_bound.
Definition least_upper_bound_subtype_is_upper_bound {A : hsubtype P}
(x : least_upper_bound_subtype A) {y : P} (A_y : A y)
: y ≤ x
:= least_upper_bound_is_upper_bound x (y,,A_y).
Definition least_upper_bound_subtype_univ {A : hsubtype P}
(x : least_upper_bound (pr1carrier A)) (x' : P)
: x ≤ x' <-> (forall y, A y -> y ≤ x').
Show proof.
split.
- intros H y A_y.
refine (pr1 (least_upper_bound_univ x x') H (_,,_)); assumption.
- intros H.
apply least_upper_bound_univ.
intros [y A_y]; apply H; assumption.
- intros H y A_y.
refine (pr1 (least_upper_bound_univ x x') H (_,,_)); assumption.
- intros H.
apply least_upper_bound_univ.
intros [y A_y]; apply H; assumption.
Comparison of least upper bounds between families and their images
Definition is_least_upper_bound_image {I} (f : I -> P) {x : P}
: is_least_upper_bound f x
<-> is_least_upper_bound (pr1carrier (image f)) x.
Show proof.
revert x. apply hconj_equiv.
- use image_same_upper_bounds.
- apply islowerbound_subtype_equiv. use image_same_upper_bounds.
- use image_same_upper_bounds.
- apply islowerbound_subtype_equiv. use image_same_upper_bounds.
Definition least_upper_bound_image {I} (f : I -> P)
: least_upper_bound f <-> least_upper_bound (pr1carrier (image f)).
Show proof.
split; intros x; apply (make_least_upper_bound x);
apply is_least_upper_bound_image, least_upper_bound_property.
apply is_least_upper_bound_image, least_upper_bound_property.
Lemma greatest_if_contains_sup
(A : hsubtype P) (x : P)
: A x -> is_least_upper_bound_subtype A x -> is_greatest_suchthat A x.
Show proof.
End LeastUpperBounds.
Section Chains.
Definition comparable {P : Poset} (x y : P) : hProp
:= (x ≤ y) ∨ (y ≤ x).
Definition is_chain {P : Poset} {I} (p : I -> P) : hProp
:= ∀ i j : I, comparable (p i) (p j).
Definition Chain (P : Poset) : UU
:= ∑ (I : UU), ∑ (p : I -> P), is_chain p.
Coercion chain_index {P} (C : Chain P) : UU
:= pr1 C.
Definition chain_family {P} (C : Chain P) : C -> P
:= pr1 (pr2 C).
Coercion chain_family : Chain >-> Funclass.
Definition chain_property {P} (C : Chain P) : is_chain C
:= pr2 (pr2 C).
Definition fmap_is_chain {P Q} (f : posetmorphism P Q)
{I : UU} (p : I -> P)
: is_chain p -> is_chain (f ∘ p).
Show proof.
intros p_chain x y.
apply (hdisj_monot' (p_chain x y));
intro; apply posetmorphism_property; assumption.
apply (hdisj_monot' (p_chain x y));
intro; apply posetmorphism_property; assumption.
Definition fmap_chain {P Q} (f : posetmorphism P Q)
: Chain P -> Chain Q.
Show proof.
Definition Chain_hsubtype (P : Poset) : UU
:= ∑ A : hsubtype P, is_chain (pr1carrier A).
Coercion pr1_Chain_hsubtype {P} : Chain_hsubtype P -> hsubtype P
:= pr1.
Coercion Chain_of_Chain_hsubtype (P : Poset)
: Chain_hsubtype P -> Chain P.
Show proof.
Definition image_is_chain {P:Poset} {I:UU} (p : I -> P)
: is_chain p -> is_chain (pr1carrier (image p)).
Show proof.
intros p_chain. unfold is_chain.
apply (image_carrier_univ p (fun x => ∀ j, comparable x _)); intros i.
apply (image_carrier_univ p); intros j.
use p_chain.
apply (image_carrier_univ p (fun x => ∀ j, comparable x _)); intros i.
apply (image_carrier_univ p); intros j.
use p_chain.
Definition image_chain {P:Poset}
: Chain P -> Chain_hsubtype P.
Show proof.
End Chains.
Section Directed.
Definition Directed_family (P : Poset) : UU
:= ∑ (I : UU), ∑ (p : I -> P), isdirected p.
Coercion directed_index {P} (C : Directed_family P) : UU
:= pr1 C.
Definition directed_family {P} (C : Directed_family P) : C -> P
:= pr1 (pr2 C).
Coercion directed_family : Directed_family >-> Funclass.
Definition directed_property {P} (C : Directed_family P) : isdirected C
:= pr2 (pr2 C).
Definition make_directed {P:Poset} {I} {p : I -> P} (p_directed : isdirected p)
: Directed_family P
:= (I,,(p,,p_directed)).
Definition fmap_is_directed {P Q} (f : posetmorphism P Q)
{I : UU} (p : I -> P)
: isdirected p -> isdirected (f ∘ p).
Show proof.
intros p_directed; split.
- eapply isdirected_inhabited, p_directed.
- intros i j.
eapply exists_monotone.
2: { exact (isdirected_compatible p_directed i j). }
intros x [le_i_x le_j_x].
split; apply posetmorphism_property; assumption.
- eapply isdirected_inhabited, p_directed.
- intros i j.
eapply exists_monotone.
2: { exact (isdirected_compatible p_directed i j). }
intros x [le_i_x le_j_x].
split; apply posetmorphism_property; assumption.
Definition fmap_directed {P Q} (f : posetmorphism P Q)
: Directed_family P -> Directed_family Q.
Show proof.
Definition Directed_hsubtype (P : Poset) : UU
:= ∑ A : hsubtype P, isdirected (pr1carrier A).
Coercion pr1_Directed_hsubtype {P} : Directed_hsubtype P -> hsubtype P
:= pr1.
Coercion Directed_of_Directed_hsubtype (P : Poset)
: Directed_hsubtype P -> Directed_family P.
Show proof.
Definition image_is_directed {P:Poset} {I:UU} (p : I -> P)
: isdirected p -> isdirected (pr1carrier (image p)).
Show proof.
intros p_directed. split.
- apply (squash_to_hProp (isdirected_inhabited p_directed)).
intros i; apply hinhpr.
apply to_image; assumption.
- use (pr1 (image_carrier_univ' p (fun x => ∀ j, ∃ k, x ≤ _ ∧ _))). intros i.
use (pr1 (image_carrier_univ' p (fun y => ∃ k, _ ∧ y ≤ _))); intros j.
apply (squash_to_hProp (isdirected_compatible p_directed i j)).
intros [k [le_ik le_jk]].
apply hinhpr. exists (to_image _ k).
split; assumption.
- apply (squash_to_hProp (isdirected_inhabited p_directed)).
intros i; apply hinhpr.
apply to_image; assumption.
- use (pr1 (image_carrier_univ' p (fun x => ∀ j, ∃ k, x ≤ _ ∧ _))). intros i.
use (pr1 (image_carrier_univ' p (fun y => ∃ k, _ ∧ y ≤ _))); intros j.
apply (squash_to_hProp (isdirected_compatible p_directed i j)).
intros [k [le_ik le_jk]].
apply hinhpr. exists (to_image _ k).
split; assumption.
Definition image_directed {P:Poset}
: Directed_family P -> Directed_hsubtype P.
Show proof.
End Directed.
Section Completeness.
Definition is_complete (P : Poset) : UU
:= ∏ A : hsubtype P, least_upper_bound (pr1carrier A).
is_complete is defined just in terms of hsubtypes, to agree with the classical definition and keep its quantification “small”.
However, it implies completeness for arbitrarily families.
Definition family_lub {P:Poset} (P_complete : is_complete P)
{I:UU} (f : I -> P)
: least_upper_bound f.
Show proof.
Definition is_chain_complete (P : Poset) : UU
:= ∏ C : Chain_hsubtype P, least_upper_bound_subtype C.
{I:UU} (f : I -> P)
: least_upper_bound f.
Show proof.
Definition is_chain_complete (P : Poset) : UU
:= ∏ C : Chain_hsubtype P, least_upper_bound_subtype C.
Like is_complete, is_chain_complete is defined just in terms of hsubtype-chains, to keep quantification small.
However, it implies least upper bounds for arbitarily-indexed chains.
Definition chain_lub {P : Poset} (P_CC : is_chain_complete P)
(p : Chain P)
: least_upper_bound p.
Show proof.
(p : Chain P)
: least_upper_bound p.
Show proof.
Version with is_chain split out, for easier application
Definition chain_lub' {P : Poset} (P_CC : is_chain_complete P)
{I:UU} (p:I->P)
: is_chain p -> least_upper_bound p.
Show proof.
Definition is_directed_complete (P : Poset) : UU
:= ∏ A : Directed_hsubtype P, least_upper_bound (directed_family A).
{I:UU} (p:I->P)
: is_chain p -> least_upper_bound p.
Show proof.
Definition is_directed_complete (P : Poset) : UU
:= ∏ A : Directed_hsubtype P, least_upper_bound (directed_family A).
Like is_complete, is_directed_complete is defined just in terms of directed subtypes, to keep quantification small.
However, it implies least upper bounds for arbitary directed families.
Definition directed_lub {P : Poset} (P_DC : is_directed_complete P)
(p : Directed_family P)
: least_upper_bound p.
Show proof.
Definition isdirected_lub {P : Poset} (P_DC : is_directed_complete P)
{I} (p : I -> P) (p_directed : isdirected p)
: least_upper_bound p.
Show proof.
End Completeness.
(p : Directed_family P)
: least_upper_bound p.
Show proof.
Definition isdirected_lub {P : Poset} (P_DC : is_directed_complete P)
{I} (p : I -> P) (p_directed : isdirected p)
: least_upper_bound p.
Show proof.
End Completeness.
Section Subposets.
Definition subposet_incl {P : Poset} {A : Subposet' P} : posetmorphism A P
:= pr1 (pr2 A).
Definition is_upper_bound_in_subposet {P : Poset} {A : Subposet P}
{I} {p : I -> A} {x : A}
: isupperbound (subposet_incl ∘ p) (subposet_incl x)
<-> isupperbound p x.
Show proof.
Definition subposet_incl {P : Poset} {A : Subposet' P} : posetmorphism A P
:= pr1 (pr2 A).
Definition is_upper_bound_in_subposet {P : Poset} {A : Subposet P}
{I} {p : I -> A} {x : A}
: isupperbound (subposet_incl ∘ p) (subposet_incl x)
<-> isupperbound p x.
Show proof.
split; auto.
Given a chain in a sub-poset with a least upper bound in the ambient poset,
if the l.u.b. lies in the sub-poset, then it’s an l.u.b. there.
Definition is_least_upper_bound_in_subposet {P : Poset} {A : Subposet P}
{I} {p : I -> A} {x : A}
(x_lub : is_least_upper_bound (subposet_incl ∘ p) (subposet_incl x))
: is_least_upper_bound p x.
Show proof.
Definition least_upper_bound_in_subposet {P : Poset} {A : Subposet P}
{I} {p : I -> A}
(x : least_upper_bound (pr1 ∘ p)) (x_A : A x)
: least_upper_bound p.
Show proof.
Definition is_chain_in_subposet {P : Poset} {A : Subposet P}
{I : Type} (p : I -> A)
: is_chain p <-> is_chain (subposet_incl ∘ p).
Show proof.
Definition is_chain_complete_subposet
{P : Poset} (P_CC : is_chain_complete P) {A : Subposet P}
(A_chain_closed : forall C : Chain_hsubtype A,
A (chain_lub P_CC (fmap_chain subposet_incl C)))
: is_chain_complete A.
Show proof.
End Subposets.
{I} {p : I -> A} {x : A}
(x_lub : is_least_upper_bound (subposet_incl ∘ p) (subposet_incl x))
: is_least_upper_bound p x.
Show proof.
split.
- apply is_upper_bound_in_subposet, x_lub.
- intros [x' x'_ub].
apply (least_upper_bound_univ (make_least_upper_bound _ x_lub)).
apply is_upper_bound_in_subposet; assumption.
- apply is_upper_bound_in_subposet, x_lub.
- intros [x' x'_ub].
apply (least_upper_bound_univ (make_least_upper_bound _ x_lub)).
apply is_upper_bound_in_subposet; assumption.
Definition least_upper_bound_in_subposet {P : Poset} {A : Subposet P}
{I} {p : I -> A}
(x : least_upper_bound (pr1 ∘ p)) (x_A : A x)
: least_upper_bound p.
Show proof.
use make_least_upper_bound.
{ exists x. apply x_A. }
apply is_least_upper_bound_in_subposet, least_upper_bound_property.
{ exists x. apply x_A. }
apply is_least_upper_bound_in_subposet, least_upper_bound_property.
Definition is_chain_in_subposet {P : Poset} {A : Subposet P}
{I : Type} (p : I -> A)
: is_chain p <-> is_chain (subposet_incl ∘ p).
Show proof.
split; auto.
Definition is_chain_complete_subposet
{P : Poset} (P_CC : is_chain_complete P) {A : Subposet P}
(A_chain_closed : forall C : Chain_hsubtype A,
A (chain_lub P_CC (fmap_chain subposet_incl C)))
: is_chain_complete A.
Show proof.
intros C.
use make_least_upper_bound.
{ exists (chain_lub P_CC (fmap_chain subposet_incl C)).
apply A_chain_closed. }
apply is_least_upper_bound_in_subposet.
apply least_upper_bound_property.
use make_least_upper_bound.
{ exists (chain_lub P_CC (fmap_chain subposet_incl C)).
apply A_chain_closed. }
apply is_least_upper_bound_in_subposet.
apply least_upper_bound_property.
End Subposets.
The most general poset of functions is just the product of a family of posets.
We set this up first, and then give other posets of functions (e.g. the poset of poset maps) as subposets of this general one.
Definition pointwiseorder {X:UU} (P : X -> Poset) : hrel (∏ x, P x)
:= fun f g => ∀ x, f x ≤ g x.
Lemma ispartialorder_pointwiseorder {X:UU} (P : X -> Poset)
: isPartialOrder (pointwiseorder P).
Show proof.
:= fun f g => ∀ x, f x ≤ g x.
Lemma ispartialorder_pointwiseorder {X:UU} (P : X -> Poset)
: isPartialOrder (pointwiseorder P).
Show proof.
repeat split.
- repeat intro. eapply istrans_posetRelation; auto.
- repeat intro. apply isrefl_posetRelation.
- intros f g le_f_g le_g_f.
use funextsec; intro.
apply isantisymm_posetRelation; auto.
- repeat intro. eapply istrans_posetRelation; auto.
- repeat intro. apply isrefl_posetRelation.
- intros f g le_f_g le_g_f.
use funextsec; intro.
apply isantisymm_posetRelation; auto.
Note: could also be called e.g. Poset_product, or various other names.
Definition forall_Poset {X:UU} (P : X -> Poset) : Poset.
Show proof.
Definition arrow_Poset (X:UU) (P : Poset) : Poset
:= forall_Poset (fun _:X => P).
Definition isupperbound_if_pointwise {X:UU} {P : X -> Poset}
{I} {f : I -> forall_Poset P}
{g : forall_Poset P}
: isupperbound f g <-> forall x, isupperbound (fun i => f i x) (g x).
Show proof.
Definition is_least_upper_bound_pointwise {X:UU} {P : X -> Poset}
{I} (f : I -> forall_Poset P)
(g : forall_Poset P)
: hProp
:= ∀ x, is_least_upper_bound (fun i => f i x) (g x).
Definition is_least_upper_bound_if_pointwise {X:UU} {P : X -> Poset}
{I} {f : I -> forall_Poset P}
{g : forall_Poset P}
: is_least_upper_bound_pointwise f g
-> is_least_upper_bound f g.
Show proof.
Lemma isaposetmorphism_pointwise_lub {P : Poset}
{I} {f : I -> P -> P} (f_monot : forall i, isaposetmorphism (f i))
{g} (g_pw_lub : is_least_upper_bound_pointwise f g)
: isaposetmorphism g.
Show proof.
End Function_Posets.
Show proof.
use make_Poset. { exact (forall_hSet P). }
use make_PartialOrder. { apply pointwiseorder. }
apply ispartialorder_pointwiseorder.
use make_PartialOrder. { apply pointwiseorder. }
apply ispartialorder_pointwiseorder.
Definition arrow_Poset (X:UU) (P : Poset) : Poset
:= forall_Poset (fun _:X => P).
Definition isupperbound_if_pointwise {X:UU} {P : X -> Poset}
{I} {f : I -> forall_Poset P}
{g : forall_Poset P}
: isupperbound f g <-> forall x, isupperbound (fun i => f i x) (g x).
Show proof.
split; intro H; repeat intro; use H.
Definition is_least_upper_bound_pointwise {X:UU} {P : X -> Poset}
{I} (f : I -> forall_Poset P)
(g : forall_Poset P)
: hProp
:= ∀ x, is_least_upper_bound (fun i => f i x) (g x).
Definition is_least_upper_bound_if_pointwise {X:UU} {P : X -> Poset}
{I} {f : I -> forall_Poset P}
{g : forall_Poset P}
: is_least_upper_bound_pointwise f g
-> is_least_upper_bound f g.
Show proof.
intro pointwise_lub.
set (g_pwlub := fun x => make_least_upper_bound _ (pointwise_lub x)).
split.
- intros i x.
apply (least_upper_bound_is_upper_bound (g_pwlub x)).
- intros [g' g'_ub] x.
apply (least_upper_bound_univ (g_pwlub x)).
apply isupperbound_if_pointwise, g'_ub.
set (g_pwlub := fun x => make_least_upper_bound _ (pointwise_lub x)).
split.
- intros i x.
apply (least_upper_bound_is_upper_bound (g_pwlub x)).
- intros [g' g'_ub] x.
apply (least_upper_bound_univ (g_pwlub x)).
apply isupperbound_if_pointwise, g'_ub.
Lemma isaposetmorphism_pointwise_lub {P : Poset}
{I} {f : I -> P -> P} (f_monot : forall i, isaposetmorphism (f i))
{g} (g_pw_lub : is_least_upper_bound_pointwise f g)
: isaposetmorphism g.
Show proof.
intros x y le_x_y.
apply (least_upper_bound_univ (make_least_upper_bound _ (g_pw_lub _))).
intros i.
eapply istrans_posetRelation.
2: { apply (least_upper_bound_is_upper_bound
(make_least_upper_bound _ (g_pw_lub _))). }
apply f_monot; assumption.
apply (least_upper_bound_univ (make_least_upper_bound _ (g_pw_lub _))).
intros i.
eapply istrans_posetRelation.
2: { apply (least_upper_bound_is_upper_bound
(make_least_upper_bound _ (g_pw_lub _))). }
apply f_monot; assumption.
End Function_Posets.
Classes of maps
Section ProgressiveMaps.
Definition isprogressive {P : Poset} : hsubtype (P -> P) : UU
:= fun f => ∀ (x : P), x ≤ f x.
Definition Progressive_map (P : Poset) := carrier (@isprogressive P).
Definition pr1_Progressive_map {P : Poset} : Progressive_map P -> (P -> P)
:= pr1carrier _.
Coercion pr1_Progressive_map : Progressive_map >-> Funclass.
Definition progressive_property {P} (f : Progressive_map P)
: isprogressive f
:= pr2 f.
Lemma isprogressive_idfun {P : Poset} : isprogressive (idfun P).
Show proof.
Lemma isprogressive_compose {P : Poset}
{f g : P -> P} (f_prog : isprogressive f) (g_prog : isprogressive g)
: isprogressive (f ∘ g).
Show proof.
Lemma progressive_pointwise_lub {P : Poset}
{I} {f : I -> P -> P} (f_prog : forall i, isprogressive (f i))
{g} (g_pw_lub : is_least_upper_bound_pointwise f g)
(I_inhab : ∥ I ∥)
: isprogressive g.
Show proof.
intros x. eapply factor_through_squash_hProp. 2: { apply I_inhab. }
intros i.
eapply istrans_posetRelation. { use f_prog; apply i. }
revert i.
refine (@least_upper_bound_is_upper_bound _ _ _ (make_least_upper_bound _ _)).
use g_pw_lub.
intros i.
eapply istrans_posetRelation. { use f_prog; apply i. }
revert i.
refine (@least_upper_bound_is_upper_bound _ _ _ (make_least_upper_bound _ _)).
use g_pw_lub.
End ProgressiveMaps.
Section Fixpoints.
Definition isfixedpoint {P : Poset} (f : P -> P) : hsubtype P
:= fun (x:P) => f x = x.
Definition Fixedpoint {P : Poset} (f : P -> P) : UU := carrier (isfixedpoint f).
Coercion pr1_Fixedpoint {P : Poset} {f : P -> P} : Fixedpoint f -> P
:= pr1carrier _.
Definition fixedpoint_property {P : Poset} {f : P -> P} (x : Fixedpoint f)
: f x = x
:= pr2 x.
Definition ispostfixedpoint {P : Poset} (f : P -> P) : hsubtype P
:= fun (x:P) => x ≤ f x.
Definition Postfixedpoint {P : Poset} (f : P -> P) : UU
:= carrier (ispostfixedpoint f).
Coercion pr1_Postfixedpoint {P : Poset} {f : P -> P} : Postfixedpoint f -> P
:= pr1carrier _.
Definition postfixedpoint_property {P : Poset} {f : P -> P} (x : Postfixedpoint f)
: x ≤ f x
:= pr2 x.
End Fixpoints.
The (Knaster–)Tarski fixpoint theorems
Section Tarski.
Theorem Knaster_Tarski_fixpoint {P:Poset} (P_complete : is_complete P)
(f : posetmorphism P P) {x0} (x0_postfix : x0 ≤ f x0)
: least_suchthat (fun x:P => f x = x ∧ x0 ≤ x).
Show proof.
Theorem Tarski_fixpoint_theorem
{P:Poset} (P_complete : is_complete P) (f : posetmorphism P P)
: is_complete ((fun x:P => f x = x) : Subposet P).
Show proof.
End Tarski.
Theorem Knaster_Tarski_fixpoint {P:Poset} (P_complete : is_complete P)
(f : posetmorphism P P) {x0} (x0_postfix : x0 ≤ f x0)
: least_suchthat (fun x:P => f x = x ∧ x0 ≤ x).
Show proof.
set (is_f_closed := (fun A => (∀ y, A y ⇒ A (f y)))
: hsubtype P -> hProp).
set (is_sup_closed
:= (fun A => ∀ C' : hsubtype P, C' ⊆ A ⇒ A (P_complete C'))
: hsubtype P -> hProp).
set (C := (fun x =>
∀ A : hsubtype P, A x0 ⇒ is_f_closed A ⇒ is_sup_closed A ⇒ A x)
: hsubtype P).
assert (C_x0 : C x0).
{ intros A A_x0 A_f_closed A_sup_closed; assumption. }
assert (C_f_closed : is_f_closed C).
{ intros x C_x A A_x0 A_f_closed A_sup_closed.
use A_f_closed. use C_x; assumption. }
assert (C_sup_closed : is_sup_closed C).
{ intros X C_X A A_x0 A_f_closed A_sup_closed.
use A_sup_closed; intros ? ?; use C_X; assumption. }
assert (C_induction : ∀ (A : hsubtype P),
A x0 ⇒ is_f_closed (A ∩ C) ⇒ is_sup_closed (A ∩ C) ⇒ C ⊆ A).
{ intros A A_x0 A_sup_closed A_f_closed x Cx.
apply (Cx (fun x => A x ∧ C x)); [ split | | ]; assumption. }
assert (postfix_supclosed : is_sup_closed (fun x => x ≤ f x)).
{ intros A A_postfix.
apply least_upper_bound_subtype_univ. intros x A_x.
eapply istrans_posetRelation. { use A_postfix; apply A_x. }
apply posetmorphism_property.
apply least_upper_bound_subtype_is_upper_bound, A_x.
}
assert (postfix_C : C ⊆ (fun x => x ≤ f x)).
{ use C_induction.
- apply x0_postfix.
- intros x [x_postfix C_x]. split. 2: { use C_f_closed; assumption. }
apply posetmorphism_property, x_postfix.
- intros A IH_A. split.
2: { use C_sup_closed;
apply (istrans_subtype_containment IH_A),
subtype_binaryintersection_leq2. }
use postfix_supclosed.
apply (istrans_subtype_containment IH_A).
apply subtype_binaryintersection_leq1.
}
assert (C_below_allfix : ∏ x, (f x = x) ⇒ x0 ≤ x ⇒ C ⊆ (fun y => y ≤ x)).
{ intros x x_fix leq_x0_x.
use C_induction.
- assumption.
- intros y [le_yx C_y]. split. 2: { use C_f_closed; assumption. }
eapply istrans_posetRelation. { apply posetmorphism_property, le_yx. }
apply isrefl'_posetRelation, x_fix.
- intros A IH_A. split.
2: { use C_sup_closed.
apply (istrans_subtype_containment IH_A),
subtype_binaryintersection_leq2. }
apply least_upper_bound_subtype_univ.
apply (istrans_subtype_containment IH_A), subtype_binaryintersection_leq1.
}
set (sup_C := P_complete C).
assert (C_sup_C : C sup_C). { use C_sup_closed. intros ? ?; assumption. }
simple refine (((sup_C : P),,(_,,_)),,_); simpl.
- apply isantisymm_posetRelation.
+ refine (least_upper_bound_is_upper_bound sup_C (_,,_)).
use C_f_closed. apply C_sup_C.
+ use postfix_C. apply C_sup_C.
- refine (least_upper_bound_is_upper_bound sup_C (_,,_)); assumption.
- intros [x [x_fix leq_x0_x]]; simpl.
apply least_upper_bound_subtype_univ, C_below_allfix; assumption.
: hsubtype P -> hProp).
set (is_sup_closed
:= (fun A => ∀ C' : hsubtype P, C' ⊆ A ⇒ A (P_complete C'))
: hsubtype P -> hProp).
set (C := (fun x =>
∀ A : hsubtype P, A x0 ⇒ is_f_closed A ⇒ is_sup_closed A ⇒ A x)
: hsubtype P).
assert (C_x0 : C x0).
{ intros A A_x0 A_f_closed A_sup_closed; assumption. }
assert (C_f_closed : is_f_closed C).
{ intros x C_x A A_x0 A_f_closed A_sup_closed.
use A_f_closed. use C_x; assumption. }
assert (C_sup_closed : is_sup_closed C).
{ intros X C_X A A_x0 A_f_closed A_sup_closed.
use A_sup_closed; intros ? ?; use C_X; assumption. }
assert (C_induction : ∀ (A : hsubtype P),
A x0 ⇒ is_f_closed (A ∩ C) ⇒ is_sup_closed (A ∩ C) ⇒ C ⊆ A).
{ intros A A_x0 A_sup_closed A_f_closed x Cx.
apply (Cx (fun x => A x ∧ C x)); [ split | | ]; assumption. }
assert (postfix_supclosed : is_sup_closed (fun x => x ≤ f x)).
{ intros A A_postfix.
apply least_upper_bound_subtype_univ. intros x A_x.
eapply istrans_posetRelation. { use A_postfix; apply A_x. }
apply posetmorphism_property.
apply least_upper_bound_subtype_is_upper_bound, A_x.
}
assert (postfix_C : C ⊆ (fun x => x ≤ f x)).
{ use C_induction.
- apply x0_postfix.
- intros x [x_postfix C_x]. split. 2: { use C_f_closed; assumption. }
apply posetmorphism_property, x_postfix.
- intros A IH_A. split.
2: { use C_sup_closed;
apply (istrans_subtype_containment IH_A),
subtype_binaryintersection_leq2. }
use postfix_supclosed.
apply (istrans_subtype_containment IH_A).
apply subtype_binaryintersection_leq1.
}
assert (C_below_allfix : ∏ x, (f x = x) ⇒ x0 ≤ x ⇒ C ⊆ (fun y => y ≤ x)).
{ intros x x_fix leq_x0_x.
use C_induction.
- assumption.
- intros y [le_yx C_y]. split. 2: { use C_f_closed; assumption. }
eapply istrans_posetRelation. { apply posetmorphism_property, le_yx. }
apply isrefl'_posetRelation, x_fix.
- intros A IH_A. split.
2: { use C_sup_closed.
apply (istrans_subtype_containment IH_A),
subtype_binaryintersection_leq2. }
apply least_upper_bound_subtype_univ.
apply (istrans_subtype_containment IH_A), subtype_binaryintersection_leq1.
}
set (sup_C := P_complete C).
assert (C_sup_C : C sup_C). { use C_sup_closed. intros ? ?; assumption. }
simple refine (((sup_C : P),,(_,,_)),,_); simpl.
- apply isantisymm_posetRelation.
+ refine (least_upper_bound_is_upper_bound sup_C (_,,_)).
use C_f_closed. apply C_sup_C.
+ use postfix_C. apply C_sup_C.
- refine (least_upper_bound_is_upper_bound sup_C (_,,_)); assumption.
- intros [x [x_fix leq_x0_x]]; simpl.
apply least_upper_bound_subtype_univ, C_below_allfix; assumption.
Theorem Tarski_fixpoint_theorem
{P:Poset} (P_complete : is_complete P) (f : posetmorphism P P)
: is_complete ((fun x:P => f x = x) : Subposet P).
Show proof.
intros A.
set (A_in_P := (fun x:P => ∑ x_fix : (f x = x)%logic, A (x,,x_fix))%prop).
set (sup_P_A := P_complete A_in_P).
assert (sup_fix_A : least_suchthat (fun x:P => f x = x ∧ sup_P_A ≤ x)).
{ apply Knaster_Tarski_fixpoint; try assumption.
apply least_upper_bound_subtype_univ.
intros y [y_fix A_y].
apply (istrans_posetRelation _ _ (f y)).
{ apply isrefl'_posetRelation, pathsinv0; assumption. }
apply posetmorphism_property, least_upper_bound_subtype_is_upper_bound.
use tpair; assumption.
}
assert (sup_A_isfix : f sup_fix_A = sup_fix_A).
{ apply (least_suchthat_satisfies sup_fix_A). }
use make_least_upper_bound.
{ exists sup_fix_A. assumption. }
split.
- intros [[x x_fix] A_x]. simpl.
apply (istrans_posetRelation _ _ (sup_P_A)).
+ apply least_upper_bound_subtype_is_upper_bound. use tpair; assumption.
+ apply (least_suchthat_satisfies sup_fix_A).
- intros [[x x_fix] x_ub]. cbn.
apply least_suchthat_is_least.
split; try assumption.
apply least_upper_bound_subtype_univ.
intros y [y_fix A_y].
use (x_ub ((_,,_),,_)); assumption.
set (A_in_P := (fun x:P => ∑ x_fix : (f x = x)%logic, A (x,,x_fix))%prop).
set (sup_P_A := P_complete A_in_P).
assert (sup_fix_A : least_suchthat (fun x:P => f x = x ∧ sup_P_A ≤ x)).
{ apply Knaster_Tarski_fixpoint; try assumption.
apply least_upper_bound_subtype_univ.
intros y [y_fix A_y].
apply (istrans_posetRelation _ _ (f y)).
{ apply isrefl'_posetRelation, pathsinv0; assumption. }
apply posetmorphism_property, least_upper_bound_subtype_is_upper_bound.
use tpair; assumption.
}
assert (sup_A_isfix : f sup_fix_A = sup_fix_A).
{ apply (least_suchthat_satisfies sup_fix_A). }
use make_least_upper_bound.
{ exists sup_fix_A. assumption. }
split.
- intros [[x x_fix] A_x]. simpl.
apply (istrans_posetRelation _ _ (sup_P_A)).
+ apply least_upper_bound_subtype_is_upper_bound. use tpair; assumption.
+ apply (least_suchthat_satisfies sup_fix_A).
- intros [[x x_fix] x_ub]. cbn.
apply least_suchthat_is_least.
split; try assumption.
apply least_upper_bound_subtype_univ.
intros y [y_fix A_y].
use (x_ub ((_,,_),,_)); assumption.
End Tarski.
Bourbaki-Witt
Section Bourbaki_Witt.
Definition Bourbaki_Witt_property (P : Poset)
:= ∏ (f : Progressive_map P), Fixedpoint f.
Theorem traditionally credited to Bourbaki (1949) and Witt (1951). This proof is based on Lang, Algebra (2002), Appendix 2, Thm 2.1.
Theorem Bourbaki_Witt_fixpoint
: LEM -> ∏ P : Poset, is_chain_complete P -> Bourbaki_Witt_property P.
Show proof.
: LEM -> ∏ P : Poset, is_chain_complete P -> Bourbaki_Witt_property P.
Show proof.
intros H_LEM P P_CC f.
set (is_f_closed := (fun A => (∀ y, A y ⇒ A (f y)))
: hsubtype P -> hProp).
set (is_chain_closed
:= (fun A => (∀ C' : Chain_hsubtype P, (∏ y:C', A (pr1 y)) ⇒ A (P_CC C')))
: hsubtype P -> hProp).
set (C := (fun x =>
∀ A : hsubtype P, is_f_closed A ⇒ is_chain_closed A ⇒ A x)
: hsubtype P).
assert (C_f_closed : is_f_closed C).
{ intros x C_x A A_f_closed A_chain_closed.
use A_f_closed. use C_x; assumption. }
assert (C_chain_closed : is_chain_closed C).
{ intros x C_x A A_f_closed A_chain_closed.
use A_chain_closed. intro; use C_x; assumption. }
assert (C_induction : ∀ (A : hsubtype P),
is_f_closed (A ∩ C) ⇒ is_chain_closed (A ∩ C) ⇒ C ⊆ A).
{ intros A A_chain_closed A_f_closed x Cx.
apply (Cx (fun x => A x ∧ C x)); assumption. }
assert (C_is_chain : is_chain (pr1carrier C)).
2: {
set (C_Chain := (C,, C_is_chain) : Chain_hsubtype P).
exists (P_CC C_Chain).
apply isantisymm_posetRelation. 2: { use progressive_property. }
refine (least_upper_bound_is_upper_bound (P_CC _) (_,,_)).
use C_f_closed.
use C_chain_closed.
intros [? ?]; assumption.
}
set (is_bottleneck := (fun x => ∀ y, C y ⇒ y ≤ x ⇒ (f y ≤ x) ∨ (y = x))
: hsubtype P).
assert (bottleneck_comparison : ∀ x, C x ⇒ is_bottleneck x
⇒ ∀ y, C y ⇒ (y ≤ x) ∨ (f x ≤ y)).
{ intros x C_x x_bottleneck. use C_induction.
- intros y [y_comp C_y]. split. 2: { use C_f_closed; assumption. }
apply (hconjtohdisj' y_comp).
2: { intros leq_fx_y. apply hdisj_in2.
eapply istrans_posetRelation; try eassumption.
use progressive_property. }
intros leq_y_x.
use (hdisj_monot' (x_bottleneck y _ _)); try assumption.
+ intro; assumption.
+ intro e_yx; destruct e_yx; apply isrefl_posetRelation.
- intros C' IH_C'. split. 2: { use C_chain_closed; intros; apply IH_C'. }
destruct (H_LEM (∃ y, C' y ∧ f x ≤ y)) as [C'_passes_fx | C'_notpasses_fx ].
+ apply hdisj_in2.
refine (factor_through_squash_hProp _ _ C'_passes_fx);
intros [y [C'_y leq_fx_y]].
eapply istrans_posetRelation; try eassumption.
use least_upper_bound_subtype_is_upper_bound; assumption.
+ apply hdisj_in1.
apply least_upper_bound_univ. intros [y C'_y].
eapply hdisjtoimpl. apply hdisj_comm, IH_C'.
intros leq_fx_y. apply C'_notpasses_fx.
apply hinhpr; exists y. split; assumption.
}
assert (all_C_bottleneck : forall x, C x ⇒ is_bottleneck x).
{ use C_induction.
- intros x [x_bottleneck C_x]. split. 2: { use C_f_closed; assumption. }
intros y C_y le_y_fx.
use (hconjtohdisj' (bottleneck_comparison x _ _ y _));
try assumption.
2: { intro. apply hdisj_in2, isantisymm_posetRelation; assumption. }
intro le_yx. apply hdisj_in1.
use (hconjtohdisj' (x_bottleneck y _ _)); try assumption.
+ intro. eapply istrans_posetRelation; try eassumption.
use progressive_property.
+ intros e_yx; destruct e_yx. apply isrefl_posetRelation.
- intros C' IH_C'. split. 2: { use C_chain_closed; intros; apply IH_C'. }
intros x C_x le_x_supC'.
destruct (H_LEM (∃ y, C' y ∧ f x ≤ y)) as [ C'_passes_fx | C'_notpasses_fx ].
{ apply hdisj_in1.
refine (factor_through_squash_hProp _ _ C'_passes_fx); intros [y [? ?]].
eapply istrans_posetRelation;
eauto using least_upper_bound_subtype_is_upper_bound.
}
apply hdisj_in2.
apply isantisymm_posetRelation; try assumption.
apply least_upper_bound_subtype_univ. intros y C'_y.
destruct (IH_C' (y,,C'_y)) as [y_bottleneck C_y].
use (hconjtohdisj' (bottleneck_comparison y _ _ x _)); try assumption.
2: { intro. eapply istrans_posetRelation; try eassumption.
use progressive_property. }
intro le_x_y. apply isrefl'_posetRelation, pathsinv0.
refine (hdisjtoimpl (y_bottleneck x C_x _) _); try assumption.
use (negexists_to_forallneg_restricted C'_notpasses_fx); assumption.
}
intros [x Cx] [y Cy]; simpl pr1carrier.
assert (comparison : x ≤ y ∨ f y ≤ x).
{ use bottleneck_comparison; try apply all_C_bottleneck; assumption. }
apply (hdisj_monot' comparison). { intro; assumption. }
intro. eapply istrans_posetRelation; try eassumption.
use progressive_property.
set (is_f_closed := (fun A => (∀ y, A y ⇒ A (f y)))
: hsubtype P -> hProp).
set (is_chain_closed
:= (fun A => (∀ C' : Chain_hsubtype P, (∏ y:C', A (pr1 y)) ⇒ A (P_CC C')))
: hsubtype P -> hProp).
set (C := (fun x =>
∀ A : hsubtype P, is_f_closed A ⇒ is_chain_closed A ⇒ A x)
: hsubtype P).
assert (C_f_closed : is_f_closed C).
{ intros x C_x A A_f_closed A_chain_closed.
use A_f_closed. use C_x; assumption. }
assert (C_chain_closed : is_chain_closed C).
{ intros x C_x A A_f_closed A_chain_closed.
use A_chain_closed. intro; use C_x; assumption. }
assert (C_induction : ∀ (A : hsubtype P),
is_f_closed (A ∩ C) ⇒ is_chain_closed (A ∩ C) ⇒ C ⊆ A).
{ intros A A_chain_closed A_f_closed x Cx.
apply (Cx (fun x => A x ∧ C x)); assumption. }
assert (C_is_chain : is_chain (pr1carrier C)).
2: {
set (C_Chain := (C,, C_is_chain) : Chain_hsubtype P).
exists (P_CC C_Chain).
apply isantisymm_posetRelation. 2: { use progressive_property. }
refine (least_upper_bound_is_upper_bound (P_CC _) (_,,_)).
use C_f_closed.
use C_chain_closed.
intros [? ?]; assumption.
}
set (is_bottleneck := (fun x => ∀ y, C y ⇒ y ≤ x ⇒ (f y ≤ x) ∨ (y = x))
: hsubtype P).
assert (bottleneck_comparison : ∀ x, C x ⇒ is_bottleneck x
⇒ ∀ y, C y ⇒ (y ≤ x) ∨ (f x ≤ y)).
{ intros x C_x x_bottleneck. use C_induction.
- intros y [y_comp C_y]. split. 2: { use C_f_closed; assumption. }
apply (hconjtohdisj' y_comp).
2: { intros leq_fx_y. apply hdisj_in2.
eapply istrans_posetRelation; try eassumption.
use progressive_property. }
intros leq_y_x.
use (hdisj_monot' (x_bottleneck y _ _)); try assumption.
+ intro; assumption.
+ intro e_yx; destruct e_yx; apply isrefl_posetRelation.
- intros C' IH_C'. split. 2: { use C_chain_closed; intros; apply IH_C'. }
destruct (H_LEM (∃ y, C' y ∧ f x ≤ y)) as [C'_passes_fx | C'_notpasses_fx ].
+ apply hdisj_in2.
refine (factor_through_squash_hProp _ _ C'_passes_fx);
intros [y [C'_y leq_fx_y]].
eapply istrans_posetRelation; try eassumption.
use least_upper_bound_subtype_is_upper_bound; assumption.
+ apply hdisj_in1.
apply least_upper_bound_univ. intros [y C'_y].
eapply hdisjtoimpl. apply hdisj_comm, IH_C'.
intros leq_fx_y. apply C'_notpasses_fx.
apply hinhpr; exists y. split; assumption.
}
assert (all_C_bottleneck : forall x, C x ⇒ is_bottleneck x).
{ use C_induction.
- intros x [x_bottleneck C_x]. split. 2: { use C_f_closed; assumption. }
intros y C_y le_y_fx.
use (hconjtohdisj' (bottleneck_comparison x _ _ y _));
try assumption.
2: { intro. apply hdisj_in2, isantisymm_posetRelation; assumption. }
intro le_yx. apply hdisj_in1.
use (hconjtohdisj' (x_bottleneck y _ _)); try assumption.
+ intro. eapply istrans_posetRelation; try eassumption.
use progressive_property.
+ intros e_yx; destruct e_yx. apply isrefl_posetRelation.
- intros C' IH_C'. split. 2: { use C_chain_closed; intros; apply IH_C'. }
intros x C_x le_x_supC'.
destruct (H_LEM (∃ y, C' y ∧ f x ≤ y)) as [ C'_passes_fx | C'_notpasses_fx ].
{ apply hdisj_in1.
refine (factor_through_squash_hProp _ _ C'_passes_fx); intros [y [? ?]].
eapply istrans_posetRelation;
eauto using least_upper_bound_subtype_is_upper_bound.
}
apply hdisj_in2.
apply isantisymm_posetRelation; try assumption.
apply least_upper_bound_subtype_univ. intros y C'_y.
destruct (IH_C' (y,,C'_y)) as [y_bottleneck C_y].
use (hconjtohdisj' (bottleneck_comparison y _ _ x _)); try assumption.
2: { intro. eapply istrans_posetRelation; try eassumption.
use progressive_property. }
intro le_x_y. apply isrefl'_posetRelation, pathsinv0.
refine (hdisjtoimpl (y_bottleneck x C_x _) _); try assumption.
use (negexists_to_forallneg_restricted C'_notpasses_fx); assumption.
}
intros [x Cx] [y Cy]; simpl pr1carrier.
assert (comparison : x ≤ y ∨ f y ≤ x).
{ use bottleneck_comparison; try apply all_C_bottleneck; assumption. }
apply (hdisj_monot' comparison). { intro; assumption. }
intro. eapply istrans_posetRelation; try eassumption.
use progressive_property.
“Pataraia’s Lemma”: on any DCPO, there is a maximal monotone+progressive endo-map.
This is the main lemma for Pataraia’s theorem, fixpoint_for_monotone_on_dcpo.
Lemma maximal_progressive_endomorphism_on_dcpo
{P : Poset} (P_DC : is_directed_complete P)
: greatest_suchthat (fun f : arrow_Poset P P
=> isaposetmorphism_hProp f ∧ isprogressive f).
Show proof.
{P : Poset} (P_DC : is_directed_complete P)
: greatest_suchthat (fun f : arrow_Poset P P
=> isaposetmorphism_hProp f ∧ isprogressive f).
Show proof.
set (mon_prog_maps := (fun f : arrow_Poset P P
=> isaposetmorphism_hProp f ∧ isprogressive f)
: hsubtype _).
cut (carrier (is_greatest_suchthat mon_prog_maps)). { intros f. exact (make_greatest_suchthat (pr1 f) (pr2 f)). }
cut (carrier (mon_prog_maps ∩ is_least_upper_bound_subtype mon_prog_maps)).
{ use subtype_inc.
intros ? [? ?]. apply greatest_if_contains_sup; assumption. }
cut (carrier (is_least_upper_bound_pointwise (@pr1carrier _ mon_prog_maps))).
{ use subtype_inc.
intros f f_pw_lub; split; [ split | ].
- eapply isaposetmorphism_pointwise_lub; try eassumption.
intros [g [g_mon g_prog]]; exact g_mon.
- eapply progressive_pointwise_lub; try eassumption.
{ intros [g [g_mon g_prog]]; exact g_prog. }
apply hinhpr. exists (idfun _); split.
+ apply isaposetmorphism_idfun.
+ apply isprogressive_idfun.
- apply is_least_upper_bound_if_pointwise; assumption.
}
use (foralltototal _ (fun _ y => is_least_upper_bound _ y)). intros x.
cut (least_upper_bound (fun g : mon_prog_maps => pr1 g x)).
{ intros p. exists p. apply least_upper_bound_property. }
apply isdirected_lub; try assumption.
split.
- apply hinhpr. exists (idfun _); split.
+ apply isaposetmorphism_idfun.
+ apply isprogressive_idfun.
- intros [f [f_mon f_prog]] [g [g_mon g_prog]].
apply hinhpr.
use tpair.
{ exists (f ∘ g); split.
+ apply isaposetmorphism_compose; assumption.
+ apply isprogressive_compose; assumption.
}
split; simpl.
+ use f_mon; use g_prog.
+ use f_prog.
=> isaposetmorphism_hProp f ∧ isprogressive f)
: hsubtype _).
cut (carrier (is_greatest_suchthat mon_prog_maps)). { intros f. exact (make_greatest_suchthat (pr1 f) (pr2 f)). }
cut (carrier (mon_prog_maps ∩ is_least_upper_bound_subtype mon_prog_maps)).
{ use subtype_inc.
intros ? [? ?]. apply greatest_if_contains_sup; assumption. }
cut (carrier (is_least_upper_bound_pointwise (@pr1carrier _ mon_prog_maps))).
{ use subtype_inc.
intros f f_pw_lub; split; [ split | ].
- eapply isaposetmorphism_pointwise_lub; try eassumption.
intros [g [g_mon g_prog]]; exact g_mon.
- eapply progressive_pointwise_lub; try eassumption.
{ intros [g [g_mon g_prog]]; exact g_prog. }
apply hinhpr. exists (idfun _); split.
+ apply isaposetmorphism_idfun.
+ apply isprogressive_idfun.
- apply is_least_upper_bound_if_pointwise; assumption.
}
use (foralltototal _ (fun _ y => is_least_upper_bound _ y)). intros x.
cut (least_upper_bound (fun g : mon_prog_maps => pr1 g x)).
{ intros p. exists p. apply least_upper_bound_property. }
apply isdirected_lub; try assumption.
split.
- apply hinhpr. exists (idfun _); split.
+ apply isaposetmorphism_idfun.
+ apply isprogressive_idfun.
- intros [f [f_mon f_prog]] [g [g_mon g_prog]].
apply hinhpr.
use tpair.
{ exists (f ∘ g); split.
+ apply isaposetmorphism_compose; assumption.
+ apply isprogressive_compose; assumption.
}
split; simpl.
+ use f_mon; use g_prog.
+ use f_prog.
A constructive fixed-point theorem, due to Pataraia.
This proof transmitted via Dacar and Bauer–Lumsdaine (where it is Thm 3.2).
Theorem fixpoint_for_monotone_on_dcpo
{P : Poset} (P_dir: is_directed_complete P)
(f : posetmorphism P P) (x : Postfixedpoint f)
: ∑ y : Fixedpoint f, x ≤ y.
Show proof.
End Bourbaki_Witt.
{P : Poset} (P_dir: is_directed_complete P)
(f : posetmorphism P P) (x : Postfixedpoint f)
: ∑ y : Fixedpoint f, x ≤ y.
Show proof.
revert x.
set (postfix_f := (fun x => x ≤ f x) : Subposet P).
assert (postfix_dc : is_directed_complete postfix_f).
{ intros [A A_dir].
use least_upper_bound_in_subposet.
{ use (isdirected_lub P_dir). assumption. }
apply least_upper_bound_univ. intros [[x x_postfix] x_A].
eapply istrans_posetRelation. { apply x_postfix. }
apply posetmorphism_property.
refine (least_upper_bound_is_upper_bound _ (_,,_)).
simple refine (value_in_image _ ((_,,_),,_)); assumption.
}
set (max_monprog_map := maximal_progressive_endomorphism_on_dcpo postfix_dc).
destruct max_monprog_map as [[max_map [max_is_mon max_is_prog]] max_is_max].
transparent assert (f_restr_postfix : (arrow_Poset postfix_f postfix_f)).
{ intros x. exists (f (pr1 x)).
apply posetmorphism_property, postfixedpoint_property.
}
assert (max_map_gives_fixedpoints : f_restr_postfix ∘ max_map ~ max_map).
{ intros x; apply isantisymm_posetRelation.
2: { apply postfixedpoint_property. }
revert x. refine (max_is_max (_,,_)); split.
- refine (@isaposetmorphism_compose _ _ _ max_map _ f_restr_postfix _).
{ assumption. }
intros ? ?; apply (posetmorphism_property f).
- refine (@isprogressive_compose _ f_restr_postfix max_map _ _).
2: { assumption. }
intro; apply postfixedpoint_property.
}
intros x. simple refine ((pr1 (max_map x),,_),,_); simpl.
- exact (maponpaths _ (max_map_gives_fixedpoints x)).
- use max_is_prog.
set (postfix_f := (fun x => x ≤ f x) : Subposet P).
assert (postfix_dc : is_directed_complete postfix_f).
{ intros [A A_dir].
use least_upper_bound_in_subposet.
{ use (isdirected_lub P_dir). assumption. }
apply least_upper_bound_univ. intros [[x x_postfix] x_A].
eapply istrans_posetRelation. { apply x_postfix. }
apply posetmorphism_property.
refine (least_upper_bound_is_upper_bound _ (_,,_)).
simple refine (value_in_image _ ((_,,_),,_)); assumption.
}
set (max_monprog_map := maximal_progressive_endomorphism_on_dcpo postfix_dc).
destruct max_monprog_map as [[max_map [max_is_mon max_is_prog]] max_is_max].
transparent assert (f_restr_postfix : (arrow_Poset postfix_f postfix_f)).
{ intros x. exists (f (pr1 x)).
apply posetmorphism_property, postfixedpoint_property.
}
assert (max_map_gives_fixedpoints : f_restr_postfix ∘ max_map ~ max_map).
{ intros x; apply isantisymm_posetRelation.
2: { apply postfixedpoint_property. }
revert x. refine (max_is_max (_,,_)); split.
- refine (@isaposetmorphism_compose _ _ _ max_map _ f_restr_postfix _).
{ assumption. }
intros ? ?; apply (posetmorphism_property f).
- refine (@isprogressive_compose _ f_restr_postfix max_map _ _).
2: { assumption. }
intro; apply postfixedpoint_property.
}
intros x. simple refine ((pr1 (max_map x),,_),,_); simpl.
- exact (maponpaths _ (max_map_gives_fixedpoints x)).
- use max_is_prog.
End Bourbaki_Witt.
Finally, we check that the promises listed in the overview have been fulfilled.
Note: we give these here to ensure that the overview always accurately reflects the theorems of the file. However, we make them local, since they should probably not be used outside this file — the original versions proved above are the versions intended for use.
Section Check_Overview.
Local Theorem fulfil_Tarski_fixpoint_theorem
: Tarski_fixpoint_theorem_statement (is_complete) (@isfixedpoint).
Show proof.
Local Theorem fulfil_fixpoint_for_monotone_on_dcpo
: fixpoint_for_monotone_on_dcpo_statement
(is_directed_complete) (@ispostfixedpoint) (@isfixedpoint).
Show proof.
Local Theorem fulfil_Tarski_fixpoint_theorem
: Tarski_fixpoint_theorem_statement (is_complete) (@isfixedpoint).
Show proof.
Local Theorem fulfil_fixpoint_for_monotone_on_dcpo
: fixpoint_for_monotone_on_dcpo_statement
(is_directed_complete) (@ispostfixedpoint) (@isfixedpoint).
Show proof.
Classical theorem, usually attrbi. Bourbaki (1949) and Witt (1951).
Local Theorem fulfil_Bourbaki_Witt_fixpoint_theorem
: Bourbaki_Witt_fixpoint_theorem_statement
(is_chain_complete) (@isprogressive) (@isfixedpoint).
Show proof.
End Check_Overview.
: Bourbaki_Witt_fixpoint_theorem_statement
(is_chain_complete) (@isprogressive) (@isfixedpoint).
Show proof.
End Check_Overview.