Zulip Chat Archive

Stream: general

Topic: group_equiv


view this post on Zulip Kevin Buzzard (Mar 04 2019 at 14:13):

structure group_equiv extends G  H :=
{ hom : is_group_hom to_fun}

I'm making group_equiv because it is convenient to have it for the perfectoid project. It's not finished yet but for what it's worth here's the current state:

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/group.lean

My question is: I have just realised that I want that if H and K are both normal subgroups of a group G, and if h : H = K, I want the obvious term of type group_equiv (quotient H) (quotient K). Mathematically, I want to write down the isomorphism G/H=G/KG/H=G/K if I know H=KH=K.

Should this construction be part of the API, or is a ridiculous thing to prove? If H = K but the proof is not rfl then it seems to me that type theory would like me to define this term explicitly, and use it where necessary. Have I understood this correctly? I'm happy to prove it, I just want to check I'm not wasting my time.

view this post on Zulip Kevin Buzzard (Mar 04 2019 at 14:16):

NB H and K have type set G

view this post on Zulip Kevin Buzzard (Mar 04 2019 at 16:07):

Is this missing?

import group_theory.quotient_group

variables (G : Type*) [group G]

lemma quotient_group.ker (N : set G) [normal_subgroup N] :
is_group_hom.ker (quotient_group.mk : G  quotient_group.quotient N) = N := sorry

view this post on Zulip Kevin Buzzard (Mar 04 2019 at 16:50):

def quot_eq_of_eq {G1 : set G} [normal_subgroup G1] {G2 : set G} [normal_subgroup G2]
(h : G1 = G2) : group_equiv (quotient G1) (quotient G2) :=
{ to_fun := λ q, quotient.lift_on' q (quotient_group.mk : G  quotient G2) $ λ a b hab, quotient.sound'
  begin
    change a⁻¹ * b  G1 at hab, rwa h at hab
  end,
  inv_fun := λ q, quotient.lift_on' q (quotient_group.mk : G  quotient G1) $ λ a b hab, quotient.sound'
  begin
    change a⁻¹ * b  G2 at hab, rwa h at hab,
  end,
  left_inv := λ x, by induction x; refl,
  right_inv := λ x, by induction x; refl,
  hom := quotient_group.is_group_hom_quotient_lift
    G1 _ $ λ x hx, by rwa [h, quotient_group.ker G2, is_group_hom.mem_ker] at hx}

view this post on Zulip Kevin Buzzard (Mar 04 2019 at 16:51):

The proof for hom should be by apply_instance but I couldn't convince Lean that it knew all the instances.

view this post on Zulip Assia Mahboubi (Apr 04 2019 at 15:33):

Mathematically, I want to write down the isomorphism G/H=G/KG/H=G/K if I know H=KH=K.

Why isomorphism? Isn't this an equality?

view this post on Zulip Patrick Massot (Apr 04 2019 at 15:37):

Oh, Assia is back! She even pretends to be a stupid mathematician like us

view this post on Zulip Johan Commelin (Apr 04 2019 at 15:42):

@Patrick Massot You might as well try to answer her question...

view this post on Zulip Johan Commelin (Apr 04 2019 at 15:42):

@Assia Mahboubi It seems to give lots of headaches and back pains if you try to treat this as an equality.

view this post on Zulip Johan Commelin (Apr 04 2019 at 15:43):

I still don't completely understand why and I still lament it. But it seems to have something to do with dependent type theory.

view this post on Zulip Johan Commelin (Apr 04 2019 at 15:43):

Is this not a problem in Coq? You do have DTT, right?

view this post on Zulip Patrick Massot (Apr 04 2019 at 15:52):

Johan, I don't think Assia is asking a question here...

view this post on Zulip Johan Commelin (Apr 04 2019 at 16:26):

/me got trolled...

view this post on Zulip Assia Mahboubi (Apr 04 2019 at 16:35):

Hi @Johan Commelin ! Yes, may be this has to do with (equality in) type theory. So in type theory, there are terms and there are types. If xx and yy are two terms of a same type TT, one can state, and may be even prove, an equality statement x=yx=y. In this case, one can substitute any occurrence of xx for yy. Well, almost all occurrences. For any 'context', i.e. for any CC of type TTypeT \rightarrow Type (or TProp)T \rightarrow Prop), one can turn P(x)P(x) into P(y)P(y), by applying a lemma expressing the so-called "elimination rule of equality". Now in the flavour of dependent type theory we all like, types are themselves terms. So the latter also apply when TT is a sort, and thus when xx and yy are types. But in this case, there are around occurrences of xx and yy that are not of the former nature, the ones that are on the right hand-side of a column, like in t:xt : x. These cannot be affected by a "rewrite" : there is no way to turn t:xt:x into t:yt:y using x=yx = y: the only useful thing here would be an f:xyf : x \rightarrow y, and in this case if t:xt:x then of course f(t):yf(t):y. Unless you not only know that x=yx=y but in fact xx is convertible to yy. And then indeed the conversion rule does the job. Conclusion: stating equality between types is mostly useless (i.e. not more useful than an equivalence).

view this post on Zulip Assia Mahboubi (Apr 04 2019 at 16:39):

But in Kevin's case, I would say that G/HG/H and G/KG/K should be equal as elements of set (set G). Sander, sitting next to me, suggests you could even attach more data if needed.

view this post on Zulip Patrick Massot (Apr 04 2019 at 16:41):

G/H is a type in our setup (remember we love quotient types in Lean)

