## Stream: Is there code for X?

### Topic: projectors

#### 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):

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?

#### 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 linear_equiv between E and 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