making isomorphism class a group

Stream: general

[Kenny Lau]

Let's say I have a bunch of groups, and I use quotient to make isomorphism classes. Is there a constructive way to make the isomorphism classes inherit the structure of a group?

[Simon Hudon]

I don't know but I'd like to find out. Let's say our groups are specified as:

variables {I : Type} (G : I -> Type) [Π i, group (G i)]

[Simon Hudon]

Are we also given the isomorphisms between those groups or to you want to construct them somehow?

[Kenny Lau]

I have already constructed the quotient

[Simon Hudon]

Can you show it?

[Kenny Lau]

import data.set.basic group_theory.subgroup

universe u

namespace group

variables {α : Type u} [group α] (S : set α)

inductive generate : set α
| basic : ∀ x ∈ S, generate x
| one : generate 1
| mul_inv : ∀ x y, generate x → generate y → generate (x * y⁻¹)

namespace generate

def is_subgroup : is_subgroup (generate S) :=
{ one_mem := generate.one S,
  mul_inv_mem := λ x y hx hy, generate.mul_inv x hx y hy }

end generate

variables {β : Type u} [group β]
variables α β

class isomorphism extends α ≃ β :=
( is_group_hom : is_group_hom to_fun )

namespace isomorphism

variables {γ : Type u} [group γ]
variables {β γ}

@[refl] protected def refl : isomorphism α α :=
{ is_group_hom := λ x y, rfl
  .. equiv.refl α }

variables {α β γ}

@[symm] protected def symm (e : isomorphism α β) : isomorphism β α :=
{ is_group_hom := λ x y, calc
          e.inv_fun (x * y)
        = e.inv_fun (e.to_fun (e.inv_fun x) * e.to_fun (e.inv_fun y)) : by rw [e.right_inv, e.right_inv]
    ... = e.inv_fun (e.to_fun (e.inv_fun x * e.inv_fun y)) : by rw e.is_group_hom
    ... = e.inv_fun x * e.inv_fun y : by rw e.left_inv,
  .. equiv.symm e.to_equiv }

@[trans] protected def trans (e₁ : isomorphism α β) (e₂ : isomorphism β γ) : isomorphism α γ :=
{ is_group_hom := λ x y, by unfold equiv.trans; dsimp; rw [e₁.is_group_hom, e₂.is_group_hom],
  .. equiv.trans e₁.to_equiv e₂.to_equiv }

end isomorphism

end group

variable (S : Type u)

namespace free_group

structure to_be_named (G : Type u) [group G] :=
( gen : set G )
( gen_gen : group.generate gen = set.univ )
( func : gen → S )
( inj : function.injective func )

def to_be_named.quotient_rel : setoid Σ G [H : group G], @to_be_named S G H :=
⟨λ G H, nonempty $ @group.isomorphism G.1 G.2.1 H.1 H.2.1,
 λ G, ⟨@group.isomorphism.refl G.1 G.2.1⟩,
 λ G H ⟨e⟩, ⟨@group.isomorphism.symm G.1 G.2.1 H.1 H.2.1 e⟩,
 λ G H K ⟨e₁⟩ ⟨e₂⟩, ⟨@group.isomorphism.trans G.1 G.2.1 H.1 H.2.1 K.1 K.2.1 e₁ e₂⟩⟩

def something : Type (u+1) :=
quotient (to_be_named.quotient_rel S)

noncomputable def rep : something S → Σ G [H : group G], @to_be_named S G H :=
λ G, classical.some (@quotient.exists_rep _ (to_be_named.quotient_rel S) G)

#check λ G, classical.some (@quotient.exists_rep _ (to_be_named.quotient_rel S) G)

structure funny_structure : Type (u+1) :=
( G : something S )
( func : S → (rep S G).1 )
( im_gen : @group.generate _ (rep S G).2.1 (func '' set.univ) = set.univ )

def some_product : Type (u+1) :=
Π A : funny_structure S, (rep S A.G).1