view this post on Zulip Patrick Massot (Apr 04 2019 at 16:42):

https://github.com/leanprover-community/mathlib/blob/78f1949719676db358ea5e68e211a73e2ce95e7b/src/group_theory/coset.lean#L160

view this post on Zulip Assia Mahboubi (Apr 04 2019 at 16:44):

I know. But may be this is not the best (let's say the only) way to express what you want. What do you want to express by G/H=G/KG/H=G/K, and what usage do you want for this statement?

view this post on Zulip Patrick Massot (Apr 04 2019 at 16:50):

I don't know what @Kevin Buzzard had in mind

view this post on Zulip Mario Carneiro (Apr 04 2019 at 17:55):

I think the situation is that we want to say H=KG/HG/KH = K\implies G/H\cong G/K, because HH and KK are sets (so they have a nice notion of equality) but G/HG/H and G/KG/K are groups, so the right notion of equality is group isomorphism

view this post on Zulip Mario Carneiro (Apr 04 2019 at 17:57):

I think Coq avoids this problem by doing "subgroup theory", so that G/H and G/K are also sets (of equivalence classes or something), in some big ambient group

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:19):

I am sufficiently confused by equality in type theory that I don't know whether Assia is trolling or not :-)

view this post on Zulip Patrick Massot (Apr 04 2019 at 18:21):

Hint: Assia mentioned several time that she thought very hard about this kind of question and wrote https://hal.inria.fr/hal-00825074v1/document that was already cited many times here

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:24):

The application was some technical result in valuation theory; if two valuations are equivalent then one is continuous if and only if the other one is. This comment of course clarifies essentially nothing. But I wrote down a careful proof of this on paper and then broke it up into tiny pieces. In some sense I am quite proud of the valuations API we have in the perfectoid project. It looks as much like a mathlib file as anything I have ever written. Many proofs are just a few lines long. The reason for this is that I am beginning to understand how to write code in these dependent type theory languages. I isolated this fact as something I needed, I was proving a whole bunch of groups were isomorphic, so I set up the notion of group_equiv and just did it the way one is supposed to do things, proved group_equiv.trans etc and proved that continuity was constant on equivalence classes.

I needed it because it is a basic fact about groups and it seemed to be a step in the process where rewriting was not such a wise idea, in short. I actually rewrote my proof so that the defining map was directly made using the quotient API; initially it was some composition which was much harder to work with.

view this post on Zulip Assia Mahboubi (Apr 05 2019 at 13:10):

Hi @Kevin Buzzard ! Thanks for explaining the context! I am not trolling by the way. And I think this is not so much about subgroup theory (or Lean vs Coq). But about the fact that types and sets are not the same in particular because they cannot be "substituted" in the same way. That's what I meant in my long message above.

My question is why would one need to state this G/K=G/HG/K=G/H at the level of types? What do you mean on paper by G/K=G/HG/K=G/H? I would say I mean that the group datas (carrier, law) are the same. And any further stuff needed should follow from the canonical group structure endowed by these sort of things. I would say that this is not what an equality stated at the level of types provides.

@Mario Carneiro , even in the Coq library you refer to, the notations G/HG/H and G/KG/K refer to terms with distinct types, because the type of groups modded by HH (like G/HG/H) is a priori different from the type of groups modded by KK (like G/KG/K). But one has access to the corresponding sets of cosets, which are equal (like, for real), and can be endowed with group structures.

view this post on Zulip Kevin Buzzard (Apr 05 2019 at 13:20):

Mathematicians use = to mean "canonically isomorphic" sometimes, where "canonical" does not have a general definition but one can often pin down what they mean.

Quotients could be thought of as being only uniquely defined up to unique isomorphism, but actually in ZFC mathematicians are often taught that the quotient "equals" the set of equivalence classes. Because of this, the two quotients really are equal in ZFC. In general there are many objects in maths which are only defined up to canonical isomorphism (universal objects are a great example, they are defined up to unique isomorphism, which is a much clearer statement). However you can imagine more than one way of constructing the object. Mathematicians don't care which way they use, because we treat these objects in a different way to computer scientists. You guys need defintions. We are completely happy with properties defining the object up to unique isomorphism. I don't care what "the group of order two" is when I'm being a mathematician, and if G and H are two groups of order 2 I would happily write G=H. Things are much more delicate in your world, which in some sense reflects a way that type theory does not capture the true essence of mathematics.

view this post on Zulip Assia Mahboubi (Apr 05 2019 at 14:05):

type theory does not capture the true essence of mathematics.

I do not know. But I guess that whatever the foundation style, one needs to get the definitions right otherwise things soon get unnecessarily more delicate. I am somehow claiming here that in your case you could have things behave as smoothly as in ZFC, if you renounce to a Type layer which, again in this case, seems to bring more troubles than support.

Anyway, I am happy to read that you eventually managed to find a satisfactory way out, which is ultimately the important criterium.

view this post on Zulip Kevin Buzzard (Apr 05 2019 at 14:45):

In my mind, the quotient G/H is only defined up to canonical isomorphism but we are happy to use = to represent this, and furthermore we are happy to rewrite with this equality because we know how to treat groups and we would never ask a question of them for which the answer depended on anything other than the information of the group up to isomorphism. This is why it is frustrating not to be able to make these rewrites.

view this post on Zulip Assia Mahboubi (Apr 05 2019 at 16:13):

Performing these substitutions would be way easier if groups were not types (beyond this very specific example where the datas are equal).


Last updated: May 12 2021 at 05:19 UTC