Where does this subgroup theorem belong, if anywhere?

Stream: general

[Martin C. Martin]

There's a theorem that any subset of a group that is also a group, must be non-empty and closed under the operation & inverse.

Mathlib embodies the opposite direction: the Subgroup class embodies "subset that includes 1, is closed under * and inverse" and has a toGroup that give the Group object corresponding to the subset.

AFAIK, the opposite doesn't exist explicitly in Mathlib. It's an important part of an undergraduate education, that those conditions aren't just sufficient but also necessary. But it's implicit in mathlib, not explicit. For example, there's only one way to create a Subgroup, by giving those 3 conditions, and every Subgroup has them.

The Xena project, one of its goals "is to get the main results of all of the pure maths courses in Imperial's undergraduate curriculum formalised in Lean's maths library." So does this belong in mathlib? On the one had, I'd argue it's a main result of group theory. On the other hand, in software at least, a library is a collection of things that are useful in creating applications, but don't contain applications themselves. In other words, library code is a set of things useful for proving theorems, and in this view should only contain things that a user might use, rather than results that e.g. show a condition is not just sufficient but also necessary.

Thoughts?

[Jireh Loreaux]

Martin, I tried to address this in the other thread, but let me explain again. When mathematicians say that "any subset of a group that is also a group†, must be non-empty and closed under the operation and inverse" (†of course, this means "with the inherited operations", otherwise the claim is patently false), they are being very sloppy, as it's essentially circular.

1. Of course it's nonempty (all groups have an identity); this is maybe the only piece with meaningful content.
2. In order for the subset to have "inherited operations" it is a prerequisite to the definition of those operations that the subset is closed under them.

[Jireh Loreaux]

Suppose G is a group. Then there are operations (· * ·) : G → G → G and (· ⁻¹) : G → G. If H : Set G, then we can always get operations mulH : H → H → G and invH : H → G given by mulH h₁ h₂ := (h₁ : G) * (h₂ : G) and invH h₁ := (h₁⁻¹ : G). But for H to be a group, we need these operations to be H → H → H and H → H. And to ensure that (and they agree when coerced to G), must presuppose that H is closed under these operations.

[Martin C. Martin]

@Yakov Pechersky gave (most of) a proof. He formalized it this way:

import Mathlib.GroupTheory.Subgroup.Basic

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

def toSubgroup (h : ∀ x y : H, ((x * y : H) : G) = x * y) : Subgroup G where ...

This seems like a great way to formalize it, at least to me. Is there a place for this somewhere, either in mathlib or somewhere else?

Subgroup.toGroup is basically "given a subgroup, give a constructive proof that it's a Group by constructing a Group object."

Having an analogous toSubgroup function for the other direction makes sense to me.

[Jireh Loreaux]

If you really want something, there's this:

import Mathlib.GroupTheory.Subgroup.Basic

-- This says that `G` is a group, and `H` is a subset of `G` which is also a group with some,
-- possibly different, operations, but the coercion ("identity") map which sends every `h : H` to
-- `h : G` is a homomorphism, which means that the operations on `H` agree with the operations on
-- `G`.
variable {G : Type*} [Group G] (H : Set G) [Group H] (f : H →* G) (h_f_eq_val : ∀ x, f x = x)

example : (MonoidHom.range f : Set G) = H := by
  ext x
  refine ⟨?_, (⟨⟨x, ·⟩, h_f_eq_val _ ▸ rfl⟩)⟩
  rw [@SetLike.mem_coe]
  rintro ⟨x, rfl⟩
  exact h_f_eq_val x ▸ x.2

[Jireh Loreaux]

But again, we don't want this in Mathlib because it's essentially just chasing one's tail.

[Kevin Buzzard]

Martin: at school I was taught that one of the axioms of a group was "closure", i.e. "if x and y are in the group, then x*y is in the group". At university I was taught that "closure" was not an axiom, and indeed if you look at the definition of a group on Wikipedia then there is no mention of a "closure" axiom. The school approach comes from a slightly muddled way of thinking, where there is assumed to be some kind of intrinsic definition of multiplication that magically works for any objects; this is not an unreasonable thing to tell a schoolchild because the groups that I saw in school (in the very limited amount of time which was spent on group theory) were concrete groups such as matrix groups or permutation groups. In university I was quickly introduced to the concept of an abstract group which was just (G : Type) [Group G] and with this change of emphasis comes a change in the whole way the theory is set up (e.g. the fact that "closure" now ceases to be an axiom and becomes something else). Mathlib is firmly in the "abstract" setting and it changes one's perspective. The statement "a set is a group" (implicit in what you write above) does not make sense in the abstract setting, because a group is a set plus some extra data, so a set literally cannot be a group because we are missing information. However in the concrete setting, the claim that "this concrete set is a group" does make some kind of sense. Such things might be used to teach undergraduates who are in the process of learning how to move from the concrete to the abstract. But with mathlib firmly in the abstract, some things we read in textbooks suitable for beginning undergraduates need to be modified or ignored, because they do not take into account the "mathlib way of doing things".

