Showing group operation is closed on a subset.

Stream: new members

[Martin C. Martin]

If I have a group G, and a subset s : Set G, and that subset is also a group under the same operator, then the operator is closed on the subset. How do I show this in Lean? Here's my #mwe , what can I put in the sorry? Or am I going about this all wrong?

import Mathlib.Algebra.Group.Basic
import Mathlib.Data.SetLike.Basic


structure SubsetOfGroup (G : Type _)
  [Group G] :=
(carrier : Set G)

-- Boilerplate for SetLike: Start
namespace SubsetOfGroup

variable {G : Type _} [Group G]

instance : SetLike (SubsetOfGroup G) G :=
⟨ SubsetOfGroup.carrier, fun p q h => by cases p; cases q; congr⟩

@[simp]
theorem mem_carrier {p : SubsetOfGroup G} : v ∈ p.carrier ↔ v ∈ (p : Set G) :=
  Iff.rfl

@[ext]
theorem ext {p q : SubsetOfGroup G} (h : ∀ v, v ∈ p ↔ v ∈ q) : p = q :=
  SetLike.ext h

end SubsetOfGroup
-- Boilerplate for SetLike: End

variable {G : Type _} [gG : Group G]
variable {p : SubsetOfGroup G} [gp: Group p]

instance : Mul p where
  mul u v := ⟨u.1 * v.1, by sorry ⟩

[Yaël Dillies]

Construct a term of type Subgroup G, where carrier := s

[Damiano Testa]

Also, you told the Zulip chat that " that subset is also a group under the same operator", but your code does not mention this to Lean. You currently seem to have two different multiplications floating around, gG and gp and you are trying to define a third one.

[Riccardo Brasca]

The way we work with subgroups in Lean is slightly different than what is usually done in standard mathematics. In particular in Lean we don't start with a subset S and say "S is a subgroup". Of course there is nothing crazy going on, a term of type Subgroup G mathematically corresponds to what you think, but for Lean it is more or less a tuple "(subset, 1, ...)".
In practice what you want is docs#IsSubgroup, that is deprecated in mathlib (because it is a pain to use) but very close to what a mathematician would say.

[Riccardo Brasca]

The idea is that "subgroup" is not a property that certains subset have and certains don't, there is no "being a subgroup" (well, it is docs#IsSubgroup). We work the other way, saying "Let H be a subgroup of G".

[Riccardo Brasca]

Mathematically there is no difference, and we know from our experience than this approach works better.

[Martin C. Martin]

Thanks, I should have been more clear. Mathematically, if G is a group and H is a subset of G, then H is a group iff H is non-empty and closed under the group operation and inverse. I understand that, in practice, it's easier to use the reverse direction, i.e. show it's closed under inverse & operation & contains the identity. But I'm interested in proving the other direction: Given that G is a group, H is a subset of G with the same operation (restricted to H of course) and H is a group, show that H is closed under the operation, inverse, and contains the identity.

[Martin C. Martin]

Damiano Testa said:

Also, you told the Zulip chat that " that subset is also a group under the same operator", but your code does not mention this to Lean. You currently seem to have two different multiplications floating around, gG and gp and you are trying to define a third one.

Thanks. I agree there are two different operators around, but I'm not trying to define a third. Rather, I'm trying to put a constraint on the second, constraining it to be the same as the first, at least on the restricted domain. If there's a better way to express what I want, I'm all ears.

[Martin C. Martin]

Does mathlib4, for example, contain a proof that any subset of a group G, where the subset is also a group using the same operator, is a Subgroup?

[Yakov Pechersky]

Question for you is how would you state H is a group in lean?

[Martin C. Martin]

Yakov Pechersky said:

Question for you is how would you state H is a group in lean?

That's what my #mwe above does, although I called it p instead of H. I use SetLike to define SubsetOfGroup as a class that is SetLike, then:

variable {H : SubsetOfGroup G} [gH: Group H]

[Ruben Van de Velde]

Well no, that says "there is a group structure on H that may be completely unrelated to the group structure on G"

[Martin C. Martin]

Right. Then you add a separate statement, saying "the group operation on H is the same one on G." And by "same" I mean isomorphic of course, and on the restricted domain.

[Yakov Pechersky]

In any case, as soon as you say Group H, whether or not it is related to another (*) by some hypothesis, that statement asserts that it is closed over the (*)_H

