n • G as a subgroup?

Stream: Is there code for X?

[Michael Stoll]

Is there really no better way to write the additive subgroup consisting of all n • g for g : G, where G is a commutative additive group, than

QuotientAddGroup.mk (s := map (nsmulAddMonoidHom (α := G) n) ⊤

?
(For n = 2, there is docs#AddSubgroup.even, but I was unable to find a more general version.)
Ideally, I would want to write n • G (which pretty certainly will not work), or at least n • (⊤ : Subgroup G).

[Eric Wieser]

docs#AddSubgroup.zmultiples ?

[Aaron Liu]

docs#AddSubgroup.zmultiples

[Michael Stoll]

That's not what I want: I want g to vary, with n fixed.

[Aaron Liu]

oh

[Eric Wieser]

Does n • (⊤ : AddSubgroup G) not work?

[Michael Stoll]

import Mathlib

variable {G : Type*} [AddCommGroup G]

#synth SMul ℤ (AddSubgroup G) -- fails

[Eric Wieser]

open scoped Pointwise

[Aaron Liu]

import Mathlib

variable {G : Type*} [AddCommGroup G]

open scoped Pointwise
#synth SMul ℤ (AddSubgroup G) -- failn't

[Eric Wieser]

docs#AddSubgroup.pointwiseMulAction is the instance

[Michael Stoll]

And while we are at it, is there a more idiomatic way to state that a s : Set G contains representatives of all cosets than

Set.SurjOn (QuotientAddGroup.mk (s := n • (⊤ : AddSubgroup G))) s ⊤)

?
There is the left hand side of docs#AddSubgroup.leftCoset_cover_const_iff_surjOn, but it doesn't appear to be more convenient to use...

[Snir Broshi]

cosets of which subgroup?

[Michael Stoll]

Cosets of n • G. (But which subgroup should not matter so much...)

[Snir Broshi]

s • H = ⊤, where H is the subgroup?

[Snir Broshi]

or are you looking for a more faithful translation rather than an equivalent statement

[Snir Broshi]

(actually I think I assumed we're using multiplication, so maybe we need +ᵥ instead)

[Snir Broshi]

import Mathlib

variable {G : Type*} [AddCommGroup G] (s : Set G) (H : AddSubgroup G)

open scoped Pointwise

def ContainsRepresentativesOfAllCosets : Prop := s +ᵥ (H : Set G) = ⊤
-- or `Set.univ` if `⊤` is weird here

[Michael Stoll]

Compare docs#AddSubgroup.leftCoset_cover_const_iff_surjOn ...
I'll see if it looks better.

[Richard Copley]

Michael Stoll said:

Compare docs#AddSubgroup.leftCoset_cover_const_iff_surjOn ...
I'll see if it looks better.

leftCoset_cover_const_iff_surjOn is really auxiliary to the main results in the file CosetCover which are, by and large, the ones mentioned the file's docstring.

If anything, it would be nice to eliminate leftCoset_cover_const_iff_surjOn in favour of some more generally useful lemma defined closer to the root of the hierarchy.

I don't know if something like the following would help.

import Mathlib.Data.Setoid.Partition
import Mathlib.GroupTheory.Coset.Basic

open scoped Pointwise

namespace Subgroup

variable {G : Type*} [Group G] (H : Subgroup G)

def leftCosets := { c : Set G | ∃ g : G, c = g • H }

theorem _root_.Setoid.isPartition_leftCosets : Setoid.IsPartition H.leftCosets := by
  constructor
  · rw [leftCosets, Set.notMem_setOf_iff]
    push_neg
    intro g
    use g • 1
    exact Set.smul_mem_smul_set H.one_mem
  · intro g
    use g • H
    simp [leftCosets, leftCoset_eq_iff, mem_leftCoset_iff, ← QuotientGroup.eq]

end Subgroup

example {G : Type*} [Group G] (H : Subgroup G) : ⋃₀ H.leftCosets = Set.univ :=
  (Setoid.isPartition_leftCosets H).sUnion_eq_univ

[Michael Stoll]

I'm now stating the condition that n • G has finite index in G as (nsmulAddMonoidHom (α := G) n).range.FiniteIndex, to avoid the problems mentioned in #mathlib4 > SMul diamond on subsets @ 💬 . It's less nice to read, but easier to work with. (See here.)