Zulip Chat Archive

Stream: general

Topic: making isomorphism class a group


view this post on Zulip 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?

view this post on Zulip 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)]

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Mar 31 2018 at 19:57):

I have already constructed the quotient

view this post on Zulip Simon Hudon (Mar 31 2018 at 19:57):

Can you show it?

view this post on Zulip 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),
  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⟩⟩

view this post on Zulip Kenny Lau (Mar 31 2018 at 19:58):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 19:58):

the quotient is appropriately named something

view this post on Zulip Simon Hudon (Mar 31 2018 at 20:11):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 20:14):

right

view this post on Zulip Kevin Buzzard (Mar 31 2018 at 20:14):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 20:14):

you'll be surprised

view this post on Zulip Simon Hudon (Mar 31 2018 at 20:22):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 20:22):

to where?

view this post on Zulip Simon Hudon (Mar 31 2018 at 20:25):

Not sure yet

view this post on Zulip Simon Hudon (Mar 31 2018 at 20:28):

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.

view this post on Zulip Simon Hudon (Mar 31 2018 at 20:29):

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

view this post on Zulip Simon Hudon (Mar 31 2018 at 20:31):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 21:52):

@Simon Hudon do we even need the quotient?

view this post on Zulip Simon Hudon (Mar 31 2018 at 21:56):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 21:56):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 21:57):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:05):

@Kevin Buzzard this can be viewed in two ways

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:05):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:07):

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

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:07):

I'm wondering if you even need the sigma type

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:08):

I did it without any quotient

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:08):

and without injectivity

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:08):

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

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:08):

And sigma type?

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:08):

well the sigma type has UMP as pi type right

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:08):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:09):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:09):

am I speaking English

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:09):

that thing there with that sigma is no longer used

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:09):

I can't English

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:09):

What's UMP?

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:09):

universal mapping property

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:10):

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

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:10):

Ah I see

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:10):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:11):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:11):

called predicativity

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:12):

Cool, I'm all ears

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:12):

inductive types are predicative

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:12):

they're philosophically well-founded

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:12):

bigger things are built on top of smaller things

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:13):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:13):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:14):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:14):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:14):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:15):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:15):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:16):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:16):

ZFC is an impredicative theory

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:16):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:17):

the common construction of free group is predicative

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:17):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:19):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:19):

there's still a limitation on the size

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:19):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:20):

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

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:21):

Why is that a problem?

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:21):

it's not very well-founded is it

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:25):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:26):

well but one universe is already big enough

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:27):

philosophy aside, this construction is quite funny

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:28):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:29):

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

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:31):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:31):

ok

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:31):

Or Johannes

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:31):

It looks like a cool construction :)

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:41):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:41):

rip universe limitation

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:41):

now it can be in any universe

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:42):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:43):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:46):

@Simon Hudon this is such a convenient construction

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:46):

basically constructing an object from its UMP

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:46):

I can probably construct the abelianization this way also

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:48):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:48):

you've seen this construction before?

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:49):

I've seen it in free monads mostly

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:50):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:50):

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

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:52):

What happens when you replace it with an underscore?

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:52):

can't synthesize that thing

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:54):

Right but what instances are in your context?

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:54):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:54):

rather, they're introduced as variables

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:55):

because of how I defined ambient

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:56):

Right, so you can write:

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:56):

I thought definitions shouldn't have any tactics

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:57):

because they're difficult to destruct

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:58):

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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:58):

hmm...

view this post on Zulip Kenny Lau (Apr 01 2018 at 00:03):

free functors on steroids

view this post on Zulip Kenny Lau (Apr 01 2018 at 00:15):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 00:15):

comes with commutators for free!

view this post on Zulip Mario Carneiro (Apr 01 2018 at 01:13):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 01:15):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 01:16):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 01:20):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 01:57):

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.

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:19):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:20):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:20):

thus it's not computable

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:21):

ok, then what should I do?

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:21):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:22):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:23):

maybe you can phrase it independently of the choice then?

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:23):

phrase what?

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:23):

your theorem, whatever it is

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:23):

that free group exists?

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:24):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:24):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:24):

it's a limitation of lean too, I say

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:24):

I just stopped using it

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:24):

and then I constructed the free group and proved its property

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:24):

did you though?

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:24):

watch your universe levels

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:25):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:25):

I'm starting to suspect so

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:26):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:27):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:28):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:29):

oh

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:29):

I get it, go on

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:30):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:30):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:31):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:32):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:32):

fair enough

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:33):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:33):

hence what you mean by moving proof obligations around

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:33):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:33):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:34):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:36):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:36):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:37):

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

view this post on Zulip Mario Carneiro (Apr 01 2018 at 04:38):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 04:45):

I'm thoroughly confused now

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:26):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:27):

but it's just moving them to Lean universe problems

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:27):

same thought here

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:27):

Why do you care about isomorphic groups?

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:27):

Why not just work with all groups?

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:27):

right, I worked with all groups at the end

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:27):

I was following the paper, which used isomorphic groups

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:28):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:28):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:28):

which i take to be a really shitty thing to do

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:28):

That just seemed to be a red herring

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:28):

right

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:28):

I didn't use that in my construction

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:28):

but then it still depends on the universe

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:28):

since you're quantifying over every group anyway

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:30):

that's the thing with impredicative constructions

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:30):

you can send the other elements of SS to the identity

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:30):

Oh I broke zulip

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:30):

I can't edit $S$ into SS

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:33):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:33):

firstly you consider only the isomorphism classes

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:33):

Bingo, I had to reload the page.

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:33):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:33):

because in some sense you can build it from S

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:34):

I don't see where the subset comes in

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:34):

but I do see where the isomorphism classes come in

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:34):

well

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:34):

they are both limitations on the size of the set

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:35):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:35):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:35):

I want my generator to have size S

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:35):

exactly

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:36):

ah

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:36):

hmm

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:36):

that's what you meant

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:36):

I suppose it's ok then

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:37):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:43):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:45):

and give this a map from S

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:45):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:46):

This should definitely be in #maths


Last updated: May 14 2021 at 04:22 UTC