[Damiano Testa]

I suspect that you are slowly converging to defining subgroups as they are defined in mathlib.

[Martin C. Martin]

Yakov Pechersky said:

In any case, as soon as you say Group H, whether or not it is related to another (*) by some hypothesis, that statement asserts that it is closed over the (*)_H

Yes. And it should be possible to use that in whatever replaces the sorry in my #mwe , where I say "and the group operator is the same group operator as in G," but of course you also need to provide a proof that it's closed on H. So you and I can both see that it follows from the fact that we have [gH : Group H]. How do we render that in Lean?

[Martin C. Martin]

Damiano Testa said:

I suspect that you are slowly converging to defining subgroups as they are defined in mathlib.

I definitely have the same definition. In my math education, when something can be defined two different ways, you pick one as the "official" definition, the prove the other is equivalent. That's what I'm trying to do here. I'm accepting that the definition of Subgroup is as defined in mathlib4, namely closed under inverse, closed under *, and contains identity. So then you need to show that any subset that is also a group is a Subgroup. That's what I'm trying to do here.

[Martin C. Martin]

For example, Linear Algebra Done Right, theorem 1.3.4 is that "A subset U of V is also a vector space of V iff U satisfies the following 3 conditions." (Contains 0, closed under addition and scalar multiplication). The proof of the forward direction is just "If U is a subset of V and U is a vector space using the same addition and scalar multiplication, then U satisfies the three conditions by the definition of vector space."

[Eric Wieser]

So then you need to show that any subset that is also a group is a Subgroup. That's what I'm trying to do here.

This is false without the extra "and the operations agree" condition

[Yakov Pechersky]

Here's a start

import Mathlib.GroupTheory.Subgroup.Basic

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

def martinSubgroup (h : ∀ x y : H, ((x * y : H) : G) = x * y) : Subgroup G where
  carrier := H
  mul_mem' := by
    intros x y hx hy
    specialize h ⟨x, hx⟩ ⟨y, hy⟩
    dsimp only at h
    simp [←h]
  one_mem' := by
    specialize h 1 1
    simp only [mul_one, self_eq_mul_right] at h
    simp [←h]
  inv_mem' := by
    intros x hx
    sorry

[Martin C. Martin]

Eric Wieser said:

So then you need to show that any subset that is also a group is a Subgroup. That's what I'm trying to do here.

This is false without the extra "and the operations agree" condition

I agree. So let me revise my statement: "then you should show that any subset of G that is a group using an operator that agrees with H, is closed under multiplication and inverse and is non-empty."

[Martin C. Martin]

For example, the Wikipedia article on Subgroup says " a subset H of G is called a subgroup of G if H also forms a group under the operation ∗. More precisely, H is a subgroup of G if the restriction of ∗ to H × H is a group operation on H. " Then, in a later section called "Subgroup tests", says "H is a subgroup of G if and only if H is nonempty and closed under products and inverses."

[Yakov Pechersky]

I think if means two different things here. One can mean "propositionally". The other meaning is "by definition". I am trying to get across that [Group H] gives you the "by definition" aspect.

[Martin C. Martin]

Yakov Pechersky said:

Here's a start

import Mathlib.GroupTheory.Subgroup.Basic

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

Thanks. But I think this doesn't work, because [Group H] doesn't say what we want? Set G is just an alias for G -> Prop, i.e. a predicate on G. I'm not sure what [Group H] would mean. Basically, in Lean, a Set is not a class that contains a subset of objects of G, or even something isomorphic to that. That's why, e.g. when we define Sub-things in mathlib4, we need to defined a structure and use SetLike.

For example, in variable (h : H), h is not what we want. We can use the notation h ∈ H for something analogous, but that doesn't let us say [Group H].

[Sebastien Gouezel]

The wikipedia wording is very bad: the sentence H is a subgroup of G if the restriction of ∗ to H × H is a group operation on H doesn't make sense, since the restriction of ∗ to H × H is a map from H × H to G, and a priori not to H, so you can not ask if it gives a group structure.

[Yakov Pechersky]

I don't know how you would state there is a group on the subset H. In mathlib, Group operates on Types. And we have a coercion of terms of Set to terms of Sorts, that is, a Type.