noncomputable instance some_product.group : group (some_product S) :=
{ mul := λ f g x, @has_mul.mul _ (@semigroup.to_has_mul _ (@monoid.to_semigroup _ (@group.to_monoid _ (rep S (x.G)).2.1))) (f x) (g x),
  mul_assoc := λ f g h, funext $ λ x, by apply mul_assoc,
  one := λ x, @has_one.one _ (@monoid.to_has_one _ (@group.to_monoid _ (rep S (x.G)).2.1)),
  one_mul := λ f, funext $ λ x, by apply one_mul,
  mul_one := λ f, funext $ λ x, by apply mul_one,
  inv := λ f x, @has_inv.inv _ (@group.to_has_inv _ (rep S (x.G)).2.1) (f x),
  mul_left_inv := λ f, funext $ λ x, by apply mul_left_inv }

def aux_func : S → some_product S :=
λ x A, A.func x

end free_group

def free_group : Type (u+1) :=
group.generate (free_group.aux_func S '' set.univ)

instance free_group.group : group (free_group S) :=
is_subgroup.group group.generate.is_subgroup

def free_group.from_S : S → free_group S :=
λ x, ⟨free_group.aux_func S x, group.generate.basic _ ⟨x, trivial, rfl⟩⟩

[Kenny Lau]

this is WIP so there are errors on the bottom, ignore those

[Kenny Lau]

the quotient is appropriately named something

[Simon Hudon]

So you'd like to remove noncomputable from your group instance?

[Kenny Lau]

right

[Kevin Buzzard]

You had to prove that the composite of group homs is a group hom?? That's not there already?

[Kenny Lau]

you'll be surprised

[Simon Hudon]

Instead of classical.some and quotient.exists_rep in rep, can you try and use quotient.lift?

[Kenny Lau]

to where?

[Simon Hudon]

Not sure yet

[Simon Hudon]

You're basically taking the value of a quotient type and sticking it in a sigma type. Because the sigma type is in Type u depending on which representative you extract, you will be able to tell members of the quotient sets apart.

[Simon Hudon]

There are two possibilities I can see to stay constructive: instead of using a sigma type, use an existential quantification (not sure if that's workable with the group) or extract something other than the element of one of the group. A representative value that will be the same for every element of a given equivalence class

[Simon Hudon]

Or maybe Mario's trunc contraption can make the sigma type into something that isn't data

[Kenny Lau]

@Simon Hudon do we even need the quotient?

[Simon Hudon]

I think you're right, you don't need it, at least not there

[Kenny Lau]

I think the reason the author introduced it is because of some foundational issues with ZFC

[Kenny Lau]

the paper is here for reference https://www3.nd.edu/~andyp/notes/CategoricalFree.pdf

[Kenny Lau]

@Kevin Buzzard this can be viewed in two ways

[Kenny Lau]

you will view it as "another reason why ZFC is stupid"

[Kenny Lau]

I will view it as "another reason why Lean is stupid"

[Simon Hudon]

I'm wondering if you even need the sigma type

[Kenny Lau]

I did it without any quotient

[Kenny Lau]

and without injectivity

[Kenny Lau]

the only reason why the paper introduced those is to justify it in ZFC

[Simon Hudon]

And sigma type?

[Kenny Lau]

well the sigma type has UMP as pi type right

[Kenny Lau]

that means, (Sigma x1 x2) -> x3 is the same as x1 -> x2 -> x3

[Kenny Lau]

since they're there, the sigma doesn't need to be there anymore

[Kenny Lau]

am I speaking English

[Kenny Lau]

that thing there with that sigma is no longer used

[Kenny Lau]

I can't English

[Simon Hudon]

What's UMP?

[Kenny Lau]

universal mapping property

[Kenny Lau]

or in CS language, "destructor" / "eliminator"

[Simon Hudon]

Ah I see

[Simon Hudon]

So why is it that not needing a quotient type makes Lean stupid?

[Kenny Lau]

well if I need to explain I would have to bring another concept from math philosophy into here :P

[Kenny Lau]

called predicativity

[Simon Hudon]

Cool, I'm all ears

[Kenny Lau]

inductive types are predicative

[Kenny Lau]

they're philosophically well-founded

[Kenny Lau]

bigger things are built on top of smaller things

[Kenny Lau]

like "canonical", this word can't be properly defined, but a common criterion is whether the quantifiers quantify over the object to be constructed

[Kenny Lau]

e.g. in ZFC, omega is constructed to be the intersection of every inductive set

[Kenny Lau]

instead of building it from below, omega is constructed from above, which makes it philosophically not well-founded, and we call that impredicative

[Kenny Lau]

in ZFC, omega := {x | x in A for every inductive A}

[Kenny Lau]

but the "for every" quantifier there, quantifiers over omega itself

[Kenny Lau]

now, the free group construction in the paper is equally impredicative

[Kenny Lau]

in the sense that it takes the product of every possible group and then find the subgroup generated by the image of S

[Kenny Lau]

but that product would have to already include that group to be constructed

[Kenny Lau]

ZFC is an impredicative theory

[Kenny Lau]

but that's unavoidable, because we want a strong foundation theory to do maths

[Kenny Lau]

the common construction of free group is predicative

[Kenny Lau]

because it builds on smaller things, i.e. individual words

[Kenny Lau]

in ZFC, i.e. in the paper, the author constructed the free product by considering every group generated by a set that injects into S

[Kenny Lau]

there's still a limitation on the size

[Kenny Lau]

in Lean, i.e. in my file, I don't even need to care about the size, since Lean allows it

[Kenny Lau]

https://github.com/kckennylau/Lean/blob/master/free_group.lean

[Simon Hudon]

Why is that a problem?

[Kenny Lau]

it's not very well-founded is it

[Simon Hudon]

Isn't the "big things built from smaller things" idea supported by the hierarchy of universes?

[Kenny Lau]

well but one universe is already big enough

[Kenny Lau]

philosophy aside, this construction is quite funny

[Kenny Lau]

what do you think of my file? is it mathematically correct? should I PR it?

[Kenny Lau]

I wonder why this construction isn't more well-known

[Simon Hudon]

I don't think I can make a judgement about your construction. Mario and Kevin probably should be the ones to comment

[Kenny Lau]

ok

[Simon Hudon]

Or Johannes

[Simon Hudon]

It looks like a cool construction :)

