Grace/Cumulus/Lattice/Sublattice.g17

Open in Workbench Download source

Imports

LatticeHom · Set.WellOrder

Declarations

Source

1-- Sublattices and the restricted order2-- 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.Sublattice8import LatticeHom9import Set.WellOrder1011predicate IsSublattice (A r B : Set) :=12  IsLattice(A, r) ∧ (B ⊆ A) ∧13  (∀ x ∈ B, ∀ y ∈ B, join(A, r, x, y) ∈ B ∧ meet(A, r, x, y) ∈ B)1415theorem IsSublattice.lattice (A r B : Set)16  requires h : IsSublattice(A, r, B)17  shows IsLattice(A, r)18proof19  simp [IsSublattice]2021theorem IsSublattice.subset (A r B : Set)22  requires h : IsSublattice(A, r, B)23  shows B ⊆ A24proof25  simp [IsSublattice]2627theorem IsSublattice.join_closed (A r B x y : Set)28  requires h : IsSublattice(A, r, B)29  requires hx : x ∈ B30  requires hy : y ∈ B31  shows join(A, r, x, y) ∈ B32proof33  rcases h with ⟨lattice, bounded, closed⟩34  have both := closed with x, hx, y, hy35  exact both.left3637theorem IsSublattice.meet_closed (A r B x y : Set)38  requires h : IsSublattice(A, r, B)39  requires hx : x ∈ B40  requires hy : y ∈ B41  shows meet(A, r, x, y) ∈ B42proof43  rcases h with ⟨lattice, bounded, closed⟩44  have both := closed with x, hx, y, hy45  exact both.right4647theorem IsSublattice.whole (A r : Set)48  requires lattice : IsLattice(A, r)49  shows IsSublattice(A, r, A)50proof51  refine ⟨lattice, Subset.reflexive at A, ?_⟩52  intros x hx y hy53  refine ⟨(join.member with lattice, hx, hy), (meet.member with lattice, hx,54      hy)⟩5556theorem IsSublattice.intersection (A r B C : Set)57  requires hB : IsSublattice(A, r, B)58  requires hC : IsSublattice(A, r, C)59  shows IsSublattice(A, r, B ∩ C)60proof61  have lattice := IsSublattice.lattice with hB62  have bounded := Subset.transitive with (intersection.subset_left at B, C),63      (IsSublattice.subset with hB)64  refine ⟨lattice, bounded, ?_⟩65  intros x hx y hy66  have xBoth := intersection.membership.forward with hx67  have yBoth := intersection.membership.forward with hy68  constructor69  . apply intersection.membership.backward70    constructor71    . exact IsSublattice.join_closed with hB, xBoth.left, yBoth.left72    . exact IsSublattice.join_closed with hC, xBoth.right, yBoth.right73  . apply intersection.membership.backward74    constructor75    . exact IsSublattice.meet_closed with hB, xBoth.left, yBoth.left76    . exact IsSublattice.meet_closed with hC, xBoth.right, yBoth.right7778-- The restriction of a partial order to a subset7980theorem restrictOrder.partial (A r B : Set)81  requires order : IsPartialOrder(A, r)82  requires hB : B ⊆ A83  shows IsPartialOrder(B, restrictOrder(r, B))84proof85  have reflexive := IsPartialOrder.reflexive with order86  have transitive := IsPartialOrder.transitive with order87  have antisymmetric := IsPartialOrder.antisymmetric with order88  constructor89  . constructor90    . exact restrictOrder.relation at r, B91    . constructor92      . intros x hx93        apply restrictOrder.relates.backward94        refine ⟨(reflexive with x, (hB with x, hx)), hx, hx⟩95      . intros x hx y hy z hz xy yz96        have first := restrictOrder.relates.forward with xy97        have second := restrictOrder.relates.forward with yz98        apply restrictOrder.relates.backward99        refine ⟨(transitive with x, (hB with x, hx), y, (hB with y, hy), z,100            (hB with z, hz), first.left, second.left), hx, hz⟩101  . intros x hx y hy xy yx102    have first := restrictOrder.relates.forward with xy103    have second := restrictOrder.relates.forward with yx104    exact antisymmetric with x, (hB with x, hx), y, (hB with y, hy),105        first.left, second.left106107theorem IsSublattice.supremum (A r B x y : Set)108  requires h : IsSublattice(A, r, B)109  requires hx : x ∈ B110  requires hy : y ∈ B111  shows Supremum(B, restrictOrder(r, B), {x, y}, join(A, r, x, y))112proof113  have lattice := IsSublattice.lattice with h114  have bounded := IsSublattice.subset with h115  have xA := bounded with x, hx116  have yA := bounded with y, hy117  have joinB := IsSublattice.join_closed with h, hx, hy118  have left : relates(restrictOrder(r, B), x, join(A, r, x, y))119    apply restrictOrder.relates.backward120    refine ⟨(join.upper_left with lattice, xA, yA), hx, joinB⟩121  have right : relates(restrictOrder(r, B), y, join(A, r, x, y))122    apply restrictOrder.relates.backward123    refine ⟨(join.upper_right with lattice, xA, yA), hy, joinB⟩124  apply Supremum.of_pair with hx, hy, joinB, left, right125  intros b hb xb yb126  have xbR := restrictOrder.relates.forward with xb127  have ybR := restrictOrder.relates.forward with yb128  apply restrictOrder.relates.backward129  refine ⟨(join.least with lattice, xA, yA, (bounded with b, hb), xbR.left,130      ybR.left), joinB, hb⟩131132theorem IsSublattice.infimum (A r B x y : Set)133  requires h : IsSublattice(A, r, B)134  requires hx : x ∈ B135  requires hy : y ∈ B136  shows Infimum(B, restrictOrder(r, B), {x, y}, meet(A, r, x, y))137proof138  have lattice := IsSublattice.lattice with h139  have bounded := IsSublattice.subset with h140  have xA := bounded with x, hx141  have yA := bounded with y, hy142  have meetB := IsSublattice.meet_closed with h, hx, hy143  have left : relates(restrictOrder(r, B), meet(A, r, x, y), x)144    apply restrictOrder.relates.backward145    refine ⟨(meet.lower_left with lattice, xA, yA), meetB, hx⟩146  have right : relates(restrictOrder(r, B), meet(A, r, x, y), y)147    apply restrictOrder.relates.backward148    refine ⟨(meet.lower_right with lattice, xA, yA), meetB, hy⟩149  apply Infimum.of_pair with hx, hy, meetB, left, right150  intros b hb bx byBound151  have bxR := restrictOrder.relates.forward with bx152  have byR := restrictOrder.relates.forward with byBound153  apply restrictOrder.relates.backward154  refine ⟨(meet.greatest with lattice, xA, yA, (bounded with b, hb), bxR.left,155      byR.left), hb, meetB⟩156157theorem IsSublattice.restricted (A r B : Set)158  requires h : IsSublattice(A, r, B)159  shows IsLattice(B, restrictOrder(r, B))160proof161  have lattice := IsSublattice.lattice with h162  have order := restrictOrder.partial with (IsLattice.order with lattice),163      (IsSublattice.subset with h)164  apply IsLattice.of_pairs with order165  . intros x hx y hy166    refine ⟨join(A, r, x, y), (IsSublattice.supremum with h, hx, hy)⟩167  . intros x hx y hy168    refine ⟨meet(A, r, x, y), (IsSublattice.infimum with h, hx, hy)⟩169170theorem IsSublattice.join (A r B x y : Set)171  requires h : IsSublattice(A, r, B)172  requires hx : x ∈ B173  requires hy : y ∈ B174  shows join(B, restrictOrder(r, B), x, y) = join(A, r, x, y)175proof176  have restricted := IsSublattice.restricted with h177  symm178  exact join.of_supremum with restricted, hx, hy, (IsSublattice.supremum with h,179      hx, hy)180181theorem IsSublattice.meet (A r B x y : Set)182  requires h : IsSublattice(A, r, B)183  requires hx : x ∈ B184  requires hy : y ∈ B185  shows meet(B, restrictOrder(r, B), x, y) = meet(A, r, x, y)186proof187  have restricted := IsSublattice.restricted with h188  symm189  exact meet.of_infimum with restricted, hx, hy, (IsSublattice.infimum with h,190      hx, hy)191192-- The image of a lattice homomorphism is a sublattice of its target.193194theorem IsLatticeHom.image_sublattice (f A r B s : Set)195  requires h : IsLatticeHom(f, A, r, B, s)196  shows IsSublattice(B, s, functionImage(f, A, B))197proof198  have source := IsLatticeHom.source with h199  have target := IsLatticeHom.target with h200  refine ⟨target, (functionImage.subset at f, A, B), ?_⟩201  intros u hu v hv202  obtain ⟨uB, x, hx, rfl⟩ := functionImage.membership.forward with hu203  obtain ⟨vB, y, hy, rfl⟩ := functionImage.membership.forward with hv204  have joinA := join.member with source, hx, hy205  have meetA := meet.member with source, hx, hy206  have joinValue := IsLatticeHom.join with h, hx, hy207  have meetValue := IsLatticeHom.meet with h, hx, hy208  constructor209  . rw ← joinValue210    exact functionImage.membership.backward with211        ⟨(IsLatticeHom.apply_member with h, joinA), join(A, r, x, y), joinA, rfl⟩212  . rw ← meetValue213    exact functionImage.membership.backward with214        ⟨(IsLatticeHom.apply_member with h, meetA), meet(A, r, x, y), meetA, rfl⟩215