Disjunction Normal Form for a generated boolean subalgebra

Stream: maths

[Yaël Dillies]

Context, which you can skip: In algebraic geometry, a constructible set in the prime spectrum of a ring R is an element of the boolean subalgebra of Set (PrimeSpectrum R) generated by open sets. I need an induction principle for constructible sets of the following form:

Let P be a predicate on Set (PrimeSpectrum R). If b is a topological basis for PrimeSpectrum R and a few side conditions are fulfilled, then P holds on all constructible sets if it is preserved under union and holds on sets of the form b i \ ⋃ j ∈ s, b j where s is a finite set.

[Yaël Dillies]

What you should definitely read: This induction principle feels a lot like Disjunction Normal Form from boolean formulas/circuits. So I thought I would try proving an induction principle based on the DNF. However, this seems hard without first defining boolean formulas/circuits.

[Yaël Dillies]

Here's my attempt so far:

import Mathlib.Order.BooleanSubalgebra
import Mathlib.Topology.Spectral.Hom

open Set TopologicalSpace

/-- An induction principle for closure membership, based on the disjunctive normal form. -/
@[elab_as_elim]
lemma BooleanSubalgebra.closure_dnf_induction {α : Type*} [BooleanAlgebra α] {s : Set α}
    {p : ∀ g ∈ closure s, Prop}
    (dnf : sorry)
    {x} (hx : x ∈ closure s) : p x hx :=
  sorry

/-- The actual induction principle I care about, motivated by the Zariski topology. -/
@[elab_as_elim]
lemma IsConstructible.induction_of_isTopologicalBasis {ι α : Type*} [TopologicalSpace α]
    [CompactSpace α]
    {P : ∀ s ∈ BooleanSubalgebra.closure
      {U : Set α | IsOpen U ∧ ∀ ⦃U⦄, IsCompact U → IsOpen U → IsCompact (s ∩ U)}, Prop}
    (b : ι → Set α) (basis : IsTopologicalBasis (range b))
    (compact_inter : ∀ i j, IsCompact (b i ∩ b j))
    (sdiff : ∀ i s (hs : Set.Finite s), P (b i \ ⋃ j ∈ s, b j) sorry) -- easy to prove
    (union : ∀ s hs t ht, P s hs → P t ht → P (s ∪ t) sorry) -- easy to prove
    (s : Set α) (hs : s ∈ BooleanSubalgebra.closure
      {U | IsOpen U ∧ ∀ ⦃s⦄, IsCompact U → IsOpen U → IsCompact (s ∩ U)}) : P s hs := by
  sorry

[Yaël Dillies]

1. Has anyone got code about boolean formulas/circuits? If so, code about the DNF/CNF?
2. Do people agree with my analysis of the situation?

[Mitchell Lee]

This is maybe close to what you're looking for: docs#supClosure_infClosure

[Mitchell Lee]

The existence of DNF is equivalent to the statement that the Boolean subalgebra closure of a set s is equal to the sup closure of the inf closure of the complement closure of s ∪ {0, 1}. I do not think this statement is in mathlib, but docs#supClosure_infClosure is at least only a few steps away.

[Mitchell Lee]

There is first-order logic in mathlib, but I am not sure if there is the propositional calculus (zeroth-order logic) with propositions as variables

[Antoine Chambert-Loir]

Just to point out that your definition of constructible is incorrect in general, you have to take the boolean algebra generated by quasicompact open sets (in a general scheme, that would be retrocompact).

[Antoine Chambert-Loir]

In the spectrum of a noetherian ring, any open set will be quasicompact, hence your definition is often correct.

[Yaël Dillies]

Is that not exactly what I have written in #20054, Antoine?

[Antoine Chambert-Loir]

Yes, but not above.

[Yaël Dillies]

Ah yeah sure :smile: I didn't want to scare the computer scientists away with big scary words like "retro-compact"

[Antoine Chambert-Loir]

For you, is compact the same as quasi-compact?

[Antoine Chambert-Loir]

But then you scared me.

[Yaël Dillies]

Mathematician's compact = algebraic geometer's quasi-compact, have I lived in a lie?

[Antoine Chambert-Loir]

I think in US/UK terminology, compact does not imply Hausdorff, and that's probably the same in mathlib, so probably you're OK.

[Antoine Chambert-Loir]

Indeed: docs#CompactSpace

[Antoine Chambert-Loir]

For your initial question: you need an induction lemma for the boolean subalgebra generated by a set of a boole algebra.

[Yaël Dillies]

Mitchell Lee said:

The existence of DNF is equivalent to the statement that the Boolean subalgebra closure of a set s is equal to the sup closure of the inf closure of the complement closure of s ∪ {0, 1}. I do not think this statement is in mathlib, but docs#supClosure_infClosure is at least only a few steps away.

Quite a mouthful, but I like it! Something like BooleanSubalgebra.closure s = supClosure (infClosure (s ∪ {a | aᶜ ∈ s} ∪ {⊥, ⊤}))

[Yaël Dillies]

Antoine Chambert-Loir said:

you need an induction lemma for the boolean subalgebra generated by a set of a boole algebra.

Is that not exactly what I stated in my initial messages? or is a "boole algebra" something I don't know?

[Antoine Chambert-Loir]

yes, i was just confused by your invocation of dnf.