Mathlib.Algebra.Ring.Subring.Defs

Module docstring

{"# Subrings

Let R be a ring. This file defines the \"bundled\" subring type Subring R, a type whose terms correspond to subrings of R. This is the preferred way to talk about subrings in mathlib. Unbundled subrings (s : Set R and IsSubring s) are not in this file, and they will ultimately be deprecated.

We prove that subrings are a complete lattice, and that you can map (pushforward) and comap (pull back) them along ring homomorphisms.

We define the closure construction from Set R to Subring R, sending a subset of R to the subring it generates, and prove that it is a Galois insertion.

Main definitions

Notation used here:

(R : Type u) [Ring R] (S : Type u) [Ring S] (f g : R →+* S) (A : Subring R) (B : Subring S) (s : Set R)

Subring R : the type of subrings of a ring R.
instance : CompleteLattice (Subring R) : the complete lattice structure on the subrings.
Subring.center : the center of a ring R.
Subring.closure : subring closure of a set, i.e., the smallest subring that includes the set.
Subring.gi : closure : Set M → Subring M and coercion (↑) : Subring M → et M form a GaloisInsertion.
comap f B : Subring A : the preimage of a subring B along the ring homomorphism f
map f A : Subring B : the image of a subring A along the ring homomorphism f.
prod A B : Subring (R × S) : the product of subrings
f.range : Subring B : the range of the ring homomorphism f.
eqLocus f g : Subring R : given ring homomorphisms f g : R →+* S, the subring of R where f x = g x

Implementation notes

A subring is implemented as a subsemiring which is also an additive subgroup. The initial PR was as a submonoid 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 subring's underlying set.

Tags

subring, subrings ","## Partial order "}

SubringClass structure

(S : Type*) (R : outParam (Type u)) [Ring R] [SetLike S R] : Prop
    extends SubsemiringClass S R, NegMemClass S R

Full source

/-- `SubringClass S R` states that `S` is a type of subsets `s ⊆ R` that
are both a multiplicative submonoid and an additive subgroup. -/
class SubringClass (S : Type*) (R : outParam (Type u)) [Ring R] [SetLike S R] : Prop
    extends SubsemiringClass S R, NegMemClass S R

Subring Class

Informal description

A structure `SubringClass S R` asserts that `S` is a type of subsets of a ring `R` that are closed under both the multiplicative and additive operations of `R`. Specifically, each subset in `S` must form a multiplicative submonoid and an additive subgroup of `R`.

SubringClass.addSubgroupClass instance

(S : Type*) (R : Type u) [SetLike S R] [Ring R] [h : SubringClass S R] : AddSubgroupClass S R

Full source

instance (priority := 100) SubringClass.addSubgroupClass (S : Type*) (R : Type u)
    [SetLike S R] [Ring R] [h : SubringClass S R] : AddSubgroupClass S R :=
  { h with }

Subring Classes are Additive Subgroup Classes

Informal description

For any type `S` representing subsets of a ring `R` with a `SetLike` instance, if `S` forms a `SubringClass` (i.e., its subsets are closed under ring operations), then `S` also forms an `AddSubgroupClass` (i.e., its subsets are closed under addition and negation).

SubringClass.nonUnitalSubringClass instance

(S : Type*) (R : Type u) [SetLike S R] [Ring R] [SubringClass S R] : NonUnitalSubringClass S R

Full source

instance (priority := 100) SubringClass.nonUnitalSubringClass (S : Type*) (R : Type u)
    [SetLike S R] [Ring R] [SubringClass S R] : NonUnitalSubringClass S R where

Subring Classes are Non-Unital Subring Classes

Informal description

For any type $S$ with a `SetLike` structure over a ring $R$, if $S$ is a `SubringClass` of $R$, then $S$ is also a `NonUnitalSubringClass` of $R$. This means that every subset in $S$ is closed under multiplication, addition, and negation, forming a non-unital subring of $R$.

intCast_mem theorem

(n : ℤ) : (n : R) ∈ s

Full source

@[aesop safe apply (rule_sets := [SetLike])]
theorem intCast_mem (n : ℤ) : (n : R) ∈ s := by simp only [← zsmul_one, zsmul_mem, one_mem]

Integer Casts Belong to Subring

Informal description

For any integer $n$, the image of $n$ under the canonical ring homomorphism from $\mathbb{Z}$ to $R$ is an element of the subring $s$ of $R$.

SubringClass.toHasIntCast instance

: IntCast s

Full source

instance (priority := 75) toHasIntCast : IntCast s :=
  ⟨fun n => ⟨n, intCast_mem s n⟩⟩

Integer Casting in Subrings

Informal description

For any subring $s$ of a ring $R$, the subring $s$ inherits the canonical integer casting operation from $R$. That is, for any integer $n$, the element $(n : R)$ belongs to $s$.

SubringClass.toRing instance

: Ring s

Full source

/-- A subring of a ring inherits a ring structure -/
instance (priority := 75) toRing : Ring s := fast_instance%
  Subtype.coe_injective.ring Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl

Subrings Inherit Ring Structure

Informal description

For any subring $s$ of a ring $R$, the subset $s$ inherits a ring structure from $R$.

SubringClass.toCommRing instance

{R} [CommRing R] [SetLike S R] [SubringClass S R] : CommRing s

Full source

/-- A subring of a `CommRing` is a `CommRing`. -/
instance (priority := 75) toCommRing {R} [CommRing R] [SetLike S R] [SubringClass S R] :
    CommRing s := fast_instance%
  Subtype.coe_injective.commRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ => rfl) fun _ => rfl

