The lattice of seminorms is not distributive

We provide an example of three seminorms over the ℝ-vector space ℝ×ℝ which don't satisfy the lattice distributivity property (p ⊔ q1) ⊓ (p ⊔ q2) ≤ p ⊔ (q1 ⊓ q2).

This proves the lattice Seminorm ℝ (ℝ × ℝ) is not distributive.

References

• https://en.wikipedia.org/wiki/Seminorm#Examples

@[simp]

theorem Counterexample.SeminormNotDistrib.p_toFun : ∀ (a : ℝ × ℝ), Counterexample.SeminormNotDistrib.p a = |a.1| ⊔ |a.2|

noncomputable def Counterexample.SeminormNotDistrib.p : Seminorm ℝ (ℝ × ℝ)

Equations

• Counterexample.SeminormNotDistrib.p = (normSeminorm ℝ ℝ).comp (LinearMap.fst ℝ ℝ ℝ) ⊔ (normSeminorm ℝ ℝ).comp (LinearMap.snd ℝ ℝ ℝ)

@[simp]

theorem Counterexample.SeminormNotDistrib.q1_toFun (x : ℝ × ℝ) : Counterexample.SeminormNotDistrib.q1 x = 4 • |x.1|

noncomputable def Counterexample.SeminormNotDistrib.q1 : Seminorm ℝ (ℝ × ℝ)

Equations

• Counterexample.SeminormNotDistrib.q1 = 4 • (normSeminorm ℝ ℝ).comp (LinearMap.fst ℝ ℝ ℝ)

@[simp]

theorem Counterexample.SeminormNotDistrib.q2_toFun (x : ℝ × ℝ) : Counterexample.SeminormNotDistrib.q2 x = 4 • |x.2|

noncomputable def Counterexample.SeminormNotDistrib.q2 : Seminorm ℝ (ℝ × ℝ)

Equations

• Counterexample.SeminormNotDistrib.q2 = 4 • (normSeminorm ℝ ℝ).comp (LinearMap.snd ℝ ℝ ℝ)

theorem Counterexample.SeminormNotDistrib.eq_one : (Counterexample.SeminormNotDistrib.p ⊔ Counterexample.SeminormNotDistrib.q1 ⊓ Counterexample.SeminormNotDistrib.q2) (1, 1) = 1

theorem Counterexample.SeminormNotDistrib.not_distrib : ¬(Counterexample.SeminormNotDistrib.p ⊔ Counterexample.SeminormNotDistrib.q1) ⊓ (Counterexample.SeminormNotDistrib.p ⊔ Counterexample.SeminormNotDistrib.q2) ≤ Counterexample.SeminormNotDistrib.p ⊔ Counterexample.SeminormNotDistrib.q1 ⊓ Counterexample.SeminormNotDistrib.q2

This is a counterexample to the distributivity of the lattice Seminorm ℝ (ℝ × ℝ).