Grace/Cumulus/Lattice/Hom.g17

Open in Workbench Download source

Imports

LatticeHom · FixedPoints

Declarations

Source

1-- Lattice homomorphisms between bundled lattices2-- 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.Hom8import LatticeHom9import FixedPoints1011-- A lattice homomorphism between bundled lattices preserves joins and12-- meets; the hypothesis supplies the orders and operations of both sides.13predicate LatticeHom (f P Q : Set) :=14  IsLatticeHom(f, points(P), le(P), points(Q), le(Q))1516notation infix 50 "≤" => Le(P, _, _) via hypothesis LatticeHom(f, P, Q) for P.points17notation infix 50 "≤" => Le(Q, _, _) via hypothesis LatticeHom(f, P, Q) for Q.points18notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LatticeHom(f, P, Q) for P.points19notation infixl 68 "⊔" => call2(sup(Q), _, _) via hypothesis LatticeHom(f, P, Q) for Q.points20notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LatticeHom(f, P, Q) for P.points21notation infixl 69 "⊓" => call2(inf(Q), _, _) via hypothesis LatticeHom(f, P, Q) for Q.points2223instance LatticeHom.unbundled (f P Q : Set)24  requires hom : LatticeHom(f, P, Q)25  shows IsLatticeHom(f, points(P), le(P), points(Q), le(Q))26proof27  simp [LatticeHom]2829theorem LatticeHom.mk (f A r B s : Set)30  requires hom : IsLatticeHom(f, A, r, B, s)31  shows LatticeHom(f, Order.mk(A, r), Order.mk(B, s))32proof33  unfold LatticeHom34  rw [Order.mk.points, Order.mk.le, Order.mk.points, Order.mk.le]35  exact hom3637instance LatticeHom.source_lattice (f P Q : Set)38  requires hom : LatticeHom(f, P, Q)39  shows Lattice(P)40proof41  unfold Join.Lattice42  exact IsLatticeHom.source with (LatticeHom.unbundled with hom)4344instance LatticeHom.target_lattice (f P Q : Set)45  requires hom : LatticeHom(f, P, Q)46  shows Lattice(Q)47proof48  unfold Join.Lattice49  exact IsLatticeHom.target with (LatticeHom.unbundled with hom)5051instance LatticeHom.monotone_of (f P Q : Set)52  requires hom : LatticeHom(f, P, Q)53  shows MonotoneMap(f, P, Q)54proof55  unfold OrderHom.MonotoneMap56  exact IsLatticeHom.monotone with (LatticeHom.unbundled with hom)5758theorem IsLatticeHom.function (f P Q : Set)59  requires hom : LatticeHom(f, P, Q)60  shows f : points(P) → points(Q)61proof62  exact IsLatticeHom.function with (LatticeHom.unbundled with hom)6364instance LatticeHom.apply_mem (f P Q : Set) (a ∈ points(P))65  requires hom : LatticeHom(f, P, Q)66  shows f(a) ∈ points(Q)67proof68  exact IsLatticeHom.apply_member with (LatticeHom.unbundled with hom), *6970section LatticeHomLaws71variable (f P Q : Set)72hypothesis hom : LatticeHom(f, P, Q)7374theorem map_sup (a b ∈ points(P))75  shows f(a ⊔ b) = f(a) ⊔ f(b)76proof77  have faIn : f(a) ∈ points(Q) := LatticeHom.apply_mem with *78  have fbIn : f(b) ∈ points(Q) := LatticeHom.apply_mem with *79  rw [sup.join, sup.join]80  exact IsLatticeHom.join with (LatticeHom.unbundled with hom), *8182theorem map_inf (a b ∈ points(P))83  shows f(a ⊓ b) = f(a) ⊓ f(b)84proof85  have faIn : f(a) ∈ points(Q) := LatticeHom.apply_mem with *86  have fbIn : f(b) ∈ points(Q) := LatticeHom.apply_mem with *87  rw [inf.meet, inf.meet]88  exact IsLatticeHom.meet with (LatticeHom.unbundled with hom), *8990theorem LatticeHom.map_le (a b ∈ points(P))91  requires hab : a ≤ b92  shows f(a) ≤ f(b)93proof94  have monotone : MonotoneMap(f, P, Q) := LatticeHom.monotone_of with hom95  exact MonotoneMap.map_le with *9697end LatticeHomLaws9899theorem LatticeHom.id (P : Set)100  requires lattice : Lattice(P)101  shows LatticeHom(identity(points(P)), P, P)102proof103  unfold LatticeHom104  exact IsLatticeHom.identity with (Lattice.unbundled with lattice)105106theorem LatticeHom.comp (f g P Q R : Set)107  requires hf : LatticeHom(f, P, Q)108  requires hg : LatticeHom(g, Q, R)109  shows LatticeHom(compose(g, f, points(P), points(Q), points(R)), P, R)110proof111  unfold LatticeHom112  exact IsLatticeHom.compose with (LatticeHom.unbundled with hf),113      (LatticeHom.unbundled with hg)114115-- An order isomorphism between lattices is a lattice homomorphism.116section OrderIsoLattice117variable (f P Q : Set)118hypothesis iso : OrderIso(f, P, Q)119hypothesis source : Lattice(P)120hypothesis target : Lattice(Q)121122theorem OrderIso.latticeHom123  shows LatticeHom(f, P, Q)124proof125  unfold LatticeHom126  exact OrderIsomorphism.lattice_hom with (OrderIso.unbundled with iso),127      (Lattice.unbundled with source), (Lattice.unbundled with target)128129end OrderIsoLattice130