Zulip Chat Archive

Stream: general

Topic: coe?

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.

Logan Murphy (Oct 29 2020 at 17:02):


Logan Murphy (Oct 29 2020 at 17:03):

see here

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.

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.

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...?

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?)

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.

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.

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.

Kevin Buzzard (Oct 29 2020 at 17:17):

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

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

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)

Patrick Massot (Oct 29 2020 at 17:25):

Do you mean docs#mul_action.orbit_equiv_quotient_stabilizer?

Patrick Massot (Oct 29 2020 at 17:26):

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

Robert Maxton (Oct 29 2020 at 17:31):

that's the one I linked, aye

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

Patrick Massot (Oct 29 2020 at 17:35):

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

Robert Maxton (Oct 29 2020 at 17:38):

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

Last updated: Dec 20 2023 at 11:08 UTC