NonUnitalSubrings

Let R be a non-unital ring. This file defines the "bundled" non-unital subring type NonUnitalSubring R, a type whose terms correspond to non-unital subrings of R. This is the preferred way to talk about non-unital subrings in mathlib.

Main definitions

Notation used here:

(R : Type u) [NonUnitalRing R] (S : Type u) [NonUnitalRing S] (f g : R →ₙ+* S) (A : NonUnitalSubring R) (B : NonUnitalSubring S) (s : Set R)

• NonUnitalSubring R : the type of non-unital subrings of a ring R.

Implementation notes

A non-unital subring is implemented as a NonUnitalSubsemiring which is also an additive subgroup.

Lattice inclusion (e.g. ≤ and ⊓) is used rather than set notation (⊆ and ∩), although ∈ is defined as membership of a non-unital subring's underlying set.

Tags

non-unital subring

class NonUnitalSubringClass (S : Type u_1) (R : Type u) [NonUnitalNonAssocRing R] [SetLike S R] extends NonUnitalSubsemiringClass S R, NegMemClass S R : Prop

NonUnitalSubringClass S R states that S is a type of subsets s ⊆ R that are both a multiplicative submonoid and an additive subgroup.

• add_mem : ∀ {s : S} {a b : R}, a ∈ s → b ∈ s → a + b ∈ s
• zero_mem : ∀ (s : S), 0 ∈ s
• mul_mem : ∀ {s : S} {a b : R}, a ∈ s → b ∈ s → a * b ∈ s
• neg_mem : ∀ {s : S} {x : R}, x ∈ s → -x ∈ s

theorem NonUnitalSubringClass.addSubgroupClass (S : Type u_1) (R : Type u) [SetLike S R] [NonUnitalNonAssocRing R] [h : NonUnitalSubringClass S R] : AddSubgroupClass S R

@[instance 75]

instance NonUnitalSubringClass.toNonUnitalNonAssocRing {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) : NonUnitalNonAssocRing ↥s

A non-unital subring of a non-unital ring inherits a non-unital ring structure

Equations

• NonUnitalSubringClass.toNonUnitalNonAssocRing s = Function.Injective.nonUnitalNonAssocRing Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance NonUnitalSubringClass.toNonUnitalRing {S : Type v} {R : Type u_1} [NonUnitalRing R] [SetLike S R] [NonUnitalSubringClass S R] (s : S) : NonUnitalRing ↥s

A non-unital subring of a non-unital ring inherits a non-unital ring structure

Equations

• NonUnitalSubringClass.toNonUnitalRing s = Function.Injective.nonUnitalRing Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance NonUnitalSubringClass.toNonUnitalCommRing {S : Type v} (s : S) {R : Type u_1} [NonUnitalCommRing R] [SetLike S R] [NonUnitalSubringClass S R] : NonUnitalCommRing ↥s

A non-unital subring of a NonUnitalCommRing is a NonUnitalCommRing.

Equations

• NonUnitalSubringClass.toNonUnitalCommRing s = Function.Injective.nonUnitalCommRing Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def NonUnitalSubringClass.subtype {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) : ↥s →ₙ+* R

The natural non-unital ring hom from a non-unital subring of a non-unital ring R to R.

Equations

