Asserting that 2ℤ forms a non-unital ring

Stream: new members

[Isak Colboubrani]

I want to assert that 2ℤ forms a non-unital ring (rng: a ring without assuming an identity):

import Mathlib
example : NonUnitalRing [something] := by infer_instance

What is the idiomatic way to express 2ℤ, and can I expect infer_instance to work here?

If this approach is wrong, what would be the correct approach?

[Eric Wieser]

I guess you want docs#zmultiples as a docs#NonUnitalSubring

[Daniel Weber]

Perhaps using Ideal.span {(2 : ℤ)}? But there doesn't seem to be such an instance for it either

[Isak Colboubrani]

@Daniel Weber Ideal.span was one of my first attempts:

import Mathlib
example : NonUnitalRing Ideal.span {(2 : ℤ)} := by infer_instance

It fails with:

application type mismatch
    NonUnitalRing Ideal.span
argument
    Ideal.span
has type
    Set ?m.4 → Ideal ?m. 4 : Type ?u.3
but is expected to have type
    Type ?u.2 : Type (?u.2 + 1)

[Daniel Weber]

You are missing parentheses

[Isak Colboubrani]

Thanks! New attempt:

import Mathlib
example : NonUnitalRing (Ideal.span {(2 : ℤ)}) := by infer_instance

It fails with:

failed to synthesize instance
  NonUnitalRing ↥(Ideal.span {2})

[Isak Colboubrani]

@Eric Wieser Thanks! it seems the first link returns a 404 error (unless the content listed below the error message was what you intended to reference).

I found the AddSubgroup:s def zmultiples (a : A) : AddSubgroup A. Is this what you were referring to? If so, would the idea be to transition from AddSubgroup to NonUnitalSubring and then to NonUnitalRing? If so, are there any examples or resources available that demonstrate this kind of progression?

These are the other zmultiples I found in Mathlib:

Mathlib/Algebra/CharZero/Quotient.lean:theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) :
Mathlib/Algebra/CharZero/Quotient.lean:theorem zmultiples_nsmul_eq_nsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {n : ℕ} (hz : n ≠ 0) :
Mathlib/Algebra/GroupPower/Lemmas.lean:def zmultiplesHom [AddGroup A] :
Mathlib/Algebra/GroupPower/Lemmas.lean:theorem zmultiplesHom_apply [AddGroup A] (x : A) (n : ℤ) : zmultiplesHom A x n = n • x :=
Mathlib/Algebra/GroupPower/Lemmas.lean:theorem zmultiplesHom_symm_apply [AddGroup A] (f : ℤ →+ A) : (zmultiplesHom A).symm f = f 1 :=
Mathlib/Algebra/GroupPower/Lemmas.lean:def zmultiplesAddHom [AddCommGroup A] : A ≃+ (ℤ →+ A) :=
Mathlib/Algebra/GroupPower/Lemmas.lean:theorem zmultiplesAddHom_apply [AddCommGroup A] (x : A) (n : ℤ) :
Mathlib/Algebra/GroupPower/Lemmas.lean:theorem zmultiplesAddHom_symm_apply [AddCommGroup A] (f : ℤ →+ A) :
Mathlib/Data/ZMod/Quotient.lean:theorem zmultiplesQuotientStabilizerEquiv_symm_apply (n : ZMod (minimalPeriod (a +ᵥ ·) b)) :
Mathlib/GroupTheory/Subgroup/ZPowers.lean:def zmultiples (a : A) : AddSubgroup A :=
Mathlib/RingTheory/Int/Basic.lean:theorem zmultiples_natAbs (a : ℤ) :

[Daniel Weber]

I believe it would be better to show that ideals are non unital subrings

[Yakov Pechersky]

import Mathlib

def Ideal.toNonUnitalSubring {R : Type*} [CommRing R] (I : Ideal R) :
    NonUnitalSubring R where
      carrier := I
      add_mem' := I.add_mem
      zero_mem' := I.zero_mem
      mul_mem' _ := I.mul_mem_left _
      neg_mem' := I.neg_mem

#synth NonUnitalRing (Ideal.span ({2} : Set ℤ)).toNonUnitalSubring

[Isak Colboubrani]

