pi subgroups

Stream: Is there code for X?

[Joachim Breitner]

I see we have

/-- Given subgroups H, K of groups G, N respectively, H × K as a subgroup of G × N. -/
def subgroup.prod {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) (K : subgroup N) : subgroup (G × N)

but I don’t see corresponding notions for subgroups of pi groups (i.e. infinite products). Are they missing so far?

[Yaël Dillies]

It would be called subgroup.pi, so I guess we don't!

[Joachim Breitner]

Ok, on it.

[Joachim Breitner]

Why is some groupy theory stuff under algebra(e.g. algebra.group.pi) and others under group_theory? How to decide what goes where?

[Yaël Dillies]

It depends on whether you see group as an algebraic structure belonging in the algebraic hierarchy, or as an object of study of its own. The separation is quite empirical.

[Joachim Breitner]

Before I go on proving the necessary lemmas (like those that we have for subgroup.prod), how is this for the definition?
https://github.com/leanprover-community/mathlib/pull/11801/files

[Yaël Dillies]

You can simplify the def of carrier to {f | ∀ i, f i ∈ s i} but I'm not sure it's terribly useful.

[Joachim Breitner]

It would make these silly trivial arguments go away, and some of the lemmas would become refl that otherwise aren’t. But it would mean not using set.pi. But maybe it’s nicer indeed.

[Yury G. Kudryashov]

Another option is to copy API of set.pi and take an argument I : set η

[Joachim Breitner]

Hmm, not sure how useful that’s is. \Pi doesn’t have an I, so why expect it for subgroups. We can generalize later if needed?

[Yury G. Kudryashov]

I don't know if it's useful either. Depends on how often you want to restrict only some coordinates.

[Yury G. Kudryashov]

If you don't go this way, then you should drop set.pi and do what @Yaël Dillies suggested.

[Yaël Dillies]

Agreed with everything Yury said.

[Eric Wieser]

Do we have docs#submodule.pi?

[Eric Wieser]

Yes, we do - so the subgroup API should match

[Joachim Breitner]

Hmm, ok, fair point. Will adjust.