coe?

Stream: general

[Robert Maxton]

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]

coercion

[Logan Murphy]

see here

[Kevin Buzzard]

every mathematician knows that $\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 $\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]

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]

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]

(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]

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]

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]

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]

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

[Robert Maxton]

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]

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]

Do you mean docs#mul_action.orbit_equiv_quotient_stabilizer?

[Patrick Massot]

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

[Robert Maxton]

that's the one I linked, aye

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

[Patrick Massot]

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

[Robert Maxton]

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