projectors

Stream: Is there code for X?

[Yury G. Kudryashov]

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]

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]

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]

kevin what do you mean by x and y?

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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

[Jalex Stark]

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

[Yury G. Kudryashov]

Yes, and have ker = q.

[Jalex Stark]

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]

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]

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

[Jalex Stark]

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