The Boolean subalgebra generated by a finite family

Every element of the Boolean subalgebra generated by a finite family φ : ι → α is the join of the minterms of φ below it. Sending an element to the set of those minterms is therefore an order isomorphism from the subalgebra onto the powerset of the nonzero minterms, and the subalgebra has 2 ^ n elements, n being the number of nonzero minterms. Its atoms are the nonzero minterms, and two such subalgebras are isomorphic iff they have equally many atoms. Two families whose minterms vanish at the same polarity assignments generate isomorphic subalgebras, by an isomorphism matching the families.

Main definitions

• BooleanSubalgebra.orderIsoMapOfInjective: a Boolean subalgebra is order-isomorphic to its image along an injective homomorphism.
• BooleanSubalgebra.toSetOfMinterms φ: the order isomorphism from closure (Set.range φ) onto the powerset of the nonzero minterms of φ.
• BooleanSubalgebra.closureOrderIsoOfMintermEqBot: the order isomorphism of the closures of two families whose minterms vanish together, carrying each φ i to ψ i.

Main results

• BooleanSubalgebra.map_closure: a homomorphism carries the closure of a set onto the closure of its image.
• BooleanSubalgebra.minterm_le_or_le_compl: a minterm lies below each element of the closure or below its complement.
• BooleanSubalgebra.card_closure: the closure has 2 ^ n elements.
• BooleanSubalgebra.isAtom_iff_mem_minterms: its atoms are the nonzero minterms.
• BooleanSubalgebra.nonempty_orderIso_closure_iff: two closures are isomorphic iff the families have equally many nonzero minterms.

[UPSTREAM] candidates for Mathlib.Order.BooleanSubalgebra.

@[simp]

theorem BooleanSubalgebra.disjoint_coe {α : Type u_1} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : ↥L} : Disjoint ↑a ↑b ↔ Disjoint a b

@[simp]

theorem BooleanSubalgebra.codisjoint_coe {α : Type u_1} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : ↥L} : Codisjoint ↑a ↑b ↔ Codisjoint a b

theorem BooleanSubalgebra.map_closure {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (s : Set α) : map f (closure s) = closure (⇑f '' s)

noncomputable def BooleanSubalgebra.orderIsoMapOfInjective {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {f : BoundedLatticeHom α β} (L : BooleanSubalgebra α) (hf : Function.Injective ⇑f) : ↥L ≃o ↥(map f L)

A Boolean subalgebra is order-isomorphic to its image along an injective homomorphism.

Equations

• L.orderIsoMapOfInjective hf = { toEquiv := Equiv.Set.image (⇑f) (↑L) hf, map_rel_iff' := ⋯ }

theorem BooleanSubalgebra.minterm_mem_closure {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} (σ : ι → Bool) : minterm φ σ ∈ closure (Set.range φ)

theorem BooleanSubalgebra.minterm_le_or_le_compl {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} {ψ : α} (hψ : ψ ∈ closure (Set.range φ)) (σ : ι → Bool) : minterm φ σ ≤ ψ ∨ minterm φ σ ≤ ψᶜ

A minterm lies below each element of the closure or below its complement.

theorem BooleanSubalgebra.mem_closure_of_mem_minterms {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} [DecidableEq ι] [DecidableEq α] {a : α} (ha : a ∈ (Finpartition.minterms φ).parts) : a ∈ closure (Set.range φ)

theorem BooleanSubalgebra.le_or_disjoint_of_mem_minterms {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} [DecidableEq ι] [DecidableEq α] {ψ a : α} (hψ : ψ ∈ closure (Set.range φ)) (ha : a ∈ (Finpartition.minterms φ).parts) : a ≤ ψ ∨ Disjoint a ψ

theorem BooleanSubalgebra.le_iff_forall_mem_minterms {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} [DecidableEq ι] [DecidableEq α] {ψ₁ ψ₂ : α} (h₁ : ψ₁ ∈ closure (Set.range φ)) : ψ₁ ≤ ψ₂ ↔ ∀ a ∈ (Finpartition.minterms φ).parts, a ≤ ψ₁ → a ≤ ψ₂

An element of the closure lies below ψ₂ iff every nonzero minterm below it does, since it is the join of those minterms.

noncomputable def BooleanSubalgebra.toSetOfMinterms {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] (φ : ι → α) [DecidableEq ι] [DecidableEq α] : ↥(closure (Set.range φ)) ≃o Set ↥(Finpartition.minterms φ).parts

Sending an element of the closure to the set of nonzero minterms below it is an order isomorphism onto the powerset of the nonzero minterms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BooleanSubalgebra.mem_toSetOfMinterms {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} [DecidableEq ι] [DecidableEq α] {ψ : ↥(closure (Set.range φ))} {a : ↥(Finpartition.minterms φ).parts} : a ∈ (toSetOfMinterms φ) ψ ↔ ↑a ≤ ↑ψ

theorem BooleanSubalgebra.card_closure {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] (φ : ι → α) [DecidableEq ι] [DecidableEq α] : Nat.card ↥(closure (Set.range φ)) = 2 ^ (Finpartition.minterms φ).parts.card

The closure of a family with n nonzero minterms has 2 ^ n elements.

theorem BooleanSubalgebra.isAtom_iff_mem_minterms {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} [DecidableEq ι] [DecidableEq α] {ψ : ↥(closure (Set.range φ))} : IsAtom ψ ↔ ↑ψ ∈ (Finpartition.minterms φ).parts

The atoms of the closure are the nonzero minterms.

noncomputable def BooleanSubalgebra.closureOrderIsoOfMintermEqBot {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} [DecidableEq ι] [DecidableEq α] {β : Type u_3} [BooleanAlgebra β] [DecidableEq β] {ψ : ι → β} (h : ∀ (σ : ι → Bool), minterm φ σ = ⊥ ↔ minterm ψ σ = ⊥) : ↥(closure (Set.range φ)) ≃o ↥(closure (Set.range ψ))

Two families whose minterms vanish at the same polarity assignments have order-isomorphic closures, by the isomorphism matching the minterms at each polarity assignment.

Equations

• One or more equations did not get rendered due to their size.

theorem BooleanSubalgebra.closureOrderIsoOfMintermEqBot_apply {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} [DecidableEq ι] [DecidableEq α] {β : Type u_3} [BooleanAlgebra β] [DecidableEq β] {ψ : ι → β} (h : ∀ (σ : ι → Bool), minterm φ σ = ⊥ ↔ minterm ψ σ = ⊥) (i : ι) : (closureOrderIsoOfMintermEqBot h) ⟨φ i, ⋯⟩ = ⟨ψ i, ⋯⟩

The isomorphism carries each φ i to ψ i.

theorem BooleanSubalgebra.nonempty_orderIso_closure_iff {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] (φ : ι → α) [DecidableEq ι] [DecidableEq α] {ι' : Type u_3} {α' : Type u_4} [BooleanAlgebra α'] [Fintype ι'] [DecidableEq ι'] [DecidableEq α'] (ψ : ι' → α') : Nonempty (↥(closure (Set.range φ)) ≃o ↥(closure (Set.range ψ))) ↔ (Finpartition.minterms φ).parts.card = (Finpartition.minterms ψ).parts.card

The closures of two families are order-isomorphic iff the families have equally many nonzero minterms.