• NonUnitalSubringClass.subtype s = { toFun := Subtype.val, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem NonUnitalSubringClass.coe_subtype {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) : ⇑(NonUnitalSubringClass.subtype s) = Subtype.val

structure NonUnitalSubring (R : Type u) [NonUnitalNonAssocRing R] extends NonUnitalSubsemiring R, AddSubgroup R : Type u

NonUnitalSubring R is the type of non-unital subrings of R. A non-unital subring of R is a subset s that is a multiplicative subsemigroup and an additive subgroup. Note in particular that it shares the same 0 as R.

• carrier : Set R
• add_mem' : ∀ {a b : R}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• mul_mem' : ∀ {a b : R}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• neg_mem' : ∀ {x : R}, x ∈ self.carrier → -x ∈ self.carrier

def NonUnitalSubring.toSubsemigroup {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : Subsemigroup R

The underlying submonoid of a NonUnitalSubring.

Equations

• s.toSubsemigroup = { carrier := s.carrier, mul_mem' := ⋯ }

instance NonUnitalSubring.instSetLike {R : Type u} [NonUnitalNonAssocRing R] : SetLike (NonUnitalSubring R) R

Equations

• NonUnitalSubring.instSetLike = { coe := fun (s : NonUnitalSubring R) => s.carrier, coe_injective' := ⋯ }

theorem NonUnitalSubring.instNonUnitalSubringClass {R : Type u} [NonUnitalNonAssocRing R] : NonUnitalSubringClass (NonUnitalSubring R) R

theorem NonUnitalSubring.mem_carrier {R : Type u} [NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R} : x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s

@[simp]

theorem NonUnitalSubring.mem_mk {R : Type u} [NonUnitalNonAssocRing R] {S : NonUnitalSubsemiring R} {x : R} (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : x ∈ { toNonUnitalSubsemiring := S, neg_mem' := h } ↔ x ∈ S

@[simp]

theorem NonUnitalSubring.coe_set_mk {R : Type u} [NonUnitalNonAssocRing R] (S : NonUnitalSubsemiring R) (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : ↑{ toNonUnitalSubsemiring := S, neg_mem' := h } = ↑S

@[simp]

theorem NonUnitalSubring.mk_le_mk {R : Type u} [NonUnitalNonAssocRing R] {S S' : NonUnitalSubsemiring R} (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) (h' : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier) : { toNonUnitalSubsemiring := S, neg_mem' := h } ≤ { toNonUnitalSubsemiring := S', neg_mem' := h' } ↔ S ≤ S'

theorem NonUnitalSubring.ext {R : Type u} [NonUnitalNonAssocRing R] {S T : NonUnitalSubring R} (h : ∀ (x : R), x ∈ S ↔ x ∈ T) : S = T

Two non-unital subrings are equal if they have the same elements.

def NonUnitalSubring.copy {R : Type u} [NonUnitalNonAssocRing R] (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : NonUnitalSubring R

Copy of a non-unital subring with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• S.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem NonUnitalSubring.coe_copy {R : Type u} [NonUnitalNonAssocRing R] (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : ↑(S.copy s hs) = s

theorem NonUnitalSubring.copy_eq {R : Type u} [NonUnitalNonAssocRing R] (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S

theorem NonUnitalSubring.toNonUnitalSubsemiring_injective {R : Type u} [NonUnitalNonAssocRing R] : Function.Injective NonUnitalSubring.toNonUnitalSubsemiring

theorem NonUnitalSubring.toNonUnitalSubsemiring_strictMono {R : Type u} [NonUnitalNonAssocRing R] : StrictMono NonUnitalSubring.toNonUnitalSubsemiring

theorem NonUnitalSubring.toNonUnitalSubsemiring_mono {R : Type u} [NonUnitalNonAssocRing R] : Monotone NonUnitalSubring.toNonUnitalSubsemiring

theorem NonUnitalSubring.toAddSubgroup_injective {R : Type u} [NonUnitalNonAssocRing R] : Function.Injective NonUnitalSubring.toAddSubgroup

theorem NonUnitalSubring.toAddSubgroup_strictMono {R : Type u} [NonUnitalNonAssocRing R] : StrictMono NonUnitalSubring.toAddSubgroup

theorem NonUnitalSubring.toAddSubgroup_mono {R : Type u} [NonUnitalNonAssocRing R] : Monotone NonUnitalSubring.toAddSubgroup

theorem NonUnitalSubring.toSubsemigroup_injective {R : Type u} [NonUnitalNonAssocRing R] : Function.Injective NonUnitalSubring.toSubsemigroup

theorem NonUnitalSubring.toSubsemigroup_strictMono {R : Type u} [NonUnitalNonAssocRing R] : StrictMono NonUnitalSubring.toSubsemigroup

theorem NonUnitalSubring.toSubsemigroup_mono {R : Type u} [NonUnitalNonAssocRing R] : Monotone NonUnitalSubring.toSubsemigroup

def NonUnitalSubring.mk' {R : Type u} [NonUnitalNonAssocRing R] (s : Set R) (sm : Subsemigroup R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : NonUnitalSubring R

Construct a NonUnitalSubring R from a set s, a subsemigroup sm, and an additive subgroup sa such that x ∈ s ↔ x ∈ sm ↔ x ∈ sa.

Equations

• NonUnitalSubring.mk' s sm sa hm ha = { carrier := (sm.copy s ⋯).carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem NonUnitalSubring.coe_mk' {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : ↑(NonUnitalSubring.mk' s sm sa hm ha) = s

@[simp]

theorem NonUnitalSubring.mem_mk' {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) {x : R} : x ∈ NonUnitalSubring.mk' s sm sa hm ha ↔ x ∈ s

@[simp]

theorem NonUnitalSubring.mk'_toSubsemigroup {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (NonUnitalSubring.mk' s sm sa hm ha).toSubsemigroup = sm

@[simp]

theorem NonUnitalSubring.mk'_toAddSubgroup {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (NonUnitalSubring.mk' s sm sa hm ha).toAddSubgroup = sa

theorem NonUnitalSubring.zero_mem {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : 0 ∈ s

A non-unital subring contains the ring's 0.

theorem NonUnitalSubring.mul_mem {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R} : x ∈ s → y ∈ s → x * y ∈ s

A non-unital subring is closed under multiplication.

theorem NonUnitalSubring.add_mem {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R} : x ∈ s → y ∈ s → x + y ∈ s

A non-unital subring is closed under addition.

theorem NonUnitalSubring.neg_mem {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x : R} : x ∈ s → -x ∈ s

A non-unital subring is closed under negation.

theorem NonUnitalSubring.sub_mem {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s

A non-unital subring is closed under subtraction

instance NonUnitalSubring.toNonUnitalRing {R : Type u_1} [NonUnitalRing R] (s : NonUnitalSubring R) : NonUnitalRing ↥s

A non-unital subring of a non-unital ring inherits a non-unital ring structure

Equations

• s.toNonUnitalRing = Function.Injective.nonUnitalRing (fun (a : ↥s) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem NonUnitalSubring.zsmul_mem {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s

@[simp]

theorem NonUnitalSubring.val_add {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (x y : ↥s) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem NonUnitalSubring.val_neg {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (x : ↥s) : ↑(-x) = -↑x

@[simp]

theorem NonUnitalSubring.val_mul {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (x y : ↥s) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem NonUnitalSubring.val_zero {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : ↑0 = 0

theorem NonUnitalSubring.coe_eq_zero_iff {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x : ↥s} : ↑x = 0 ↔ x = 0

instance NonUnitalSubring.toNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] (s : NonUnitalSubring R) : NonUnitalCommRing ↥s

A non-unital subring of a NonUnitalCommRing is a NonUnitalCommRing.

Equations

• s.toNonUnitalCommRing = Function.Injective.nonUnitalCommRing (fun (a : ↥s) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

Partial order

@[simp]

theorem NonUnitalSubring.mem_toSubsemigroup {R : Type u} [NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R} : x ∈ s.toSubsemigroup ↔ x ∈ s

@[simp]

theorem NonUnitalSubring.coe_toSubsemigroup {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : ↑s.toSubsemigroup = ↑s

@[simp]

theorem NonUnitalSubring.mem_toAddSubgroup {R : Type u} [NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R} : x ∈ s.toAddSubgroup ↔ x ∈ s

@[simp]

theorem NonUnitalSubring.coe_toAddSubgroup {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : ↑s.toAddSubgroup = ↑s

@[simp]

theorem NonUnitalSubring.mem_toNonUnitalSubsemiring {R : Type u} [NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R} : x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s

@[simp]

theorem NonUnitalSubring.coe_toNonUnitalSubsemiring {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : ↑s.toNonUnitalSubsemiring = ↑s

def NonUnitalSubring.inclusion {R : Type u} [NonUnitalNonAssocRing R] {S T : NonUnitalSubring R} (h : S ≤ T) : ↥S →ₙ+* ↥T

The ring homomorphism associated to an inclusion of NonUnitalSubrings.

Equations

• NonUnitalSubring.inclusion h = NonUnitalRingHom.codRestrict (NonUnitalSubringClass.subtype S) T ⋯