@Daniel Weber

Personally I find that (to go the Ideal.span route) more intuitive too, but I'm a beginner.

I suppose this is one of the more typical scenarios in which non-unital rings arise in practice, as every ideal of a ring forms a non-unital ring (a ring without a multiplicative identity) under the induced operations.

[Isak Colboubrani]

@Yakov Pechersky Very nice! Thanks!

Some background:

Since the following works as expected out of the box ...

example : CommRing (ℤ ⧸ Ideal.span {(2 : ℤ)}) := by infer_instance

... I expected to be able to write ...

example : NonUnitalRing (Ideal.span {(2 : ℤ)}) := by infer_instance

However, this didn't work without your implementation of Ideal.toNonUnitalSubring. But with your implementation, the following now works:

example : NonUnitalRing (Ideal.span {(2 : ℤ)}).toNonUnitalSubring := by infer_instance

Is it simply that Ideal.toNonUnitalSubring PR hasn't been submitted to Mathlib yet, or is there some reason that adding it wouldn't be a good idea?

I'm seeking to understand whether it was reasonable to assume that example : NonUnitalRing (Ideal.span {(2 : ℤ)}) := by infer_instance would work, or if that assumption was perhaps misguided.

[Daniel Weber]

I imagine the problem is that an instance of Mul on ideals would interact badly with the multiplication of the ring

[Eric Wieser]

I think

instance {R} [Semiring R] : NonUnitalSubsemiringClass (Ideal R) R where
  mul_mem _ hb := Ideal.mul_mem_left _ _ hb

instance {R} [Ring R] : NonUnitalSubringClass (Ideal R) R where

example : NonUnitalRing (Ideal.span {(2 : ℤ)}) := by infer_instance

would be better

[Isak Colboubrani]

@Eric Wieser That's fantastic! Now all of my test cases, which I expected to work, indeed function as anticipated:

example : NonUnitalRing (Ideal.span {(2 : ℤ)}) := by infer_instance
example : NonUnitalRing (Ideal.span ({2} : Set ℤ)) := by infer_instance
example (n : ℤ) : NonUnitalRing (Ideal.span {n}) := by infer_instance
example (n : ℤ) : NonUnitalRing (Ideal.span ({n} : Set ℤ)) := by infer_instance

Would it be appropriate to include the following in Mathlib to ensure that this functionality is available out of the box? If so, is there any contributor willing to submit a PR?

instance {R} [Semiring R] : NonUnitalSubsemiringClass (Ideal R) R where
  mul_mem _ hb := Ideal.mul_mem_left _ _ hb
instance {R} [Ring R] : NonUnitalSubringClass (Ideal R) R where

[Ruben Van de Velde]

Are you willing to submit a pr?

[Jireh Loreaux]

Yes, this instance likely got overlooked when I created all these non-unital subobject classes. We need to make sure this instance is also added for the quite new docs#TwoSidedIdeal

[Isak Colboubrani]

I'm unsure how to formalize the TwoSidedIdeal case in Lean.

On paper, I'd demonstrate that a two-sided ideal is indeed an ideal (of course!) and then apply the fact that an ideal forms a non-unital subring under the induced operations from its parent ring (as formalized above).

Would this approach be the best for formalization? If so, any hints on how to express that in Lean?

[Yakov Pechersky]

Exactly the same as above:

import Mathlib

instance {R} [NonUnitalNonAssocRing R] : NonUnitalSubsemiringClass (TwoSidedIdeal R) R where
  mul_mem _ hb := TwoSidedIdeal.mul_mem_left _ _ _ hb

instance {R} [Ring R] : NonUnitalSubringClass (TwoSidedIdeal R) R where

def TwoSidedIdeal.span {R} [NonUnitalNonAssocRing R] (s : Set R) : TwoSidedIdeal R :=
  sInf {p : TwoSidedIdeal R | s ⊆ p}

example : NonUnitalRing (TwoSidedIdeal.span {(2 : ℤ)}) := by infer_instance

[Isak Colboubrani]

Thanks Yakov!

I tried that, but turns out I missed [NonUnitalNonAssocRing R]. Now it all works as expected!

[Yakov Pechersky]

My "exactly" was doing some heavy lifting