Zulip Chat Archive

Stream: maths

Topic: New linear algebra notation


view this post on Zulip Heather Macbeth (Dec 30 2020 at 16:00):

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?

view this post on Zulip Heather Macbeth (Dec 30 2020 at 16:01):

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).

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:02):

is \perp the same character as \bot ?

view this post on Zulip Heather Macbeth (Dec 30 2020 at 16:02):

Yes, unfortunately.

view this post on Zulip Heather Macbeth (Dec 30 2020 at 16:13):

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.

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:15):

Oh this one is nice: Vᗮ

view this post on Zulip Heather Macbeth (Dec 30 2020 at 16:17):

Oh, that's perfect!

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:18):

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

view this post on Zulip Heather Macbeth (Dec 30 2020 at 16:19):

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

view this post on Zulip Heather Macbeth (Dec 30 2020 at 16:24):

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?

view this post on Zulip Bryan Gin-ge Chen (Dec 30 2020 at 16:24):

Yes and yes.

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:25):

Maybe ^perp?

view this post on Zulip Heather Macbeth (Dec 30 2020 at 16:26):

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?

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:27):

Yeah, but maybe everyone just uses \bot.

view this post on Zulip Johan Commelin (Dec 30 2020 at 16:28):

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

view this post on Zulip Heather Macbeth (Dec 30 2020 at 23:06):

#5536 and #5538

view this post on Zulip Eric Wieser (Dec 30 2020 at 23:41):

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

view this post on Zulip Eric Wieser (Dec 30 2020 at 23:43):

("" show unicode character names)

view this post on Zulip Heather Macbeth (Dec 30 2020 at 23:46):

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

view this post on Zulip Mario Carneiro (Dec 30 2020 at 23:58):

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

view this post on Zulip Heather Macbeth (Dec 31 2020 at 00:25):

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

view this post on Zulip Eric Wieser (Dec 31 2020 at 08:39):

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

view this post on Zulip Patrick Massot (Dec 31 2020 at 09:22):

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

view this post on Zulip Patrick Massot (Dec 31 2020 at 09:24):

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}

view this post on Zulip Mario Carneiro (Dec 31 2020 at 09:29):

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

view this post on Zulip Mario Carneiro (Dec 31 2020 at 09:30):

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

view this post on Zulip Heather Macbeth (Dec 31 2020 at 16:53):

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

view this post on Zulip Heather Macbeth (Dec 31 2020 at 16:53):

/poll name for ᗮ
\perp
\^perp

view this post on Zulip Eric Wieser (Dec 31 2020 at 16:55):

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

view this post on Zulip Heather Macbeth (Dec 31 2020 at 16:55):

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

view this post on Zulip Eric Wieser (Dec 31 2020 at 16:56):

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

view this post on Zulip Eric Wieser (Dec 31 2020 at 17:00):

ᚆ (Ogham letter uath) suffers from the same flaw

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:01):

V┴

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:02):

Box drawings light up and horizontal

view this post on Zulip Johan Commelin (Dec 31 2020 at 17:03):

that doesn't seem too bad (-;

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:04):

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

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

view this post on Zulip Eric Wieser (Dec 31 2020 at 17:04):

Is that $V^\perp$?

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:04):

Yeah, V^\perp is the latex

view this post on Zulip Eric Wieser (Dec 31 2020 at 17:05):

Strikes me as a bug in mathjax

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:05):

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

view this post on Zulip Eric Wieser (Dec 31 2020 at 17:07):

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

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:07):

So, &#x22A5; is just the plain old \bot

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:08):

I actually like V┴ a bit better than Vᗮ

view this post on Zulip Eric Wieser (Dec 31 2020 at 17:09):

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

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:10):

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 V1V^1

view this post on Zulip Eric Wieser (Dec 31 2020 at 17:11):

VScode renders it for me as

view this post on Zulip Eric Wieser (Dec 31 2020 at 17:11):

image.png

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:12):

That's reasonable imo

view this post on Zulip Heather Macbeth (Dec 31 2020 at 17:12):

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

view this post on Zulip Heather Macbeth (Dec 31 2020 at 17:12):

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

view this post on Zulip Heather Macbeth (Dec 31 2020 at 17:12):

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

view this post on Zulip Mario Carneiro (Dec 31 2020 at 17:13):

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

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:13):

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

view this post on Zulip Eric Wieser (Dec 31 2020 at 17:14):

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

view this post on Zulip Adam Topaz (Dec 31 2020 at 17:15):

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

view this post on Zulip Heather Macbeth (Jan 01 2021 at 18:59):

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

view this post on Zulip Mario Carneiro (Jan 01 2021 at 19:00):

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

view this post on Zulip Heather Macbeth (Jan 01 2021 at 19:08):

Ok, I added that too.


Last updated: May 10 2021 at 07:15 UTC