universe levels for is_free_group

Stream: general

[Joachim Breitner]

I’m a bit stuck with docs#is_free_group.of_mul_equiv restricting the two groups to the same universe. How would I go about generalizing that?
Is it important that is_free_group.generators is a type, and not just a set G?
Or is it important that this index type lives in the same universe as G? (Can we bundle universes? Probably not)

[Eric Wieser]

Don't we have the lemma that lifts the universe?

[Eric Wieser]

I guess that doesn't help you much here

[Joachim Breitner]

Maybe I’ll work around it by constructing the instance directly, instead of going via ≃* multiplicative ℤ. Might be easier.

[Eric Wieser]

Is something like h ⁻¹' set.range (generators G) in the right universe to use as the generators?

[Eric Wieser]

Certainly that lemma should be universe polymorphic

[Joachim Breitner]

I tried, but h doesn’t apply to generators G, as it is its own type; the only thing I can do with the generators is use of. well, more tomorrow I guess …

[Eric Wieser]

Ah sorry, I meant to say set.range of

[Thomas Browning]

Shouldn't docs#is_free_group.of_mul_equiv generalize to injective homomorphisms?

[Thomas Browning]

Ah, but the mathlib proof of this just talks about subgroups, and sticks to the same universe.

[David Wärn]

There's a number of small things to prove:

