## Stream: general

### Topic: making isomorphism class a group

#### Kenny Lau (Mar 31 2018 at 19:49):

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 (Mar 31 2018 at 19:55):

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 (Mar 31 2018 at 19:56):

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

#### Kenny Lau (Mar 31 2018 at 19:57):

I have already constructed the quotient

Can you show it?

#### Kenny Lau (Mar 31 2018 at 19:58):

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

#### Kenny Lau (Apr 01 2018 at 16:33):

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

#### Kenny Lau (Apr 01 2018 at 16:33):

firstly you consider only the isomorphism classes

#### Kenny Lau (Apr 01 2018 at 16:33):

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

#### Kenny Lau (Apr 01 2018 at 16:33):

because in some sense you can build it from S

#### Kevin Buzzard (Apr 01 2018 at 16:34):

I don't see where the subset comes in

#### Kevin Buzzard (Apr 01 2018 at 16:34):

but I do see where the isomorphism classes come in

well

#### Kenny Lau (Apr 01 2018 at 16:34):

they are both limitations on the size of the set

#### Kenny Lau (Apr 01 2018 at 16:35):

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 (Apr 01 2018 at 16:35):

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

#### Kenny Lau (Apr 01 2018 at 16:35):

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

#### Kevin Buzzard (Apr 01 2018 at 16:35):

I want my generator to have size S

exactly

ah

hmm

#### Kenny Lau (Apr 01 2018 at 16:36):

that's what you meant

#### Kenny Lau (Apr 01 2018 at 16:36):

I suppose it's ok then

#### Kevin Buzzard (Apr 01 2018 at 16:36):

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 (Apr 01 2018 at 16:37):

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

#### Kevin Buzzard (Apr 01 2018 at 16:37):

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

#### Kenny Lau (Apr 01 2018 at 16:39):

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

#### Kevin Buzzard (Apr 01 2018 at 16:43):

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

#### Kevin Buzzard (Apr 01 2018 at 16:44):

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

#### Kevin Buzzard (Apr 01 2018 at 16:45):

and give this a map from S

#### Kevin Buzzard (Apr 01 2018 at 16:45):

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

#### Kevin Buzzard (Apr 01 2018 at 16:46):

This should definitely be in #maths

Last updated: May 14 2021 at 04:22 UTC