A question of type class inference

Stream: new members

[Stepan Nesterov]

I am watching talks on Lean for the curious mathematician 2020 and one thing that Kevin mentions in his talk on algebraic hierarchy is how Lean knows that if G and H are groups, then so is G \times H by the virtue of type class inference system. But what would happen if I try to feed it instances which make a certain set in a group in more than one way? Let's say I defined 'If Y is an H-space, then so is Hom(X,Y)', 'If Y is a space, then \OmegaY is an H-space', and 'Hom(\Sigma X, Y) is an H-space'. Then I can define two group structures on Hom(\Sigma X, \Omega Y), and in fact I can prove that they are the same. But will Lean accept this definition or will it complain that the type class inference in ambiguous?

[Eric Wieser]

In my understanding of your example there's no ambiguity:

import tactic

class is_H_space (X : Type*).

def omega (X : Type*) : Type* := sorry
def sigma' (X : Type*) : Type* := sorry

variables (X Y : Type*)

instance pi.is_H_space [is_H_space Y] : is_H_space (X → Y) := sorry

instance [is_H_space Y] : is_H_space (omega Y) := sorry
instance [is_H_space Y] : is_H_space (sigma' Y) := sorry

set_option pp.implicit true

instance foo [is_H_space Y] : is_H_space (sigma' X → omega Y) :=
by show_term {apply_instance}
-- @pi.is_H_space (sigma' X) (omega Y) (@omega.is_H_space Y _inst_1)

[Eric Wieser]

(also, you can use $$\LaTeX$$ in your zulip posts to make \Sigma X typeset possibly as you want it, $\Sigma X$)

[Stepan Nesterov]

\Sigma Y is not an H-space!
It is a co-H-space, making Hom(\Sigma X, Y) in an H-space

[Stepan Nesterov]

So I can subtitute Y=\Omega Z to get a group structure

[Stepan Nesterov]

But I then have a different group structure because \Omega Z is an H-space

[Eric Wieser]

I should probably withdraw at this point as I have no idea what an H-space structure is! Have I given you enough information to write your problem statement in lean?

[Stepan Nesterov]

And in topology we prove that the two are the same by what's called Eckmann-Hilton argument

[Eric Rodriguez]

eckmann-hilton is absolutely gorgeous btw

[Eric Wieser]

Perhaps as a concrete example of this type of "diamond" that doesn't involve anything sophisticated, there are two different algebra structures on nat - docs#algebra.id and docs#algebra_nat

[Eric Wieser]

Lean will happily pick one or the other, and only complain when it expects one but finds the other; and even then, only if they turn out to actually hold different values

[Stepan Nesterov]

It says 'invalid definition, a declaration named 'pi.is_H_space' has already been declared'

[Stepan Nesterov]

but it says so on the line 'instance [is_H_space Y] : is_H_space (sigma' Y → X) := sorry'

[Stepan Nesterov]

Which is not where the problem really is

[Eric Wieser]

Just give it a different name

[Eric Wieser]

instance a_different_name_because_the_default_already_existed instead of instance

[Stepan Nesterov]

Ok, now it works

[Stepan Nesterov]

It says Try this: refine @pi.is_H_space (sigma' X) (omega Y) (omega.is_H_space Y)

[Eric Wieser]

Right, so it still arbitrarily prefers that path over the other one

[Eric Wieser]

Is your sigma docs#sigma, or something else?

[Stepan Nesterov]

Eric Wieser said:

Is your sigma docs#sigma, or something else?

My \Sigma is reduced suspension from topology :)
https://ncatlab.org/nlab/show/suspension

[Kevin Buzzard]

In short, if X is a class then there is supposed to only be one X structure on any type up to definitional equality, and there are tricks to make this happen in situations where you end up with two equal, but not definitionally equal, constructions of an X. For example, the product of two metric spaces becomes a topological space in two different ways, one via product of metric spaces is a metric space and then metric space is a topological space, and the other via metric space is a topological space and product of topological spaces is a topological space. For example the topologies on $\R^2$ generated by open discs and open rectangles are equal but not definitionally equal. This is dealt with in Lean by embedding secondary structures within the primary ones, a rather surprising solution, but it works. For example the internal definition of a metric space in Lean also carries a topology plus a proof that the topology is the one generated by the metric (and if the user doesn't supply it, a tactic creates it from the metric). That way, when forming the product of two metric spaces, you can insert the proof that the diagram commutes here and the user is none the wiser that anything sneaky is going on and the system works.

[Kevin Buzzard]

See for example this library note

[Scott Morrison]

I think @Stepan Nesterov's example Hom(\Sigma X, \Omega Y) is an interesting one, and I don't see how it's covered by the technique Kevin has just pointed to.

We would get two instances here, and they would not be definitionally equal.

[Eric Wieser]

Presumably in that case they're at least propositionally equal?

[Stepan Nesterov]

Yes, the two group operations are equal in the respective category, and I was just curious if there is a way to state that in Lean cleanly and/or if there was a recommended detour if we need both for some reason.

[Stepan Nesterov]

And maybe in this example we do, because the proof via Eckmann-Hilton argument (https://ncatlab.org/nlab/show/Eckmann-Hilton+argument) shows that both group laws are commutative, something that is not obvious from their direct definitions

[Patrick Massot]

https://leanprover-community.github.io/mathlib_docs/group_theory/eckmann_hilton.html

[Patrick Massot]

You should be able to find rather concrete answers at the above link :wink:

[Stepan Nesterov]

Patrick Massot said:

https://leanprover-community.github.io/mathlib_docs/group_theory/eckmann_hilton.html

But are higher homotopy groups defined in Lean? If so, how is the equality of two group laws stated there?

[Patrick Massot]

No, they are not defined in mathlib.

[Stepan Nesterov]

I guess a simpler example of all this would be to consider $\Omega G$ for $G$ a topological group and in this case we obtain a nontrivial result that $\pi_1(G)$ is commutative.

[Stepan Nesterov]

Is $\pi_1$ also not in mathlib, though?

[Scott Morrison]

Nope, not in mathlib. Are you wondering if the fact that there are "two essentially different proofs" it is commutative will be a problem?

[Scott Morrison]

The two constructions only differ in Prop fields, not data, so I don't see why Lean would care. Even if you produced two different comm_group instances this way, Lean will happily agree they were defeq.

[Kevin Buzzard]

$\pi_1$ not in mathlib -- that's right. There's absolutely nothing stopping it being in mathlib -- indeed an Imperial undergraduate did $\pi_1$ in Lean in 2018 as a summer project (and proved $\pi_1(\R)=0$, but never tidied up the code enough to get it into mathlib.

[Stepan Nesterov]

Scott Morrison said:

Nope, not in mathlib. Are you wondering if the fact that there are "two essentially different proofs" it is commutative will be a problem?

No, I wonder if I can access two instances of group on $\Omega G$ in this hypothetical proof if Lean just arbitrarily prefers one over the other.

[Stepan Nesterov]

That's what I would do in math: I define $\gamma \cdot \delta$ to be the $\pi_1$ multiplication, and $\gamma * \delta = \lambda t, \gamma(t)\delta(t)$ to be the pointwise multiplication, and then I get the result by Eckmann-Hilton

[Stepan Nesterov]

Scott Morrison said:

The two constructions only differ in Prop fields, not data, so I don't see why Lean would care. Even if you produced two different comm_group instances this way, Lean will happily agree they were defeq.

How are they defeq? The fact that the two are equal is by Eckmann-Hilton

[Kevin Buzzard]

The "pre-multiplications" on the paths are different, but $\pi_1$ is classes of paths, so it's not so clear (to me) that they're not defeq (but I am a bit unclear about how quotients work under the hood)

[Scott Morrison]

Ah, I had in mind a different proof, where you only ever introduce the \pi_1 multiplication, but then give two different proofs of commutativity (transporting \gamma around \delta, or transporting \delta around \gamma). This doesn't use Eckmann-Hilton directly, and doesn't have any defeq problems, because the two versions only differ at the Prop level.

The usual approach to implement the proof that you had in mind is just to have a type synonym for the "other" multiplication, and then just apply Eckmann-Hilton as it is formulated in the file Patrick linked above.

Type synonyms are an easy and apparently-sufficiently-powerful mechanism to deal with "conflicting" instances, and so far seem to have been sufficient. I like your H-space example above because it's not immediately obvious how to use type synonyms.

[Johan Commelin]

But only introducing the $\pi_1$-multiplication is not "good enough", in some sense, right? Because sometimes you have only the one and not the other, or vice versa. (I mean, this can show up in topology, in practice.)

[Scott Morrison]

Yes, that's true. But I think this example doesn't show it super clearly. While both multiplications are very natural, the pointwise multiplication is only natural on honest paths, and it's a pretty specialised application to consider pointwise multiplication on homotopy classes of paths.

[David Wärn]

One group structure is on $\pi_1(G, 1)$, the other is on $\pi_0(\Omega G)$ (path components of a topological group is a group). Of course these two types are equivalent, and may or may not end up defeq, but this identification should still be opaque to typeclass inference? I think they're automatically the kind of synonym Scott described