Zulip Chat Archive

Stream: general

Topic: Aligning submodule.quotient and add_subgroup.quotient

Eric Wieser (Feb 16 2022 at 21:58):

Right now these two aren't defeq:

import data.rat.basic
import linear_algebra.quotient
import algebra.algebra.basic
def qmodz := ℚ ⧸ (algebra_map ℤ ℚ).range.to_add_subgroup
def qmodz' := ℚ ⧸ (algebra.linear_map ℤ ℚ).range
example : qmodz = qmodz' := rfl  -- fails

The first quotient is by the relation -x + y ∈ s (docs#quotient_add_group.left_rel), the second by x - y ∈ s (docs#submodule.quotient_rel). Can we change them to match? Or is there a good reason for different conventions here?

Kevin Buzzard (Feb 16 2022 at 22:15):

Mathematically there's no reason of course -- I can quite imagine people chose essentially randomly

Yaël Dillies (Feb 16 2022 at 22:19):

I remember there being some reason to prefer one over the other... cancellation happening better one way, but I don't remember the details.

Eric Wieser (Feb 16 2022 at 23:10):

Presumably we're stuck with the add_group one because left cosets are "standard" for quotients?

Eric Wieser (Feb 16 2022 at 23:12):

In which case, I guess we only have the option of changing the submodule one

Yury G. Kudryashov (Feb 17 2022 at 00:20):

Yury G. Kudryashov (Feb 17 2022 at 00:22):

What do you think about using orbits.rel for all these quotients? This way we don't get nice definitional equalities for x ≈ y but we'll be able to apply theorems about quotients by group actions to group/module quotients.

Eric Wieser (Feb 17 2022 at 00:23):

(docs#orbits.rel? docs#orbit_rel?)

Eric Wieser (Feb 17 2022 at 00:25):

Ah, it's docs#mul_action.orbit_rel

Reid Barton (Feb 17 2022 at 11:12):

Seems reasonable to me because "by hand" reasoning about elements that become equal in the quotient should go through some API anyways. On the other hand, it's not yet clear to me what specifically we gain

Reid Barton (Feb 17 2022 at 11:14):

but it seems plausible that somewhere, you would want to think of G/H as the orbits of G under multiplication by H (probably in the non-abelian and maybe non-normal case)

Yury G. Kudryashov (Feb 17 2022 at 13:12):

I want to generalize docs#measure_theory.is_fundamental_domain.smul_invariant_measure_map and other theorems in the same files from "quotient group" to "quotient by a group action", then be able to apply the more general theorem to get the old one for free.

Eric Wieser (Apr 23 2022 at 05:06):

I've made the change to align these in #13620

Eric Wieser (Apr 23 2022 at 05:07):

I haven't gone as far as using orbit.rel, mainly because it creates more work and I don't care about it (yet)

Last updated: Dec 20 2023 at 11:08 UTC