[Martin C. Martin]

@Kevin Buzzard Thank you for your kind words. I definitely appreciate the distinction between the concrete and the abstract. My Group Theory text was W. Ledermann's "Introduction to Group Theory," and its first group axiom is closure, and that always struck me as strange. As you say, in the abstract setting, what else would it be? If a group is essentially an ordered pair of a set G and an operation *, why elevate to a "group axiom" that the range of * is G, but say nothing about the domain of *? I think the Lean way of handling this makes the most sense, and there's no debate there.

I do think the situation for subgroup is different. In that case, there's a "parent" group G (really (G, ) ), and you take a subset of those elements H, but you keep the same operation, just restricting its domain to H × H. This is naturally more like your concrete setting above, because there is a natural "wider set" G, and it's reasonable to ask, for h₁, h₂ ∈ H, is h₁ h₂ also in H?

@Yakov Pechersky 's formalization seems to sum things up nicely to me: Given (H : Set G) [Group G] [Group H], plus the hypothesis that the two *s are compatible, show that the Subgroup criteria are satisfied. In other words, we already have a Subgroup.toGroup that shows our Subgroup is effectively a Group. This goes the other direction, showing that a Group H is also a Subgroup.

But I understand that my arguments don't seem to be convincing the members of this forum, and that's ok, we can agree to disagree.

[Yakov Pechersky]

Note that after you construct the Subgroup, your statement H = asSubgroup H will look pretty awkward (coercions). And I don't remember if my construction would make that theorem rfl.

[Martin C. Martin]

(The other thread, with the construction, is here for those interested.)

[Yakov Pechersky]

Martin, that definition of "This is naturally more like your concrete setting above, because there is a natural "wider set" G, and it's reasonable to ask, for h₁, h₂ ∈ H, is h₁ h₂ also in H?" is exactly how Subgroup works, you show that even with H x H -> G, all the range is inside H. The whole time, I think you were asking for the other direction.

[Jireh Loreaux]

Martin, can you write out, very explicitly, what you think it means to say that "G is a group, H is a subset of G, and H is a group with the operations inherited from G"?

[Martin C. Martin]

@Jireh Loreaux sure, it's what I wrote above, here it is again:

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

def toSubgroup (h : ∀ x y : H, ((x * y : H) : G) = x * y) : Subgroup G where ...

It translates from your statement, pretty directly, to [Group G] (H : Set G) [Group H] with the added hypothesis h : ∀ x y : H, ((x * y : H) : G) = x * y, where the * on the RHS is understood to be the * in [Group G].

[Martin C. Martin]

And the toSubgroup function simply takes those 4 Lean objects and returns a Subgroup object.

[Jireh Loreaux]

import Mathlib.GroupTheory.Subgroup.Basic

variable {G : Type*} {H : Set G} [Group G] [inst : Group H] (h : ∀ x y : H, ((x * y : H) : G) = x * y)

lemma one_eq_one : (1 : H) = (1 : G) := by
  simpa using h 1 1

lemma inv_eq_inv (x : H) : ↑(x⁻¹ : H) = (x⁻¹ : G) := by
  symm
  apply inv_eq_iff_mul_eq_one.mpr
  rw [← h]
  simp [one_eq_one h]

def toSubgroup : Subgroup G where
  carrier := H
  one_mem' := one_eq_one h ▸ (1 : H).2
  mul_mem' {a b} ha hb := by
    lift a to H using ha
    lift b to H using hb
    exact h a b ▸ (a * b).2
  inv_mem' {a} ha := by
    lift a to H using ha
    exact inv_eq_inv h a ▸ (a⁻¹).2

[Martin C. Martin]

@Jireh Loreaux perfect!

[Kyle Miller]

Even more fun would be also stating that toSubgroup gives the "same" group instance... I don't think it will be defeq, which I think strongly points toward why this isn't done. At least it's not much of a pain to say that toSubgroup h is isomorphic to H.

