Documentation

Mathlib.RingTheory.NonUnitalSubring.Basic

NonUnitalSubrings #

Let R be a non-unital ring. We prove that non-unital 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 NonUnitalSubring R, sending a subset of R to the non-unital subring it generates, and prove that it is a Galois insertion.

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)

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

theorem NonUnitalSubring.list_sum_mem {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {l : List R} :
(∀ xl, x s)l.sum s

Sum of a list of elements in a non-unital subring is in the non-unital subring.

theorem NonUnitalSubring.multiset_sum_mem {R : Type u_1} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (m : Multiset R) :
(∀ am, a s)m.sum s

Sum of a multiset of elements in a NonUnitalSubring of a NonUnitalRing is in the NonUnitalSubring.

theorem NonUnitalSubring.sum_mem {R : Type u_1} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {ι : Type u_2} {t : Finset ι} {f : ιR} (h : ct, f c s) :
it, f i s

Sum of elements in a NonUnitalSubring of a NonUnitalRing indexed by a Finset is in the NonUnitalSubring.

top #

The non-unital subring R of the ring R.

Equations
    @[simp]

    The ring equiv between the top element of NonUnitalSubring R and R.

    Equations
      Instances For
        @[simp]

        comap #

        The preimage of a NonUnitalSubring along a ring homomorphism is a NonUnitalSubring.

        Equations
          Instances For
            @[simp]
            theorem NonUnitalSubring.coe_comap {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (s : NonUnitalSubring S) (f : F) :
            (comap f s) = f ⁻¹' s
            @[simp]
            theorem NonUnitalSubring.mem_comap {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] {s : NonUnitalSubring S} {f : F} {x : R} :
            x comap f s f x s

            map #

            The image of a NonUnitalSubring along a ring homomorphism is a NonUnitalSubring.

            Equations
              Instances For
                @[simp]
                theorem NonUnitalSubring.coe_map {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) (s : NonUnitalSubring R) :
                (map f s) = f '' s
                @[simp]
                theorem NonUnitalSubring.mem_map {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] {f : F} {s : NonUnitalSubring R} {y : S} :
                y map f s xs, f x = y
                theorem NonUnitalSubring.map_map {R : Type u} {S : Type v} {T : Type u_1} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [NonUnitalNonAssocRing T] (s : NonUnitalSubring R) (g : S →ₙ+* T) (f : R →ₙ+* S) :
                map g (map f s) = map (g.comp f) s
                noncomputable def NonUnitalSubring.equivMapOfInjective {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (s : NonUnitalSubring R) (f : F) (hf : Function.Injective f) :
                s ≃+* (map f s)

                A NonUnitalSubring is isomorphic to its image under an injective function

                Equations
                  Instances For
                    @[simp]
                    theorem NonUnitalSubring.coe_equivMapOfInjective_apply {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (s : NonUnitalSubring R) (f : F) (hf : Function.Injective f) (x : s) :
                    ((s.equivMapOfInjective f hf) x) = f x

                    range #

                    The range of a ring homomorphism, as a NonUnitalSubring of the target. See Note [range copy pattern].

                    Equations
                      Instances For
                        @[simp]
                        theorem NonUnitalRingHom.mem_range {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f : R →ₙ+* S} {y : S} :
                        y f.range ∃ (x : R), f x = y

                        The range of a ring homomorphism is a fintype, if the domain is a fintype. Note: this instance can form a diamond with Subtype.fintype in the presence of Fintype S.

                        Equations

                          bot #

                          inf #

                          The inf of two NonUnitalSubrings is their intersection.

                          Equations
                            @[simp]
                            theorem NonUnitalSubring.coe_inf {R : Type u} [NonUnitalNonAssocRing R] (p p' : NonUnitalSubring R) :
                            (pp') = p p'
                            @[simp]
                            theorem NonUnitalSubring.mem_inf {R : Type u} [NonUnitalNonAssocRing R] {p p' : NonUnitalSubring R} {x : R} :
                            x pp' x p x p'
                            @[simp]
                            theorem NonUnitalSubring.coe_sInf {R : Type u} [NonUnitalNonAssocRing R] (S : Set (NonUnitalSubring R)) :
                            (sInf S) = sS, s
                            theorem NonUnitalSubring.mem_sInf {R : Type u} [NonUnitalNonAssocRing R] {S : Set (NonUnitalSubring R)} {x : R} :
                            x sInf S pS, x p
                            @[simp]
                            theorem NonUnitalSubring.coe_iInf {R : Type u} [NonUnitalNonAssocRing R] {ι : Sort u_1} {S : ιNonUnitalSubring R} :
                            (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                            theorem NonUnitalSubring.mem_iInf {R : Type u} [NonUnitalNonAssocRing R] {ι : Sort u_1} {S : ιNonUnitalSubring R} {x : R} :
                            x ⨅ (i : ι), S i ∀ (i : ι), x S i

                            Center of a ring #

                            The center of a ring R is the set of elements that commute with everything in R

                            Equations
                              Instances For

                                The center is commutative and associative.

                                Equations

                                  The center of isomorphic (not necessarily unital or associative) rings are isomorphic.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem NonUnitalSubring.centerCongr_apply_coe {R : Type u} [NonUnitalNonAssocRing R] {S : Type u_1} [NonUnitalNonAssocRing S] (e : R ≃+* S) (r : (Subsemigroup.center R)) :
                                      ((centerCongr e) r) = e r
                                      @[simp]

                                      The center of a (not necessarily uintal or associative) ring is isomorphic to the center of its opposite.

                                      Equations
                                        Instances For
                                          theorem NonUnitalSubring.mem_center_iff {R : Type u} [NonUnitalRing R] {z : R} :
                                          z center R ∀ (g : R), g * z = z * g

                                          NonUnitalSubring closure of a subset #

                                          The NonUnitalSubring generated by a set.

                                          Equations
                                            Instances For
                                              theorem NonUnitalSubring.mem_closure {R : Type u} [NonUnitalNonAssocRing R] {x : R} {s : Set R} :
                                              x closure s ∀ (S : NonUnitalSubring R), s Sx S
                                              @[simp]

                                              The NonUnitalSubring generated by a set includes the set.

                                              theorem NonUnitalSubring.notMem_of_notMem_closure {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {P : R} (hP : Pclosure s) :
                                              Ps
                                              @[deprecated NonUnitalSubring.notMem_of_notMem_closure (since := "2025-05-23")]
                                              theorem NonUnitalSubring.not_mem_of_not_mem_closure {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {P : R} (hP : Pclosure s) :
                                              Ps

                                              Alias of NonUnitalSubring.notMem_of_notMem_closure.

                                              @[simp]

                                              A NonUnitalSubring t includes closure s if and only if it includes s.

                                              theorem NonUnitalSubring.closure_mono {R : Type u} [NonUnitalNonAssocRing R] s t : Set R (h : s t) :

                                              NonUnitalSubring closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t.

                                              theorem NonUnitalSubring.closure_eq_of_le {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {t : NonUnitalSubring R} (h₁ : s t) (h₂ : t closure s) :
                                              theorem NonUnitalSubring.closure_induction {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {p : (x : R) → x closure sProp} (mem : ∀ (x : R) (hx : x s), p x ) (zero : p 0 ) (add : ∀ (x y : R) (hx : x closure s) (hy : y closure s), p x hxp y hyp (x + y) ) (neg : ∀ (x : R) (hx : x closure s), p x hxp (-x) ) (mul : ∀ (x y : R) (hx : x closure s) (hy : y closure s), p x hxp y hyp (x * y) ) {x : R} (hx : x closure s) :
                                              p x hx

                                              An induction principle for closure membership. If p holds for 0, 1, and all elements of s, and is preserved under addition, negation, and multiplication, then p holds for all elements of the closure of s.

                                              theorem NonUnitalSubring.closure_induction₂ {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {p : (x y : R) → x closure sy closure sProp} (mem_mem : ∀ (x y : R) (hx : x s) (hy : y s), p x y ) (zero_left : ∀ (x : R) (hx : x closure s), p 0 x hx) (zero_right : ∀ (x : R) (hx : x closure s), p x 0 hx ) (neg_left : ∀ (x y : R) (hx : x closure s) (hy : y closure s), p x y hx hyp (-x) y hy) (neg_right : ∀ (x y : R) (hx : x closure s) (hy : y closure s), p x y hx hyp x (-y) hx ) (add_left : ∀ (x y z : R) (hx : x closure s) (hy : y closure s) (hz : z closure s), p x z hx hzp y z hy hzp (x + y) z hz) (add_right : ∀ (x y z : R) (hx : x closure s) (hy : y closure s) (hz : z closure s), p x y hx hyp x z hx hzp x (y + z) hx ) (mul_left : ∀ (x y z : R) (hx : x closure s) (hy : y closure s) (hz : z closure s), p x z hx hzp y z hy hzp (x * y) z hz) (mul_right : ∀ (x y z : R) (hx : x closure s) (hy : y closure s) (hz : z closure s), p x y hx hyp x z hx hzp x (y * z) hx ) {x y : R} (hx : x closure s) (hy : y closure s) :
                                              p x y hx hy

                                              An induction principle for closure membership, for predicates with two arguments.

                                              def NonUnitalSubring.closureNonUnitalCommRingOfComm {R : Type u} [NonUnitalRing R] {s : Set R} (hcomm : as, bs, a * b = b * a) :

                                              If all elements of s : Set A commute pairwise, then closure s is a commutative ring.

                                              Equations
                                                Instances For

                                                  closure forms a Galois insertion with the coercion to set.

                                                  Equations
                                                    Instances For
                                                      @[simp]

                                                      Closure of a NonUnitalSubring S equals S.

                                                      theorem NonUnitalSubring.closure_iUnion {R : Type u} [NonUnitalNonAssocRing R] {ι : Sort u_1} (s : ιSet R) :
                                                      closure (⋃ (i : ι), s i) = ⨆ (i : ι), closure (s i)
                                                      theorem NonUnitalSubring.map_sup {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (s t : NonUnitalSubring R) (f : F) :
                                                      map f (st) = map f smap f t
                                                      theorem NonUnitalSubring.map_iSup {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] {ι : Sort u_1} (f : F) (s : ιNonUnitalSubring R) :
                                                      map f (iSup s) = ⨆ (i : ι), map f (s i)
                                                      theorem NonUnitalSubring.map_inf {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (s t : NonUnitalSubring R) (f : F) (hf : Function.Injective f) :
                                                      map f (st) = map f smap f t
                                                      theorem NonUnitalSubring.map_iInf {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] {ι : Sort u_1} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ιNonUnitalSubring R) :
                                                      map f (iInf s) = ⨅ (i : ι), map f (s i)
                                                      theorem NonUnitalSubring.comap_inf {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (s t : NonUnitalSubring S) (f : F) :
                                                      comap f (st) = comap f scomap f t
                                                      theorem NonUnitalSubring.comap_iInf {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] {ι : Sort u_1} (f : F) (s : ιNonUnitalSubring S) :
                                                      comap f (iInf s) = ⨅ (i : ι), comap f (s i)

                                                      Given NonUnitalSubrings s, t of rings R, S respectively, s.prod t is s ×ˢ t as a NonUnitalSubring of R × S.

                                                      Equations
                                                        Instances For
                                                          theorem NonUnitalSubring.mem_prod {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {s : NonUnitalSubring R} {t : NonUnitalSubring S} {p : R × S} :
                                                          p s.prod t p.1 s p.2 t
                                                          theorem NonUnitalSubring.prod_mono {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] s₁ s₂ : NonUnitalSubring R (hs : s₁ s₂) t₁ t₂ : NonUnitalSubring S (ht : t₁ t₂) :
                                                          s₁.prod t₁ s₂.prod t₂

                                                          Product of NonUnitalSubrings is isomorphic to their product as rings.

                                                          Equations
                                                            Instances For
                                                              theorem NonUnitalSubring.mem_iSup_of_directed {R : Type u} [NonUnitalNonAssocRing R] {ι : Sort u_1} [ : Nonempty ι] {S : ιNonUnitalSubring R} (hS : Directed (fun (x1 x2 : NonUnitalSubring R) => x1 x2) S) {x : R} :
                                                              x ⨆ (i : ι), S i ∃ (i : ι), x S i

                                                              The underlying set of a non-empty directed Sup of NonUnitalSubrings is just a union of the NonUnitalSubrings. Note that this fails without the directedness assumption (the union of two NonUnitalSubrings is typically not a NonUnitalSubring)

                                                              theorem NonUnitalSubring.coe_iSup_of_directed {R : Type u} [NonUnitalNonAssocRing R] {ι : Sort u_1} [Nonempty ι] {S : ιNonUnitalSubring R} (hS : Directed (fun (x1 x2 : NonUnitalSubring R) => x1 x2) S) :
                                                              (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
                                                              theorem NonUnitalSubring.mem_sSup_of_directedOn {R : Type u} [NonUnitalNonAssocRing R] {S : Set (NonUnitalSubring R)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : NonUnitalSubring R) => x1 x2) S) {x : R} :
                                                              x sSup S sS, x s
                                                              theorem NonUnitalSubring.coe_sSup_of_directedOn {R : Type u} [NonUnitalNonAssocRing R] {S : Set (NonUnitalSubring R)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : NonUnitalSubring R) => x1 x2) S) :
                                                              (sSup S) = sS, s
                                                              theorem NonUnitalSubring.mem_map_equiv {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f : R ≃+* S} {K : NonUnitalSubring R} {x : S} :
                                                              x map (↑f) K f.symm x K

                                                              Restriction of a ring homomorphism to its range interpreted as a NonUnitalSubring.

                                                              This is the bundled version of Set.rangeFactorization.

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem NonUnitalRingHom.coe_rangeRestrict {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (x : R) :
                                                                  (f.rangeRestrict x) = f x
                                                                  @[deprecated NonUnitalRingHom.range_eq_top (since := "2024-11-11")]

                                                                  Alias of NonUnitalRingHom.range_eq_top.

                                                                  @[simp]

                                                                  The range of a surjective ring homomorphism is the whole of the codomain.

                                                                  @[deprecated NonUnitalRingHom.range_eq_top_of_surjective (since := "2024-11-11")]

                                                                  Alias of NonUnitalRingHom.range_eq_top_of_surjective.


                                                                  The range of a surjective ring homomorphism is the whole of the codomain.

                                                                  The NonUnitalSubring of elements x : R such that f x = g x, i.e., the equalizer of f and g as a NonUnitalSubring of R

                                                                  Equations
                                                                    Instances For
                                                                      theorem NonUnitalRingHom.eqOn_set_closure {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f g : R →ₙ+* S} {s : Set R} (h : Set.EqOn (⇑f) (⇑g) s) :

                                                                      If two ring homomorphisms are equal on a set, then they are equal on its NonUnitalSubring closure.

                                                                      theorem NonUnitalRingHom.eq_of_eqOn_set_top {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f g : R →ₙ+* S} (h : Set.EqOn f g ) :
                                                                      f = g
                                                                      theorem NonUnitalRingHom.eq_of_eqOn_set_dense {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {s : Set R} (hs : NonUnitalSubring.closure s = ) {f g : R →ₙ+* S} (h : Set.EqOn (⇑f) (⇑g) s) :
                                                                      f = g

                                                                      The image under a ring homomorphism of the NonUnitalSubring generated by a set equals the NonUnitalSubring generated by the image of the set.

                                                                      def RingEquiv.nonUnitalSubringCongr {R : Type u} [NonUnitalRing R] {s t : NonUnitalSubring R} (h : s = t) :
                                                                      s ≃+* t

                                                                      Makes the identity isomorphism from a proof two NonUnitalSubrings of a multiplicative monoid are equal.

                                                                      Equations
                                                                        Instances For
                                                                          def RingEquiv.ofLeftInverse' {R : Type u} {S : Type v} [NonUnitalRing R] [NonUnitalRing S] {g : SR} {f : R →ₙ+* S} (h : Function.LeftInverse g f) :
                                                                          R ≃+* f.range

                                                                          Restrict a ring homomorphism with a left inverse to a ring isomorphism to its RingHom.range.

                                                                          Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem RingEquiv.ofLeftInverse'_apply {R : Type u} {S : Type v} [NonUnitalRing R] [NonUnitalRing S] {g : SR} {f : R →ₙ+* S} (h : Function.LeftInverse g f) (x : R) :
                                                                              ((ofLeftInverse' h) x) = f x
                                                                              @[simp]
                                                                              theorem RingEquiv.ofLeftInverse'_symm_apply {R : Type u} {S : Type v} [NonUnitalRing R] [NonUnitalRing S] {g : SR} {f : R →ₙ+* S} (h : Function.LeftInverse g f) (x : f.range) :
                                                                              (ofLeftInverse' h).symm x = g x