Grace/Cumulus/Lattice/Ideal.g17

Open in Workbench Download source

Imports

Bounded · Set.WellOrder

Declarations

Source

1-- Ideals, filters, and prime ideals of a lattice2-- 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.Ideal8import Bounded9import Set.WellOrder1011-- An ideal is a nonempty lower set closed under joins; a filter is a12-- nonempty upper set closed under meets.13predicate IsLatticeIdeal (A r I : Set) :=14  IsLattice(A, r) ∧ (I ⊆ A) ∧ Nonempty(I) ∧15  (∀ x ∈ I, ∀ y ∈ I, join(A, r, x, y) ∈ I) ∧16  (∀ x ∈ I, ∀ y ∈ A, relates(r, y, x) → y ∈ I)1718predicate IsLatticeFilter (A r F : Set) :=19  IsLattice(A, r) ∧ (F ⊆ A) ∧ Nonempty(F) ∧20  (∀ x ∈ F, ∀ y ∈ F, meet(A, r, x, y) ∈ F) ∧21  (∀ x ∈ F, ∀ y ∈ A, relates(r, x, y) → y ∈ F)2223predicate IsLatticePrimeIdeal (A r I : Set) :=24  IsLatticeIdeal(A, r, I) ∧ I ≠ A ∧25  (∀ x ∈ A, ∀ y ∈ A, meet(A, r, x, y) ∈ I → x ∈ I ∨ y ∈ I)2627-- The upper set of a point, dual to the initial segment below it.28def upperSegment (A r a : Set) : Set := { x ∈ A | relates(r, a, x) }2930theorem upperSegment.subset (A r a : Set)31  shows upperSegment(A, r, a) ⊆ A32proof33  intros x hx34  have member := upperSegment.membership.forward with hx35  exact member.left3637-- Projections3839theorem IsLatticeIdeal.lattice (A r I : Set)40  requires h : IsLatticeIdeal(A, r, I)41  shows IsLattice(A, r)42proof43  simp [IsLatticeIdeal]4445theorem IsLatticeIdeal.subset (A r I : Set)46  requires h : IsLatticeIdeal(A, r, I)47  shows I ⊆ A48proof49  simp [IsLatticeIdeal]5051theorem IsLatticeIdeal.nonempty (A r I : Set)52  requires h : IsLatticeIdeal(A, r, I)53  shows Nonempty(I)54proof55  simp [IsLatticeIdeal]5657theorem IsLatticeIdeal.join_closed (A r I x y : Set)58  requires h : IsLatticeIdeal(A, r, I)59  requires hx : x ∈ I60  requires hy : y ∈ I61  shows join(A, r, x, y) ∈ I62proof63  rcases h with ⟨lattice, bounded, nonempty, joins, downward⟩64  exact joins with x, hx, y, hy6566theorem IsLatticeIdeal.downward (A r I x y : Set)67  requires h : IsLatticeIdeal(A, r, I)68  requires hx : x ∈ I69  requires hy : y ∈ A70  requires hyx : relates(r, y, x)71  shows y ∈ I72proof73  rcases h with ⟨lattice, bounded, nonempty, joins, downward⟩74  exact downward with x, hx, y, hy, hyx7576theorem IsLatticeFilter.lattice (A r F : Set)77  requires h : IsLatticeFilter(A, r, F)78  shows IsLattice(A, r)79proof80  simp [IsLatticeFilter]8182theorem IsLatticeFilter.subset (A r F : Set)83  requires h : IsLatticeFilter(A, r, F)84  shows F ⊆ A85proof86  simp [IsLatticeFilter]8788theorem IsLatticeFilter.nonempty (A r F : Set)89  requires h : IsLatticeFilter(A, r, F)90  shows Nonempty(F)91proof92  simp [IsLatticeFilter]9394theorem IsLatticeFilter.meet_closed (A r F x y : Set)95  requires h : IsLatticeFilter(A, r, F)96  requires hx : x ∈ F97  requires hy : y ∈ F98  shows meet(A, r, x, y) ∈ F99proof100  rcases h with ⟨lattice, bounded, nonempty, meets, upward⟩101  exact meets with x, hx, y, hy102103theorem IsLatticeFilter.upward (A r F x y : Set)104  requires h : IsLatticeFilter(A, r, F)105  requires hx : x ∈ F106  requires hy : y ∈ A107  requires hxy : relates(r, x, y)108  shows y ∈ F109proof110  rcases h with ⟨lattice, bounded, nonempty, meets, upward⟩111  exact upward with x, hx, y, hy, hxy112113theorem IsLatticePrimeIdeal.ideal (A r I : Set)114  requires h : IsLatticePrimeIdeal(A, r, I)115  shows IsLatticeIdeal(A, r, I)116proof117  simp [IsLatticePrimeIdeal]118119theorem IsLatticePrimeIdeal.proper (A r I : Set)120  requires h : IsLatticePrimeIdeal(A, r, I)121  shows I ≠ A122proof123  simp [IsLatticePrimeIdeal]124125theorem IsLatticePrimeIdeal.prime (A r I x y : Set)126  requires h : IsLatticePrimeIdeal(A, r, I)127  requires hx : x ∈ A128  requires hy : y ∈ A129  requires hxy : meet(A, r, x, y) ∈ I130  shows x ∈ I ∨ y ∈ I131proof132  rcases h with ⟨ideal, proper, prime⟩133  exact prime with x, hx, y, hy, hxy134135-- Closure properties136137theorem IsLatticeIdeal.meet_closed (A r I x y : Set)138  requires h : IsLatticeIdeal(A, r, I)139  requires hx : x ∈ I140  requires hy : y ∈ A141  shows meet(A, r, x, y) ∈ I142proof143  have lattice := IsLatticeIdeal.lattice with h144  have xA := IsLatticeIdeal.subset with h, x, hx145  have meetA := meet.member with lattice, xA, hy146  have below := meet.lower_left with lattice, xA, hy147  exact IsLatticeIdeal.downward with h, hx, meetA, below148149theorem IsLatticeFilter.join_closed (A r F x y : Set)150  requires h : IsLatticeFilter(A, r, F)151  requires hx : x ∈ F152  requires hy : y ∈ A153  shows join(A, r, x, y) ∈ F154proof155  have lattice := IsLatticeFilter.lattice with h156  have xA := IsLatticeFilter.subset with h, x, hx157  have joinA := join.member with lattice, xA, hy158  have above := join.upper_left with lattice, xA, hy159  exact IsLatticeFilter.upward with h, hx, joinA, above160161theorem IsLatticeIdeal.join_iff (A r I x y : Set)162  requires h : IsLatticeIdeal(A, r, I)163  requires hx : x ∈ A164  requires hy : y ∈ A165  shows join(A, r, x, y) ∈ I ↔ x ∈ I ∧ y ∈ I166proof167  have lattice := IsLatticeIdeal.lattice with h168  constructor169  . intro joined170    constructor171    . exact IsLatticeIdeal.downward with h, joined, hx,172        (join.upper_left with lattice, hx, hy)173    . exact IsLatticeIdeal.downward with h, joined, hy,174        (join.upper_right with lattice, hx, hy)175  . intro both176    exact IsLatticeIdeal.join_closed with h, both.left, both.right177178theorem IsLatticeFilter.meet_iff (A r F x y : Set)179  requires h : IsLatticeFilter(A, r, F)180  requires hx : x ∈ A181  requires hy : y ∈ A182  shows meet(A, r, x, y) ∈ F ↔ x ∈ F ∧ y ∈ F183proof184  have lattice := IsLatticeFilter.lattice with h185  constructor186  . intro met187    constructor188    . exact IsLatticeFilter.upward with h, met, hx,189        (meet.lower_left with lattice, hx, hy)190    . exact IsLatticeFilter.upward with h, met, hy,191        (meet.lower_right with lattice, hx, hy)192  . intro both193    exact IsLatticeFilter.meet_closed with h, both.left, both.right194195theorem IsLatticeIdeal.bottom (A r bot top I : Set)196  requires bounded : IsBoundedLattice(A, r, bot, top)197  requires h : IsLatticeIdeal(A, r, I)198  shows bot ∈ I199proof200  obtain ⟨x, hx⟩ := IsLatticeIdeal.nonempty with h201  have xA := IsLatticeIdeal.subset with h, x, hx202  have botA := IsBoundedLattice.bottom_member with bounded203  exact IsLatticeIdeal.downward with h, hx, botA,204      (IsBoundedLattice.bottom_le with bounded, xA)205206theorem IsLatticeFilter.top (A r bot top F : Set)207  requires bounded : IsBoundedLattice(A, r, bot, top)208  requires h : IsLatticeFilter(A, r, F)209  shows top ∈ F210proof211  obtain ⟨x, hx⟩ := IsLatticeFilter.nonempty with h212  have xA := IsLatticeFilter.subset with h, x, hx213  have topA := IsBoundedLattice.top_member with bounded214  exact IsLatticeFilter.upward with h, hx, topA,215      (IsBoundedLattice.le_top with bounded, xA)216217-- Examples: the whole lattice, principal ideals and filters, intersections218219theorem IsLatticeIdeal.whole (A r : Set)220  requires lattice : IsLattice(A, r)221  requires nonempty : Nonempty(A)222  shows IsLatticeIdeal(A, r, A)223proof224  refine ⟨lattice, Subset.reflexive at A, nonempty, ?_, ?_⟩225  . intros x hx y hy226    exact join.member with lattice, hx, hy227  . intros x hx y hy hyx228    exact hy229230theorem IsLatticeFilter.whole (A r : Set)231  requires lattice : IsLattice(A, r)232  requires nonempty : Nonempty(A)233  shows IsLatticeFilter(A, r, A)234proof235  refine ⟨lattice, Subset.reflexive at A, nonempty, ?_, ?_⟩236  . intros x hx y hy237    exact meet.member with lattice, hx, hy238  . intros x hx y hy hxy239    exact hy240241theorem IsLatticeIdeal.principal (A r a : Set)242  requires lattice : IsLattice(A, r)243  requires ha : a ∈ A244  shows IsLatticeIdeal(A, r, segment(A, r, a))245proof246  have reflexive := IsLattice.reflexive with lattice247  have transitive := IsLattice.transitive with lattice248  have self : a ∈ segment(A, r, a) :=249    segment.membership.backward with ⟨ha, (reflexive with a, ha)⟩250  have nonempty : Nonempty(segment(A, r, a)) := ⟨a, self⟩251  refine ⟨lattice, (segment.subset at A, r, a), nonempty, ?_, ?_⟩252  . intros x hx y hy253    have xS := segment.membership.forward with hx254    have yS := segment.membership.forward with hy255    have joinA := join.member with lattice, xS.left, yS.left256    have below := join.least with lattice, xS.left, yS.left, ha, xS.right,257        yS.right258    exact segment.membership.backward with ⟨joinA, below⟩259  . intros x hx y hy hyx260    have xS := segment.membership.forward with hx261    have below := transitive with y, hy, x, xS.left, a, ha, hyx, xS.right262    exact segment.membership.backward with ⟨hy, below⟩263264theorem IsLatticeFilter.principal (A r a : Set)265  requires lattice : IsLattice(A, r)266  requires ha : a ∈ A267  shows IsLatticeFilter(A, r, upperSegment(A, r, a))268proof269  have reflexive := IsLattice.reflexive with lattice270  have transitive := IsLattice.transitive with lattice271  have self : a ∈ upperSegment(A, r, a) :=272    upperSegment.membership.backward with ⟨ha, (reflexive with a, ha)⟩273  have nonempty : Nonempty(upperSegment(A, r, a)) := ⟨a, self⟩274  refine ⟨lattice, (upperSegment.subset at A, r, a), nonempty, ?_, ?_⟩275  . intros x hx y hy276    have xS := upperSegment.membership.forward with hx277    have yS := upperSegment.membership.forward with hy278    have meetA := meet.member with lattice, xS.left, yS.left279    have above := meet.greatest with lattice, xS.left, yS.left, ha, xS.right,280        yS.right281    exact upperSegment.membership.backward with ⟨meetA, above⟩282  . intros x hx y hy hxy283    have xS := upperSegment.membership.forward with hx284    have above := transitive with a, ha, x, xS.left, y, hy, xS.right, hxy285    exact upperSegment.membership.backward with ⟨hy, above⟩286287theorem IsLatticeIdeal.intersection (A r I J : Set)288  requires hI : IsLatticeIdeal(A, r, I)289  requires hJ : IsLatticeIdeal(A, r, J)290  shows IsLatticeIdeal(A, r, I ∩ J)291proof292  have lattice := IsLatticeIdeal.lattice with hI293  have bounded := Subset.transitive with (intersection.subset_left at I, J),294      (IsLatticeIdeal.subset with hI)295  have nonempty : Nonempty(I ∩ J)296    obtain ⟨x, hx⟩ := IsLatticeIdeal.nonempty with hI297    obtain ⟨y, hy⟩ := IsLatticeIdeal.nonempty with hJ298    have xA := IsLatticeIdeal.subset with hI, x, hx299    have yA := IsLatticeIdeal.subset with hJ, y, hy300    have inI := IsLatticeIdeal.meet_closed with hI, hx, yA301    have swap := meet.commutative with lattice, xA, yA302    have inJ := IsLatticeIdeal.meet_closed with hJ, hy, xA303    rw ← swap at inJ304    refine ⟨meet(A, r, x, y), (intersection.membership.backward with ⟨inI,305        inJ⟩)⟩306  refine ⟨lattice, bounded, nonempty, ?_, ?_⟩307  . intros x hx y hy308    have xBoth := intersection.membership.forward with hx309    have yBoth := intersection.membership.forward with hy310    apply intersection.membership.backward311    constructor312    . exact IsLatticeIdeal.join_closed with hI, xBoth.left, yBoth.left313    . exact IsLatticeIdeal.join_closed with hJ, xBoth.right, yBoth.right314  . intros x hx y hy hyx315    have xBoth := intersection.membership.forward with hx316    apply intersection.membership.backward317    constructor318    . exact IsLatticeIdeal.downward with hI, xBoth.left, hy, hyx319    . exact IsLatticeIdeal.downward with hJ, xBoth.right, hy, hyx320321-- Duality: ideals of the converse order are filters.322323theorem IsLatticeIdeal.converse (A r I : Set)324  requires h : IsLatticeIdeal(A, r, I)325  shows IsLatticeFilter(A, converse(r, A, A), I)326proof327  have lattice := IsLatticeIdeal.lattice with h328  have bounded := IsLatticeIdeal.subset with h329  refine ⟨(IsLattice.converse with lattice), bounded,330      (IsLatticeIdeal.nonempty with h), ?_, ?_⟩331  . intros x hx y hy332    have swap := meet.converse with lattice, (bounded with x, hx),333        (bounded with y, hy)334    rw swap335    exact IsLatticeIdeal.join_closed with h, hx, hy336  . intros x hx y hy hxy337    have reversed := converse.reflects with hxy338    exact IsLatticeIdeal.downward with h, hx, hy, reversed339340theorem IsLatticeFilter.converse (A r F : Set)341  requires h : IsLatticeFilter(A, r, F)342  shows IsLatticeIdeal(A, converse(r, A, A), F)343proof344  have lattice := IsLatticeFilter.lattice with h345  have bounded := IsLatticeFilter.subset with h346  refine ⟨(IsLattice.converse with lattice), bounded,347      (IsLatticeFilter.nonempty with h), ?_, ?_⟩348  . intros x hx y hy349    have swap := join.converse with lattice, (bounded with x, hx),350        (bounded with y, hy)351    rw swap352    exact IsLatticeFilter.meet_closed with h, hx, hy353  . intros x hx y hy hyx354    have reversed := converse.reflects with hyx355    exact IsLatticeFilter.upward with h, hx, hy, reversed356