# 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.

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)

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

• instance : CompleteLattice (NonUnitalSubring R) : the complete lattice structure on the non-unital subrings.

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

• NonUnitalSubring.closure : non-unital subring closure of a set, i.e., the smallest non-unital subring that includes the set.

• NonUnitalSubring.gi : closure : Set M → NonUnitalSubring M and coercion coe : NonUnitalSubring M → Set M form a GaloisInsertion.

• comap f B : NonUnitalSubring A : the preimage of a non-unital subring B along the non-unital ring homomorphism f

• map f A : NonUnitalSubring B : the image of a non-unital subring A along the non-unital ring homomorphism f.

• Prod A B : NonUnitalSubring (R × S) : the product of non-unital subrings

• f.range : NonUnitalSubring B : the range of the non-unital ring homomorphism f.

• eq_locus f g : NonUnitalSubring R : given non-unital ring homomorphisms f g : R →ₙ+* S, the non-unital subring of R where f x = g x

## 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) [SetLike S R] extends , :

NonUnitalSubringClass 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 NonUnitalSubringClass.addSubgroupClass (S : Type u_1) (R : Type u) [SetLike S R] [h : ] :
Equations
• =
@[instance 75]
instance NonUnitalSubringClass.toNonUnitalNonAssocRing {R : Type u} {S : Type v} [SetLike S R] [hSR : ] (s : S) :

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

Equations
@[instance 75]
instance NonUnitalSubringClass.toNonUnitalRing {S : Type v} {R : Type u_1} [] [SetLike S R] [] (s : S) :

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

Equations
@[instance 75]
instance NonUnitalSubringClass.toNonUnitalCommRing {S : Type v} (s : S) {R : Type u_1} [SetLike S R] [] :

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

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

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