Subrings of Commutative Rings are Commutative Rings

Informal description

For any commutative ring $R$ and any subring $s$ of $R$ (where $S$ is a type of subsets of $R$ that form subrings), the subring $s$ inherits a commutative ring structure from $R$.

SubringClass.instIsDomainSubtypeMem instance

{R} [Ring R] [IsDomain R] [SetLike S R] [SubringClass S R] : IsDomain s

Full source

/-- A subring of a domain is a domain. -/
instance (priority := 75) {R} [Ring R] [IsDomain R] [SetLike S R] [SubringClass S R] : IsDomain s :=
  NoZeroDivisors.to_isDomain _

Subrings of Domains are Domains

Informal description

For any ring $R$ that is a domain and any subring $s$ of $R$, the subring $s$ is also a domain.

SubringClass.subtype definition

(s : S) : s →+* R

Full source

/-- The natural ring hom from a subring of ring `R` to `R`. -/
def subtype (s : S) : s →+* R :=
  { SubmonoidClass.subtype s, AddSubgroupClass.subtype s with
    toFun := (↑) }

Inclusion homomorphism of a subring

Informal description

The natural inclusion homomorphism from a subring $ s $ of a ring $ R $ to $ R $, which maps each element of $ s $ to itself in $ R $. This homomorphism preserves both the additive and multiplicative structures, including the additive identity, multiplicative identity, addition, multiplication, and negation.

SubringClass.subtype_apply theorem

(x : s) : SubringClass.subtype s x = x

Full source

@[simp]
lemma subtype_apply (x : s) :
    SubringClass.subtype s x = x := rfl

Inclusion Homomorphism Acts as Identity on Subring Elements

Informal description

For any element $x$ in a subring $s$ of a ring $R$, the inclusion homomorphism $\text{subtype}(s)$ maps $x$ to itself in $R$, i.e., $\text{subtype}(s)(x) = x$.

SubringClass.subtype_injective theorem

: Function.Injective (subtype s)

Full source

lemma subtype_injective :
    Function.Injective (subtype s) :=
  Subtype.coe_injective

Injectivity of Subring Inclusion Homomorphism

Informal description

The inclusion homomorphism from a subring $s$ of a ring $R$ to $R$ is injective. That is, if two elements of $s$ are equal in $R$, then they are equal in $s$.

SubringClass.coe_subtype theorem

: (subtype s : s → R) = ((↑) : s → R)

Full source

@[simp]
theorem coe_subtype : (subtype s : s → R) = ((↑) : s → R) :=
  rfl

Inclusion Homomorphism Equals Coercion for Subrings

Informal description

The inclusion homomorphism from a subring $s$ of a ring $R$ to $R$ coincides with the canonical coercion map from $s$ to $R$, i.e., $\text{subtype}(s) = (\uparrow) : s \to R$.

SubringClass.coe_natCast theorem

(n : ℕ) : ((n : s) : R) = n

Full source

@[simp, norm_cast]
theorem coe_natCast (n : ℕ) : ((n : s) : R) = n := rfl

Natural Number Embedding in Subrings Preserves Numerals

Informal description

For any natural number $n$ and any subring $s$ of a ring $R$, the canonical inclusion map from $s$ to $R$ preserves the natural number embedding, i.e., $(n : s) = n$ in $R$.

SubringClass.coe_intCast theorem

(n : ℤ) : ((n : s) : R) = n

Full source

@[simp, norm_cast]
theorem coe_intCast (n : ℤ) : ((n : s) : R) = n := rfl

Coercion of Integer Casts in Subrings Preserves Value

Informal description

For any integer $n \in \mathbb{Z}$ and any subring $s$ of a ring $R$, the canonical inclusion map from $s$ to $R$ maps the integer $n$ (interpreted in $s$) to the integer $n$ in $R$. In other words, the coercion of the integer $n$ from the subring $s$ to the ring $R$ is equal to $n$ itself.

Subring structure

(R : Type u) [Ring R] extends Subsemiring R, AddSubgroup R

Full source

/-- `Subring R` is the type of subrings of `R`. A subring of `R` is a subset `s` that is a
  multiplicative submonoid and an additive subgroup. Note in particular that it shares the
  same 0 and 1 as R. -/
structure Subring (R : Type u) [Ring R] extends Subsemiring R, AddSubgroup R

Subring

Informal description

A subring of a ring $R$ is a subset $s$ of $R$ that is closed under addition, multiplication, and additive inverses, and contains the multiplicative identity $1$ and the additive identity $0$ of $R$. Formally, a subring is both a subsemiring (closed under addition, multiplication, and contains $0$ and $1$) and an additive subgroup (closed under addition and additive inverses).

Subring.instSetLike instance

: SetLike (Subring R) R

Full source

instance : SetLike (Subring R) R where
  coe s := s.carrier
  coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h