-- then you should show that any subset of G that is a group using an operator that agrees with H,
-- is closed under multiplication and inverse and is non-empty.
lemma martin (h : ∀ x y : H, ((x * y : H) : G) = x * y) :
    (∀ x y : H, ((x * y : H) : G) ∈ H) ∧
    (∀ x : H, ((x⁻¹ : H) : G) ∈ H) ∧
    H.Nonempty := by
  refine' ⟨_, _, _⟩
  · intro ⟨_, _⟩ ⟨_, _⟩
    simp
  · intro ⟨_, _⟩
    simp
  · specialize h 1 1
    simp only [mul_one, self_eq_mul_right] at h
    exact ⟨1, by simp [←h]⟩

[Yakov Pechersky]

And you can't define an operation (*) that only works on a subset. You can define operations on types. So H has to be promoted from a Set (read: subset) to a Type (read: set).

[Yakov Pechersky]

Basically, in Lean, a Set is not a class that contains a subset of objects of G, or even something isomorphic to that.

On the contrary, I think it is that. Or more exactly, one possible implementation of that. The fact that Set X = X -> Prop is an implementation detail. Would you feel more comfortable if it was

structure NewSet (X : Type*) :=
  predicate : X → Prop

[Martin C. Martin]

Yes. My approach in my #mwe above, was to define:

structure SubsetOfGroup (G : Type _)
  [Group G] :=
(carrier : Set G)

And then have the SetLike boilerplate. So same as when we define a Subgroup in mathlib, but leave out all the other properties. Then it's just a subset without structure. But perhaps that's not the right approach.

[Martin C. Martin]

Yakov Pechersky said:

Basically, in Lean, a Set is not a class that contains a subset of objects of G, or even something isomorphic to that.

On the contrary, I think it is that. Or more exactly, one possible implementation of that. The fact that Set X = X -> Prop is an implementation detail. Would you feel more comfortable if it was

structure NewSet (X : Type*) :=
  predicate : X → Prop

Sorry, I meant isomorphic in a specific way (the way that SetLike gives, where you can cast back and forth between elements of the types), but I didn't say that.

Basically, given [Group G], you can say #check (1 : G) that that typechecks just fine. But if you then define H : Set G and try #check (1 : H), you get a type error. You need to say #check (1 ∈ H) instead. However, this means you can't just say plain old [Group H], since H is the wrong kind of object. Anyway, I think we agree on this point?

Part of the problem here is that Lean's type system is very different from the naive set theory used in undergrad math texts. So mapping undergrad math texts to Lean can run into issues. For example, undergrad math texts define Group as a set with an operator; but in Lean, Set means something very different, you really need a Type with an operator, and there's really no such thing as sub-Types, e.g. in Lean, ℕ is not a sub-Type of ℝ , but a completely disjoint Type composed of different objects, so that (1 : ℕ) is a different object than (1 : ℝ).

[Eric Wieser]

The SetLike boilerplate is a distraction for you here: you could use Set G directly

[Eric Wieser]

The only reason we need SetLike in mathlib is because we need to store additional things after the carrier

[Martin C. Martin]

Anyway, thank you very much for your time and effort in explaining this to me. Perhaps the answer is, the standard undergrad way of thinking of this is kind of sloppy, and Lean doesn't even allow us to express it because of that. As you say, if meaning "by definition" vs "propositionally."

[Eric Wieser]

But if you then define H : Set G and try #check (1 : H), you get a type error

It works just find if you add [Group H]:

import Mathlib.GroupTheory.Subgroup.Basic
variable {G : Type*} (H : Set G) [Group H]
#check (1 : H) -- just fine

[Martin C. Martin]

Huh, maybe I'm confused then.

[Damiano Testa]

Also, to point out another sloppiness of informal mathematics: when you say that 1 ∈ ℕ is the same as 1 ∈ ℤ, you are probably wrong. The "usual" definitions are that 1 ∈ ℕ is the set containing the empty set, while 1 ∈ ℤ is the equivalence class of (1, 0) under some relation.

These are very far from being the same. If you then go as far as going via ℚ, further pairs and then onto ℝ via Cauchy sequences, you quickly see that every time you say that these are subsets of each other, you never literally mean that anyway.

[Martin C. Martin]

