quotient groups

Stream: maths

[Antoine Chambert-Loir]

I have been willing to prove an obvious lemma on quotient groups, but I am struggling with basic syntax errors.
It seems I can't answer the following:

1. Under G: Type*, group G, N: subgroup G, normal N, one has a group quotient N. How to get its multiplicative law ? How to tell this law is commutative ?

2. Under an isomorphism such as the one in Noether's second isomorphism theorem G ≃* H, how to use that hypothesis ? (For example, to deduce a property of H from a property of G or conversely ?

Explicit solutions and/or links to the relevant parts of the documentation are welcome, I'm completely lost.

[Johan Commelin]

@Antoine Chambert-Loir (2) is a nasty problem. Humans find this trivial. Lean disagrees (sadly).

[Johan Commelin]

At the moment, we have to basically do the work ourselves. There is a tactic equiv_rw, but no promises that it will help with the property that you want to transfer.

[Johan Commelin]

For (1): what exactly do you have in mind? If you have x y : quotient N then x * y should "just work"

[Johan Commelin]

Or do you mean that you want to look under the hood of x * y?

[Johan Commelin]

That would be a job for widgets. In VScode, in your goal state, click on the * and drill down. You can use the buttons in the pop-up window to "go to definition" etc.

[Johan Commelin]