[Kenny Lau]

@Simon Hudon https://github.com/kckennylau/Lean/commit/c6eac863b23d58d40deaab62489f6069f860407e#diff-fdee7d198ee1f7316cba5649313e084a

[Kenny Lau]

rip universe limitation

[Kenny Lau]

now it can be in any universe

[Simon Hudon]

Yeah, that's universe polymorphism for you ;-)

[Kenny Lau]

I wonder if free_group.{u v} S and free_group.{u w} S are different

[Kenny Lau]

@Simon Hudon this is such a convenient construction

[Kenny Lau]

basically constructing an object from its UMP

[Kenny Lau]

I can probably construct the abelianization this way also

[Simon Hudon]

That looks like the free objects I've worked with before. I remember being blown away by how cool they are :D

[Kenny Lau]

you've seen this construction before?

[Simon Hudon]

I've seen it in free monads mostly

[Kenny Lau]

do you have any idea how I can fix the file to remove the need for manual typeclassing?

[Kenny Lau]

group to monoid, monoid to semigroup, semigroup to has_mul...

[Simon Hudon]

What happens when you replace it with an underscore?

[Kenny Lau]

can't synthesize that thing

[Simon Hudon]

Right but what instances are in your context?

[Kenny Lau]

the thing is that the instances aren't declared to the left of the colon

[Kenny Lau]

rather, they're introduced as variables

[Kenny Lau]

because of how I defined ambient

[Simon Hudon]

Right, so you can write:

λ x y G HG f, by resetI ; exact @has_mul.mul _ _ ...

[Kenny Lau]

I thought definitions shouldn't have any tactics

[Kenny Lau]

because they're difficult to destruct

[Simon Hudon]

This tactic won't create a complicated term. But it's also useful to just try it and see if it works. Otherwise, you can also use a separate def

[Kenny Lau]

hmm...

[Kenny Lau]

free functors on steroids

[Kenny Lau]

https://github.com/kckennylau/Lean/blob/master/abelianization.lean

[Kenny Lau]

comes with commutators for free!

[Mario Carneiro]

I'm familiar with this construction, which is sometimes used as an application of category theory: use the adjoint functor theorem to construct free groups. When you unwind the category theory it's exactly this construction: taking a suitable quotient over all groups

[Mario Carneiro]