@Damiano Testa very true. Although I always thought that, e.g. once you define ℤ, you the redefine the natural numbers as being those. So 1 is redefined as being the equivalence class of ({{}}, {}) under that relation. But if you do that I suppose there's the question of where you stop, e.g. the 1 in Real analysis is a real number, so a Cauchy sequence (or equiv class of Cauchy sequences?), where as in Complex analysis, it's now an ordered pair of those equiv classes. So within a given textbook it has a defined meaning, but different texts define it differently.
Unless your Real Analysis textbook has a chapter at the end, "introduction to Complex Analysis," in which case things are kind of hopeless. :) So I think I'm agreeing with you.

[Damiano Testa]

You could replace your older definitions by their images in the new sets, but the gain is just in obfuscation. Informal mathematics is perfectly able to handle the imprecision. It is only when you decide to formalise mathematical results that you need to get to grips with actual implementations. And even then, you do that very briefly, until you form an API layer to allow you to get your imprecise intuition back!

[Yakov Pechersky]

I think we can say the same here for subgroup definitions. They're really laying out an API, a set of very basic axioms about some object, and we're free to implement it however. The pudding will be the ease of use of your implemented object in proving downstream theorems.

[Damiano Testa]

Anyway, Martin, I did not mean to seem dismissive: I think that a great way to really learn something is to break it apart and rebuild it, just like you were doing.

In this case, the sorry that Yakov left further upstream is a very cute exercise, where you actually use a not-entirely-trivial fact about inverses in a group.

[Martin C. Martin]

Eric Wieser said:

But if you then define H : Set G and try #check (1 : H), you get a type error

It works just find if you add [Group H]:

import Mathlib.GroupTheory.Subgroup.Basic
variable {G : Type*} (H : Set G) [Group H]
#check (1 : H) -- just fine

I take back that (1 : H) doesn't type check, it does as you say. However, it means something very different. (H : G → Prop). For example, imagine G is Fin 6, so we're defining a finite group of size 6. Imagine H is the proposition where H (0 : Fin 6), H (2 : Fin 6) and H (4 : Fin 6) are true (or derivable or whatever), and the others false (not derivable). What does "h : H" mean?

[Yakov Pechersky]

Then if you're giving a term h of type H, you're giving me a packet of information: (h : G, proof that h \in H).

[Martin C. Martin]

Is h : H a proof that H 0, H 2 and H 4 are true or something? By proof irrelevance, are h i : H considered equal?

[Yakov Pechersky]

Consider my angle brackets in my proofs above. I was deconstructing that packet of information of x : H into x : G, hx : x \in H.

[Yakov Pechersky]

Note, we do not have in mathlib a coercion of terms of type G -> Prop to types.

[Yakov Pechersky]

We _do_ for terms of type Set G. Even if their underlying implementation is the same, we can associate different semantics/operations on each.

[Riccardo Brasca]

I admit I didn't read the whole conversation, but what's wrong with docs#IsSubgroup ?

[Riccardo Brasca]

(deleted)

[Martin C. Martin]

@Riccardo Brasca do you have a working link? My Google-fu is failing me, and I can't find a definition of it or information about it.

[Riccardo Brasca]

Now it works

[Martin C. Martin]

@Riccardo Brasca perhaps that's the way to go. It seems like a parallel definition. We have Subgroup, and separately, we have IsSubgroup, which express the same mathematical truth. But maybe that's not a bad thing?

[Riccardo Brasca]