[Jireh Loreaux]

Note that in the above code, the first two lemmas are the only things with mathematical content (if something is a group, then its identity and inverse functions are determined by the multiplication alone). In the latter case, this is basically the existing Mathlib statement docs#inv_eq_iff_mul_eq_one. In the former case, this is basically docs#self_eq_mul_right, which is hidden in the simpa call.

However, the toSubgroup declaration then essentially has no mathematical content aside from these two lemas. lift is something you would never write in mathematics.

[Jireh Loreaux]

In particular, if you look at the proof of mul_mem', what you'll see is that saying "H is closed under multiplication" is nearly exactly the same as saying "H has a multiplication inherited from G". This is what I meant before when I said "it's essentially just chasing one's tail."

[Martin C. Martin]

I totally agree that the proof, or mathematical content, is minimal. In LADR, the full proof of the equivalent for subspaces is "by the definition of vector space."

[Jireh Loreaux]

@Kyle Miller

example : ↥(toSubgroup h) = ↥H := rfl

example : (toSubgroup h).toGroup = inst := by
  ext x y
  change (↑(x * y : H) : G) = _
  simpa only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid] using (h x y).symm

[Martin C. Martin]

The entire proof of this in Dummit and Foote's book Abstract Algebra is "If H is a subgroup of G, then certainly (1) and (2) hold because H contains the identity of G and the inverse of each of its elements and because H is closed under multiplication."

However trivial the proof, both books thought it worth stating. As a student, it was useful to remember that the conditions in our Subgroup were the only game in town.

If it's considered too trivial or obvious to include in mathlib, that's fine with me. That's why the subject of this chat ends with "if anywhere?"

[Jireh Loreaux]

It's not so much about them being "too trivial", but rather that, because they are equivalent, you can't have both. In the first rfl proof above, we see that Lean recognizes H and toSubgroup H as the same type. This is problematic because it means that H can have two definitionally different Group instances (one from the [inst : Group H] variable, and the other from (toSubgroup h).toGroup). This is bad because it leads to goals like the one right before the change, where we're asked to prove Mul.mul x y = Mul.mul x y, but that isn't true by rfl, and this would cause no end of headaches.

[Jireh Loreaux]

So, in Mathlib, we pick the one which makes life easy, which is docs#Subgroup.

[Kyle Miller]

I think it's worth considering that Dummit and Foote use different foundations from mathlib, and the concepts are organized somewhat differently as a result.

I'd say that Subgroup is closer to what they mean by a group. A mathlib Group is some ambient universe that all the groups under consideration live as subsets.

In this setting, you have "groups" H H' : Subgroup G along with H ≤ H' meaning "H is a subgroup of H'."

This makes it much more straightforward to say what you mean by a subset that's a group, without all these typeclass issues that don't have much to do with the mathematics, and that's docs#IsSubgroup

[Kyle Miller]

Interestingly in Assia Mahboubi, The Rooster and the Butterflies they use group for what mathlib calls Subgroup. This paper I understand is a strong inspiration for mathlib's design of algebraic objects and subobjects.

[Jireh Loreaux]

Martin, I think you are misinterpreting Dummit and Foote, and I agreee with Kyle that what D&F call subgroup is very close to Mathlib's docs#Subgroup (with the exception that they replace docs#Subgroup.one_mem' with the subset being nonempty).

They say:

Definition. Let G be a grouip. The subset H of G is a subgroup of G if H is nonempty and H is closed under products and inverses (i.e., x ∈ H, y ∈ H implies x⁻¹ ∈ H and x * y ∈ H). If H is a subgroup of G, we shall write H ≤ G.

Subgroups of G are just subsets of G which are themselves groups with respect to the operation defined on G, i.e., the binary operation on G restricts to give a binary operation on H which is associative, has an identity in H, and has inverses in H for all the elemens of H."

The text after the definition says "the binary operation on G restricts to give a binary operation on H" which is just another way to say x ∈ H, y ∈ H → x * y ∈ H. And the rest I believe is really more a statement (without proof) of docs#Subgroup.toGroup than anything else.

Note that in the proof of Proposition 1 on the next page, in the second paragraph (where they show that (1) and (2) imply H is a subgroup of G), they show that 1 ∈ H, and x ∈ H → x⁻¹ ∈ H and x ∈ H → y ∈ H → x * y ∈ H, which are exactly the conditions in docs#Subgroup.