Stream: Is there code for X?
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)?
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
Kevin Buzzard (Apr 30 2020 at 23:10):
@[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?
Jalex Stark (Apr 30 2020 at 23:18):
kevin what do you mean by x and y?
Yury G. Kudryashov (Apr 30 2020 at 23:21):
There was a typo. I fixed it after Kevin's comment.
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
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)
Jalex Stark (Apr 30 2020 at 23:24):
and presumably you want that linear map to be the projection onto p?
Yury G. Kudryashov (Apr 30 2020 at 23:25):
Yes, and have
ker = q.
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
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
Yury G. Kudryashov (Apr 30 2020 at 23:26):
Another way to express this is to define
p × q.
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