New linear algebra notation

Stream: maths

[Heather Macbeth]

I would like to introduce notation for (1) the span of a single vector, (2) the orthogonal complement. I was thinking of using 𝕜 ∙ v (that's \.) and K† (that's \dagger). So:

import analysis.normed_space.inner_product

open_locale real_inner_product_space
open submodule

notation 𝕜`∙`:1000 x := span 𝕜 (@singleton _ _ set.has_singleton x)
notation K`†`:1000 := submodule.orthogonal K

variables {E : Type*} [inner_product_space ℝ E]

example {v w : E} (hw : w ∈ (ℝ ∙ v)†) : ⟪w, v⟫ = 0 :=
inner_left_of_mem_orthogonal (mem_span_singleton_self v) hw

Any alternative suggestions, or objections, before I do this? One point is that obviously ⊥ (\bot) would have been ideal for the orthogonal complement notation, but it is already taken. Does anyone know of a visual twin?

[Heather Macbeth]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20span for brief previous discussion of the span notation (mostly focused on getting the notation to work).

[Adam Topaz]

is \perp the same character as \bot ?

[Heather Macbeth]

Yes, unfortunately.

[Heather Macbeth]

Actually, I just found a OCR site for unicode
https://shapecatcher.com/
which provided some visual twins for ⊥, namely ⟂ and ┴. Let me try to use one of them.

[Adam Topaz]

Oh this one is nice: Vᗮ

[Heather Macbeth]

Oh, that's perfect!

[Adam Topaz]

That's a really cool webpage btw. Similar to detexify (in case you don't know about that yet :) ) https://detexify.kirelabs.org/classify.html

[Heather Macbeth]

Yes, I found it by thinking to myself, "I need detexify for unicode!" :)

[Heather Macbeth]

So, at the moment, \perp in vscode gives the same result as \bot. Do I understand correctly that if
https://github.com/leanprover/vscode-lean/blob/master/translations.json
is edited to

"perp": "ᗮ",

then \perp would produce the new notation? Is this a kind of PR to vscode-lean that would be accepted?

[Bryan Gin-ge Chen]

Yes and yes.

[Adam Topaz]

Maybe ^perp?

[Heather Macbeth]

Adam Topaz said:

Maybe ^perp?

I would rather save the extra character, is your concern that some people might be used to writing \perp for \bot?

[Adam Topaz]

Yeah, but maybe everyone just uses \bot.

[Johan Commelin]

I would prefer \perp. People can get used to writing \bot quite easily, I think.

[Heather Macbeth]

#5536 and #5538

[Eric Wieser]

Shouldn't \bot be "up tack", \perp be "perpendicular", and \^perp be the character you use?

[Eric Wieser]

("" show unicode character names)

[Heather Macbeth]

Hmm ... but personally, I like it when the vscode input is the same as the LaTeX input. I find it easier to remember.

[Mario Carneiro]

latex doesn't use unicode anyway, it has its own character naming convention

[Heather Macbeth]

Ok, more precisely, it's nice when the vscode input matches the Latex character naming convention for the corresponding mathematical symbol.

[Eric Wieser]

Wait, but isn't what I suggest above closer to latex anyway? "\perp", isn't automatically superscript: $\perp$

[Patrick Massot]

I agree with Eric actually. I think \^perp makes more sense even from a LaTeX perspective.

[Patrick Massot]

Mario Carneiro said:

latex doesn't use unicode anyway, it has its own character naming convention

You meant: "Mario doesn't use unicode in LaTeX", right? Modern LaTeX has no trouble with unicode:

\documentclass{article}

\usepackage{unicode-math}

\begin{document}
  $Δ ⊥ Δ'$
\end{document}

[Mario Carneiro]

I mean that latex and unicode are independent approaches to having lots of squiggly things in text

[Mario Carneiro]

there are latex symbols that are not in unicode and vice versa

[Heather Macbeth]

I don't really mind, but let's decide before the vscode extension PR goes through.
https://github.com/leanprover/vscode-lean/pull/246

[Heather Macbeth]

/poll name for ᗮ
\perp
\^perp

[Eric Wieser]

^\perp would be cool, but it's not consistent with \^1 etc right now

[Heather Macbeth]

aagh, disregard the middle option with the typo! I can't figure out how to delete it.

[Eric Wieser]

ᗮ (canadian syllabics carrier p) at least semantically seems like a really odd choice of symbol

[Eric Wieser]

ᚆ (Ogham letter uath) suffers from the same flaw

[Adam Topaz]

V┴

[Adam Topaz]

Box drawings light up and horizontal

[Johan Commelin]

that doesn't seem too bad (-;

[Adam Topaz]

Mathjax renders $V^\perp$ as the following mathml:

<math xmlns="http://www.w3.org/1998/Math/MathML">
  <msup>
    <mi>V</mi>
    <mo>&#x22A5;</mo>
  </msup>
</math>

[Eric Wieser]

Is that $V^\perp$?

[Adam Topaz]

Yeah, V^\perp is the latex

[Eric Wieser]

Strikes me as a bug in mathjax

[Adam Topaz]

I think the <msup> tag puts the character in the superscript.

[Eric Wieser]

Right, but 22A5 is "up tack", and there's a dedicated unicode character for "perpendicular"

[Adam Topaz]

So, ⊥ is just the plain old \bot

[Adam Topaz]

I actually like V┴ a bit better than Vᗮ

[Eric Wieser]

I agree, 0x2534 Box drawings light up and horizontal seems like a good character to me

[Kevin Buzzard]

Adam Topaz said:

I actually like V┴ a bit better than Vᗮ

I might need my glasses to check whether that second one isn't just a $V^1$

[Eric Wieser]

VScode renders it for me as

[Eric Wieser]

image.png

[Adam Topaz]

That's reasonable imo

[Heather Macbeth]

Really? I like the small one, I think it looks more natural.

[Heather Macbeth]

https://github.com/leanprover-community/mathlib/blob/10f6c151e5abd7711c1cb06e720cc98f86234803/src/analysis/normed_space/inner_product.lean#L1715

[Heather Macbeth]

lemma submodule.inf_orthogonal (K₁ K₂ : submodule 𝕜 E) : K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ :=

[Mario Carneiro]

I think we already make it pretty hard to distinguish all our crazy unicode stuffs. Bigger is better

[Kevin Buzzard]

ctrl-shift-+ is usually a good replacement for when I've mislaid my glasses

[Eric Wieser]

Also what if people want to state theorems about canadian syllabics? /s

[Adam Topaz]

Here's what it looks like in my emacs:
Screenshot-from-2020-12-31-10-13-35.png

[Heather Macbeth]

\^perp is the winner. I've updated https://github.com/leanprover/vscode-lean/pull/246

[Mario Carneiro]

By the way, I voted for \^bot as well because both abbreviations can refer to the same symbol

[Heather Macbeth]

Ok, I added that too.

[Eric Wieser]

Eric Wieser said:

Shouldn't \bot be "up tack" (⊥, 0x22A5), \perp be "perpendicular" (⟂, 0x27C2), and \^perp be the character you use?

In #18705 I claim "perpendicular" (⟂, 0x27C2) to write U ⟂ V as a symmetric shorthand for Uᗮ ≤ V.