group_equiv

Stream: general

[Kevin Buzzard]

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/K$ if I know $H=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.

[Kevin Buzzard]

NB H and K have type set G

[Kevin Buzzard]

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

[Kevin Buzzard]

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}

[Kevin Buzzard]

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

[Assia Mahboubi]

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

Why isomorphism? Isn't this an equality?

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

/me got trolled...

[Assia Mahboubi]

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 $x$ and $y$ are two terms of a same type $T$, one can state, and may be even prove, an equality statement $x=y$. In this case, one can substitute any occurrence of $x$ for $y$. Well, almost all occurrences. For any 'context', i.e. for any $C$ of type $T \rightarrow Type$ (or $T \rightarrow Prop)$, one can turn $P(x)$ into $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 $T$ is a sort, and thus when $x$ and $y$ are types. But in this case, there are around occurrences of $x$ and $y$ that are not of the former nature, the ones that are on the right hand-side of a column, like in $t : x$. These cannot be affected by a "rewrite" : there is no way to turn $t:x$ into $t:y$ using $x = y$: the only useful thing here would be an $f : x \rightarrow y$, and in this case if $t:x$ then of course $f(t):y$. Unless you not only know that $x=y$ but in fact $x$ is convertible to $y$. 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).

[Assia Mahboubi]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Assia Mahboubi]

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/K$, and what usage do you want for this statement?

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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.

[Assia Mahboubi]

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/H$ at the level of types? What do you mean on paper by $G/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/H$ and $G/K$ refer to terms with distinct types, because the type of groups modded by $H$ (like $G/H$) is a priori different from the type of groups modded by $K$ (like $G/K$). But one has access to the corresponding sets of cosets, which are equal (like, for real), and can be endowed with group structures.

[Kevin Buzzard]

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.

[Assia Mahboubi]

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.

[Kevin Buzzard]

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.

[Assia Mahboubi]

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