Subdirect irreducibility and simplicity of lattices

We prove that there exists a lattice that is subdirectly irreducible but not simple.

0 /
| 4 3 | | 2 \ / 1

def congruence {L : Type u_1} (l : Lattice L) (R : L → L → Prop) : Prop

R is a congruence of the lattice L if it is an equivalence relation that preserves ∨ and ∧.

Equations

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

theorem Fin.lcm.proof {n : ℕ} {a b : Fin n} (h : ¬(↑a).lcm ↑b < n) : 0 < n

theorem Fin.gcd.proof {n : ℕ} {a b : Fin n} : (↑a).gcd ↑b < n

def Fin.lcm {n : ℕ} (a b : Fin n) : Fin n

Fin.lcm on Fin n is 0 if Nat.lcm is not in Fin n.

Equations

• a.lcm b = if h : (↑a).lcm ↑b < n then ⟨(↑a).lcm ↑b, h⟩ else ⟨0, ⋯⟩

def Fin.gcd {n : ℕ} (a b : Fin n) : Fin n

The gcd on ℕ works without modification on Fin n.

Equations

• a.gcd b = ⟨(↑a).gcd ↑b, ⋯⟩

theorem D.sup_le (n : ℕ) (a b c : Fin n) (h₀ : (↑a).lcm ↑b ∣ ↑c) (g₀ : ↑c ≠ 0) : (↑a).lcm ↑b ≤ ↑c

noncomputable def D (n : ℕ) : Lattice (Fin n)

Fin n as a partial divisor lattice.

Equations

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

def SubdirectlyIrreducible {A : Type u_1} (l : Lattice A) : Prop

A lattice L is subdirectly irreducible if it contains two elements a, b that are identified by any nontrivial congruence.

(We also allow the trivial case |L| ≤ 1.)

Equations

• SubdirectlyIrreducible l = ((∀ (a b : A), a = b) ∨ ∃ (a : A) (b : A), a ≠ b ∧ ∀ (R : A → A → Prop), congruence l R → R ≠ Eq → R a b)

def Simple {A : Type u_1} (l : Lattice A) : Prop

A lattice is simple if it has no nontrivial congruences.

Equations

• Simple l = ∀ (R : A → A → Prop), congruence l R → R = Eq ∨ R = fun (x x_1 : A) => True

def principalEquiv {A : Type u_1} (x y : A) (hxy : x ≠ y) : IsEquiv A fun (a b : A) => a = b ∨ {a, b} = {x, y}

The equivalence relation that identifies two elements x ≠ y. (The assumption x ≠ y is not strictly speaking needed.)

Equations

• ⋯ = ⋯

