Grace/Cumulus/Lattice/OrderHom.g17

Open in Workbench Download source

Imports

Monotone · CompleteLattice

Declarations

Source

1-- Monotone maps, Galois connections, and closure operators on bundled orders2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Lattice.OrderHom8import Monotone9import CompleteLattice1011-- Maps between bundled orders, as properties of the map and the two12-- ordered sets. A Galois connection is written with its lower adjoint13-- first: l : P → Q is left adjoint to u : Q → P.14predicate MonotoneMap (f P Q : Set) :=15  IsMonotoneMap(f, points(P), le(P), points(Q), le(Q))16predicate AntitoneMap (f P Q : Set) :=17  IsAntitoneMap(f, points(P), le(P), points(Q), le(Q))18predicate GaloisConnection (l u P Q : Set) :=19  IsGaloisConnection(l, points(P), le(P), u, points(Q), le(Q))20predicate ClosureOperator (c P : Set) := IsClosureOperator(c, points(P), le(P))21predicate OrderIso (f P Q : Set) :=22  OrderIsomorphism(f, points(P), le(P), points(Q), le(Q))2324-- A map hypothesis supplies the orders of both of its ordered sets; an25-- operand is placed by its membership in a points or as a value f(a).26notation infix 50 "≤" => Le(P, _, _) via hypothesis MonotoneMap(f, P, Q) for P.points27notation infix 50 "≤" => Le(Q, _, _) via hypothesis MonotoneMap(f, P, Q) for Q.points28notation infix 50 "≤" => Le(P, _, _) via hypothesis AntitoneMap(f, P, Q) for P.points29notation infix 50 "≤" => Le(Q, _, _) via hypothesis AntitoneMap(f, P, Q) for Q.points30notation infix 50 "≤" => Le(P, _, _) via hypothesis GaloisConnection(l, u, P, Q) for P.points31notation infix 50 "≤" => Le(Q, _, _) via hypothesis GaloisConnection(l, u, P, Q) for Q.points32notation infix 50 "≤" => Le(P, _, _) via hypothesis ClosureOperator(c, P) for P.points33notation infix 50 "≤" => Le(P, _, _) via hypothesis OrderIso(f, P, Q) for P.points34notation infix 50 "≤" => Le(Q, _, _) via hypothesis OrderIso(f, P, Q) for Q.points35notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis MonotoneMap(f, P, Q) for P.points36notation infixl 68 "⊔" => call2(sup(Q), _, _) via hypothesis MonotoneMap(f, P, Q) for Q.points37notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis MonotoneMap(f, P, Q) for P.points38notation infixl 69 "⊓" => call2(inf(Q), _, _) via hypothesis MonotoneMap(f, P, Q) for Q.points3940-- Bridges to the unbundled forms.41instance MonotoneMap.unbundled (f P Q : Set)42  requires monotone : MonotoneMap(f, P, Q)43  shows IsMonotoneMap(f, points(P), le(P), points(Q), le(Q))44proof45  simp [MonotoneMap]4647instance AntitoneMap.unbundled (f P Q : Set)48  requires antitone : AntitoneMap(f, P, Q)49  shows IsAntitoneMap(f, points(P), le(P), points(Q), le(Q))50proof51  simp [AntitoneMap]5253instance GaloisConnection.unbundled (l u P Q : Set)54  requires gc : GaloisConnection(l, u, P, Q)55  shows IsGaloisConnection(l, points(P), le(P), u, points(Q), le(Q))56proof57  simp [GaloisConnection]5859instance ClosureOperator.unbundled (c P : Set)60  requires closure : ClosureOperator(c, P)61  shows IsClosureOperator(c, points(P), le(P))62proof63  simp [ClosureOperator]6465instance OrderIso.unbundled (f P Q : Set)66  requires iso : OrderIso(f, P, Q)67  shows OrderIsomorphism(f, points(P), le(P), points(Q), le(Q))68proof69  simp [OrderIso]7071theorem MonotoneMap.mk (f A r B s : Set)72  requires monotone : IsMonotoneMap(f, A, r, B, s)73  shows MonotoneMap(f, Order.mk(A, r), Order.mk(B, s))74proof75  unfold MonotoneMap76  rw [Order.mk.points, Order.mk.le, Order.mk.points, Order.mk.le]77  exact monotone7879theorem AntitoneMap.mk (f A r B s : Set)80  requires antitone : IsAntitoneMap(f, A, r, B, s)81  shows AntitoneMap(f, Order.mk(A, r), Order.mk(B, s))82proof83  unfold AntitoneMap84  rw [Order.mk.points, Order.mk.le, Order.mk.points, Order.mk.le]85  exact antitone8687theorem GaloisConnection.mk (l A r u B s : Set)88  requires gc : IsGaloisConnection(l, A, r, u, B, s)89  shows GaloisConnection(l, u, Order.mk(A, r), Order.mk(B, s))90proof91  unfold GaloisConnection92  rw [Order.mk.points, Order.mk.le, Order.mk.points, Order.mk.le]93  exact gc9495theorem ClosureOperator.mk (c A r : Set)96  requires closure : IsClosureOperator(c, A, r)97  shows ClosureOperator(c, Order.mk(A, r))98proof99  unfold ClosureOperator100  rw [Order.mk.points, Order.mk.le]101  exact closure102103theorem OrderIso.mk (f A r B s : Set)104  requires iso : OrderIsomorphism(f, A, r, B, s)105  shows OrderIso(f, Order.mk(A, r), Order.mk(B, s))106proof107  unfold OrderIso108  rw [Order.mk.points, Order.mk.le, Order.mk.points, Order.mk.le]109  exact iso110111-- Monotone maps112113theorem IsMonotoneMap.function (f P Q : Set)114  requires monotone : MonotoneMap(f, P, Q)115  shows f : points(P) → points(Q)116proof117  exact IsMonotoneMap.function with (MonotoneMap.unbundled with monotone)118119instance MonotoneMap.apply_mem (f P Q : Set) (a ∈ points(P))120  requires monotone : MonotoneMap(f, P, Q)121  shows f(a) ∈ points(Q)122proof123  exact IsMonotoneMap.apply_member with (MonotoneMap.unbundled with monotone), *124125theorem IsAntitoneMap.function (f P Q : Set)126  requires antitone : AntitoneMap(f, P, Q)127  shows f : points(P) → points(Q)128proof129  exact IsAntitoneMap.function with (AntitoneMap.unbundled with antitone)130131section MonotoneLaws132variable (f P Q : Set)133hypothesis monotone : MonotoneMap(f, P, Q)134135theorem MonotoneMap.map_le (a b ∈ points(P))136  requires hab : a ≤ b137  shows f(a) ≤ f(b)138proof139  unfold Le140  exact IsMonotoneMap.preserves with (MonotoneMap.unbundled with monotone),141      (Le.relates with hab), *142143theorem MonotoneMap.dual144  shows MonotoneMap(f, dual(P), dual(Q))145proof146  unfold MonotoneMap147  rw [dual.points, dual.le, dual.points, dual.le]148  exact IsMonotoneMap.converse with (MonotoneMap.unbundled with monotone)149150end MonotoneLaws151152section AntitoneLaws153variable (f P Q : Set)154hypothesis antitone : AntitoneMap(f, P, Q)155156theorem AntitoneMap.map_le (a b ∈ points(P))157  requires hab : a ≤ b158  shows f(b) ≤ f(a)159proof160  unfold Le161  exact IsAntitoneMap.reverses with (AntitoneMap.unbundled with antitone),162      (Le.relates with hab), *163164theorem AntitoneMap.monotone_dual165  shows MonotoneMap(f, P, dual(Q))166proof167  unfold MonotoneMap168  rw [dual.points, dual.le]169  exact IsAntitoneMap.monotone_converse with (AntitoneMap.unbundled with antitone)170171end AntitoneLaws172173theorem MonotoneMap.id (P : Set)174  shows MonotoneMap(identity(points(P)), P, P)175proof176  unfold MonotoneMap177  exact IsMonotoneMap.identity at points(P), le(P)178179theorem MonotoneMap.comp (f g P Q R : Set)180  requires hf : MonotoneMap(f, P, Q)181  requires hg : MonotoneMap(g, Q, R)182  shows MonotoneMap(compose(g, f, points(P), points(Q), points(R)), P, R)183proof184  unfold MonotoneMap185  exact IsMonotoneMap.compose with (MonotoneMap.unbundled with hf),186      (MonotoneMap.unbundled with hg)187188instance OrderIso.monotone_of (f P Q : Set)189  requires iso : OrderIso(f, P, Q)190  shows MonotoneMap(f, P, Q)191proof192  unfold MonotoneMap193  exact OrderIsomorphism.monotone with (OrderIso.unbundled with iso)194195-- A monotone map between lattices sends joins above the join of the images196-- and meets below the meet of the images.197section MonotoneLattice198variable (f P Q : Set)199hypothesis monotone : MonotoneMap(f, P, Q)200hypothesis source : Lattice(P)201hypothesis target : Lattice(Q)202203theorem MonotoneMap.map_sup_le (a b ∈ points(P))204  shows f(a) ⊔ f(b) ≤ f(a ⊔ b)205proof206  have faIn : f(a) ∈ points(Q) := MonotoneMap.apply_mem with *207  have fbIn : f(b) ∈ points(Q) := MonotoneMap.apply_mem with *208  unfold Le209  rw [sup.join, sup.join]210  exact IsMonotoneMap.join_le at f, points(P), le(P), points(Q), le(Q), a, b211      with (MonotoneMap.unbundled with monotone), *212213theorem MonotoneMap.le_map_inf (a b ∈ points(P))214  shows f(a ⊓ b) ≤ f(a) ⊓ f(b)215proof216  have faIn : f(a) ∈ points(Q) := MonotoneMap.apply_mem with *217  have fbIn : f(b) ∈ points(Q) := MonotoneMap.apply_mem with *218  unfold Le219  rw [inf.meet, inf.meet]220  exact IsMonotoneMap.meet_ge at f, points(P), le(P), points(Q), le(Q), a, b221      with (MonotoneMap.unbundled with monotone), *222223end MonotoneLattice224225-- Galois connections226227theorem GaloisConnection.l_function (l u P Q : Set)228  requires gc : GaloisConnection(l, u, P, Q)229  shows l : points(P) → points(Q)230proof231  exact IsGaloisConnection.lower_function with (GaloisConnection.unbundled with gc)232233theorem GaloisConnection.u_function (l u P Q : Set)234  requires gc : GaloisConnection(l, u, P, Q)235  shows u : points(Q) → points(P)236proof237  exact IsGaloisConnection.upper_function with (GaloisConnection.unbundled with gc)238239instance GaloisConnection.l_apply_mem (l u P Q : Set) (a ∈ points(P))240  requires gc : GaloisConnection(l, u, P, Q)241  shows l(a) ∈ points(Q)242proof243  have function := GaloisConnection.l_function with gc244  exact FunctionBetween.apply_closed with function, *245246instance GaloisConnection.u_apply_mem (l u P Q : Set) (b ∈ points(Q))247  requires gc : GaloisConnection(l, u, P, Q)248  shows u(b) ∈ points(P)249proof250  have function := GaloisConnection.u_function with gc251  exact FunctionBetween.apply_closed with function, *252253section GaloisLaws254variable (l u P Q : Set)255hypothesis gc : GaloisConnection(l, u, P, Q)256hypothesis source : PartialOrder(P)257hypothesis target : PartialOrder(Q)258259theorem GaloisConnection.le_iff_le (a ∈ points(P)) (b ∈ points(Q))260  shows l(a) ≤ b ↔ a ≤ u(b)261proof262  have adjoint := IsGaloisConnection.adjunction263      with (GaloisConnection.unbundled with gc), *264  constructor265  . intro h266    exact Le.of_relates with (adjoint.forward with (Le.relates with h))267  . intro h268    exact Le.of_relates with (adjoint.backward with (Le.relates with h))269270theorem GaloisConnection.le_u_l (a ∈ points(P))271  shows a ≤ u(l(a))272proof273  unfold Le274  exact IsGaloisConnection.unit with (GaloisConnection.unbundled with gc),275      (PartialOrder.unbundled with target), *276277theorem GaloisConnection.l_u_le (b ∈ points(Q))278  shows l(u(b)) ≤ b279proof280  unfold Le281  exact IsGaloisConnection.counit with (GaloisConnection.unbundled with gc),282      (PartialOrder.unbundled with source), *283284theorem GaloisConnection.monotone_l285  shows MonotoneMap(l, P, Q)286proof287  unfold MonotoneMap288  exact IsGaloisConnection.lower_monotone with (GaloisConnection.unbundled with gc),289      (PartialOrder.unbundled with source), (PartialOrder.unbundled with target)290291theorem GaloisConnection.monotone_u292  shows MonotoneMap(u, Q, P)293proof294  unfold MonotoneMap295  exact IsGaloisConnection.upper_monotone with (GaloisConnection.unbundled with gc),296      (PartialOrder.unbundled with source), (PartialOrder.unbundled with target)297298theorem GaloisConnection.l_u_l_eq_l (a ∈ points(P))299  shows l(u(l(a))) = l(a)300proof301  exact IsGaloisConnection.lower_upper_lower with (GaloisConnection.unbundled with gc),302      (PartialOrder.unbundled with source),303      (PartialOrder.unbundled with target), *304305theorem GaloisConnection.u_l_u_eq_u (b ∈ points(Q))306  shows u(l(u(b))) = u(b)307proof308  exact IsGaloisConnection.upper_lower_upper with (GaloisConnection.unbundled with gc),309      (PartialOrder.unbundled with source),310      (PartialOrder.unbundled with target), *311312theorem GaloisConnection.l_isLUB (S s : Set)313  requires lub : IsLUB(P, S, s)314  shows IsLUB(Q, functionImage(l, S, points(Q)), l(s))315proof316  unfold IsLUB at lub317  unfold IsLUB318  exact IsGaloisConnection.lower_supremum with (GaloisConnection.unbundled with gc),319      (PartialOrder.unbundled with source),320      (PartialOrder.unbundled with target), lub321322theorem GaloisConnection.u_isGLB (T t : Set)323  requires glb : IsGLB(Q, T, t)324  shows IsGLB(P, functionImage(u, T, points(P)), u(t))325proof326  unfold IsGLB at glb327  unfold IsGLB328  exact IsGaloisConnection.upper_infimum with (GaloisConnection.unbundled with gc),329      (PartialOrder.unbundled with source),330      (PartialOrder.unbundled with target), glb331332theorem IsGaloisConnection.closure333  shows ClosureOperator(compose(u, l, points(P), points(Q), points(P)), P)334proof335  unfold ClosureOperator336  exact IsGaloisConnection.closure with (GaloisConnection.unbundled with gc),337      (PartialOrder.unbundled with source), (PartialOrder.unbundled with target)338339end GaloisLaws340341theorem GaloisConnection.id (P : Set)342  shows GaloisConnection(identity(points(P)), identity(points(P)), P, P)343proof344  unfold GaloisConnection345  exact IsGaloisConnection.identity at points(P), le(P)346347theorem GaloisConnection.comp (l u k v P Q R : Set)348  requires first : GaloisConnection(l, u, P, Q)349  requires second : GaloisConnection(k, v, Q, R)350  shows GaloisConnection(compose(k, l, points(P), points(Q), points(R)),351    compose(u, v, points(R), points(Q), points(P)), P, R)352proof353  unfold GaloisConnection354  exact IsGaloisConnection.compose with (GaloisConnection.unbundled with first),355      (GaloisConnection.unbundled with second)356357-- Closure operators358359theorem IsClosureOperator.function (c P : Set)360  requires closure : ClosureOperator(c, P)361  shows c : points(P) → points(P)362proof363  exact IsClosureOperator.function with (ClosureOperator.unbundled with closure)364365instance ClosureOperator.apply_mem (c P : Set) (a ∈ points(P))366  requires closure : ClosureOperator(c, P)367  shows c(a) ∈ points(P)368proof369  exact IsClosureOperator.apply_member with (ClosureOperator.unbundled with closure),370      *371372instance ClosureOperator.monotone_of (c P : Set)373  requires closure : ClosureOperator(c, P)374  shows MonotoneMap(c, P, P)375proof376  unfold MonotoneMap377  exact IsClosureOperator.monotone with (ClosureOperator.unbundled with closure)378379section ClosureLaws380variable (c P : Set)381hypothesis closure : ClosureOperator(c, P)382383theorem ClosureOperator.le_closure (a ∈ points(P))384  shows a ≤ c(a)385proof386  unfold Le387  exact IsClosureOperator.extensive with (ClosureOperator.unbundled with closure),388      *389390theorem ClosureOperator.closure_closure (a ∈ points(P))391  shows c(c(a)) = c(a)392proof393  exact IsClosureOperator.idempotent with (ClosureOperator.unbundled with closure),394      *395396theorem ClosureOperator.le_closure_iff (a b ∈ points(P))397  requires order : PartialOrder(P)398  shows a ≤ c(b) ↔ c(a) ≤ c(b)399proof400  have characterization := IsClosureOperator.le_iff at c, points(P), le(P), a, b401      with (ClosureOperator.unbundled with closure),402      (PartialOrder.unbundled with order), *403  constructor404  . intro h405    exact Le.of_relates with (characterization.forward with (Le.relates with h))406  . intro h407    exact Le.of_relates with (characterization.backward with (Le.relates with h))408409end ClosureLaws410411theorem ClosureOperator.id (P : Set)412  requires order : PartialOrder(P)413  shows ClosureOperator(identity(points(P)), P)414proof415  unfold ClosureOperator416  exact IsClosureOperator.identity with (PartialOrder.unbundled with order)417