Grace/Cumulus/Lattice/LatticeHom.g17

Open in Workbench Download source

Imports

Monotone

Declarations

Source

1-- Lattice homomorphisms2-- 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.LatticeHom8import Monotone910predicate IsLatticeHom (f A r B s : Set) :=11  IsLattice(A, r) ∧ IsLattice(B, s) ∧ FunctionBetween(f, A, B) ∧12  (∀ x ∈ A, ∀ y ∈ A, f(join(A, r, x, y)) = join(B, s, f(x), f(y))) ∧13  (∀ x ∈ A, ∀ y ∈ A, f(meet(A, r, x, y)) = meet(B, s, f(x), f(y)))1415theorem IsLatticeHom.source (f A r B s : Set)16  requires h : IsLatticeHom(f, A, r, B, s)17  shows IsLattice(A, r)18proof19  simp [IsLatticeHom]2021theorem IsLatticeHom.target (f A r B s : Set)22  requires h : IsLatticeHom(f, A, r, B, s)23  shows IsLattice(B, s)24proof25  simp [IsLatticeHom]2627theorem IsLatticeHom.function (f A r B s : Set)28  requires h : IsLatticeHom(f, A, r, B, s)29  shows f : A → B30proof31  simp [IsLatticeHom]3233theorem IsLatticeHom.join (f A r B s x y : Set)34  requires h : IsLatticeHom(f, A, r, B, s)35  requires hx : x ∈ A36  requires hy : y ∈ A37  shows f(join(A, r, x, y)) = join(B, s, f(x), f(y))38proof39  rcases h with ⟨source, target, function, joins, meets⟩40  exact joins with x, hx, y, hy4142theorem IsLatticeHom.meet (f A r B s x y : Set)43  requires h : IsLatticeHom(f, A, r, B, s)44  requires hx : x ∈ A45  requires hy : y ∈ A46  shows f(meet(A, r, x, y)) = meet(B, s, f(x), f(y))47proof48  rcases h with ⟨source, target, function, joins, meets⟩49  exact meets with x, hx, y, hy5051theorem IsLatticeHom.apply_member (f A r B s x : Set)52  requires h : IsLatticeHom(f, A, r, B, s)53  requires hx : x ∈ A54  shows f(x) ∈ B55proof56  exact FunctionBetween.apply_closed with (IsLatticeHom.function with h), hx5758theorem IsLatticeHom.monotone (f A r B s : Set)59  requires h : IsLatticeHom(f, A, r, B, s)60  shows IsMonotoneMap(f, A, r, B, s)61proof62  have source := IsLatticeHom.source with h63  have target := IsLatticeHom.target with h64  constructor65  . exact IsLatticeHom.function with h66  . intros x hx y hy hxy67    have fxB := IsLatticeHom.apply_member with h, hx68    have fyB := IsLatticeHom.apply_member with h, hy69    have joined := join.of_le with source, hx, hy, hxy70    have preserved := IsLatticeHom.join with h, hx, hy71    rw joined at preserved72    symm at preserved73    exact join.eq_right_iff.backward with target, fxB, fyB, preserved7475theorem IsLatticeHom.identity (A r : Set)76  requires lattice : IsLattice(A, r)77  shows IsLatticeHom(identity(A), A, r, A, r)78proof79  refine ⟨lattice, lattice, identity.function at A, ?_, ?_⟩80  . intros x hx y hy81    have valueX := identity.apply with hx82    have valueY := identity.apply with hy83    have valueJoin := identity.apply with (join.member with lattice, hx, hy)84    rw [valueX, valueY, valueJoin]85    rfl86  . intros x hx y hy87    have valueX := identity.apply with hx88    have valueY := identity.apply with hy89    have valueMeet := identity.apply with (meet.member with lattice, hx, hy)90    rw [valueX, valueY, valueMeet]91    rfl9293theorem IsLatticeHom.compose (f g A r B s C t : Set)94  requires hf : IsLatticeHom(f, A, r, B, s)95  requires hg : IsLatticeHom(g, B, s, C, t)96  shows IsLatticeHom(compose(g, f, A, B, C), A, r, C, t)97proof98  have source := IsLatticeHom.source with hf99  have middle := IsLatticeHom.target with hf100  have target := IsLatticeHom.target with hg101  have fFunction := IsLatticeHom.function with hf102  have gFunction := IsLatticeHom.function with hg103  refine ⟨source, target, (compose.function with fFunction, gFunction), ?_, ?_⟩104  . intros x hx y hy105    have joinA := join.member with source, hx, hy106    have fxB := IsLatticeHom.apply_member with hf, hx107    have fyB := IsLatticeHom.apply_member with hf, hy108    have valueX := compose.apply with fFunction, gFunction, hx109    have valueY := compose.apply with fFunction, gFunction, hy110    have valueJoin := compose.apply with fFunction, gFunction, joinA111    have innerJoin := IsLatticeHom.join with hf, hx, hy112    have outerJoin := IsLatticeHom.join with hg, fxB, fyB113    rw [valueX, valueY, valueJoin, innerJoin]114    exact outerJoin115  . intros x hx y hy116    have meetA := meet.member with source, hx, hy117    have fxB := IsLatticeHom.apply_member with hf, hx118    have fyB := IsLatticeHom.apply_member with hf, hy119    have valueX := compose.apply with fFunction, gFunction, hx120    have valueY := compose.apply with fFunction, gFunction, hy121    have valueMeet := compose.apply with fFunction, gFunction, meetA122    have innerMeet := IsLatticeHom.meet with hf, hx, hy123    have outerMeet := IsLatticeHom.meet with hg, fxB, fyB124    rw [valueX, valueY, valueMeet, innerMeet]125    exact outerMeet126127-- An order isomorphism between lattices preserves joins and meets.128129theorem OrderIsomorphism.join (f A r B s x y : Set)130  requires h : OrderIsomorphism(f, A, r, B, s)131  requires source : IsLattice(A, r)132  requires target : IsLattice(B, s)133  requires hx : x ∈ A134  requires hy : y ∈ A135  shows f(join(A, r, x, y)) = join(B, s, f(x), f(y))136proof137  have embedding := OrderIsomorphism.embedding with h138  have monotone := OrderEmbedding.monotone with embedding139  have surjective := Bijective.surjective with140      (OrderIsomorphism.bijective with h)141  have joinA := join.member with source, hx, hy142  have fxB := IsMonotoneMap.apply_member with monotone, hx143  have fyB := IsMonotoneMap.apply_member with monotone, hy144  have fJ := IsMonotoneMap.apply_member with monotone, joinA145  have xJ := IsMonotoneMap.preserves with monotone, hx, joinA,146      (join.upper_left with source, hx, hy)147  have yJ := IsMonotoneMap.preserves with monotone, hy, joinA,148      (join.upper_right with source, hx, hy)149  have supremum : Supremum(B, s, {f(x), f(y)}, f(join(A, r, x, y)))150    apply Supremum.of_pair with fxB, fyB, fJ, xJ, yJ151    intros b hb xb yb152    rcases surjective with ⟨function, onto⟩153    obtain ⟨a, ha, mapped⟩ := onto with b, hb154    have value := FunctionBetween.apply_value with function, ha, mapped155    rw ← value at xb156    rw ← value at yb157    rw ← value158    have xa := OrderEmbedding.reflects with embedding, hx, ha, xb159    have ya := OrderEmbedding.reflects with embedding, hy, ha, yb160    have below := join.least with source, hx, hy, ha, xa, ya161    exact IsMonotoneMap.preserves with monotone, joinA, ha, below162  exact join.of_supremum with target, fxB, fyB, supremum163164theorem OrderIsomorphism.meet (f A r B s x y : Set)165  requires h : OrderIsomorphism(f, A, r, B, s)166  requires source : IsLattice(A, r)167  requires target : IsLattice(B, s)168  requires hx : x ∈ A169  requires hy : y ∈ A170  shows f(meet(A, r, x, y)) = meet(B, s, f(x), f(y))171proof172  have embedding := OrderIsomorphism.embedding with h173  have monotone := OrderEmbedding.monotone with embedding174  have surjective := Bijective.surjective with175      (OrderIsomorphism.bijective with h)176  have meetA := meet.member with source, hx, hy177  have fxB := IsMonotoneMap.apply_member with monotone, hx178  have fyB := IsMonotoneMap.apply_member with monotone, hy179  have fM := IsMonotoneMap.apply_member with monotone, meetA180  have mX := IsMonotoneMap.preserves with monotone, meetA, hx,181      (meet.lower_left with source, hx, hy)182  have mY := IsMonotoneMap.preserves with monotone, meetA, hy,183      (meet.lower_right with source, hx, hy)184  have infimum : Infimum(B, s, {f(x), f(y)}, f(meet(A, r, x, y)))185    apply Infimum.of_pair with fxB, fyB, fM, mX, mY186    intros b hb bx byBound187    rcases surjective with ⟨function, onto⟩188    obtain ⟨a, ha, mapped⟩ := onto with b, hb189    have value := FunctionBetween.apply_value with function, ha, mapped190    rw ← value at bx191    rw ← value at byBound192    rw ← value193    have ax := OrderEmbedding.reflects with embedding, ha, hx, bx194    have ay := OrderEmbedding.reflects with embedding, ha, hy, byBound195    have above := meet.greatest with source, hx, hy, ha, ax, ay196    exact IsMonotoneMap.preserves with monotone, ha, meetA, above197  exact meet.of_infimum with target, fxB, fyB, infimum198199theorem OrderIsomorphism.lattice_hom (f A r B s : Set)200  requires h : OrderIsomorphism(f, A, r, B, s)201  requires source : IsLattice(A, r)202  requires target : IsLattice(B, s)203  shows IsLatticeHom(f, A, r, B, s)204proof205  have function := Injective.function with206      (Bijective.injective with (OrderIsomorphism.bijective with h))207  refine ⟨source, target, function, ?_, ?_⟩208  . intros x hx y hy209    exact OrderIsomorphism.join with h, source, target, hx, hy210  . intros x hx y hy211    exact OrderIsomorphism.meet with h, source, target, hx, hy212