Grace/Cumulus/Lattice/Ideals.g17

Open in Workbench Download source

Imports

Ideal · Sublattices

Declarations

Source

1-- Ideals, filters, and prime ideals of a bundled 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.Ideals8import Ideal9import Sublattices1011-- An ideal is a nonempty lower set closed under joins, a filter a nonempty12-- upper set closed under meets, and a prime ideal a proper ideal that13-- contains a factor of every meet it contains.14predicate LatticeIdeal (P I : Set) := IsLatticeIdeal(points(P), le(P), I)15predicate LatticeFilter (P F : Set) := IsLatticeFilter(points(P), le(P), F)16predicate LatticePrimeIdeal (P I : Set) := IsLatticePrimeIdeal(points(P), le(P), I)1718notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LatticeIdeal(P, I) for P.points19notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LatticeIdeal(P, I) for P.points20notation infix 50 "≤" => Le(P, _, _) via hypothesis LatticeIdeal(P, I) for P.points21notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LatticeFilter(P, F) for P.points22notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LatticeFilter(P, F) for P.points23notation infix 50 "≤" => Le(P, _, _) via hypothesis LatticeFilter(P, F) for P.points24notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LatticePrimeIdeal(P, I) for P.points25notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LatticePrimeIdeal(P, I) for P.points26notation infix 50 "≤" => Le(P, _, _) via hypothesis LatticePrimeIdeal(P, I) for P.points2728instance LatticeIdeal.unbundled (P I : Set)29  requires ideal : LatticeIdeal(P, I)30  shows IsLatticeIdeal(points(P), le(P), I)31proof32  simp [LatticeIdeal]3334instance LatticeFilter.unbundled (P F : Set)35  requires filter : LatticeFilter(P, F)36  shows IsLatticeFilter(points(P), le(P), F)37proof38  simp [LatticeFilter]3940instance LatticePrimeIdeal.unbundled (P I : Set)41  requires prime : LatticePrimeIdeal(P, I)42  shows IsLatticePrimeIdeal(points(P), le(P), I)43proof44  simp [LatticePrimeIdeal]4546theorem LatticeIdeal.mk (A r I : Set)47  requires ideal : IsLatticeIdeal(A, r, I)48  shows LatticeIdeal(Order.mk(A, r), I)49proof50  unfold LatticeIdeal51  rw [Order.mk.points, Order.mk.le]52  exact ideal5354theorem LatticeFilter.mk (A r F : Set)55  requires filter : IsLatticeFilter(A, r, F)56  shows LatticeFilter(Order.mk(A, r), F)57proof58  unfold LatticeFilter59  rw [Order.mk.points, Order.mk.le]60  exact filter6162theorem LatticePrimeIdeal.mk (A r I : Set)63  requires prime : IsLatticePrimeIdeal(A, r, I)64  shows LatticePrimeIdeal(Order.mk(A, r), I)65proof66  unfold LatticePrimeIdeal67  rw [Order.mk.points, Order.mk.le]68  exact prime6970instance LatticeIdeal.lattice_of (P I : Set)71  requires ideal : LatticeIdeal(P, I)72  shows Lattice(P)73proof74  unfold Join.Lattice75  exact IsLatticeIdeal.lattice with (LatticeIdeal.unbundled with ideal)7677instance LatticeFilter.lattice_of (P F : Set)78  requires filter : LatticeFilter(P, F)79  shows Lattice(P)80proof81  unfold Join.Lattice82  exact IsLatticeFilter.lattice with (LatticeFilter.unbundled with filter)8384instance LatticePrimeIdeal.ideal_of (P I : Set)85  requires prime : LatticePrimeIdeal(P, I)86  shows LatticeIdeal(P, I)87proof88  unfold LatticeIdeal89  exact IsLatticePrimeIdeal.ideal with (LatticePrimeIdeal.unbundled with prime)9091-- The principal lower and upper sets of a point.92def Iic (P a : Set) : Set := segment(points(P), le(P), a)93def Ici (P a : Set) : Set := upperSegment(points(P), le(P), a)9495theorem Iic.membership (P a x : Set)96  shows x ∈ Iic(P, a) ↔ (x ∈ points(P) ∧ relates(le(P), x, a))97proof98  simp [Iic, segment]99100theorem Ici.membership (P a x : Set)101  shows x ∈ Ici(P, a) ↔ (x ∈ points(P) ∧ relates(le(P), a, x))102proof103  simp [Ici, upperSegment]104105section IdealLaws106variable (P I : Set)107hypothesis ideal : LatticeIdeal(P, I)108109theorem LatticeIdeal.subset_points110  shows I ⊆ points(P)111proof112  exact IsLatticeIdeal.subset with (LatticeIdeal.unbundled with ideal)113114theorem LatticeIdeal.mem_points (a : Set)115  requires aIn : a ∈ I116  shows a ∈ points(P)117proof118  have subset := LatticeIdeal.subset_points with ideal119  exact subset with a, aIn120121theorem LatticeIdeal.nonempty_of122  shows Nonempty(I)123proof124  exact IsLatticeIdeal.nonempty with (LatticeIdeal.unbundled with ideal)125126instance LatticeIdeal.sup_mem (a b : Set)127  requires aIn : a ∈ I128  requires bIn : b ∈ I129  shows a ⊔ b ∈ I130proof131  have aCarrier := LatticeIdeal.mem_points with ideal, aIn132  have bCarrier := LatticeIdeal.mem_points with ideal, bIn133  rw sup.join134  exact IsLatticeIdeal.join_closed with (LatticeIdeal.unbundled with ideal), aIn,135      bIn136137theorem LatticeIdeal.mem_of_le (a : Set) (b ∈ points(P))138  requires aIn : a ∈ I139  requires hba : b ≤ a140  shows b ∈ I141proof142  exact IsLatticeIdeal.downward with (LatticeIdeal.unbundled with ideal), aIn,143      assumption, (Le.relates with hba)144145instance LatticeIdeal.inf_mem_left (a : Set) (b ∈ points(P))146  requires aIn : a ∈ I147  shows a ⊓ b ∈ I148proof149  have aCarrier := LatticeIdeal.mem_points with ideal, aIn150  rw inf.meet151  exact IsLatticeIdeal.meet_closed with (LatticeIdeal.unbundled with ideal), aIn,152      assumption153154theorem LatticeIdeal.sup_mem_iff (a b ∈ points(P))155  shows a ⊔ b ∈ I ↔ (a ∈ I ∧ b ∈ I)156proof157  rw sup.join158  exact IsLatticeIdeal.join_iff with (LatticeIdeal.unbundled with ideal),159      assumption, assumption160161end IdealLaws162163section IdealBounds164variable (P I : Set)165hypothesis bounded : BoundedLattice(P)166hypothesis ideal : LatticeIdeal(P, I)167168theorem LatticeIdeal.bot_mem169  shows bot(P) ∈ I170proof171  exact IsLatticeIdeal.bottom with (BoundedLattice.unbundled with bounded),172      (LatticeIdeal.unbundled with ideal)173174end IdealBounds175176section FilterLaws177variable (P F : Set)178hypothesis filter : LatticeFilter(P, F)179180theorem LatticeFilter.subset_points181  shows F ⊆ points(P)182proof183  exact IsLatticeFilter.subset with (LatticeFilter.unbundled with filter)184185theorem LatticeFilter.mem_points (a : Set)186  requires aIn : a ∈ F187  shows a ∈ points(P)188proof189  have subset := LatticeFilter.subset_points with filter190  exact subset with a, aIn191192theorem LatticeFilter.nonempty_of193  shows Nonempty(F)194proof195  exact IsLatticeFilter.nonempty with (LatticeFilter.unbundled with filter)196197instance LatticeFilter.inf_mem (a b : Set)198  requires aIn : a ∈ F199  requires bIn : b ∈ F200  shows a ⊓ b ∈ F201proof202  have aCarrier := LatticeFilter.mem_points with filter, aIn203  have bCarrier := LatticeFilter.mem_points with filter, bIn204  rw inf.meet205  exact IsLatticeFilter.meet_closed with (LatticeFilter.unbundled with filter),206      aIn, bIn207208theorem LatticeFilter.mem_of_le (a : Set) (b ∈ points(P))209  requires aIn : a ∈ F210  requires hab : a ≤ b211  shows b ∈ F212proof213  exact IsLatticeFilter.upward with (LatticeFilter.unbundled with filter), aIn,214      assumption, (Le.relates with hab)215216instance LatticeFilter.sup_mem_left (a : Set) (b ∈ points(P))217  requires aIn : a ∈ F218  shows a ⊔ b ∈ F219proof220  have aCarrier := LatticeFilter.mem_points with filter, aIn221  rw sup.join222  exact IsLatticeFilter.join_closed with (LatticeFilter.unbundled with filter),223      aIn, assumption224225theorem LatticeFilter.inf_mem_iff (a b ∈ points(P))226  shows a ⊓ b ∈ F ↔ (a ∈ F ∧ b ∈ F)227proof228  rw inf.meet229  exact IsLatticeFilter.meet_iff with (LatticeFilter.unbundled with filter),230      assumption, assumption231232end FilterLaws233234section FilterBounds235variable (P F : Set)236hypothesis bounded : BoundedLattice(P)237hypothesis filter : LatticeFilter(P, F)238239theorem LatticeFilter.top_mem240  shows top(P) ∈ F241proof242  exact IsLatticeFilter.top with (BoundedLattice.unbundled with bounded),243      (LatticeFilter.unbundled with filter)244245end FilterBounds246247section PrimeLaws248variable (P I : Set)249hypothesis prime : LatticePrimeIdeal(P, I)250251theorem LatticePrimeIdeal.ne_points252  shows I ≠ points(P)253proof254  exact IsLatticePrimeIdeal.proper with (LatticePrimeIdeal.unbundled with prime)255256theorem LatticePrimeIdeal.mem_or_mem (a b ∈ points(P))257  requires meetIn : a ⊓ b ∈ I258  shows a ∈ I ∨ b ∈ I259proof260  rw inf.meet at meetIn261  exact IsLatticePrimeIdeal.prime with (LatticePrimeIdeal.unbundled with prime),262      assumption,263      assumption, meetIn264265end PrimeLaws266267-- The whole points, principal ideals and filters, intersections, and268-- duality.269theorem LatticeIdeal.univ (P : Set)270  requires lattice : Lattice(P)271  requires nonempty : Nonempty(points(P))272  shows LatticeIdeal(P, points(P))273proof274  unfold LatticeIdeal275  exact IsLatticeIdeal.whole with (Lattice.unbundled with lattice), nonempty276277theorem LatticeFilter.univ (P : Set)278  requires lattice : Lattice(P)279  requires nonempty : Nonempty(points(P))280  shows LatticeFilter(P, points(P))281proof282  unfold LatticeFilter283  exact IsLatticeFilter.whole with (Lattice.unbundled with lattice), nonempty284285theorem IsLatticeIdeal.principal (P a : Set)286  requires lattice : Lattice(P)287  requires aIn : a ∈ points(P)288  shows LatticeIdeal(P, Iic(P, a))289proof290  unfold LatticeIdeal291  unfold Iic292  exact IsLatticeIdeal.principal with (Lattice.unbundled with lattice), aIn293294theorem IsLatticeFilter.principal (P a : Set)295  requires lattice : Lattice(P)296  requires aIn : a ∈ points(P)297  shows LatticeFilter(P, Ici(P, a))298proof299  unfold LatticeFilter300  unfold Ici301  exact IsLatticeFilter.principal with (Lattice.unbundled with lattice), aIn302303theorem LatticeIdeal.inter (P I J : Set)304  requires hI : LatticeIdeal(P, I)305  requires hJ : LatticeIdeal(P, J)306  shows LatticeIdeal(P, I ∩ J)307proof308  unfold LatticeIdeal309  exact IsLatticeIdeal.intersection with (LatticeIdeal.unbundled with hI),310      (LatticeIdeal.unbundled with hJ)311312theorem LatticeIdeal.dual (P I : Set)313  requires ideal : LatticeIdeal(P, I)314  shows LatticeFilter(dual(P), I)315proof316  unfold LatticeFilter317  rw [dual.points, dual.le]318  exact IsLatticeIdeal.converse with (LatticeIdeal.unbundled with ideal)319320theorem LatticeFilter.dual (P F : Set)321  requires filter : LatticeFilter(P, F)322  shows LatticeIdeal(dual(P), F)323proof324  unfold LatticeIdeal325  rw [dual.points, dual.le]326  exact IsLatticeFilter.converse with (LatticeFilter.unbundled with filter)327