Topology question

Stream: maths

[Peter Nelson]

Is the following provable? I don't have any reasonable sense for what non-Hausdorff spaces look like.

import Mathlib

example {M : Type*} [CommMonoid M] [CompleteLattice M] [IsOrderedMonoid M]
    [TopologicalSpace M] [SupConvergenceClass M] [CanonicallyOrderedMul M] :
    T2Space M := sorry

[Peter Nelson]

For that matter, I also don't know if the following is provable:

example {M : Type*} [CommMonoid M] [CompleteLattice M] [IsOrderedMonoid M]
     [CanonicallyOrderedMul M] [TopologicalSpace M] [OrderTopology M] :
    SupConvergenceClass M := sorry

[Aaron Liu]

The first one is false

[Aaron Liu]

Take M := Bool with multiplication given by || and one given by false, with the order a < b ↔ a = false ∧ b = true, and whose topology is ⊤

[Yury G. Kudryashov]

docs#SupConvergenceClass provides a lower estimate on inst : TopologicalSpace M, thus you can take \top as topology on any nontrivial ordered monoid M and get a counterexample.

[Yury G. Kudryashov]

Semi-offtopic: @Aaron Liu fixed CoeTC.coe in this file in #24047. I'm fixing the other file using CoeTC.coe in #24051. It would be nice if someone fixes Coe.coe, see https://loogle.lean-lang.org/?q=Coe.coe too. I won't have time for this today and tomorrow.

[Yury G. Kudryashov]

see also https://loogle.lean-lang.org/?q=CoeFun.coe

[Yury G. Kudryashov]

(not sure if the category theory one is intentional)