• we need to now that of : generators G -> G is injective (there's an abstract proof of this, as in docs#free_product.of_injective)
• from this you can deduce that if G ≃* H with H : Type u then generators G is u-small (it is equivalent to set.range (h ∘ of)).
• now one should be able to prove the universe-polymorphic version of of_mul_equiv: H is freely generated by the u-small resizing of generators G (we have already the universe-polymorphic docs#is_free_group.unique_lift)
• finally one can prove a universe-polymorphic of_injective by combining of_equiv with docs#subgroup_is_free_of_is_free

[David Wärn]

It might be easier to do all of this if we first introduce some predicate like is_freely_generated_by where generators is unbundled and can have a different universe level from G. Then you can state (and prove!) that is_freely_generated_by transports across equivs in generators across different universe levels, and that generators is u-small iff G is.

[Eric Wieser]

I think unbundling the generators is a good idea

[Joachim Breitner]

Yay, even more ways to state that a group is freely generates (is_free_group, free_group X, and, a bit remote, free_product) :-)

[Joachim Breitner]

Or having _only_ the unbundled one? Seems very reasonable to me, and I believe what I am working on right now would be much more natural that way. Should I give it a shot?

[Eric Wieser]

If nothing breaks when unbundling, go for it

[Joachim Breitner]

should the of be still bundled in is_freely_generated_by? Or not (in which case it becomes simply a name for the universal property)?

[David Wärn]

The only reason the generators are bundled at the moment is that saying "G is freely generated by (some complicated type of generators)" is less elegant than saying "G is free" (in particular the Nielsen-Schreier file will look less pretty in the unbundled way). But it's not a very strong reason, and there are good reasons to unbundle the generators

[David Wärn]

Joachim Breitner said:

should the of be still bundled in is_freely_generated_by? Or not (in which case it becomes simply a name for the universal property)?

I would say we can still bundle of, in line with docs#basis. It may also be a good idea to change the definition to match up with basis, i.e. to say a group is free when it is isomorphic to a free_group (and have a lemma saying a group is free when it has the right universal property). This would certainly alleviate universe polymorphism headache

[Joachim Breitner]

Ah, I think I understand now: using the universal property as or in the definition is appealing from a mathematical point of view, but the quantifier over the “other” type only quantities over types of the same universe level as the definition itself, so it's not really the full universal property, and that's why the existing API has to jump through hoops to get the more general one. If the definition is just the equivalence to “the” free group, and the universal property a separate lemma, this issue is avoided. Is that roughly correct?

[Joachim Breitner]

In that light I'm in favor of is_freely_generated_by like basis to replace our is_free_group, as suggested above. Can probably easily live in free_group.lean then. Maybe I'll give it a shot. Or maybe after I finish the ping pong lemma (phrased using equivalence to free_group to be compatible with that then)

[Joachim Breitner]

I experimented with

class is_freely_generated_by (G : Type*) [group G] (X : Type*) :=
  ( mul_equiv : free_group X ≃* G )

but it has its downsides over is_free_group, which has the generators bundled. In particular, the ext-lemma doesn't apply automatically when equating monoid-homs from G (because the lemma search wouldn’t know which Xs to use).

Maybe I’ll first refactor is_free_group to use free_group X ≃* G internally, instead of the universal property, to avoid the universe level issues, but otherwise keeping that API.

[Johan Commelin]

@Joachim Breitner You could try to make X an out_param.

[Johan Commelin]

That might solve those issues.

[Johan Commelin]

And I think it is unlikely that we'll often want is_freely_generated_by G X for two different values of X.

[Joachim Breitner]

I can try. Will this just guide the lemma/instance search? Or does it actually forbid instances with different generators?

[Johan Commelin]

It only guides.

[Johan Commelin]

Lean never forbids multiple instances of the same class. But in the case of out_params this can certainly cause Lean to be mightily confused.

[Joachim Breitner]

Hmm, it seems that regresses instance search in one case that went through without out_param:

failed to synthesize type class instance for
ι : Type ?,
G : ι → Type ?,
_inst_3 : Π (i : ι), group (G i),
X : ι → Type ?,
hG : Π (i : ι), is_freely_generated_by (G i) (X i),
x : Σ (i : ι), X i
⊢ is_freely_generated_by (G x.fst) ?m_1

Note that hG should provide that instance here easily.

[Johan Commelin]

Hmm, no idea why that fails :cry:

[Joachim Breitner]

This is what trace.class_instance says about this instance:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_1 : @is_freely_generated_by (G x.fst) (_inst_3 x.fst) ?x_0 := hG ?x_2
failed is_def_eq

I have no idea why it tries to put _inst_3 here, which is

_inst_3 : Π (i : ι), group (G i),

Maybe an out_param of type Type* is too unrestricted, and the solver sees _inst_3 and thinks “oh, let’s try that for X”?

[Eric Wieser]

Is this on a branch somewhere I can play with?

[Joachim Breitner]

sorry for the delay; it is now: joachim/is_freely_generated_by, commit 881f96934a, failure in src/group_theory/free_product.lean. Note how code fails that worked before that commit.

[Eric Wieser]

@is_freely_generated_by.of _ _ _ _ x.2 works fine there even though is_freely_generated_by.of x.2 doesn't

[Eric Wieser]

attribute [elab_simple] is_freely_generated_by.of also seems to work

[Joachim Breitner]

Thanks, indeed! What does that tell us? I guess I can proceed with this API design and use [elab_simple] on of and see how far that gets us?

[Eric Wieser]

There's probably something to lean about how out_params work there, but ultimately lean is just elaborating things in a bad order

[Anne Baanen]

Here's the relevant part of the trace with type_context.is_def_eq_detail and pp.all on:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_1 : @is_freely_generated_by.{?u_0 0} (G (@sigma.fst.{?l__fresh.172.284190 ?l__fresh.172.284191} ι (λ (i : ι), X i) x))
  (_inst_3 (@sigma.fst.{?l__fresh.172.284190 ?l__fresh.172.284191} ι (λ (i : ι), X i) x))
  ?x_0 := hG ?x_2
[type_context.is_def_eq_detail] [1]: @is_freely_generated_by.{?u_0 0} (G (@sigma.fst.{?l__fresh.172.284190 ?l__fresh.172.284191} ι (λ (i : ι), X i) x))
  (_inst_3 (@sigma.fst.{?l__fresh.172.284190 ?l__fresh.172.284191} ι (λ (i : ι), X i) x))
  ?x_0 =?= @is_freely_generated_by.{?l__fresh.172.3587 ?l__fresh.172.3588} (G ?x_2) (_inst_3 ?x_2) (X ?x_2)
[type_context.is_def_eq_detail] [2]: is_freely_generated_by.{?u_0 0} =?= is_freely_generated_by.{?l__fresh.172.3587 ?l__fresh.172.3588}
[type_context.is_def_eq_detail] on failure: @is_freely_generated_by.{?u_0 0} (G (@sigma.fst.{?l__fresh.172.284190 ?l__fresh.172.284191} ι (λ (i : ι), X i) x))
  (_inst_3 (@sigma.fst.{?l__fresh.172.284190 ?l__fresh.172.284191} ι (λ (i : ι), X i) x))
  ?x_0 =?= @is_freely_generated_by.{?l__fresh.172.3587 ?l__fresh.172.3588} (G ?x_2) (_inst_3 ?x_2) (X ?x_2)
failed is_def_eq

[Anne Baanen]

As I understand it, to produce the on failure: message, either the universe levels in is_freely_generated_by.{?u_0 0} =?= is_freely_generated_by.{?l__fresh.172.3587 ?l__fresh.172.3588} could not be unified, or one of the arguments failed the quick_is_def_eq check.

[Anne Baanen]

Yup, set_option trace.type_context.univ_is_def_eq true gives the answer:

[type_context.univ_is_def_eq] 0 =?= ?_mlocal._fresh.297.3563 ... failed

[Anne Baanen]

Since the non-temporary metavariable ?u_0 can be assigned, the conclusion seems to be something like: there are some temporary universe metavariables on the right hand side that Lean tries to unify in a non-temporary context, so they are unable to be assigned and unification fails.

[Anne Baanen]

Why we got to this place is unclear to me, though.

[Joachim Breitner]

Ah I noticed I had

variables {G : Type*} [group G] {X : Type} [is_freely_generated_by G X]

instead of

variables {G : Type*} [group G] {X : Type*} [is_freely_generated_by G X]

in scope when defining of. And with that fixed I don’t [elab_simple] it seem.

[Joachim Breitner]

Hmm, looking at how is_free_group is used in nielson-schreier.lean, in particular

instance subgroup_is_free_of_is_free {G : Type u} [group G] [is_free_group G]  (H : subgroup G) : is_free_group H

I doubt that an unbundled is_freely_generated_by G X will look nice here, given that this theorem doesn't tell us what the generators of H are.
I could write Σ Y. is_freely_generated_by H Y.
Or I could keep is_free_group with bundled generators (but defined via an equivalence to the free_group, not the universal property, to avoid universe issues), in which case we have three APIs to maintain – free_group X, is_freely_generated_by G X and is_free_group G.
WDYT?

[Joachim Breitner]

Hmm, probably the latter - is_free_group is a class, and type class inference just works better without the type of generator being around explicitly.

[Eric Wieser]

I think the sigma type is ok

[Eric Wieser]

Or more specifically, use the sigma as an auxiliary construction, then create the instance on its first entry

[Eric Wieser]

(docs#subgroup_is_free_of_is_free)

[Joachim Breitner]

“create the instance on its first entry” – for that we still need a is_free_group G class, and can’t get rid of it, correct?

[Eric Wieser]

I was thinking of something like:

def aux : Σ I, is_freely_generated_by H I := ...

def generators := aux.1

instance : is_freely_generated_by H generators := aux.2

[Joachim Breitner]

For now, I did the change where is_free_group is now defined via isomorphism to the free group, but other the API is mostly left alone: <https://github.com/leanprover-community/mathlib/pull/13633>