More elegant construction of ZariskiLattice

[MatthiasHu]

Here is an idea for an improvement in ZariskiLattice.Base .

The current set-quotient construction begins by defining a preorder (without using this name) and deriving the equivalence relation _∼_ from that:

cubical/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda

Lines 72 to 83 in 1011201

	_≼_ : A → A → Type ℓ
	(_ , α) ≼ (_ , β) = ∀ i → α i ∈ √ ⟨ β ⟩
	private
	isRefl≼ : ∀ {a} → a ≼ a
	isRefl≼ i = ∈→∈√ _ _ (indInIdeal _ _ i)
	isTrans≼ : ∀ {a b c : A} → a ≼ b → b ≼ c → a ≼ c
	isTrans≼ a≼b b≼c i = (√FGIdealCharRImpl _ _ b≼c) _ (a≼b i)
	_∼_ : A → A → Type ℓ -- \sim
	α ∼ β = (α ≼ β) × (β ≼ α)

So the set-quotient is actually an instance of a general (not formalized yet, I think) preorder-to-poset construction. I propose to actually implement it as such and then to use the resulting poset structure to define the lattice structure more easily.

Advantages:

• Because meets and joins in a poset are unique, we only need to show mere existence and don't need to prove the well-definedness of the _∨z_ and _∧z_ operations.
• We don't need to prove any of the monoid axioms (assoc, comm, L/Rid) on _∨z_ and _∧z_ by hand, only the distributive law remains.

Prerequisites:

• the preorder-to-poset construction (perhaps in Order.Preorder.Properties)
• the poset-plus-finite-meets/joins-to-lattice construction

[MatthiasHu]

@mzeuner What do you think?

[mzeuner]

Sorry for the late reply. I guess there is a general question about whether we want a (bounded) distributive lattice to be a poset with induced joins and meets or an algebraic structure with an induced order. I went for the latter when setting everything up, but I'm not sure anymore that that was the right choice. So I'm all for trying the other approach.

[anshwad10]

Cubical.Algebra.LindenbaumTarski could also use this improvement: It starts with defining a preorder Γ ⊢_⇒_, and then takes the quotient by its symmetric kernel to get a poset (it also subsequently proves that it is a lattice).