Zulip Chat Archive

Stream: Is there code for X?

Topic: projectors


view this post on Zulip Yury G. Kudryashov (Apr 30 2020 at 23:05):

What of the following do we have?

  • predicate for f ∘ f = f;
  • Π (p q : subspace k E), p ⊓ q = ⊥ → p ⊔ q = ⊤ → (E →ₗ[k] p)?

view this post on Zulip Jalex Stark (Apr 30 2020 at 23:09):

Is that square the right character?
EDIT: oh i see that it's the inf character. sad that it doesn't display the same here as in VSCode.
EDIT: oh there's two of them, one for inf and one for bot. I guess whenever one encouners a zulip message with squares in it, one should copy out to VSCode to be able to read it

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 23:10):

We have

@[algebra] class is_idempotent (α : Type u) (op : α  α  α) : Prop :=
(idempotent :  a, op a a = a)

which you could apply with alpha=X->X and op = function.comp. For the second one, x=p and y=q presumably?

view this post on Zulip Jalex Stark (Apr 30 2020 at 23:18):

kevin what do you mean by x and y?

view this post on Zulip Yury G. Kudryashov (Apr 30 2020 at 23:21):

There was a typo. I fixed it after Kevin's comment.

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 23:23):

You can click on "edited X minutes ago" to view the edit history and see the now-fixed typos. As for the squares, this is presumably a font issue. They look like the lean sup and inf to me on a pc and they're rendering as junk right now on my phone

view this post on Zulip Yury G. Kudryashov (Apr 30 2020 at 23:23):

Here is a version without unicode: p (inf) q = (bot) -> p (sup) q = (top) -> (linear_map k E p)

view this post on Zulip Jalex Stark (Apr 30 2020 at 23:24):

and presumably you want that linear map to be the projection onto p?

view this post on Zulip Yury G. Kudryashov (Apr 30 2020 at 23:25):

Yes, and have ker = q.

view this post on Zulip Jalex Stark (Apr 30 2020 at 23:25):

the linear map character I wasn't able to investigate by bringing it into lean, but probably that's just because I don't have the right linear algebra importa

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 23:25):

We don't want to say that E= p oplus q because this is type theory, but I guess the projections plus the proof that they're one sided inverses with the right kernel is the correct substitute

view this post on Zulip Yury G. Kudryashov (Apr 30 2020 at 23:26):

Another way to express this is to define linear_equiv between E and p × q.

view this post on Zulip Jalex Stark (Apr 30 2020 at 23:27):

(and the glue between those two definitions seems easier than the content of either one)


Last updated: May 07 2021 at 21:10 UTC