The universe issues that arise in ZFC also arise in lean, because they are valid concerns and can cause inconsistency if they are not attended to. In lean this expresses as a bumping up of the universe level of the constructed free group

[Mario Carneiro]

To prove that the universe doesn't need to increase, you need a size limitation which amounts to doing the standard (internal) free group construction anyway. This is why I'm not a big fan of this approach - it's just shuffling proof obligations around

[Mario Carneiro]

When you write the UMP predicatively, it ends up weaker than people want (and use), because the free group you've constructed lives in max u (v+1) but is only universal wrt groups in Type v, which is strictly lower. In particular, the free group UMP doesn't apply to itself, which we want to be true for it to really be a free group. Otherwise it's only an approximation - if you try proving equivalence to the standard internal definition you will get stuck

[Mario Carneiro]

Re: making the isomorphism class a group, it is impossible to do this computably for some reasonable definitions of the problem. Suppose we want to take a quotient of all groups (in some universe) with respect to isomorphism. First of all, note that a quotient is with respect to a relation, meaning a Prop, meaning data about the isomorphism itself will be lost. We can define such a quotient, let's call it Q. Now each element q : Q somehow "represents" a group unique up to isomorphism, but I claim that there is no computable function rep : Q -> Group such that G ~= rep (mk G) for all groups G.

Now one way to define such a function is by applying choice as you've done to just pick one of the groups in the class, but maybe you thought there might be a way of using all the groups at once to form a new group which is isomorphic to each of the groups in the equivalence class. Supposing this is possible, and supposing also that you computably have the isomorphism f G : G ~= rep (mk G), i.e. that's not just an existence statement, then you have choice for group isomorphisms, since if nonempty (G ~= H) then mk G = mk H and hence you can construct G ~= rep (mk G) = rep (mk H) ~= H.

To turn this into at least unique choice, we can construct a group H which is isomorphic to G = C_2 iff α is nonempty. For example, H := Σ g : G, g ≠ 0 → trunc α will do the trick. Then given an isomorphism f : G ~= H, we have f 1 : psum (trunc α) (1 = 0) from which we obtain an element of trunc α. This is not as strong as full choice, but it is known unprovable in lean.

[Kenny Lau]

@Mario Carneiro so what should I do? I'm confused, you keep saying it's unprovable but you're giving an algorithm

[Mario Carneiro]

I'm showing that if you could construct it you could prove something that is known unprovable

[Mario Carneiro]

thus it's not computable

[Kenny Lau]

ok, then what should I do?

[Mario Carneiro]

Live with the fact that going from an isomorphism class to a specific group is nonconstructive?

[Kenny Lau]

oh well, but I didn't use isomorphism class in the end

[Mario Carneiro]

maybe you can phrase it independently of the choice then?

[Kenny Lau]

phrase what?

[Mario Carneiro]

your theorem, whatever it is

[Kenny Lau]

that free group exists?

[Mario Carneiro]

I'm not sure what you are trying to do now...

[Kenny Lau]

I realized that using isomorphism class is because of some stupid limitation of ZFC

[Mario Carneiro]

it's a limitation of lean too, I say

[Kenny Lau]

I just stopped using it

[Kenny Lau]

and then I constructed the free group and proved its property

[Mario Carneiro]

did you though?

[Mario Carneiro]

watch your universe levels

[Mario Carneiro]

I'm claiming you didn't construct the real free group

[Kenny Lau]

I'm starting to suspect so

[Mario Carneiro]

Have you ever heard of system F encodings or church encodings?

[Kenny Lau]

I've heard of church encodings, if you're referring to the numbers

[Mario Carneiro]

I'm talking about the types. Something like this:

def unit := ∀ X : Type, X → X
def nat := ∀ X : Type, X → (X → X) → X
def prod (α β) := ∀ X : Type, (α → β → X) → X

[Kenny Lau]

oh

[Kenny Lau]

I get it, go on

[Mario Carneiro]

This sort of thing works great in system F, where there is only one impredicative data type Type, because then unit : Type etc and this has the expected universal property

[Mario Carneiro]

But in lean, it's not as strong as you want because the elimination property only goes to Type 0 in this case while the constructed type lives in Type 1

[Mario Carneiro]