(To get a goal state with widgets, just write example : x * y = x * y := begin .. end

[Alex J. Best]

For (2) we also found quite often that a stronger property than transferring along equivalences was true, e.g. noetherianness descends down any surjective map so that property is the one that should be proved and applied rather than something specifically for equivalences. At least this way it feels like you are proving a real result if you have to do the work yourself, rather than something super obvious mathematically speaking.

[Kevin Buzzard]

I no longer have any good example of a natural mathematical property that moves along isomorphisms and which doesn't move along a more general kind of map. My go-to example was being a local ring, which doesn't move along surjections for the stupid reason that the target could be 0. But being "pre-local" (having at most one maximal ideal) does and the rest is easy.

In short Antoine, every mathematical definition you make (like being Cohen-Macauley or whatever) has to satisfy a basic sanity test within the formal framework that you make it (eg it doesn't talk about elements of elements of the ring or whatever) in order to check that it passes along isomorphisms. It's easy to give examples of predicates which don't pass along isomorphisms eg "I am equal to the integers". I used to be very upset that there wasn't some magic tactic which moved mathematically meaningful predicates along isomorphisms but when I discovered that most predicates I could think of passed along surjections or injections or other nice classes of maps, and that such theorems were typically in the library, I decided to just wait and see whether this was something I could live with, and it turned out that I could.

[Antoine Chambert-Loir]

Thanks to your comments, I could make some progress, but I fear my question is even more basic Lean coding.

I am actually given some isomorphism φ : G ≃* H' by quotient_inf_equiv_prod_normal_quotient', I know that G is commutative, and I need to prove that H is commutative. What I understand mathematically, @Alex J. Best and @Kevin Buzzard , is that, mathematically, the surjectivity of φ suffices to my goal.

Question : How do I recover the surjectivity of that map (which is proved in quotient_ker_equiv_of_surjective…

[Kevin Buzzard]

you have to write down the proof youself (h1+h2=phi (phi.symm (h1 + h2))=phi(phi.symm h1 + phi.symm h2)=...) or find the theorem in the library which says that if G is commutative and G -> H is a surjection then H is commutative.

[Kevin Buzzard]

PS I can't find it in the library

[Johan Commelin]

@Antoine Chambert-Loir φ.surjective should work

[Antoine Chambert-Loir]

Kevin Buzzard said:

PS I can't find it in the library

There is something like that in data.equiv.basic, but it seems ≃* does not return the correct type…

[Kevin Buzzard]

import tactic

lemma group.commutative_of_surjective_of_commutative {G H : Type*} [group G] [group H] (φ : G →* H)
  (hφ : function.surjective φ) (hG : ∀ a b : G, a * b = b * a) : ∀ a b : H, a * b = b * a :=
begin
  choose s hs using hφ,
  intros a b,
  have h : s a * s b = s b * s a := hG _ _,
  apply_fun φ at h,
  simpa [φ.map_mul, hs] using h,
end

[Johan Commelin]

Or maybe φ.to_equiv.surjective

[Alex J. Best]

There is docs#function.surjective.comm_group

[Kevin Buzzard]

PS Antoine yesterday I was faced with proving that two empty types were isomorphic ;-) Formalising is sometimes slow! But it's straightforward if you keep your head...

[Johan Commelin]

Right, so hopefully you can write φ.to_equiv.surjective.comm_group _ _ _ _ _ (add or remove _ as needed).

[Johan Commelin]

@Antoine Chambert-Loir If you provide a MWE, then we can tell you exactly how to apply it.

[Kevin Buzzard]

You'll also have to make the comm_group instance on G.

[Kevin Buzzard]

Antoine I spent 6 months doing a bunch of even easier stuff than this ("introduction to proof" level stuff) before I felt confident to go on to schemes.

[Johan Commelin]

I was assuming that G already had such an instance

[Kevin Buzzard]

Right, but it could be a group with hG : \forall a b, a * b = b * a

[Kevin Buzzard]

I spent the first six months working out what the right questions were. For example "what is the formula for the multiplication on quotient N?" is a wrong question. The definition of the product has come from a diagram chase which boils down to (two applications of) the universal property of quotients, which is an inbuilt axiom ie has no proof. The correct question is what the API for the quotient is ie what are the theorems in the library which enable you to do everything you ever want to do with the multiplication on the quotient without ever seeing its definition.

[Kevin Buzzard]

Quotients are opaque in Lean, they are not sets of equivalence classes or whatever. However they come with a robust API so this doesn't get in the way. The theorem that equivalence relations are the same as partitions is in mathlib but is never used.

[Alex J. Best]

Rather interestingly the following works:

import algebra.group.hom_instances
import algebra.group.inj_surj


lemma a {G H : Type*} [comm_group G] [group H] (f : G →* H) (hf : function.surjective (f : G → H))
  (x y : H) : x * y = y * x :=
begin
  letI := function.surjective.comm_group f hf (monoid_hom.map_one _)
    (monoid_hom.map_mul _) (monoid_hom.map_inv _) (monoid_hom.map_div _),
  rw mul_comm,
end

I wasn't sure if lean would be able to handle this, as we now have two group instances on H, the fields should refer to the same operations though, so thats why it works out. Unsure if this goes ok with more complicated examples.

[Kevin Buzzard]

The other issue Antoine is that you are not supplying a #mwe . The reason this is so important is that there are sometimes several different ways in lean to say one thing in maths. For example your claim "I know that G is commutative" can either mean "I have a term of type group G and a proof of \forall a b, a*b=b*a, or "I have a term of type comm_group G" and of course there's the same issue for the conclusion that H is commutative. This means that sometimes people can talk at cross purposes -- the answers will be slightly different in each case. If you don't say "I want to prove H is commutative" but instead post a self-contained piece of lean code which compiles for everyone then suddenly your question is crystal clear.

[Eric Wieser]

@Alex J. Best, the whole point in the surjective APIs like that one is that they don't construct any new data, and just reuse the existing data

[Antoine Chambert-Loir]

I saw your remark, @Kevin Buzzard , and tried to produce a #mwe. (The issue for me is to have it minimal).
I could produce a proof.

import group_theory.coset
open function

/-- If G and H have multiplications *
and φ : G → H is a surjective multiplicative map,
and if G is commutative, then H is commutative.

Since I only use it with groups,
I should probably use function.surjective.comm_semigroup
--/
lemma surj_to_comm {G H : Type*} [has_mul G] [has_mul H] (φ: mul_hom G H) :
   surjective φ → is_commutative G (*) → is_commutative H (*) :=

begin
  intros is_surj is_comm,
  apply is_commutative.mk,
  intros a b,
    obtain ⟨a', ha'⟩ := is_surj a, obtain ⟨b', hb'⟩ := is_surj b,
    rw ← ha', rw ← hb',
    let z := ⇑φ, let z₂ := φ.to_fun, have : z = z₂  , by refl,
    rw ← mul_hom.map_mul φ a' b',
    rw ← mul_hom.map_mul φ b' a',
    apply φ.congr_arg,
    refine is_commutative.cases_on is_comm _, intro,
    exact comm a' b',
end

[Antoine Chambert-Loir]

For the rest, I see another issue appearing in test2 below.
I have a complicated subquotient, which is a quotient, but I can't have Lean understand it.

import group_theory.coset
import group_theory.abelianization
import group_theory.quotient_group

open function


variables {G : Type*} [group G] (N : subgroup G) [nN : N.normal] (H : subgroup G)
include nN

lemma test₁ : is_commutative (quotient_group.quotient N) (*) ↔ commutator G ≤ N :=
begin
  split,
  { /-  intro is_comm,
     let hcomm : ∀ (a b: quotient_group.quotient N), a * b = b * a
        := is_commutative.cases_on is_comm id , -/
    rintro ⟨hcomm : ∀ (a b: quotient_group.quotient N), a * b = b * a ⟩,
    rw commutator, apply subgroup.normal_closure_subset_iff.1,
    intros x hx, simp at hx, obtain ⟨p, q, hpq⟩ := hx,
    -- suffices hpq': p * q = x * q * p ,
    apply (quotient_group.eq_one_iff x).1,
    rw ← hpq, simp,
    specialize hcomm ↑p ↑q,
    rw mul_inv_eq_one,
  apply mul_inv_eq_iff_eq_mul.2, assumption, assumption, },
  { intro hGN, refine is_commutative.mk _,
    intro x', apply quotient_group.induction_on x', intro x,
    intro y', apply quotient_group.induction_on y', intro y,
    have hxy: (x * y)⁻¹ * (y * x)  ∈ N,
    begin
      simp, rw ← mul_assoc,
      apply set.mem_of_mem_of_subset _ hGN,
      rw commutator,
      apply subgroup.subset_normal_closure, simp,
      existsi y⁻¹ , existsi x⁻¹ , rw inv_inv x, rw inv_inv y,
    end,
    apply quotient_group.eq'.2 hxy, },
end

lemma test₂ (hHN : H ⊔ N = ⊤) (hH: subgroup.is_commutative H) :
  commutator G ≤ N
  :=
begin
  let Q₁ := (quotient_group.quotient ((H ⊓ N).comap H.subtype)) ,
  let Q₂  := quotient_group.quotient (subgroup.comap (H ⊔ N).subtype N),
  let equiv := quotient_group.quotient_inf_equiv_prod_normal_quotient H N,
  let φ :=  mul_equiv.to_mul_hom equiv,
  let hφ := equiv.surjective,
  -- Q₁ is commutative as a quotient of the commutative group N
  have hc₁ : is_commutative Q₁ (*) := comm_semigroup.to_is_commutative,
  --Q₂ is commutative as isomorphic to Q₁
    have hc₂ : is_commutative Q₂ (*) := surj_to_comm φ hφ hc₁,
  -- Deduce (from Q₂ and hc₂, and hHN) that quotient N is commutative
  have hc : is_commutative (quotient_group.quotient N) (*) ,
  sorry,

  -- Deduce that commutator G ≤ N, using test₁ : is_commutative (quotient_group.quotient N) (*) ↔ commutator G ≤ N
  exact (test₁ N).1 hc,
end

[Antoine Chambert-Loir]

Kevin Buzzard said:

Quotients are opaque in Lean, they are not sets of equivalence classes or whatever. However they come with a robust API so this doesn't get in the way. The theorem that equivalence relations are the same as partitions is in mathlib but is never used.

I believe I am happy with this, at least category theoretically… My trouble is in understanding how to use the API…
For example, I spent a long time guessing how to use is_commutative (via is_commutative.mk or is_commutative.dcases). Is it explained explicitly somewhere, in the mathlib files ? in a general documentation ? Is it hoped that somebody adds it at some point ?
And instances are still kind of sorcery to me. (I could not find any explicit enough explanation.)

[Eric Wieser]

If you look at src#is_commutative, I think it's just a one-field structure

[Eric Wieser]

It's awkward to use because it's supposed to be used as a typeclass, but also because it was also part of a refactor of lean itself that was abandoned

[Eric Wieser]

docs#commutative (mathlib not lean, and not a typeclass) might be easier to work with

[Kevin Buzzard]

Re the proof: the way you've set things up I agree that this is now messy to finish. To change H ⊔ N to ⊤ you can use docs#quotient_group.equiv_quotient_subgroup_of_of_eq but I'm not sure this is the easiest way forward. You can use docs#quotient_group.map to write down the map from Q2 to G/N but then you have to prove it's surjective, and I don't see that lemma. Probably the shortest route to the end is to show that if G -> H is surjective then G/N -> H/M is surjective (conditions as in the map lemma) and deduce it from that. This is one of these situations where type theory is a lot messier than set theory. See all the kerfuffle before the isomorphism theorems, and all the various ways they've been stated.