Subrings as Set-like Structures

Informal description

For any ring $R$, the type of subrings of $R$ is equipped with a set-like structure, where each subring can be viewed as a subset of $R$ via a canonical injection.

Subring.ofClass definition

{S R : Type*} [Ring R] [SetLike S R] [SubringClass S R] (s : S) : Subring R

Full source

/-- The actual `Subring` obtained from an element of a `SubringClass`. -/
@[simps]
def ofClass {S R : Type*} [Ring R] [SetLike S R] [SubringClass S R]
    (s : S) : Subring R where
  carrier := s
  add_mem' := add_mem
  zero_mem' := zero_mem _
  mul_mem' := mul_mem
  neg_mem' := neg_mem
  one_mem' := one_mem _

Subring construction from a subring class element

Informal description

Given a type `S` representing a collection of subsets of a ring `R` that form subrings (i.e., are closed under addition, multiplication, and additive inverses, and contain the multiplicative and additive identities), the function `Subring.ofClass` constructs an actual `Subring R` from an element `s : S`. Specifically, for a subset `s : S`, the carrier set of the resulting subring is `s` itself, and the closure properties (additive closure, multiplicative closure, etc.) are inherited from the `SubringClass` instance.

Subring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg instance

 :
  CanLift (Set R) (Subring R) (↑)
    (fun s ↦
      0 ∈ s ∧
        (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → -x ∈ s)

Full source

instance (priority := 100) : CanLift (Set R) (Subring R) (↑)
    (fun s ↦ 0 ∈ s0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧
      (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → -x ∈ s) where
  prf s h :=
    ⟨ { carrier := s
        zero_mem' := h.1
        add_mem' := h.2.1
        one_mem' := h.2.2.1
        mul_mem' := h.2.2.2.1
        neg_mem' := h.2.2.2.2 },
      rfl ⟩

Lifting Subsets to Subrings under Closure Conditions

Informal description

For any ring $R$, there is a canonical way to lift a subset $s$ of $R$ to a subring of $R$ provided that $s$ contains $0$ and $1$, is closed under addition and multiplication, and is closed under additive inverses.

Subring.instSubringClass instance

: SubringClass (Subring R) R

Full source

instance : SubringClass (Subring R) R where
  zero_mem s := s.zero_mem'
  add_mem {s} := s.add_mem'
  one_mem s := s.one_mem'
  mul_mem {s} := s.mul_mem'
  neg_mem {s} := s.neg_mem'

Subrings as Subring Classes

Informal description

For any ring $R$, the type of subrings of $R$ forms a `SubringClass`, meaning that each subring is closed under the ring operations (addition, multiplication, and additive inverses) and contains the multiplicative and additive identities.

Subring.toNonUnitalSubring definition

(S : Subring R) : NonUnitalSubring R

Full source

/-- Turn a `Subring` into a `NonUnitalSubring` by forgetting that it contains `1`. -/
def toNonUnitalSubring (S : Subring R) : NonUnitalSubring R where __ := S

Forgetting the multiplicative identity in a subring to obtain a non-unital subring

Informal description

Given a subring $S$ of a ring $R$, the function `Subring.toNonUnitalSubring` constructs a non-unital subring from $S$ by forgetting the multiplicative identity condition. The resulting non-unital subring has the same underlying set as $S$ and inherits the additive and multiplicative structures from $S$.

Subring.mem_toSubsemiring theorem

{s : Subring R} {x : R} : x ∈ s.toSubsemiring ↔ x ∈ s

Full source

@[simp]
theorem mem_toSubsemiring {s : Subring R} {x : R} : x ∈ s.toSubsemiringx ∈ s.toSubsemiring ↔ x ∈ s := Iff.rfl

Membership in Subring and Subsemiring Coincide

Informal description

For any subring $s$ of a ring $R$ and any element $x \in R$, $x$ belongs to the underlying subsemiring of $s$ if and only if $x$ belongs to $s$.

Subring.mem_carrier theorem

{s : Subring R} {x : R} : x ∈ s.carrier ↔ x ∈ s

Full source

theorem mem_carrier {s : Subring R} {x : R} : x ∈ s.carrierx ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl

Membership in Subring Carrier Set

Informal description

For any subring $s$ of a ring $R$ and any element $x \in R$, the element $x$ belongs to the underlying set of $s$ (denoted by `s.carrier`) if and only if $x$ is a member of the subring $s$.

Subring.mem_mk theorem

{S : Subsemiring R} {x : R} (h) : x ∈ (⟨S, h⟩ : Subring R) ↔ x ∈ S

Full source

@[simp]
theorem mem_mk {S : Subsemiring R} {x : R} (h) : x ∈ (⟨S, h⟩ : Subring R)x ∈ (⟨S, h⟩ : Subring R) ↔ x ∈ S := Iff.rfl

Membership in Subring Construction from Subsemiring

Informal description

For any subsemiring $S$ of a ring $R$, any element $x \in R$, and any proof $h$ that $S$ is closed under additive inverses, we have $x \in \langle S, h \rangle$ if and only if $x \in S$. Here, $\langle S, h \rangle$ denotes the subring of $R$ constructed from the subsemiring $S$ with the additional property $h$.

Subring.coe_set_mk theorem

(S : Subsemiring R) (h) : ((⟨S, h⟩ : Subring R) : Set R) = S

Full source

@[simp] theorem coe_set_mk (S : Subsemiring R) (h) : ((⟨S, h⟩ : Subring R) : Set R) = S := rfl

Subring Construction Preserves Underlying Set

Informal description

For any subsemiring $S$ of a ring $R$ and any proof $h$ that $S$ is also an additive subgroup, the underlying set of the subring $\langle S, h \rangle$ is equal to $S$ as a subset of $R$.

Subring.mk_le_mk theorem

{S S' : Subsemiring R} (h₁ h₂) : (⟨S, h₁⟩ : Subring R) ≤ (⟨S', h₂⟩ : Subring R) ↔ S ≤ S'

Full source

@[simp]
theorem mk_le_mk {S S' : Subsemiring R} (h₁ h₂) :
    (⟨S, h₁⟩ : Subring R) ≤ (⟨S', h₂⟩ : Subring R) ↔ S ≤ S' :=
  Iff.rfl

Subring Containment via Subsemiring Containment

Informal description

For any two subsemirings $S$ and $S'$ of a ring $R$, and any proofs $h_1$ and $h_2$ that they are closed under additive inverses, the subring $\langle S, h_1 \rangle$ is contained in the subring $\langle S', h_2 \rangle$ if and only if $S$ is contained in $S'$ as subsemirings.

Subring.one_mem_toNonUnitalSubring theorem

(S : Subring R) : 1 ∈ S.toNonUnitalSubring

Full source

lemma one_mem_toNonUnitalSubring (S : Subring R) : 1 ∈ S.toNonUnitalSubring := S.one_mem

Multiplicative Identity Belongs to Non-unital Subring Associated with a Subring

Informal description

For any subring $S$ of a ring $R$, the multiplicative identity $1$ is an element of the underlying non-unital subring associated with $S$.

Subring.ext theorem

{S T : Subring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T

Full source

/-- Two subrings are equal if they have the same elements. -/
@[ext]
theorem ext {S T : Subring R} (h : ∀ x, x ∈ Sx ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

Extensionality of Subrings: $S = T \iff \forall x \in R, x \in S \leftrightarrow x \in T$

Informal description

Let $R$ be a ring, and let $S$ and $T$ be subrings of $R$. If for every element $x \in R$, $x$ belongs to $S$ if and only if $x$ belongs to $T$, then $S = T$.

Subring.copy definition

(S : Subring R) (s : Set R) (hs : s = ↑S) : Subring R

Full source

/-- Copy of a subring with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[simps coe toSubsemiring]
protected def copy (S : Subring R) (s : Set R) (hs : s = ↑S) : Subring R :=
  { S.toSubsemiring.copy s hs with
    carrier := s
    neg_mem' := hs.symm ▸ S.neg_mem' }

Copy of a subring with a specified carrier set

Informal description

Given a subring $S$ of a ring $R$ and a subset $s$ of $R$ equal to the underlying set of $S$, the function constructs a new subring with carrier set $s$ that is definitionally equal to $S$.

Subring.copy_eq theorem

(S : Subring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S

Full source

theorem copy_eq (S : Subring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S :=
  SetLike.coe_injective hs

Copy of Subring Equals Original

Informal description

Let $R$ be a ring, $S$ a subring of $R$, and $s$ a subset of $R$ such that $s$ equals the underlying set of $S$. Then the subring $S.\text{copy}\ s\ hs$ is equal to $S$.

Subring.toSubsemiring_injective theorem

: Function.Injective (toSubsemiring : Subring R → Subsemiring R)

Full source

theorem toSubsemiring_injective : Function.Injective (toSubsemiring : Subring R → Subsemiring R)
  | _, _, h => ext (SetLike.ext_iff.mp h :)

Injectivity of the Subring-to-Subsemiring Map

Informal description

The canonical map from the type of subrings of a ring $R$ to the type of subsemirings of $R$ is injective. In other words, if two subrings $S$ and $T$ of $R$ have the same underlying subsemiring, then $S = T$.

Subring.toAddSubgroup_injective theorem

: Function.Injective (toAddSubgroup : Subring R → AddSubgroup R)

Full source

theorem toAddSubgroup_injective : Function.Injective (toAddSubgroup : Subring R → AddSubgroup R)
  | _, _, h => ext (SetLike.ext_iff.mp h :)

Injectivity of Subring to Additive Subgroup Map

Informal description

The canonical map from a subring $S$ of a ring $R$ to its underlying additive subgroup is injective. That is, if two subrings $S_1$ and $S_2$ of $R$ have the same underlying additive subgroup, then $S_1 = S_2$.

Subring.toSubmonoid_injective theorem

: Function.Injective (fun s : Subring R => s.toSubmonoid)

Full source

theorem toSubmonoid_injective : Function.Injective (fun s : Subring R => s.toSubmonoid)
  | _, _, h => ext (SetLike.ext_iff.mp h :)

Injectivity of Subring-to-Submonoid Mapping

Informal description

The function that maps a subring $S$ of a ring $R$ to its underlying submonoid is injective. In other words, if two subrings $S$ and $T$ of $R$ have the same underlying submonoid, then $S = T$.

Subring.mk' definition

(s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : Subring R

Full source

/-- Construct a `Subring R` from a set `s`, a submonoid `sm`, and an additive
subgroup `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`. -/
@[simps! coe]
protected def mk' (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s)
    (ha : ↑sa = s) : Subring R :=
  { sm.copy s hm.symm, sa.copy s ha.symm with }

Construction of a subring from matching submonoid and additive subgroup

Informal description

Given a set $s$ in a ring $R$, a submonoid $sm$ of $R$ with underlying set equal to $s$, and an additive subgroup $sa$ of $R$ with underlying set equal to $s$, the function `Subring.mk'` constructs a subring of $R$ with underlying set $s$, where the multiplicative structure is inherited from $sm$ and the additive structure is inherited from $sa$.

Subring.mem_mk' theorem

 {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) {x : R} :
  x ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s

Full source

@[simp]
theorem mem_mk' {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s)
    {x : R} : x ∈ Subring.mk' s sm sa hm hax ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s :=
  Iff.rfl

Membership in Constructed Subring via Matching Submonoid and Additive Subgroup

Informal description

Let $R$ be a ring, $s$ a subset of $R$, $sm$ a submonoid of $R$ with underlying set $s$, and $sa$ an additive subgroup of $R$ with underlying set $s$. For any element $x \in R$, we have $x$ belongs to the subring $\text{Subring.mk'}\ s\ sm\ sa\ hm\ ha$ if and only if $x \in s$.

Subring.mk'_toSubmonoid theorem

 {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) :
  (Subring.mk' s sm sa hm ha).toSubmonoid = sm

Full source

@[simp]
theorem mk'_toSubmonoid {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R}
    (ha : ↑sa = s) : (Subring.mk' s sm sa hm ha).toSubmonoid = sm :=
  SetLike.coe_injective hm.symm

Subring Construction Preserves Submonoid Component

Informal description

Given a set $s$ in a ring $R$, a submonoid $sm$ of $R$ with underlying set equal to $s$, and an additive subgroup $sa$ of $R$ with underlying set equal to $s$, the submonoid associated with the subring constructed via `Subring.mk'` is equal to $sm$.

Subring.mk'_toAddSubgroup theorem

 {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) :
  (Subring.mk' s sm sa hm ha).toAddSubgroup = sa

Full source

@[simp]
theorem mk'_toAddSubgroup {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R}
    (ha : ↑sa = s) : (Subring.mk' s sm sa hm ha).toAddSubgroup = sa :=
  SetLike.coe_injective ha.symm

Additive Subgroup Component of Constructed Subring

Informal description

Given a set $s$ in a ring $R$, a submonoid $sm$ of $R$ with underlying set equal to $s$, and an additive subgroup $sa$ of $R$ with underlying set equal to $s$, the additive subgroup component of the subring constructed via `Subring.mk'` is equal to $sa$.

Subsemiring.toSubring definition

(s : Subsemiring R) (hneg : (-1 : R) ∈ s) : Subring R

Full source

/-- A `Subsemiring` containing -1 is a `Subring`. -/
@[simps toSubsemiring]
def Subsemiring.toSubring (s : Subsemiring R) (hneg : (-1 : R) ∈ s) : Subring R where
  toSubsemiring := s
  neg_mem' h := by
    rw [← neg_one_mul]
    exact mul_mem hneg h

Subring construction from a subsemiring containing -1

Informal description

Given a subsemiring $s$ of a ring $R$ that contains $-1$, the structure `Subsemiring.toSubring` constructs a subring of $R$ with the same underlying set as $s$. The condition $(-1) \in s$ ensures that the resulting structure is closed under additive inverses, making it a subring.

Subring.one_mem theorem

: (1 : R) ∈ s

Full source

/-- A subring contains the ring's 1. -/
protected theorem one_mem : (1 : R) ∈ s :=
  one_mem _

Subring Contains One

Informal description

For any subring $s$ of a ring $R$, the multiplicative identity $1$ is an element of $s$.

Subring.zero_mem theorem

: (0 : R) ∈ s

Full source

/-- A subring contains the ring's 0. -/
protected theorem zero_mem : (0 : R) ∈ s :=
  zero_mem _

Subrings Contain Zero

Informal description

For any subring $s$ of a ring $R$, the additive identity $0$ is an element of $s$.

Subring.mul_mem theorem

{x y : R} : x ∈ s → y ∈ s → x * y ∈ s

Full source

/-- A subring is closed under multiplication. -/
protected theorem mul_mem {x y : R} : x ∈ s → y ∈ s → x * y ∈ s :=
  mul_mem

Closure of Subrings under Multiplication

Informal description

For any subring $s$ of a ring $R$ and any elements $x, y \in R$, if $x$ and $y$ belong to $s$, then their product $x * y$ also belongs to $s$.

Subring.add_mem theorem

{x y : R} : x ∈ s → y ∈ s → x + y ∈ s

Full source

/-- A subring is closed under addition. -/
protected theorem add_mem {x y : R} : x ∈ s → y ∈ s → x + y ∈ s :=
  add_mem

Closure of Subrings under Addition

Informal description

For any subring $s$ of a ring $R$ and any elements $x, y \in R$, if $x \in s$ and $y \in s$, then $x + y \in s$.

Subring.neg_mem theorem

{x : R} : x ∈ s → -x ∈ s

Full source

/-- A subring is closed under negation. -/
protected theorem neg_mem {x : R} : x ∈ s → -x ∈ s :=
  neg_mem

Closure under Negation in Subrings

Informal description

For any element $x$ in a subring $s$ of a ring $R$, the additive inverse $-x$ is also in $s$.

Subring.sub_mem theorem

{x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s

Full source

/-- A subring is closed under subtraction -/
protected theorem sub_mem {x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s :=
  sub_mem hx hy

Subring Closure Under Subtraction

Informal description

For any subring $s$ of a ring $R$ and any elements $x, y \in R$, if $x$ and $y$ belong to $s$, then their difference $x - y$ also belongs to $s$.

Subring.toRing instance

: Ring s

Full source

/-- A subring of a ring inherits a ring structure -/
instance toRing : Ring s := SubringClass.toRing s

Subrings Inherit Ring Structure

Informal description

Every subring $s$ of a ring $R$ inherits a ring structure from $R$.

Subring.zsmul_mem theorem

{x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s

Full source

protected theorem zsmul_mem {x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s :=
  zsmul_mem hx n

Closure of Subring under Integer Scalar Multiplication

Informal description

For any element $x$ in a subring $s$ of a ring $R$ and any integer $n$, the scalar multiple $n \cdot x$ is also in $s$.

Subring.pow_mem theorem

{x : R} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s

Full source

protected theorem pow_mem {x : R} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s :=
  pow_mem hx n

Closure of Subring under Natural Powers

Informal description

Let $R$ be a ring and $s$ a subring of $R$. For any element $x \in s$ and any natural number $n$, the power $x^n$ belongs to $s$.

Subring.coe_add theorem

(x y : s) : (↑(x + y) : R) = ↑x + ↑y

Full source

@[simp, norm_cast]
theorem coe_add (x y : s) : (↑(x + y) : R) = ↑x + ↑y :=
  rfl

Subring Addition Preserved Under Inclusion

Informal description

For any two elements $x$ and $y$ in a subring $s$ of a ring $R$, the canonical inclusion of their sum $x + y$ in $R$ equals the sum of their individual inclusions, i.e., $(x + y) = x + y$ under the inclusion map.

Subring.coe_neg theorem

(x : s) : (↑(-x) : R) = -↑x

Full source

@[simp, norm_cast]
theorem coe_neg (x : s) : (↑(-x) : R) = -↑x :=
  rfl

Negation Commutes with Subring Inclusion

Informal description

For any element $x$ in a subring $s$ of a ring $R$, the canonical injection of the additive inverse $-x$ in $s$ equals the additive inverse of the canonical injection of $x$ in $R$. In other words, if $x \in s$, then $(-x) = -x$ under the inclusion map.

Subring.coe_mul theorem

(x y : s) : (↑(x * y) : R) = ↑x * ↑y

Full source

@[simp, norm_cast]
theorem coe_mul (x y : s) : (↑(x * y) : R) = ↑x * ↑y :=
  rfl

Multiplication Preservation in Subring Inclusion

Informal description

For any elements $x$ and $y$ in a subring $s$ of a ring $R$, the canonical inclusion map preserves multiplication, i.e., $(x \cdot y) = x \cdot y$ under the inclusion map.

Subring.coe_zero theorem

: ((0 : s) : R) = 0

Full source

@[simp, norm_cast]
theorem coe_zero : ((0 : s) : R) = 0 :=
  rfl

Inclusion Preserves Zero in Subrings

Informal description

For any subring $s$ of a ring $R$, the image of the additive identity $0$ in $s$ under the inclusion map is equal to the additive identity $0$ in $R$.

Subring.coe_one theorem

: ((1 : s) : R) = 1

Full source

@[simp, norm_cast]
theorem coe_one : ((1 : s) : R) = 1 :=
  rfl

Preservation of Multiplicative Identity in Subring Inclusion

Informal description

For any subring $s$ of a ring $R$, the image of the multiplicative identity $1$ in $s$ under the canonical inclusion map is equal to the multiplicative identity $1$ in $R$, i.e., $1_s = 1_R$.

Subring.coe_pow theorem

(x : s) (n : ℕ) : ↑(x ^ n) = (x : R) ^ n

Full source

@[simp, norm_cast]
theorem coe_pow (x : s) (n : ℕ) : ↑(x ^ n) = (x : R) ^ n :=
  SubmonoidClass.coe_pow x n

Subring Power Coercion: $(x^n)_s = x^n_R$

Informal description

Let $R$ be a ring and $s$ a subring of $R$. For any element $x \in s$ and natural number $n$, the $n$-th power of $x$ in $s$ (when viewed as an element of $R$) equals the $n$-th power of $x$ in $R$. In other words, $(x^n)_s = x^n_R$ where $(\cdot)_s$ denotes the power operation in $s$ and $(\cdot)_R$ denotes the power operation in $R$.

Subring.coe_eq_zero_iff theorem

{x : s} : (x : R) = 0 ↔ x = 0

Full source

theorem coe_eq_zero_iff {x : s} : (x : R) = 0 ↔ x = 0 :=
  ⟨fun h => Subtype.ext (Trans.trans h s.coe_zero.symm), fun h => h.symm ▸ s.coe_zero⟩

Zero Preservation in Subring Inclusion: $x_R = 0 \leftrightarrow x_s = 0$

Informal description

For any element $x$ in a subring $s$ of a ring $R$, the image of $x$ under the inclusion map equals $0$ in $R$ if and only if $x$ is the zero element in $s$.

Subring.toCommRing instance

{R} [CommRing R] (s : Subring R) : CommRing s

Full source

/-- A subring of a `CommRing` is a `CommRing`. -/
instance toCommRing {R} [CommRing R] (s : Subring R) : CommRing s :=
  SubringClass.toCommRing s

Subrings of Commutative Rings are Commutative Rings

Informal description

For any commutative ring $R$ and any subring $s$ of $R$, the subring $s$ inherits a commutative ring structure from $R$.

Subring.instNontrivialSubtypeMem instance

{R} [Ring R] [Nontrivial R] (s : Subring R) : Nontrivial s

Full source

/-- A subring of a non-trivial ring is non-trivial. -/
instance {R} [Ring R] [Nontrivial R] (s : Subring R) : Nontrivial s :=
  s.toSubsemiring.nontrivial

Nontriviality of Subrings in Nontrivial Rings

Informal description

For any nontrivial ring $R$ and any subring $s$ of $R$, the subring $s$ is also nontrivial.

Subring.instNoZeroDivisorsSubtypeMem instance

{R} [Ring R] [NoZeroDivisors R] (s : Subring R) : NoZeroDivisors s

Full source

/-- A subring of a ring with no zero divisors has no zero divisors. -/
instance {R} [Ring R] [NoZeroDivisors R] (s : Subring R) : NoZeroDivisors s :=
  s.toSubsemiring.noZeroDivisors

Subrings Inherit No Zero Divisors Property

Informal description

For any ring $R$ with no zero divisors and any subring $s$ of $R$, the subring $s$ also has no zero divisors.

Subring.instIsDomainSubtypeMem instance

{R} [Ring R] [IsDomain R] (s : Subring R) : IsDomain s

Full source

/-- A subring of a domain is a domain. -/
instance {R} [Ring R] [IsDomain R] (s : Subring R) : IsDomain s :=
  NoZeroDivisors.to_isDomain _

Subrings of Domains are Domains

Informal description

For any domain $R$ and any subring $s$ of $R$, $s$ is also a domain.

Subring.subtype definition

(s : Subring R) : s →+* R

Full source

/-- The natural ring hom from a subring of ring `R` to `R`. -/
def subtype (s : Subring R) : s →+* R :=
  { s.toSubmonoid.subtype, s.toAddSubgroup.subtype with toFun := (↑) }

Inclusion homomorphism of a subring

Informal description

For a subring $ s $ of a ring $ R $, the natural inclusion homomorphism $ s \to R $ maps each element of $ s $ to itself in $ R $. This homomorphism preserves both the additive and multiplicative structures, including the additive identity $ 0 $, the multiplicative identity $ 1 $, addition, and multiplication.

Subring.subtype_apply theorem

{s : Subring R} (x : s) : s.subtype x = x

Full source

@[simp]
lemma subtype_apply {s : Subring R} (x : s) :
    s.subtype x = x := rfl

Inclusion Homomorphism Acts as Identity on Subring Elements

Informal description

For any subring $s$ of a ring $R$ and any element $x \in s$, the inclusion homomorphism $\text{subtype}(s)$ maps $x$ to itself in $R$, i.e., $\text{subtype}(s)(x) = x$.

Subring.subtype_injective theorem

(s : Subring R) : Function.Injective s.subtype

Full source

lemma subtype_injective (s : Subring R) :
    Function.Injective s.subtype :=
  s.toSubmonoid.subtype_injective

Injectivity of Subring Inclusion Homomorphism

Informal description

For any subring $s$ of a ring $R$, the inclusion homomorphism $\text{subtype} \colon s \to R$ is injective. That is, if $\text{subtype}(x) = \text{subtype}(y)$ for $x, y \in s$, then $x = y$.

Subring.coe_subtype theorem

: ⇑s.subtype = ((↑) : s → R)

Full source

@[simp]
theorem coe_subtype : ⇑s.subtype = ((↑) : s → R) :=
  rfl

Inclusion Homomorphism Coincides with Coercion for Subrings

Informal description

For any subring $s$ of a ring $R$, the underlying function of the inclusion homomorphism $s.subtype$ is equal to the coercion map from $s$ to $R$.

Subring.coe_natCast theorem

(n : ℕ) : ((n : s) : R) = n

Full source

@[norm_cast]
theorem coe_natCast (n : ℕ) : ((n : s) : R) = n := rfl

Natural Number Coercion from Subring to Ring Preserves Value

Informal description

For any natural number $n$ and any subring $s$ of a ring $R$, the canonical inclusion map from $s$ to $R$ maps the natural number $n$ (interpreted in $s$) to the natural number $n$ in $R$. In other words, the coercion of the natural number $n$ from the subring $s$ to the ring $R$ is equal to $n$ itself.

Subring.coe_intCast theorem

(n : ℤ) : ((n : s) : R) = n

Full source

@[norm_cast]
theorem coe_intCast (n : ℤ) : ((n : s) : R) = n := rfl

Integer Cast Inclusion in Subrings Preserves Value

Informal description

For any subring $s$ of a ring $R$ and any integer $n \in \mathbb{Z}$, the image of $n$ under the canonical inclusion map from $s$ to $R$ is equal to $n$ itself.

Subring.coe_toSubsemiring theorem

(s : Subring R) : (s.toSubsemiring : Set R) = s

Full source

@[simp]
theorem coe_toSubsemiring (s : Subring R) : (s.toSubsemiring : Set R) = s :=
  rfl

Subring and Subsemiring Underlying Set Equality

Informal description

For any subring $s$ of a ring $R$, the underlying set of $s$ viewed as a subsemiring is equal to the underlying set of $s$ itself.

Subring.mem_toSubmonoid theorem

{s : Subring R} {x : R} : x ∈ s.toSubmonoid ↔ x ∈ s

Full source

theorem mem_toSubmonoid {s : Subring R} {x : R} : x ∈ s.toSubmonoidx ∈ s.toSubmonoid ↔ x ∈ s :=
  Iff.rfl

Membership in Subring's Submonoid is Equivalent to Membership in Subring

Informal description

For any subring $s$ of a ring $R$ and any element $x \in R$, $x$ belongs to the underlying submonoid of $s$ if and only if $x$ belongs to $s$.

Subring.coe_toSubmonoid theorem

(s : Subring R) : (s.toSubmonoid : Set R) = s

Full source

@[simp]
theorem coe_toSubmonoid (s : Subring R) : (s.toSubmonoid : Set R) = s :=
  rfl

Subring to Submonoid Set Equality

Informal description

For any subring $s$ of a ring $R$, the underlying set of the submonoid associated with $s$ is equal to $s$ itself, i.e., $(s.\text{toSubmonoid} : \text{Set } R) = s$.

Subring.mem_toAddSubgroup theorem

{s : Subring R} {x : R} : x ∈ s.toAddSubgroup ↔ x ∈ s

Full source

theorem mem_toAddSubgroup {s : Subring R} {x : R} : x ∈ s.toAddSubgroupx ∈ s.toAddSubgroup ↔ x ∈ s :=
  Iff.rfl

Membership in Subring's Additive Subgroup is Equivalent to Membership in Subring

Informal description

For any subring $s$ of a ring $R$ and any element $x \in R$, $x$ belongs to the underlying additive subgroup of $s$ if and only if $x$ belongs to $s$.

Subring.coe_toAddSubgroup theorem

(s : Subring R) : (s.toAddSubgroup : Set R) = s

Full source

@[simp]
theorem coe_toAddSubgroup (s : Subring R) : (s.toAddSubgroup : Set R) = s :=
  rfl

Equality of Subring and its Additive Subgroup's Underlying Set

Informal description

For any subring $s$ of a ring $R$, the underlying set of the additive subgroup associated with $s$ is equal to $s$ itself, i.e., $(s.\text{toAddSubgroup} : \text{Set } R) = s$.

NonUnitalSubring.toSubring definition

(S : NonUnitalSubring R) (h1 : (1 : R) ∈ S) : Subring R

Full source

/-- Turn a non-unital subring containing `1` into a subring. -/
def NonUnitalSubring.toSubring (S : NonUnitalSubring R) (h1 : (1 : R) ∈ S) : Subring R where
  __ := S
  one_mem' := h1

Subring from non-unital subring containing 1

Informal description

Given a non-unital subring $S$ of a ring $R$ that contains the multiplicative identity $1$, the function constructs a subring of $R$ with the same underlying set as $S$.

Subring.toNonUnitalSubring_toSubring theorem

(S : Subring R) : S.toNonUnitalSubring.toSubring S.one_mem = S

Full source

lemma Subring.toNonUnitalSubring_toSubring (S : Subring R) :
    S.toNonUnitalSubring.toSubring S.one_mem = S := by cases S; rfl

Subring-NonUnitalSubring Roundtrip Identity

Informal description

For any subring $S$ of a ring $R$, the subring obtained by first converting $S$ to a non-unital subring and then back to a subring (using the fact that $1 \in S$) is equal to $S$ itself.

NonUnitalSubring.toSubring_toNonUnitalSubring theorem

(S : NonUnitalSubring R) (h1 : (1 : R) ∈ S) : (NonUnitalSubring.toSubring S h1).toNonUnitalSubring = S

Full source

lemma NonUnitalSubring.toSubring_toNonUnitalSubring (S : NonUnitalSubring R) (h1 : (1 : R) ∈ S) :
    (NonUnitalSubring.toSubring S h1).toNonUnitalSubring = S := by cases S; rfl

Subring-NonUnitalSubring Roundtrip Equality

Informal description

Let $R$ be a ring and $S$ be a non-unital subring of $R$ containing the multiplicative identity $1$. Then the non-unital subring obtained by forgetting the multiplicative identity condition from the subring $\text{NonUnitalSubring.toSubring}(S, h1)$ is equal to $S$ itself.