Note that real eliminators such as are generated by inductive eliminate to Sort u where u is independent of the universes involved in the definition of the inductive type itself

[Mario Carneiro]

This allows creation of type families over the inductive type in very large universes

[Kenny Lau]

fair enough

[Mario Carneiro]

There is a curious property about these weak eliminators, though: If there exists a real type with the right eliminator, then you can prove that the weak type and the strong type are isomorphic, so the weak type inherits the strong eliminator

[Kenny Lau]

hence what you mean by moving proof obligations around

[Mario Carneiro]

That means that your free group construction is correct if there is a free group

[Kenny Lau]

and here am I thinking that it's a brand new construction that nobody knows :P

[Mario Carneiro]

The size limitation thing is really important but manifests in weird ways in ZFC and lean

[Mario Carneiro]

I think it's also related to the "B" in BNF, bounded natural functors used in isabelle for generating arbitrary (co)inductive types

[Mario Carneiro]

which literally have an axiom on limitation of size, to prevent universe issues

[Kenny Lau]

:b_button:ounded :b_button:atural :b_button:unctors

[Mario Carneiro]

now I need to make a "bounded natural blunders" joke

[Kenny Lau]

I'm thoroughly confused now

[Kevin Buzzard]

Well that's really annoying. I thought that type theory was getting around these silly ZFC universe problems

[Kevin Buzzard]

but it's just moving them to Lean universe problems

[Kenny Lau]

same thought here

[Kevin Buzzard]

Why do you care about isomorphic groups?

[Kevin Buzzard]

Why not just work with all groups?

[Kenny Lau]

right, I worked with all groups at the end

[Kenny Lau]

I was following the paper, which used isomorphic groups

[Kenny Lau]

my conjecture is that the author used isomorphism classes to make it justified in ZFC

[Kevin Buzzard]

Similarly you don't need to work with "generated by a subset of S"

[Kenny Lau]

which i take to be a really shitty thing to do

[Kevin Buzzard]

That just seemed to be a red herring

[Kenny Lau]

right

[Kenny Lau]

I didn't use that in my construction

[Kenny Lau]

but then it still depends on the universe

[Kenny Lau]

since you're quantifying over every group anyway

[Kenny Lau]

that's the thing with impredicative constructions

[Kevin Buzzard]

you can send the other elements of $S$ to the identity

[Kevin Buzzard]

Oh I broke zulip

[Kevin Buzzard]

I can't edit $S$ into $S$

[Kenny Lau]

you see, in ZFC this is the way you would do it:

[Kenny Lau]

firstly you consider only the isomorphism classes

[Kevin Buzzard]

Bingo, I had to reload the page.

[Kenny Lau]

and you only consider the groups generated by a subset of S

[Kenny Lau]

because in some sense you can build it from S

[Kevin Buzzard]

I don't see where the subset comes in

[Kevin Buzzard]

but I do see where the isomorphism classes come in

[Kenny Lau]

well

[Kenny Lau]

they are both limitations on the size of the set

[Kenny Lau]

after these two restrictions, you can justify the existence of the set by building it from a large enough set that you still build from S

[Kevin Buzzard]

I don't see where they're needed in the ZFC proof.

[Kenny Lau]

if you don't limit the size of the generator, your set is still too big

[Kevin Buzzard]

I want my generator to have size S

[Kevin Buzzard]

exactly

[Kenny Lau]

ah

[Kenny Lau]

hmm

[Kenny Lau]

that's what you meant

[Kenny Lau]

I suppose it's ok then

[Kevin Buzzard]

So in ZFC I start with S and then I choose some cardinal kappa such that in V_kappa there is a copy of every group generated by S

[Kevin Buzzard]

Lean is better because in Lean I don't think you even need that S generates G

[Kevin Buzzard]

But as Mario points out, your answer is in the wrong universe.

[Kenny Lau]

I think you do need that S generates G if you don't want to run into universe problems

[Kevin Buzzard]

In ZFC you do, but I don't see where you need it in Lean.

[Kevin Buzzard]

You just put a group structure on the product of G over all pairs (G,f:S -> G)

[Kevin Buzzard]

and give this a map from S

[Kevin Buzzard]

and then take the intersection over all the subgroups containing the image of S

[Kevin Buzzard]

This should definitely be in #maths