two different quotients by subgroup

Stream: maths

[Heather Macbeth]

We have

import group_theory.group_action.basic

example {G : Type*} [group G] (H : subgroup G) :
  (@mul_action.orbit_rel H.opposite G _ _).r = (quotient_group.left_rel H).r :=
begin
  ext i j,
  change _ ∈ set.range _ ↔ _ ∈ H,
  split,
  { rintros ⟨h, rfl⟩,
    convert H.inv_mem h.prop,
    change  (_ * _)⁻¹ * _ = _,
    simp },
  { intros h,
    let x : H.opposite := ⟨mul_opposite.op (i⁻¹ * j)⁻¹, H.inv_mem h⟩,
    use x,
    change j * _⁻¹ = _,
    simp }
end

[Heather Macbeth]

But these are not defeq. So the quotients by the associated setoids are not the same type.

[Heather Macbeth]

I encountered this when trying to use docs#t2_space_of_properly_discontinuous_smul_of_t2_space (which uses the first quotient) on a quotient group (which is created from the second quotient).

[Heather Macbeth]

Not sure how to fix this ...

[Eric Wieser]

I think I remember @Yury G. Kudryashov suggesting in the past that we redefine left_rel in terms of orbit_rel

[Eric Wieser]

(I already redefined submodule quotients to match additive quotients, so I think such a change would be reasonable)

[Yury G. Kudryashov]

I see two ways to fix this.

1. Redefine group/submodule quotients to use mul_action.orbit_rel.
2. Reformulate your statement in terms of (proj : X → Y) (h : quotient_map proj) (h' : proj x = proj y <-> ...).
   I prefer the first approach but I have no time to do this refactor myself.

[Yury G. Kudryashov]

BTW, should we redefine orbit_rel so that it is always an equivalence relation? E.g., x ~ y if there exist a and b such that ax = by.

[Heather Macbeth]

Yury G. Kudryashov said:

BTW, should we redefine orbit_rel so that it is always an equivalence relation? E.g., x ~ y if there exist a and b such that ax = by.

If I remember correctly, @Joseph Myers did something like this in the special case of docs#ray_vector.setoid

[Heather Macbeth]

Yury G. Kudryashov said:

I prefer the first approach but I have no time to do this refactor myself.

OK, I'm trying this out in branch#var-quotient, but I still don't have a sense of how big a refactor it would be.

[Heather Macbeth]

The first real consequence of the refactor I've encountered is that it breaks the following, which used to be definitional equalities:

import group_theory.coset

variables (G : Type*) [group G] (H : subgroup G)

example :
  @quotient_group.left_rel G _ H = @quotient_add_group.left_rel (additive G) _ H.to_add_subgroup :=
rfl

example : (G ⧸ H) = (additive G ⧸ H.to_add_subgroup) := rfl

Still trying to figure out exactly why, and whether this defeq is something worth caring about.

[Heather Macbeth]

Perhaps the more natural way to phrase this is that

example : additive (G ⧸ H) = (additive G ⧸ H.to_add_subgroup) := rfl

breaks. So I claim we have to choose between that and

example : quotient (mul_action.orbit_rel H.opposite G) = (G ⧸ H) := rfl

(the goal of the refactor).

[Kevin Buzzard]

I have been doing category theory in Lean for a while and have kind of become immune to this phenomenon -- I expect things to be isomorphic, not equal (equality is kind of banned in category theory). If M=N then G/M and G/N are not equal in Lean, or perhaps not equal without some pain attached; instead we write down an isomorphism between them: docs#quotient_group.equiv_quotient_of_eq (and the proof is nothing like refl). This has the same feeling.

[Heather Macbeth]

Indeed, but by the same logic maybe the whole refactor is not worth while, and instead we should go with Yury's second suggestion?

[Heather Macbeth]

On the other hand, @Yury G. Kudryashov considered this the less preferable option of the two.

[Heather Macbeth]

I wonder if we can fix it by redefining the group quotient using right rather than left cosets, which avoids the need for opposite ...

[Yury G. Kudryashov]

Another approach: you use your proof to define isomorphisms (equiv, homeomorph, measurable_equiv) between two quotient spaces, then use these isomorphisms to transfer some properties.

[Yury G. Kudryashov]

I'm not sure which approach is better in the long term.

[Eric Wieser]

Heather Macbeth said:

Still trying to figure out exactly why,

Here's some progress:

import group_theory.coset

variables (G : Type*) [group G] (H : subgroup G)

example :
  @quotient_group.left_rel G _ H =
    (@quotient_add_group.left_rel (additive G) _ H.to_add_subgroup).comap additive.of_mul :=
begin
  ext,
  dsimp [quotient_group.left_rel, quotient_add_group.left_rel, mul_action.orbit_rel,
    add_action.orbit_rel, setoid.rel, mul_action.orbit, add_action.orbit, subgroup.opposite,
      add_subgroup.opposite, set.range, set_like.has_coe_to_sort, subgroup.set_like,
         add_subgroup.set_like, submonoid.to_add_submonoid, function.on_fun, coe_sort,
          set_like.has_mem, set.preimage, additive.add_action, add_action.to_has_vadd,
          op_smul_eq_mul, subgroup.mul_action, submonoid.mul_action],
  sorry
end

[Eric Wieser]

attribute [semireducible] mul_opposite fixes your original issue

[Eric Wieser]

For some reason docs#mul_opposite is irreducible but docs#add_opposite is semireducible

[Heather Macbeth]

Thanks for the detective work @Eric Wieser !!

[Eric Wieser]

I'm not sure whether or not mul_opposite _should_ be irreducible, but at any rate people who care about the defeq you mention are likely to want to make mul_opposite semireducible locally anyway

[Eric Wieser]

This does raise that even with structure eta in Lean 4, making multiplicative a structure loses some useful defeqs

[Heather Macbeth]

#15045