Zulip Chat Archive

Stream: general

Topic: coe?


view this post on Zulip Robert Maxton (Oct 29 2020 at 16:59):

What does 'coe' refer to? Use of 'coe' and related commands seems ubiquitous in the library, but I don't recognize the acronym and (being so short) I can't find it with google either.

view this post on Zulip Logan Murphy (Oct 29 2020 at 17:02):

coercion

view this post on Zulip Logan Murphy (Oct 29 2020 at 17:03):

see here

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 17:06):

every mathematician knows that NR\mathbb{N}\subseteq\mathbb{R}. However, if you actually build maths from the axioms, this isn't actually true! Instead, there's a natural function NR\mathbb{N}\to\mathbb{R} and this function actually has a name, but nobody wants to remember the name, so the real number associated to the natural number n is called ↑n.

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 17:08):

If n is actually a natural number, and you write n : ℝ in Lean, you won't get a type error, Lean will secretly just apply the coercion. For more information, see the coercions section of TPIL.

view this post on Zulip Robert Maxton (Oct 29 2020 at 17:11):

Ah, okay. I'm familiar with coercion, but not with the abbreviation (and it doesn't really surprise me in retrospect that mathlib is very careful about exactly how that's used.)

That said, I'm then not sure how I should interpret the orbit-stabilizer theorem as interpreted in Lean. Or like, what exactly is being coerced here? The orbit to...?

view this post on Zulip Robert Maxton (Oct 29 2020 at 17:12):

(Relatedly, the order of a group/index of a set in a group doesn't seem to have an explicit definition anywhere; if I call sizeof on a possibly-infinite group, will Lean yell at me?)

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 17:15):

Where's the coercion in orbit-stabilizer?

Everything has an explicit definition :-) If you have the code up and running in VS Code then you can just right click on something and jump to its definition.

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 17:17):

sizeof is some internal function which has nothing to do with the size of anything IIRC. We have the cardinality of a group, which will be a possibly infinite cardinal, and we also have a different size function which takes in an object known to be finite and spits out a natural.

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 17:17):

We might even have a third size function which takes an object not known to be finite, and spits out a natural, which will be 0 if the size is infinite.

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 17:17):

(but this function might not be on the master branch)

view this post on Zulip Robert Maxton (Oct 29 2020 at 17:18):

Sure, but that doesn't mean it'll be a legible definition :V.

Oh, whoops, sizeof is the byte of the memory type isn't it lol. Either of those are good; I'm trying to implement the class equation for fun/for practice

view this post on Zulip Floris van Doorn (Oct 29 2020 at 17:21):

sizeof is an internal function to quantify how complication a value of a type is. The size of sum.inl t is the size of tplus 1.

If you want the cardinality of something, see docs#cardinal.mk (or docs#fintype.card)

view this post on Zulip Patrick Massot (Oct 29 2020 at 17:25):

Do you mean docs#mul_action.orbit_equiv_quotient_stabilizer?

view this post on Zulip Patrick Massot (Oct 29 2020 at 17:26):

The orbit is a set which is coerced to being a type.

view this post on Zulip Robert Maxton (Oct 29 2020 at 17:31):

that's the one I linked, aye

Ah, okay. That makes sense I ... think....

view this post on Zulip Patrick Massot (Oct 29 2020 at 17:35):

No, you linked to docs#mul_action.orbit, but that's fine

view this post on Zulip Robert Maxton (Oct 29 2020 at 17:38):

Oh, whoops. Serves me right for forgetting my anchors.


Last updated: May 08 2021 at 10:12 UTC