Documentation

Mathlib.Algebra.Ring.Subring.Defs

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)

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

class SubringClass (S : Type u_1) (R : outParam (Type u)) [Ring R] [SetLike S R] extends SubsemiringClass S R, NegMemClass S R :

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

Instances
    @[instance 100]
    instance SubringClass.addSubgroupClass (S : Type u_1) (R : Type u) [SetLike S R] [Ring R] [h : SubringClass S R] :
    @[instance 100]
    theorem intCast_mem {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ) :
    n s
    @[instance 75]
    instance SubringClass.toHasIntCast {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) :
    IntCast s
    Equations
      @[instance 75]
      instance SubringClass.toRing {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) :
      Ring s

      A subring of a ring inherits a ring structure

      Equations
        @[instance 75]
        instance SubringClass.toCommRing {S : Type v} (s : S) {R : Type u_1} [CommRing R] [SetLike S R] [SubringClass S R] :

        A subring of a CommRing is a CommRing.

        Equations
          @[instance 75]
          instance SubringClass.instIsDomainSubtypeMem {S : Type v} (s : S) {R : Type u_1} [Ring R] [IsDomain R] [SetLike S R] [SubringClass S R] :

          A subring of a domain is a domain.

          def SubringClass.subtype {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) :
          s →+* R

          The natural ring hom from a subring of ring R to R.

          Equations
            Instances For
              @[simp]
              theorem SubringClass.subtype_apply {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] {s : S} (x : s) :
              (subtype s) x = x
              theorem SubringClass.subtype_injective {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) :
              @[simp]
              theorem SubringClass.coe_subtype {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) :
              @[deprecated SubringClass.coe_subtype (since := "2025-02-18")]
              theorem SubringClass.coeSubtype {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) :

              Alias of SubringClass.coe_subtype.

              @[simp]
              theorem SubringClass.coe_natCast {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ) :
              n = n
              @[simp]
              theorem SubringClass.coe_intCast {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ) :
              n = n
              structure Subring (R : Type u) [Ring R] extends Subsemiring R, AddSubgroup R :

              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.

              Instances For
                instance Subring.instSetLike {R : Type u} [Ring R] :
                Equations
                  def Subring.ofClass {S : Type u_1} {R : Type u_2} [Ring R] [SetLike S R] [SubringClass S R] (s : S) :

                  The actual Subring obtained from an element of a SubringClass.

                  Equations
                    Instances For
                      @[simp]
                      theorem Subring.coe_ofClass {S : Type u_1} {R : Type u_2} [Ring R] [SetLike S R] [SubringClass S R] (s : S) :
                      (ofClass s) = s
                      @[instance 100]
                      instance Subring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg {R : Type u} [Ring R] :
                      CanLift (Set R) (Subring R) SetLike.coe fun (s : Set R) => 0 s (∀ {x y : R}, x sy sx + y s) 1 s (∀ {x y : R}, x sy sx * y s) ∀ {x : R}, x s-x s

                      Turn a Subring into a NonUnitalSubring by forgetting that it contains 1.

                      Equations
                        Instances For
                          @[simp]
                          theorem Subring.mem_toSubsemiring {R : Type u} [Ring R] {s : Subring R} {x : R} :
                          theorem Subring.mem_carrier {R : Type u} [Ring R] {s : Subring R} {x : R} :
                          x s.carrier x s
                          @[simp]
                          theorem Subring.mem_mk {R : Type u} [Ring R] {S : Subsemiring R} {x : R} (h : ∀ {x : R}, x S.carrier-x S.carrier) :
                          x { toSubsemiring := S, neg_mem' := h } x S
                          @[simp]
                          theorem Subring.coe_set_mk {R : Type u} [Ring R] (S : Subsemiring R) (h : ∀ {x : R}, x S.carrier-x S.carrier) :
                          { toSubsemiring := S, neg_mem' := h } = S
                          @[simp]
                          theorem Subring.mk_le_mk {R : Type u} [Ring R] {S S' : Subsemiring R} (h₁ : ∀ {x : R}, x S.carrier-x S.carrier) (h₂ : ∀ {x : R}, x S'.carrier-x S'.carrier) :
                          { toSubsemiring := S, neg_mem' := h₁ } { toSubsemiring := S', neg_mem' := h₂ } S S'
                          theorem Subring.ext {R : Type u} [Ring R] {S T : Subring R} (h : ∀ (x : R), x S x T) :
                          S = T

                          Two subrings are equal if they have the same elements.

                          theorem Subring.ext_iff {R : Type u} [Ring R] {S T : Subring R} :
                          S = T ∀ (x : R), x S x T
                          def Subring.copy {R : Type u} [Ring R] (S : Subring R) (s : Set R) (hs : s = S) :

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

                          Equations
                            Instances For
                              @[simp]
                              theorem Subring.copy_toSubsemiring {R : Type u} [Ring R] (S : Subring R) (s : Set R) (hs : s = S) :
                              (S.copy s hs).toSubsemiring = { carrier := s, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := }
                              @[simp]
                              theorem Subring.coe_copy {R : Type u} [Ring R] (S : Subring R) (s : Set R) (hs : s = S) :
                              (S.copy s hs) = s
                              theorem Subring.copy_eq {R : Type u} [Ring R] (S : Subring R) (s : Set R) (hs : s = S) :
                              S.copy s hs = S
                              def Subring.mk' {R : Type u} [Ring R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : sm = s) (ha : sa = s) :

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

                              Equations
                                Instances For
                                  @[simp]
                                  theorem Subring.coe_mk' {R : Type u} [Ring R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : sm = s) (ha : sa = s) :
                                  (Subring.mk' s sm sa hm ha) = s
                                  @[simp]
                                  theorem Subring.mem_mk' {R : Type u} [Ring R] {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
                                  @[simp]
                                  theorem Subring.mk'_toSubmonoid {R : Type u} [Ring R] {s : Set R} {sm : Submonoid R} (hm : sm = s) {sa : AddSubgroup R} (ha : sa = s) :
                                  (Subring.mk' s sm sa hm ha).toSubmonoid = sm
                                  @[simp]
                                  theorem Subring.mk'_toAddSubgroup {R : Type u} [Ring R] {s : Set R} {sm : Submonoid R} (hm : sm = s) {sa : AddSubgroup R} (ha : sa = s) :
                                  (Subring.mk' s sm sa hm ha).toAddSubgroup = sa
                                  def Subsemiring.toSubring {R : Type u} [Ring R] (s : Subsemiring R) (hneg : -1 s) :

                                  A Subsemiring containing -1 is a Subring.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem Subsemiring.toSubring_toSubsemiring {R : Type u} [Ring R] (s : Subsemiring R) (hneg : -1 s) :
                                      theorem Subring.one_mem {R : Type u} [Ring R] (s : Subring R) :
                                      1 s

                                      A subring contains the ring's 1.

                                      theorem Subring.zero_mem {R : Type u} [Ring R] (s : Subring R) :
                                      0 s

                                      A subring contains the ring's 0.

                                      theorem Subring.mul_mem {R : Type u} [Ring R] (s : Subring R) {x y : R} :
                                      x sy sx * y s

                                      A subring is closed under multiplication.

                                      theorem Subring.add_mem {R : Type u} [Ring R] (s : Subring R) {x y : R} :
                                      x sy sx + y s

                                      A subring is closed under addition.

                                      theorem Subring.neg_mem {R : Type u} [Ring R] (s : Subring R) {x : R} :
                                      x s-x s

                                      A subring is closed under negation.

                                      theorem Subring.sub_mem {R : Type u} [Ring R] (s : Subring R) {x y : R} (hx : x s) (hy : y s) :
                                      x - y s

                                      A subring is closed under subtraction

                                      instance Subring.toRing {R : Type u} [Ring R] (s : Subring R) :
                                      Ring s

                                      A subring of a ring inherits a ring structure

                                      Equations
                                        theorem Subring.zsmul_mem {R : Type u} [Ring R] (s : Subring R) {x : R} (hx : x s) (n : ) :
                                        n x s
                                        theorem Subring.pow_mem {R : Type u} [Ring R] (s : Subring R) {x : R} (hx : x s) (n : ) :
                                        x ^ n s
                                        @[simp]
                                        theorem Subring.coe_add {R : Type u} [Ring R] (s : Subring R) (x y : s) :
                                        ↑(x + y) = x + y
                                        @[simp]
                                        theorem Subring.coe_neg {R : Type u} [Ring R] (s : Subring R) (x : s) :
                                        ↑(-x) = -x
                                        @[simp]
                                        theorem Subring.coe_mul {R : Type u} [Ring R] (s : Subring R) (x y : s) :
                                        ↑(x * y) = x * y
                                        @[simp]
                                        theorem Subring.coe_zero {R : Type u} [Ring R] (s : Subring R) :
                                        0 = 0
                                        @[simp]
                                        theorem Subring.coe_one {R : Type u} [Ring R] (s : Subring R) :
                                        1 = 1
                                        @[simp]
                                        theorem Subring.coe_pow {R : Type u} [Ring R] (s : Subring R) (x : s) (n : ) :
                                        ↑(x ^ n) = x ^ n
                                        theorem Subring.coe_eq_zero_iff {R : Type u} [Ring R] (s : Subring R) {x : s} :
                                        x = 0 x = 0
                                        instance Subring.toCommRing {R : Type u_1} [CommRing R] (s : Subring R) :

                                        A subring of a CommRing is a CommRing.

                                        Equations
                                          instance Subring.instNontrivialSubtypeMem {R : Type u_1} [Ring R] [Nontrivial R] (s : Subring R) :

                                          A subring of a non-trivial ring is non-trivial.

                                          A subring of a ring with no zero divisors has no zero divisors.

                                          instance Subring.instIsDomainSubtypeMem {R : Type u_1} [Ring R] [IsDomain R] (s : Subring R) :

                                          A subring of a domain is a domain.

                                          def Subring.subtype {R : Type u} [Ring R] (s : Subring R) :
                                          s →+* R

                                          The natural ring hom from a subring of ring R to R.

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem Subring.subtype_apply {R : Type u} [Ring R] {s : Subring R} (x : s) :
                                              s.subtype x = x
                                              @[simp]
                                              theorem Subring.coe_subtype {R : Type u} [Ring R] (s : Subring R) :
                                              @[deprecated Subring.coe_subtype (since := "2025-02-18")]
                                              theorem Subring.coeSubtype {R : Type u} [Ring R] (s : Subring R) :

                                              Alias of Subring.coe_subtype.

                                              theorem Subring.coe_natCast {R : Type u} [Ring R] (s : Subring R) (n : ) :
                                              n = n
                                              theorem Subring.coe_intCast {R : Type u} [Ring R] (s : Subring R) (n : ) :
                                              n = n

                                              Partial order #

                                              @[simp]
                                              theorem Subring.coe_toSubsemiring {R : Type u} [Ring R] (s : Subring R) :
                                              s.toSubsemiring = s
                                              theorem Subring.mem_toSubmonoid {R : Type u} [Ring R] {s : Subring R} {x : R} :
                                              @[simp]
                                              theorem Subring.coe_toSubmonoid {R : Type u} [Ring R] (s : Subring R) :
                                              s.toSubmonoid = s
                                              theorem Subring.mem_toAddSubgroup {R : Type u} [Ring R] {s : Subring R} {x : R} :
                                              @[simp]
                                              theorem Subring.coe_toAddSubgroup {R : Type u} [Ring R] (s : Subring R) :
                                              s.toAddSubgroup = s
                                              def NonUnitalSubring.toSubring {R : Type u} [Ring R] (S : NonUnitalSubring R) (h1 : 1 S) :

                                              Turn a non-unital subring containing 1 into a subring.

                                              Equations
                                                Instances For