Yes, the difference is purely practical. In theory one can do everything with IsSubgroup, and at the beginning this looks closer to standard math. For example I do that with my undergraduate students (well, I define IsSubsbace) since a lot of their linear algebra exercises are of of the kind "show that blah blah is a subspace of blah blah". But the point is that one we start doing serious mathematics (and I don't mean anything complicated, for example when we want to consider the "set" of all subgroups) then it becomes a pain to use IsSubgroup, while our approach with Subgroup works better.

[Riccardo Brasca]

So it really depends on what you want to do. If your goal is to advanced mathematics, so you need to use mathlib, you are essentially forced to use Subgroup, since virtually all the library is written in that way.

[Martin C. Martin]

@Yakov Pechersky getting back to what h : H means, Set X is an alias for X → Prop, i.e. a predicate. So e.g. is_even on ℕ can be viewed as a Set ℕ:

def is_even := fun (a : Nat) => ∃ b, a = 2 * b

#check (is_even : ℕ → Prop)

#check (is_even : Set ℕ)

variable (h : is_even)

In this case, I get an error, "type expected, got (is_even : ℕ → Prop)".

So it seems analogous here. Given an arbitrary type G (which could be ℕ ), and H : Set G (where in some application H could be is_even), I don't think h : H has much meaning in Lean in general. Or I'm confused, which is quite possible.

[Yakov Pechersky]

What I'm saying is that Set X should not be thought of as an alias of X -> Prop.

[Yakov Pechersky]

Sure, we defined it that way, but now let's pinky promise to never peek behind the curtain.

[Yakov Pechersky]

And a way of respecting that is like

def is_even := fun (a : Nat) => ∃ b, a = 2 * b

def evens : Set Nat = {n | is_even n}

[Yakov Pechersky]

The crucial thing you're missing in your mwe is the following globally available coercion in mathlib: docs#Set.instCoeSortSetType

[Yakov Pechersky]

Note that a set is a term, not a type. There is a coercion from Set α to Type* sending s to the corresponding subtype ↥s.

[Riccardo Brasca]

@Martin C. Martin is_even is not a well formed type, it hasn't terms.

[Riccardo Brasca]

Not everything is a type. Everything (almost...) is a term.

[Martin C. Martin]

Riccardo Brasca said:

So it really depends on what you want to do. If your goal is to advanced mathematics, so you need to use mathlib, you are essentially forced to use Subgroup, since virtually all the library is written in that way.

My current goal is to understand how regular math maps to Lean, and my secondary goal is pedagogy. I'm translating Linear Algebra Done Right into Lean, both so that I can learn it, and also hopefully that others can use it as a kind of Rosetta Stone, if they know linear algebra but not Lean, they can see how concepts from Linear Algebra are rendered in Lean.

So defining Subgroup as a structure the way mathlib does, then wanting to prove that it's equivalent to "any subset of a group that is also a group" by ignoring our new definition, and instead introducing an IsSubset, seem a little unsatisfying. Perhaps better to just say "since we need to create a separate type that's isomorphic to the subset, we can't even represent a non-closed function" and leave it at that.

[Riccardo Brasca]

Lean is able to decide whether "something" is a well formed type, and in particular it complains when you write (t : is_even)

[Riccardo Brasca]

I really think the mathlib approach is the best one. Just forget about all these questions that ask to prove that "something is a subblah"

[Riccardo Brasca]

But this is a problem only for explicit examples.

[Riccardo Brasca]

When you arrive at "the intersection of two subspaces is a subspace" this is perfectly translated in mathlib. The difference is that it is not a statement about the set theoretic intersection.

[Yakov Pechersky]

I very much like LADR as a book, but I don't think it maps well to mathlib much. Because LADR is highly specialized to vector spaces over R and C, while mathlib discusses modules (read: semimodules) and tries to avoid restricting to fields wherever possible.

[Riccardo Brasca]

It is a definition that takes two subspaces A and B and gives another one A inter B. Then one can prove that (A inter B).carrier = A.carrier ∩ B.carrier

[Riccardo Brasca]

Yakov Pechersky said:

I very much like LADR as a book, but I don't think it maps well to mathlib much. Because LADR is highly specialized to vector spaces over R and C, while mathlib discusses modules (read: semimodules) and tries to avoid restricting to fields wherever possible.

Sure, but you can suppose that you are working with modules over a field (aka vector spaces). Of course if one theorem is true over any ring we state it in such generality (but it will apply to your case). If a theorem really need the base ring to be a field we don't have any problem with it, we state with a field.

[Riccardo Brasca]

Then it is true that not a lot of theorems really need the base ring to be a field, they probably need the module to be free or something, this is way you don't see a lot of linear algebra over fields in mathlib.

[Martin C. Martin]

Yakov Pechersky said:

Note that a set is a term, not a type. There is a coercion from Set α to Type* sending s to the corresponding subtype ↥s.

Ah, interesting, thanks!

[Yakov Pechersky]

Agreed. My point was in bridging mathlib API to LADR "API" -- the gadgets LADR discusses and builds are done with less generality, so one has to carry around more assumptions on the mathlib gadgets, and thus some basic-LADR-gadget-theorems are annoying to express in mathlib.

[Martin C. Martin]

Riccardo Brasca said:

Not everything is a type. Everything (almost...) is a term.

Interesting, I hadn't appreciated the difference, or that there could be an coercion when a non-type term is used in a type context. Thanks!

[Martin C. Martin]

Yakov Pechersky said:

The crucial thing you're missing in your mwe is the following globally available coercion in mathlib: docs#Set.instCoeSortSetType

The comment just before the definition says:

-- It is currently an abbreviation so that instance coming from `Subtype` are available.
-- If you're interested in making it a `def`, as it probably should be,
-- you'll then need to create additional instances (and possibly prove lemmas about them).
-- The first error should appear below at `monotoneOn_iff_monotone`.

however, it looks like a def to me. Is that comment old? Should it be removed?

[Riccardo Brasca]

I guess the comment refers to the reducible attribute.

[Riccardo Brasca]

(but I agree it is misleading)

[Martin C. Martin]

Thank you all, this has been very helpful. I somehow had thought that Set X was an actual alias for X -> Prop, using an alias keyword, like a C typedef. I don't know where I got that idea, as there's clearly a def in the definition. Also, I hadn't appreciated the coercion. Now that I have a deeper understanding of these fundamentals, I'll go read up on the details again.

[Eric Wieser]

I think you're getting more confused unfortunately, the alias keyword is just def + "autogenerate a docstring". And docs#Set is just a def.Maybe you mean abbrev, which is "just" @[reducible] def

[Martin C. Martin]

Damiano Testa said:

Anyway, Martin, I did not mean to seem dismissive: I think that a great way to really learn something is to break it apart and rebuild it, just like you were doing.

In this case, the sorry that Yakov left further upstream is a very cute exercise, where you actually use a not-entirely-trivial fact about inverses in a group.

Thank you very much for your encouraging words. "The devil is in the details," and it often takes an experience like this for me to appreciate these things which seem like subtleties to me on a first reading.

[Martin C. Martin]

Eric Wieser said:

I think you're getting more confused unfortunately, the alias keyword is just def + "autogenerate a docstring". And docs#Set is just a def.

Thanks. I do think things are clearing up. I had thought that Set X and X -> Prop were indistinguishable to the Lean compiler, but now I understand they are clearly different, and there's coercion, so now I can go back to some of the example code earlier in this thread that made no sense to me.

[Eric Wieser]

There is no coercion between those types

[Martin C. Martin]

Yep, I understand. But there is coercion involved in h : H when H : Set X, but not when H : X -> Prop, and that's where I was stuck before.

[Riccardo Brasca]

Yes, the point is that h : H doesn't make sense neither when H : Set X nor when H : X -> Prop. The only difference is that in the former case Lean knows how to modify what you wrote and in the latter it doesn't.

[Jireh Loreaux]

It seems like this was already sufficiently resolved, but I just wanted to point out that Sebastien put his finger on the key issue:
Sebastien Gouezel said:

The wikipedia wording is very bad: the sentence H is a subgroup of G if the restriction of ∗ to H × H is a group operation on H doesn't make sense, since the restriction of ∗ to H × H is a map from H × H to G, and a priori not to H, so you can not ask if it gives a group structure.

When mathematicians (IMO, sloppily) define "Given a group G, a nonempty subset H is a subgroup of G if it is a group with the same operations as on G", this already presupposes that for x y ∈ H, that x * y ∈ H (because the multiplication has to agree with that of G, but it has to be a function H × H → H for H to be a group) and for x ∈ H, that x⁻¹ ∈ H (for similar reasons). Then the only part of docs#Subgroup which is not already presupposed by the mathematician's sloppy definition of subgroup is that 1 ∈ H. This actually requires proof: since H is nonempty, there is some x ∈ H, and then 1 = x * x⁻¹ ∈ H.

[Junyan Xu]

Yeah, H being closed under the operations is mathematically trivial, and 1 ∈ H is the only nontrivial part. You can actually leave out the inverse operation from the definition of a group and still get 1 ∈ H, because multiplication in a group is cancellative: 1H * 1H = 1H = 1G * 1H implies that 1H = 1G. For the same reason, a subset in a vector space that is a vector space with the inherited operations must have the same zero as the ambient vector space. This is not true for the identity 1 in a ring, since multiplication is not necessarily cancellative in a ring; for example, given two rings A and B, A × {0} forms a ring under the operations inherited from A × B, but has identity (1,0), which is different from the identity (1,1) in A × B. docs#Subring requires 1 to be in the subring and rules out such cases, but docs#NonUnitalSubring includes such cases (and it's introduced with applications in operator algebras in mind, I think).