theorem preserve_sup_of_indiscernible {A : Type u_1} (l : Lattice A) (x y : A) (hxy' : ∀ z ∉ Set.Icc x y, ∀ w₀ ∈ Set.Icc x y, ∀ w₁ ∈ Set.Icc x y, (w₀ ≤ z ↔ w₁ ≤ z) ∧ (z ≤ w₀ ↔ z ≤ w₁)) (x₀ x₁ y₀ y₁ : A) : (fun (a b : A) => a = b ∨ {a, b} ⊆ Set.Icc x y) x₀ x₁ → (fun (a b : A) => a = b ∨ {a, b} ⊆ Set.Icc x y) y₀ y₁ → (fun (a b : A) => a = b ∨ {a, b} ⊆ Set.Icc x y) (SemilatticeSup.sup x₀ y₀) (SemilatticeSup.sup x₁ y₁)

An interval [x,y] is indiscernible if its elements u agree on whether they are above or below a given element z ∉ [x,y]. The equivalence relation formed by collapsing such an interval preserves ∨.

theorem sdi_of_simple {A : Type u_1} (l : Lattice A) (h : Simple l) : SubdirectlyIrreducible l

Simple implies subdirectly irreducible. ((D 5) is an example of the failure of the converse.) M₃ is simple.

theorem N₅omega {n : ℕ} {u : Fin (n + 5)} {c₀ c₁ : ℕ} (hc₀ : ↑u = 2 * c₀) (hc₁ : 4 = ↑u * c₁) : u = 2 ∨ u = 4

theorem N₅helper {n : ℕ} : {u : Fin (n + 5) | 2 ∣ ↑u ∧ ↑u ∣ 4} = {2, 4}

theorem D₅_congr_sup_case_general {n : ℕ} {x₀ y₀ : Fin (n + 5)} (h : y₀ ∈ {2, 4}) (H : x₀ ∈ {2, 4}) : SemilatticeSup.sup x₀ y₀ ∈ {2, 4}

theorem D_zero_max {n : ℕ} (x : Fin (n + 1)) : SemilatticeSup.sup 0 x = 0

theorem D₅_congr_sup (x₀ x₁ y₀ y₁ : Fin 5) : (fun (a b : Fin 5) => a = b ∨ {a, b} ⊆ {x : Fin 5 | 2 ∣ ↑x ∧ ↑x ∣ 4}) x₀ x₁ → (fun (a b : Fin 5) => a = b ∨ {a, b} ⊆ {x : Fin 5 | 2 ∣ ↑x ∧ ↑x ∣ 4}) y₀ y₁ → (fun (a b : Fin 5) => a = b ∨ {a, b} ⊆ {x : Fin 5 | 2 ∣ ↑x ∧ ↑x ∣ 4}) (SemilatticeSup.sup x₀ y₀) (SemilatticeSup.sup x₁ y₁)

theorem D₅_congr_inf (x₀ x₁ y₀ y₁ : Fin 5) : (fun (a b : Fin 5) => a = b ∨ {a, b} ⊆ {x : Fin 5 | 2 ∣ ↑x ∧ ↑x ∣ 4}) x₀ x₁ → (fun (a b : Fin 5) => a = b ∨ {a, b} ⊆ {x : Fin 5 | 2 ∣ ↑x ∧ ↑x ∣ 4}) y₀ y₁ → (fun (a b : Fin 5) => a = b ∨ {a, b} ⊆ {x : Fin 5 | 2 ∣ ↑x ∧ ↑x ∣ 4}) (Lattice.inf x₀ y₀) (Lattice.inf x₁ y₁)

The principal equivalence relation with block {2,4} preserves ∧ in (D 5).

theorem N₅indiscernibleInterval (z : Fin 5) : z ∉ {u : Fin 5 | 2 ∣ ↑u ∧ ↑u ∣ 4} → ∀ w₀ ∈ {u : Fin 5 | 2 ∣ ↑u ∧ ↑u ∣ 4}, ∀ w₁ ∈ {u : Fin 5 | 2 ∣ ↑u ∧ ↑u ∣ 4}, (↑w₀ ∣ ↑z ↔ ↑w₁ ∣ ↑z) ∧ (↑z ∣ ↑w₀ ↔ ↑z ∣ ↑w₁)

The interval [2,4] in (D 5) is indiscernible.

theorem not_simple_D₅ : ¬Simple (D 5)

The lattice (D 5) is not simple.

theorem ofIcc {A : Type u_1} {l : Lattice A} {R : A → A → Prop} (hR₀ : congruence l R) {a b c d : A} (o₀ : a ≤ b) (o₁ : b ≤ c) (o₂ : c ≤ d) (h : R a d) : R b c

If R is a congruence of a lattice L then its blocks are convex: if a ≤ b ≤ c ≤ d and R(a,d) then R(b,c).

theorem of₃₀D₅ {R : Fin 5 → Fin 5 → Prop} (hR₀ : congruence (D 5) R) (H : R 3 0) : R 2 4

Any congruence of (D 5) with 3∼0 makes 2∼4.

theorem of₃₂D₅ {R : Fin 5 → Fin 5 → Prop} (hR₀ : congruence (D 5) R) (H : R 3 2) : R 2 4

Any congruence of (D 5) with 3∼2 makes 2∼4.

theorem of₃₄D₅ {R : Fin 5 → Fin 5 → Prop} (hR₀ : congruence (D 5) R) (H : R 3 4) : R 2 4

theorem of₃₁D₅ {R : Fin 5 → Fin 5 → Prop} (hR₀ : congruence (D 5) R) (H : R 3 1) : R 2 4

Any congruence of (D 5) with 3∼1 makes 2∼4.

theorem of₂₁D₅ {R : Fin 5 → Fin 5 → Prop} (hR₀ : congruence (D 5) R) (H : R 2 1) : R 2 4

Any congruence of (D 5) with 2∼1 makes 2∼4.

theorem of₄₀D₅ {R : Fin 5 → Fin 5 → Prop} (hR₀ : congruence (D 5) R) (H : R 4 0) : R 2 4

Any congruence of (D 5) with 4∼0 makes 2∼4.

theorem of₃D₅ (R : Fin 5 → Fin 5 → Prop) (hR₀ : congruence (D 5) R) (H : ∃ (i : Fin 5), i ≠ 3 ∧ R 3 i) : R 2 4

Any congruence of (D 5) with 3 equivalent to something else makes 2∼4.

theorem sdi_D₅ : SubdirectlyIrreducible (D 5)

The lattice (D 5) is subdirectly irreducible.

theorem exists_sdi_not_simple : ∃ (l : Lattice (Fin 5)), SubdirectlyIrreducible l ∧ ¬Simple l

There exists a lattice that is subdirectly irreducible but not simple, namely N₅.

def mysetoid {A : Type u_1} (F : Set A) : Setoid A

Equations

• mysetoid F = { r := fun (a b : A) => a = b ∨ {a, b} ⊆ F, iseqv := ⋯ }

@[reducible]

noncomputable def freese {A : Type u_1} (L : Lattice A) (F : Set A) (hF : ∀ x ∈ F, ∀ (y : A), x ≤ y → y ∈ F) (hm : ∀ x ∈ F, ∀ y ∈ F, Lattice.inf x y ∈ F) : Lattice (Quotient (mysetoid F))

Equations

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