Equations
• = let __src := ; let __src := s; { toFun := Subtype.val, map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem NonUnitalSubringClass.coe_subtype {R : Type u} {S : Type v} [SetLike S R] [hSR : ] (s : S) :
= Subtype.val
structure NonUnitalSubring (R : Type u) extends :

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.carrierb self.carriera + b self.carrier
• zero_mem' : 0 self.carrier
• mul_mem' : ∀ {a b : R}, a self.carrierb self.carriera * b self.carrier
• neg_mem' : ∀ {x : R}, x self.carrier-x self.carrier

G is closed under negation

Instances For
@[reducible]
abbrev NonUnitalSubring.toAddSubgroup {R : Type u} (self : ) :

Reinterpret a NonUnitalSubring as an AddSubgroup.

Equations
Instances For

The underlying submonoid of a NonUnitalSubring.

Equations
• s.toSubsemigroup = let __src := s.toSubsemigroup; { carrier := s.carrier, mul_mem' := }
Instances For
Equations
• NonUnitalSubring.instSetLike = { coe := fun (s : ) => s.carrier, coe_injective' := }
Equations
• =
theorem NonUnitalSubring.mem_carrier {R : Type u} {s : } {x : R} :
x s.toNonUnitalSubsemiring x s
@[simp]
theorem NonUnitalSubring.mem_mk {R : Type u} {S : } {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} (S : ) (h : ∀ {x : R}, x S.carrier-x S.carrier) :
{ toNonUnitalSubsemiring := S, neg_mem' := h } = S
@[simp]
theorem NonUnitalSubring.mk_le_mk {R : Type u} {S : } {S' : } (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} {S : } {T : } (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} (S : ) (s : Set R) (hs : s = S) :

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 = let __src := S.copy s hs; { carrier := s, add_mem' := , zero_mem' := , mul_mem' := , neg_mem' := }
Instances For
@[simp]
theorem NonUnitalSubring.coe_copy {R : Type u} (S : ) (s : Set R) (hs : s = S) :
(S.copy s hs) = s
theorem NonUnitalSubring.copy_eq {R : Type u} (S : ) (s : Set R) (hs : s = S) :
S.copy s hs = S
theorem NonUnitalSubring.toNonUnitalSubsemiring_injective {R : Type u} :
Function.Injective NonUnitalSubring.toNonUnitalSubsemiring
theorem NonUnitalSubring.toNonUnitalSubsemiring_strictMono {R : Type u} :
StrictMono NonUnitalSubring.toNonUnitalSubsemiring
theorem NonUnitalSubring.toNonUnitalSubsemiring_mono {R : Type u} :
Monotone NonUnitalSubring.toNonUnitalSubsemiring
theorem NonUnitalSubring.toAddSubgroup_injective {R : Type u} :
theorem NonUnitalSubring.toAddSubgroup_strictMono {R : Type u} :
theorem NonUnitalSubring.toAddSubgroup_mono {R : Type u} :
theorem NonUnitalSubring.toSubsemigroup_injective {R : Type u} :
Function.Injective NonUnitalSubring.toSubsemigroup
theorem NonUnitalSubring.toSubsemigroup_strictMono {R : Type u} :
StrictMono NonUnitalSubring.toSubsemigroup
theorem NonUnitalSubring.toSubsemigroup_mono {R : Type u} :
Monotone NonUnitalSubring.toSubsemigroup
def NonUnitalSubring.mk' {R : Type u} (s : Set R) (sm : ) (sa : ) (hm : sm = s) (ha : sa = s) :

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 = let __src := sm.copy s ; let __src_1 := sa.copy s ; { carrier := __src.carrier, add_mem' := , zero_mem' := , mul_mem' := , neg_mem' := }
Instances For
@[simp]
theorem NonUnitalSubring.coe_mk' {R : Type u} {s : Set R} {sm : } (hm : sm = s) {sa : } (ha : sa = s) :
(NonUnitalSubring.mk' s sm sa hm ha) = s
@[simp]
theorem NonUnitalSubring.mem_mk' {R : Type u} {s : Set R} {sm : } (hm : sm = s) {sa : } (ha : sa = s) {x : R} :
x NonUnitalSubring.mk' s sm sa hm ha x s
@[simp]
theorem NonUnitalSubring.mk'_toSubsemigroup {R : Type u} {s : Set R} {sm : } (hm : sm = s) {sa : } (ha : sa = s) :
(NonUnitalSubring.mk' s sm sa hm ha).toSubsemigroup = sm
@[simp]
theorem NonUnitalSubring.mk'_toAddSubgroup {R : Type u} {s : Set R} {sm : } (hm : sm = s) {sa : } (ha : sa = s) :
(NonUnitalSubring.mk' s sm sa hm ha).toAddSubgroup = sa
theorem NonUnitalSubring.zero_mem {R : Type u} (s : ) :
0 s

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

theorem NonUnitalSubring.mul_mem {R : Type u} (s : ) {x : R} {y : R} :
x sy sx * y s

A non-unital subring is closed under multiplication.

theorem NonUnitalSubring.add_mem {R : Type u} (s : ) {x : R} {y : R} :
x sy sx + y s

A non-unital subring is closed under addition.

theorem NonUnitalSubring.neg_mem {R : Type u} (s : ) {x : R} :
x s-x s

A non-unital subring is closed under negation.

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

A non-unital subring is closed under subtraction

theorem NonUnitalSubring.list_sum_mem {R : Type u} (s : ) {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} (s : ) (m : ) :
(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} (s : ) {ι : Type u_2} {t : } {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.

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

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

Equations
theorem NonUnitalSubring.zsmul_mem {R : Type u} (s : ) {x : R} (hx : x s) (n : ) :
n x s
@[simp]
theorem NonUnitalSubring.val_add {R : Type u} (s : ) (x : s) (y : s) :
(x + y) = x + y
@[simp]
theorem NonUnitalSubring.val_neg {R : Type u} (s : ) (x : s) :
(-x) = -x
@[simp]
theorem NonUnitalSubring.val_mul {R : Type u} (s : ) (x : s) (y : s) :
(x * y) = x * y
@[simp]
theorem NonUnitalSubring.val_zero {R : Type u} (s : ) :
0 = 0
theorem NonUnitalSubring.coe_eq_zero_iff {R : Type u} (s : ) {x : s} :
x = 0 x = 0
instance NonUnitalSubring.toNonUnitalCommRing {R : Type u_1} (s : ) :

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

Equations

## Partial order #

@[simp]
theorem NonUnitalSubring.mem_toSubsemigroup {R : Type u} {s : } {x : R} :
x s.toSubsemigroup x s
@[simp]
theorem NonUnitalSubring.coe_toSubsemigroup {R : Type u} (s : ) :
s.toSubsemigroup = s
@[simp]
theorem NonUnitalSubring.mem_toAddSubgroup {R : Type u} {s : } {x : R} :
@[simp]
theorem NonUnitalSubring.coe_toAddSubgroup {R : Type u} (s : ) :
@[simp]
theorem NonUnitalSubring.mem_toNonUnitalSubsemiring {R : Type u} {s : } {x : R} :
x s.toNonUnitalSubsemiring x s
@[simp]
theorem NonUnitalSubring.coe_toNonUnitalSubsemiring {R : Type u} (s : ) :
s.toNonUnitalSubsemiring = s

## top #

instance NonUnitalSubring.instTop {R : Type u} :

The non-unital subring R of the ring R.

Equations
• NonUnitalSubring.instTop = { top := let __src := ; let __src_1 := ; { carrier := __src.carrier, add_mem' := , zero_mem' := , mul_mem' := , neg_mem' := } }
@[simp]
theorem NonUnitalSubring.mem_top {R : Type u} (x : R) :
@[simp]
theorem NonUnitalSubring.coe_top {R : Type u} :
= Set.univ
@[simp]
theorem NonUnitalSubring.topEquiv_symm_apply_coe {R : Type u} (x : R) :
(NonUnitalSubring.topEquiv.symm x) = x
@[simp]
theorem NonUnitalSubring.topEquiv_apply {R : Type u} (x : ) :
NonUnitalSubring.topEquiv x = x

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

Equations
• NonUnitalSubring.topEquiv = NonUnitalSubsemiring.topEquiv
Instances For

## comap #

def NonUnitalSubring.comap {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (f : F) (s : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem NonUnitalSubring.coe_comap {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (s : ) (f : F) :
() = f ⁻¹' s
@[simp]
theorem NonUnitalSubring.mem_comap {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] {s : } {f : F} {x : R} :
f x s
theorem NonUnitalSubring.comap_comap {R : Type u} {S : Type v} {T : Type u_1} (s : ) (g : S →ₙ+* T) (f : R →ₙ+* S) :

## map #

def NonUnitalSubring.map {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (f : F) (s : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem NonUnitalSubring.coe_map {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (f : F) (s : ) :
() = f '' s
@[simp]
theorem NonUnitalSubring.mem_map {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] {f : F} {s : } {y : S} :
xs, f x = y
@[simp]
theorem NonUnitalSubring.map_id {R : Type u} (s : ) :
theorem NonUnitalSubring.map_map {R : Type u} {S : Type v} {T : Type u_1} (s : ) (g : S →ₙ+* T) (f : R →ₙ+* S) :
= NonUnitalSubring.map (g.comp f) s
theorem NonUnitalSubring.map_le_iff_le_comap {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] {f : F} {s : } {t : } :
theorem NonUnitalSubring.gc_map_comap {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (f : F) :
noncomputable def NonUnitalSubring.equivMapOfInjective {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (s : ) (f : F) (hf : ) :
s ≃+* ()

A NonUnitalSubring is isomorphic to its image under an injective function

Equations
• s.equivMapOfInjective f hf = let __src := Equiv.Set.image (f) (s) hf; { toEquiv := __src, map_mul' := , map_add' := }
Instances For
@[simp]
theorem NonUnitalSubring.coe_equivMapOfInjective_apply {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (s : ) (f : F) (hf : ) (x : s) :
((s.equivMapOfInjective f hf) x) = f x

## range #

def NonUnitalRingHom.range {R : Type u} {S : Type v} (f : R →ₙ+* S) :

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

Equations
• f.range = .copy ()
Instances For
@[simp]
theorem NonUnitalRingHom.coe_range {R : Type u} {S : Type v} (f : R →ₙ+* S) :
f.range =
@[simp]
theorem NonUnitalRingHom.mem_range {R : Type u} {S : Type v} {f : R →ₙ+* S} {y : S} :
y f.range ∃ (x : R), f x = y
theorem NonUnitalRingHom.range_eq_map {R : Type u} {S : Type v} (f : R →ₙ+* S) :
f.range =
theorem NonUnitalRingHom.mem_range_self {R : Type u} {S : Type v} (f : R →ₙ+* S) (x : R) :
f x f.range
theorem NonUnitalRingHom.map_range {R : Type u} {S : Type v} {T : Type u_1} (g : S →ₙ+* T) (f : R →ₙ+* S) :
NonUnitalSubring.map g f.range = (g.comp f).range
instance NonUnitalRingHom.fintypeRange {R : Type u} {S : Type v} [] [] (f : R →ₙ+* S) :
Fintype f.range

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
• f.fintypeRange =

## bot #

instance NonUnitalSubring.instBot {R : Type u} :
Equations
• NonUnitalSubring.instBot = { bot := }
Equations
• NonUnitalSubring.instInhabited = { default := }
theorem NonUnitalSubring.coe_bot {R : Type u} :
= {0}
theorem NonUnitalSubring.mem_bot {R : Type u} {x : R} :
x x = 0

## inf #

instance NonUnitalSubring.instInf {R : Type u} :

The inf of two NonUnitalSubrings is their intersection.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalSubring.coe_inf {R : Type u} (p : ) (p' : ) :
(p p') = p p'
@[simp]
theorem NonUnitalSubring.mem_inf {R : Type u} {p : } {p' : } {x : R} :
x p p' x p x p'
Equations
• NonUnitalSubring.instInfSet = { sInf := fun (s : ) => NonUnitalSubring.mk' (ts, t) (ts, t.toSubsemigroup) (ts, t.toAddSubgroup) }
@[simp]
theorem NonUnitalSubring.coe_sInf {R : Type u} (S : ) :
(sInf S) = sS, s
theorem NonUnitalSubring.mem_sInf {R : Type u} {S : } {x : R} :
x sInf S pS, x p
@[simp]
theorem NonUnitalSubring.coe_iInf {R : Type u} {ι : Sort u_2} {S : ι} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
theorem NonUnitalSubring.mem_iInf {R : Type u} {ι : Sort u_2} {S : ι} {x : R} :
x ⨅ (i : ι), S i ∀ (i : ι), x S i
@[simp]
theorem NonUnitalSubring.sInf_toSubsemigroup {R : Type u} (s : ) :
(sInf s).toSubsemigroup = ts, t.toSubsemigroup
@[simp]
theorem NonUnitalSubring.sInf_toAddSubgroup {R : Type u} (s : ) :

NonUnitalSubrings of a ring form a complete lattice.

Equations
• NonUnitalSubring.instCompleteLattice = let __src := ; CompleteLattice.mk
theorem NonUnitalSubring.eq_top_iff' {R : Type u} (A : ) :
A = ∀ (x : R), x A

## Center of a ring #

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

Equations
• = let __src := ; { toNonUnitalSubsemiring := __src, neg_mem' := }
Instances For
@[simp]
theorem NonUnitalSubring.center_toNonUnitalSubsemiring (R : Type u) :
.toNonUnitalSubsemiring =

The center is commutative and associative.

Equations
• One or more equations did not get rendered due to their size.
theorem NonUnitalSubring.mem_center_iff {R : Type u} [] {z : R} :
∀ (g : R), g * z = z * g
instance NonUnitalSubring.decidableMemCenter {R : Type u} [] [] [] :
DecidablePred fun (x : R) =>
Equations
@[simp]

## NonUnitalSubring closure of a subset #

def NonUnitalSubring.closure {R : Type u} (s : Set R) :

The NonUnitalSubring generated by a set.

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

The NonUnitalSubring generated by a set includes the set.

theorem NonUnitalSubring.not_mem_of_not_mem_closure {R : Type u} {s : Set R} {P : R} (hP : ) :
Ps
@[simp]
theorem NonUnitalSubring.closure_le {R : Type u} {s : Set R} {t : } :
s t

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

theorem NonUnitalSubring.closure_mono {R : Type u} ⦃s : Set R ⦃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} {s : Set R} {t : } (h₁ : s t) (h₂ : ) :
theorem NonUnitalSubring.closure_induction {R : Type u} {s : Set R} {p : RProp} {x : R} (h : ) (mem : xs, p x) (zero : p 0) (add : ∀ (x y : R), p xp yp (x + y)) (neg : ∀ (x : R), p xp (-x)) (mul : ∀ (x y : R), p xp yp (x * y)) :
p x

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} {s : Set R} {p : } (a : ) (mem : ∀ (x : R) (hx : x s), p x, ) (zero : p 0) (add : ∀ (x y : ), p xp yp (x + y)) (neg : ∀ (x : ), p xp (-x)) (mul : ∀ (x y : ), p xp yp (x * y)) :
p a

The difference with NonUnitalSubring.closure_induction is that this acts on the subtype.

theorem NonUnitalSubring.closure_induction₂ {R : Type u} {s : Set R} {p : RRProp} {a : R} {b : R} (ha : ) (hb : ) (Hs : xs, ys, p x y) (H0_left : ∀ (x : R), p 0 x) (H0_right : ∀ (x : R), p x 0) (Hneg_left : ∀ (x y : R), p x yp (-x) y) (Hneg_right : ∀ (x y : R), p x yp x (-y)) (Hadd_left : ∀ (x₁ x₂ y : R), p x₁ yp x₂ yp (x₁ + x₂) y) (Hadd_right : ∀ (x y₁ y₂ : R), p x y₁p x y₂p x (y₁ + y₂)) (Hmul_left : ∀ (x₁ x₂ y : R), p x₁ yp x₂ yp (x₁ * x₂) y) (Hmul_right : ∀ (x y₁ y₂ : R), p x y₁p x y₂p x (y₁ * y₂)) :
p a b

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

theorem NonUnitalSubring.mem_closure_iff {R : Type u} {s : Set R} {x : R} :
def NonUnitalSubring.closureNonUnitalCommRingOfComm {R : Type u} [] {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
• = let __src := .toNonUnitalRing;
Instances For
def NonUnitalSubring.gi (R : Type u) :
GaloisInsertion NonUnitalSubring.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations
• = { choice := fun (s : Set R) (x : ) => , gc := , le_l_u := , choice_eq := }
Instances For
theorem NonUnitalSubring.closure_eq {R : Type u} (s : ) :

Closure of a NonUnitalSubring S equals S.

@[simp]
theorem NonUnitalSubring.closure_union {R : Type u} (s : Set R) (t : Set R) :
theorem NonUnitalSubring.closure_iUnion {R : Type u} {ι : Sort u_2} (s : ιSet R) :
NonUnitalSubring.closure (⋃ (i : ι), s i) = ⨆ (i : ι),
theorem NonUnitalSubring.closure_sUnion {R : Type u} (s : Set (Set R)) :
= ts,
theorem NonUnitalSubring.map_sup {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (s : ) (t : ) (f : F) :
theorem NonUnitalSubring.map_iSup {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] {ι : Sort u_2} (f : F) (s : ι) :
= ⨆ (i : ι), NonUnitalSubring.map f (s i)
theorem NonUnitalSubring.comap_inf {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (s : ) (t : ) (f : F) :
theorem NonUnitalSubring.comap_iInf {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] {ι : Sort u_2} (f : F) (s : ι) :
= ⨅ (i : ι), NonUnitalSubring.comap f (s i)
@[simp]
theorem NonUnitalSubring.map_bot {R : Type u} {S : Type v} (f : R →ₙ+* S) :
@[simp]
theorem NonUnitalSubring.comap_top {R : Type u} {S : Type v} (f : R →ₙ+* S) :
def NonUnitalSubring.prod {R : Type u} {S : Type v} (s : ) (t : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem NonUnitalSubring.coe_prod {R : Type u} {S : Type v} (s : ) (t : ) :
(s.prod t) = s ×ˢ t
theorem NonUnitalSubring.mem_prod {R : Type u} {S : Type v} {s : } {t : } {p : R × S} :
p s.prod t p.1 s p.2 t
theorem NonUnitalSubring.prod_mono {R : Type u} {S : Type v} ⦃s₁ : ⦃s₂ : (hs : s₁ s₂) ⦃t₁ : ⦃t₂ : (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂
theorem NonUnitalSubring.prod_mono_right {R : Type u} {S : Type v} (s : ) :
Monotone fun (t : ) => s.prod t
theorem NonUnitalSubring.prod_mono_left {R : Type u} {S : Type v} (t : ) :
Monotone fun (s : ) => s.prod t
theorem NonUnitalSubring.prod_top {R : Type u} {S : Type v} (s : ) :
s.prod =
theorem NonUnitalSubring.top_prod {R : Type u} {S : Type v} (s : ) :
.prod s =
@[simp]
theorem NonUnitalSubring.top_prod_top {R : Type u} {S : Type v} :
.prod =
def NonUnitalSubring.prodEquiv {R : Type u} {S : Type v} (s : ) (t : ) :
(s.prod t) ≃+* s × t

Product of NonUnitalSubrings is isomorphic to their product as rings.

Equations
• s.prodEquiv t = let __src := Equiv.Set.prod s t; { toEquiv := __src, map_mul' := , map_add' := }
Instances For
theorem NonUnitalSubring.mem_iSup_of_directed {R : Type u} {ι : Sort u_2} [hι : ] {S : ι} (hS : Directed (fun (x x_1 : ) => x x_1) 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} {ι : Sort u_2} [] {S : ι} (hS : Directed (fun (x x_1 : ) => x x_1) S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem NonUnitalSubring.mem_sSup_of_directedOn {R : Type u} {S : } (Sne : S.Nonempty) (hS : DirectedOn (fun (x x_1 : ) => x x_1) S) {x : R} :
x sSup S sS, x s
theorem NonUnitalSubring.coe_sSup_of_directedOn {R : Type u} {S : } (Sne : S.Nonempty) (hS : DirectedOn (fun (x x_1 : ) => x x_1) S) :
(sSup S) = sS, s
theorem NonUnitalSubring.mem_map_equiv {R : Type u} {S : Type v} {f : R ≃+* S} {K : } {x : S} :
x NonUnitalSubring.map (f) K f.symm x K
theorem NonUnitalSubring.comap_equiv_eq_map_symm {R : Type u} {S : Type v} (f : R ≃+* S) (K : ) :
def NonUnitalRingHom.rangeRestrict {R : Type u} {S : Type v} (f : R →ₙ+* S) :
R →ₙ+* f.range

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} (f : R →ₙ+* S) (x : R) :
(f.rangeRestrict x) = f x
theorem NonUnitalRingHom.rangeRestrict_surjective {R : Type u} {S : Type v} (f : R →ₙ+* S) :
Function.Surjective f.rangeRestrict
theorem NonUnitalRingHom.range_top_iff_surjective {R : Type u} {S : Type v} {f : R →ₙ+* S} :
f.range =
@[simp]
theorem NonUnitalRingHom.range_top_of_surjective {R : Type u} {S : Type v} (f : R →ₙ+* S) (hf : ) :
f.range =

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

def NonUnitalRingHom.eqLocus {R : Type u} {S : Type v} (f : R →ₙ+* S) (g : R →ₙ+* S) :

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
• f.eqLocus g = let __src := (f).eqLocus g; let __src := (f).eqLocus g; { carrier := {x : R | f x = g x}, add_mem' := , zero_mem' := , mul_mem' := , neg_mem' := }
Instances For
@[simp]
theorem NonUnitalRingHom.eqLocus_same {R : Type u} {S : Type v} (f : R →ₙ+* S) :
f.eqLocus f =
theorem NonUnitalRingHom.eqOn_set_closure {R : Type u} {S : Type v} {f : R →ₙ+* S} {g : R →ₙ+* S} {s : Set R} (h : Set.EqOn (f) (g) s) :
Set.EqOn f g

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} {f : R →ₙ+* S} {g : R →ₙ+* S} (h : Set.EqOn f g ) :
f = g
theorem NonUnitalRingHom.eq_of_eqOn_set_dense {R : Type u} {S : Type v} {s : Set R} (hs : ) {f : R →ₙ+* S} {g : R →ₙ+* S} (h : Set.EqOn (f) (g) s) :
f = g
theorem NonUnitalRingHom.closure_preimage_le {R : Type u} {S : Type v} (f : R →ₙ+* S) (s : Set S) :
theorem NonUnitalRingHom.map_closure {R : Type u} {S : Type v} (f : R →ₙ+* S) (s : Set R) :

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

def NonUnitalSubring.inclusion {R : Type u} {S : } {T : } (h : S T) :
S →ₙ+* T

The ring homomorphism associated to an inclusion of NonUnitalSubrings.

Equations
Instances For
@[simp]
theorem NonUnitalSubring.range_subtype {R : Type u} (s : ) :
.range = s
theorem NonUnitalSubring.range_fst {R : Type u} {S : Type v} :
theorem NonUnitalSubring.range_snd {R : Type u} {S : Type v} :
def RingEquiv.nonUnitalSubringCongr {R : Type u} [] {s : } {t : } (h : s = t) :
s ≃+* t

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

Equations
• = let __src := ; { toEquiv := __src, map_mul' := , map_add' := }
Instances For
def RingEquiv.ofLeftInverse' {R : Type u} {S : Type v} [] [] {g : SR} {f : R →ₙ+* S} (h : ) :
R ≃+* f.range

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem RingEquiv.ofLeftInverse'_apply {R : Type u} {S : Type v} [] [] {g : SR} {f : R →ₙ+* S} (h : ) (x : R) :
() = f x
@[simp]
theorem RingEquiv.ofLeftInverse'_symm_apply {R : Type u} {S : Type v} [] [] {g : SR} {f : R →ₙ+* S} (h : ) (x : f.range) :
.symm x = g x
theorem NonUnitalSubring.closure_preimage_le {F : Type w} {R : Type u} {S : Type v} [FunLike F R S] [] (f : F) (s : Set S) :