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)

• 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

theorem NonUnitalSubring.list_sum_mem {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {l : List R} : (∀ x ∈ l, 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) : (∀ a ∈ m, 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 : ∀ c ∈ t, f c ∈ s) : ∑ i ∈ t, f i ∈ s

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

top

@[instance_reducible]

instance NonUnitalSubring.instTop {R : Type u} [NonUnitalNonAssocRing R] : Top (NonUnitalSubring R)

The non-unital subring R of the ring R.

Equations

• NonUnitalSubring.instTop = { top := let __src := ⊤; have __src_1 := ⊤; { carrier := __src.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ } }

@[simp]

theorem NonUnitalSubring.mem_top {R : Type u} [NonUnitalNonAssocRing R] (x : R) : x ∈ ⊤

@[simp]

theorem NonUnitalSubring.coe_top {R : Type u} [NonUnitalNonAssocRing R] : ↑⊤ = Set.univ

@[simp]

theorem NonUnitalSubring.toNonUnitalSubsemiring_top {R : Type u} [NonUnitalNonAssocRing R] : ⊤.toNonUnitalSubsemiring = ⊤

@[simp]

theorem NonUnitalSubring.toAddSubgroup_top {R : Type u} [NonUnitalNonAssocRing R] : ⊤.toAddSubgroup = ⊤

@[simp]

theorem NonUnitalSubring.toNonUnitalSubsemiring_eq_top {R : Type u} [NonUnitalNonAssocRing R] {S : NonUnitalSubring R} : S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

@[simp]

theorem NonUnitalSubring.toAddSubgroup_eq_top {R : Type u} [NonUnitalNonAssocRing R] {S : NonUnitalSubring R} : S.toAddSubgroup = ⊤ ↔ S = ⊤

def NonUnitalSubring.topEquiv {R : Type u} [NonUnitalNonAssocRing R] : ↥⊤ ≃+* R

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

Equations

• NonUnitalSubring.topEquiv = NonUnitalSubsemiring.topEquiv

@[simp]

theorem NonUnitalSubring.topEquiv_apply {R : Type u} [NonUnitalNonAssocRing R] (x : ↥⊤) : topEquiv x = ↑x

@[simp]

theorem NonUnitalSubring.topEquiv_symm_apply_coe {R : Type u} [NonUnitalNonAssocRing R] (x : R) : ↑(topEquiv.symm x) = x

comap

def NonUnitalSubring.comap {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 S) : NonUnitalSubring R

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

Equations

• NonUnitalSubring.comap f s = { carrier := ⇑f ⁻¹' s.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

@[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

theorem NonUnitalSubring.comap_comap {R : Type u} {S : Type v} {T : Type u_1} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [NonUnitalNonAssocRing T] (s : NonUnitalSubring T) (g : S →ₙ+* T) (f : R →ₙ+* S) : comap f (comap g s) = comap (g.comp f) s

map

def NonUnitalSubring.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) : NonUnitalSubring S

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

Equations

• NonUnitalSubring.map f s = { carrier := ⇑f '' s.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

@[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 ↔ ∃ x ∈ s, f x = y

@[simp]

theorem NonUnitalSubring.map_id {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : map (NonUnitalRingHom.id R) s = s

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

theorem NonUnitalSubring.map_le_iff_le_comap {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} {t : NonUnitalSubring S} : map f s ≤ t ↔ s ≤ comap f t

theorem NonUnitalSubring.gc_map_comap {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) : GaloisConnection (map f) (comap f)

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

• s.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑s) hf, map_mul' := ⋯, map_add' := ⋯ }

@[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

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

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

Equations

• f.range = (NonUnitalSubring.map f ⊤).copy (Set.range ⇑f) ⋯

@[simp]

theorem NonUnitalRingHom.coe_range {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : ↑f.range = Set.range ⇑f

@[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

theorem NonUnitalRingHom.range_eq_map {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : f.range = NonUnitalSubring.map f ⊤

theorem NonUnitalRingHom.mem_range_self {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (x : R) : f x ∈ f.range

theorem NonUnitalRingHom.map_range {R : Type u} {S : Type v} {T : Type u_1} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [NonUnitalNonAssocRing T] (g : S →ₙ+* T) (f : R →ₙ+* S) : NonUnitalSubring.map g f.range = (g.comp f).range

@[instance_reducible]

instance NonUnitalRingHom.fintypeRange {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [Fintype R] [DecidableEq S] (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 = Set.fintypeRange ⇑f

bot

@[instance_reducible]

instance NonUnitalSubring.instBot {R : Type u} [NonUnitalNonAssocRing R] : Bot (NonUnitalSubring R)

Equations

• NonUnitalSubring.instBot = { bot := NonUnitalRingHom.range 0 }

@[instance_reducible]

instance NonUnitalSubring.instInhabited {R : Type u} [NonUnitalNonAssocRing R] : Inhabited (NonUnitalSubring R)

Equations

• NonUnitalSubring.instInhabited = { default := ⊥ }

theorem NonUnitalSubring.coe_bot {R : Type u} [NonUnitalNonAssocRing R] : ↑⊥ = {0}

theorem NonUnitalSubring.mem_bot {R : Type u} [NonUnitalNonAssocRing R] {x : R} : x ∈ ⊥ ↔ x = 0

inf

@[instance_reducible]

instance NonUnitalSubring.instMin {R : Type u} [NonUnitalNonAssocRing R] : Min (NonUnitalSubring R)

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} [NonUnitalNonAssocRing R] (p p' : NonUnitalSubring R) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem NonUnitalSubring.mem_inf {R : Type u} [NonUnitalNonAssocRing R] {p p' : NonUnitalSubring R} {x : R} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[instance_reducible]

instance NonUnitalSubring.instInfSet {R : Type u} [NonUnitalNonAssocRing R] : InfSet (NonUnitalSubring R)

Equations

• NonUnitalSubring.instInfSet = { sInf := fun (s : Set (NonUnitalSubring R)) => NonUnitalSubring.mk' (⋂ t ∈ s, ↑t) (⨅ t ∈ s, t.toSubsemigroup) (⨅ t ∈ s, t.toAddSubgroup) ⋯ ⋯ }

@[simp]

theorem NonUnitalSubring.coe_sInf {R : Type u} [NonUnitalNonAssocRing R] (S : Set (NonUnitalSubring R)) : ↑(sInf S) = ⋂ s ∈ S, ↑s

@[simp]

theorem NonUnitalSubring.mem_sInf {R : Type u} [NonUnitalNonAssocRing R] {S : Set (NonUnitalSubring R)} {x : R} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

@[simp]

theorem NonUnitalSubring.coe_iInf {R : Type u} [NonUnitalNonAssocRing R] {ι : Sort u_1} {S : ι → NonUnitalSubring R} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

@[simp]

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

@[simp]

theorem NonUnitalSubring.sInf_toSubsemigroup {R : Type u} [NonUnitalNonAssocRing R] (s : Set (NonUnitalSubring R)) : (sInf s).toSubsemigroup = ⨅ t ∈ s, t.toSubsemigroup

@[simp]

theorem NonUnitalSubring.sInf_toAddSubgroup {R : Type u} [NonUnitalNonAssocRing R] (s : Set (NonUnitalSubring R)) : (sInf s).toAddSubgroup = ⨅ t ∈ s, t.toAddSubgroup

@[instance_reducible]

instance NonUnitalSubring.instCompleteLattice {R : Type u} [NonUnitalNonAssocRing R] : CompleteLattice (NonUnitalSubring R)

NonUnitalSubrings of a ring form a complete lattice.

Equations

• One or more equations did not get rendered due to their size.

theorem NonUnitalSubring.eq_top_iff' {R : Type u} [NonUnitalNonAssocRing R] (A : NonUnitalSubring R) : A = ⊤ ↔ ∀ (x : R), x ∈ A

Center of a ring

def NonUnitalSubring.center (R : Type u) [NonUnitalNonAssocRing R] : NonUnitalSubring R

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

Equations

• NonUnitalSubring.center R = { toNonUnitalSubsemiring := NonUnitalSubsemiring.center R, neg_mem' := ⋯ }

theorem NonUnitalSubring.coe_center (R : Type u) [NonUnitalNonAssocRing R] : ↑(center R) = Set.center R

@[simp]

theorem NonUnitalSubring.center_toNonUnitalSubsemiring (R : Type u) [NonUnitalNonAssocRing R] : (center R).toNonUnitalSubsemiring = NonUnitalSubsemiring.center R

@[instance_reducible]

instance NonUnitalSubring.center.instNonUnitalCommRing (R : Type u) [NonUnitalNonAssocRing R] : NonUnitalCommRing ↥(center R)

The center is commutative and associative.

Equations

• One or more equations did not get rendered due to their size.

def NonUnitalSubring.centerCongr {R : Type u} [NonUnitalNonAssocRing R] {S : Type u_1} [NonUnitalNonAssocRing S] (e : R ≃+* S) : ↥(center R) ≃+* ↥(center S)

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

Equations

• NonUnitalSubring.centerCongr e = NonUnitalSubsemiring.centerCongr e

@[simp]

theorem NonUnitalSubring.centerCongr_symm_apply_coe {R : Type u} [NonUnitalNonAssocRing R] {S : Type u_1} [NonUnitalNonAssocRing S] (e : R ≃+* S) (s : ↥(Subsemigroup.center S)) : ↑((centerCongr e).symm s) = e.symm ↑s

@[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

def NonUnitalSubring.centerToMulOpposite {R : Type u} [NonUnitalNonAssocRing R] : ↥(center R) ≃+* ↥(center Rᵐᵒᵖ)

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

Equations

• NonUnitalSubring.centerToMulOpposite = NonUnitalSubsemiring.centerToMulOpposite

@[simp]

theorem NonUnitalSubring.centerToMulOpposite_symm_apply_coe {R : Type u} [NonUnitalNonAssocRing R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)) : ↑(centerToMulOpposite.symm r) = MulOpposite.unop ↑r

@[simp]

theorem NonUnitalSubring.centerToMulOpposite_apply_coe {R : Type u} [NonUnitalNonAssocRing R] (r : ↥(Subsemigroup.center R)) : ↑(centerToMulOpposite r) = MulOpposite.op ↑r

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

@[instance_reducible]

instance NonUnitalSubring.decidableMemCenter {R : Type u} [NonUnitalRing R] [DecidableEq R] [Fintype R] : DecidablePred fun (x : R) => x ∈ center R

Equations

• NonUnitalSubring.decidableMemCenter x✝ = decidable_of_iff' (∀ (g : R), g * x✝ = x✝ * g) ⋯

@[simp]

theorem NonUnitalSubring.center_eq_top (R : Type u_1) [NonUnitalCommRing R] : center R = ⊤

def NonUnitalSubring.centralizer {R : Type u_1} [NonUnitalRing R] (s : Set R) : NonUnitalSubring R

The centralizer of a set as non-unital subring.

Equations

• NonUnitalSubring.centralizer s = { carrier := s.centralizer, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem NonUnitalSubring.coe_centralizer {R : Type u_1} [NonUnitalRing R] (s : Set R) : ↑(centralizer s) = s.centralizer

theorem NonUnitalSubring.centralizer_toNonUnitalSubsemiring {R : Type u_1} [NonUnitalRing R] (s : Set R) : (centralizer s).toNonUnitalSubsemiring = NonUnitalSubsemiring.centralizer s

theorem NonUnitalSubring.mem_centralizer_iff {R : Type u_1} [NonUnitalRing R] {s : Set R} {z : R} : z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g

theorem NonUnitalSubring.center_le_centralizer {R : Type u_1} [NonUnitalRing R] (s : Set R) : center R ≤ centralizer s

theorem NonUnitalSubring.centralizer_le {R : Type u_1} [NonUnitalRing R] (s t : Set R) (h : s ⊆ t) : centralizer t ≤ centralizer s

@[simp]

theorem NonUnitalSubring.centralizer_eq_top_iff_subset {R : Type u_1} [NonUnitalRing R] {s : Set R} : centralizer s = ⊤ ↔ s ⊆ ↑(center R)

@[simp]

theorem NonUnitalSubring.centralizer_univ {R : Type u_1} [NonUnitalRing R] : centralizer Set.univ = center R

NonUnitalSubring closure of a subset

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

The NonUnitalSubring generated by a set.

Equations

• NonUnitalSubring.closure s = sInf {S : NonUnitalSubring R | s ⊆ ↑S}

theorem NonUnitalSubring.mem_closure {R : Type u} [NonUnitalNonAssocRing R] {x : R} {s : Set R} : x ∈ closure s ↔ ∀ (S : NonUnitalSubring R), s ⊆ ↑S → x ∈ S

@[simp]

theorem NonUnitalSubring.subset_closure {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} : s ⊆ ↑(closure s)

The NonUnitalSubring generated by a set includes the set.

theorem NonUnitalSubring.mem_closure_of_mem {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {x : R} (hx : x ∈ s) : x ∈ closure s

theorem NonUnitalSubring.notMem_of_notMem_closure {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {P : R} (hP : P ∉ closure s) : P ∉ s

@[simp]

theorem NonUnitalSubring.closure_le {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {t : NonUnitalSubring R} : closure s ≤ t ↔ s ⊆ ↑t

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) : closure s ≤ closure 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) : closure s = t

theorem NonUnitalSubring.closure_induction {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {p : (x : R) → x ∈ closure s → Prop} (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 hx → p y hy → p (x + y) ⋯) (neg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) ⋯) (mul : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (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 s → y ∈ closure s → Prop} (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 hy → p (-x) y ⋯ hy) (neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p 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 hz → p y z hy hz → p (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 hy → p x z hx hz → p 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 hz → p y z hy hz → p (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 hy → p x z hx hz → p 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.

theorem NonUnitalSubring.mem_closure_iff {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {x : R} : x ∈ closure s ↔ x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

theorem NonUnitalSubring.closure_le_centralizer_centralizer {R : Type u_1} [NonUnitalRing R] (s : Set R) : closure s ≤ centralizer ↑(centralizer s)

theorem NonUnitalSubring.isMulCommutative_closure {R : Type u_1} [NonUnitalRing R] {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : IsMulCommutative ↥(closure s)

If all the elements of a set s commute, then closure s is a non-unital commutative semiring.

@[reducible, inline, deprecated NonUnitalSubring.isMulCommutative_closure (since := "2026-03-11")]

abbrev NonUnitalSubring.closureNonUnitalCommRingOfComm {R : Type u_1} [NonUnitalRing R] {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : NonUnitalCommRing ↥(closure s)

If all the elements of a set s commute, then closure s is a non-unital commutative ring.

Equations

• NonUnitalSubring.closureNonUnitalCommRingOfComm hcomm = inferInstance

instance NonUnitalSubring.instIsMulCommutative_closure {S : Type u_1} {R : Type u_2} [NonUnitalRing R] [SetLike S R] [MulMemClass S R] (s : S) [IsMulCommutative ↥s] : IsMulCommutative ↥(closure ↑s)

def NonUnitalSubring.gi (R : Type u) [NonUnitalNonAssocRing R] : GaloisInsertion closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• NonUnitalSubring.gi R = { choice := fun (s : Set R) (x : ↑(NonUnitalSubring.closure s) ⊆ s) => NonUnitalSubring.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

@[simp]

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

Closure of a NonUnitalSubring S equals S.

@[simp]

theorem NonUnitalSubring.closure_empty {R : Type u} [NonUnitalNonAssocRing R] : closure ∅ = ⊥

@[simp]

theorem NonUnitalSubring.closure_univ {R : Type u} [NonUnitalNonAssocRing R] : closure Set.univ = ⊤

theorem NonUnitalSubring.closure_union {R : Type u} [NonUnitalNonAssocRing R] (s t : Set R) : closure (s ∪ t) = closure s ⊔ closure t

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.closure_sUnion {R : Type u} [NonUnitalNonAssocRing R] (s : Set (Set R)) : closure (⋃₀ s) = ⨆ t ∈ s, closure t

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 (s ⊔ t) = map f s ⊔ map 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 (s ⊓ t) = map f s ⊓ map 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 (s ⊓ t) = comap f s ⊓ comap 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)

@[simp]

theorem NonUnitalSubring.map_bot {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : map f ⊥ = ⊥

@[simp]

theorem NonUnitalSubring.comap_top {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : comap f ⊤ = ⊤

def NonUnitalSubring.prod {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (s : NonUnitalSubring R) (t : NonUnitalSubring S) : NonUnitalSubring (R × S)

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

Equations

• s.prod t = { carrier := ↑s ×ˢ ↑t, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

theorem NonUnitalSubring.coe_prod {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (s : NonUnitalSubring R) (t : NonUnitalSubring S) : ↑(s.prod t) = ↑s ×ˢ ↑t

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₂

theorem NonUnitalSubring.prod_mono_right {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (s : NonUnitalSubring R) : Monotone fun (t : NonUnitalSubring S) => s.prod t

theorem NonUnitalSubring.prod_mono_left {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (t : NonUnitalSubring S) : Monotone fun (s : NonUnitalSubring R) => s.prod t

theorem NonUnitalSubring.prod_top {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (s : NonUnitalSubring R) : s.prod ⊤ = comap (NonUnitalRingHom.fst R S) s

theorem NonUnitalSubring.top_prod {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (s : NonUnitalSubring S) : ⊤.prod s = comap (NonUnitalRingHom.snd R S) s

@[simp]

theorem NonUnitalSubring.top_prod_top {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : ⊤.prod ⊤ = ⊤

theorem NonUnitalSubring.center_prod {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : center (R × S) = (center R).prod (center S)

def NonUnitalSubring.prodEquiv {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (s : NonUnitalSubring R) (t : NonUnitalSubring S) : ↥(s.prod t) ≃+* ↥s × ↥t

Product of NonUnitalSubrings is isomorphic to their product as rings.

Equations

• s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_mul' := ⋯, map_add' := ⋯ }

theorem NonUnitalSubring.mem_iSup_of_directed {R : Type u} [NonUnitalNonAssocRing R] {ι : Sort u_1} [hι : 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 ↔ ∃ s ∈ S, 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) = ⋃ s ∈ S, ↑s

theorem NonUnitalSubring.isMulCommutative_iSup {R : Type u} [NonUnitalNonAssocRing R] {ι : Sort u_1} [Nonempty ι] {S : ι → NonUnitalSubring R} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)] (dir : Directed (fun (x1 x2 : NonUnitalSubring R) => x1 ≤ x2) S) : IsMulCommutative ↥(⨆ (i : ι), S i)

instance NonUnitalSubring.instIsMulCommutative_iSup {R : Type u} [NonUnitalNonAssocRing R] {ι : Type u_1} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι] {S : ι →o NonUnitalSubring R} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)] : IsMulCommutative ↥(⨆ (i : ι), S i)

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

theorem NonUnitalSubring.map_equiv_eq_comap_symm {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R ≃+* S) (K : NonUnitalSubring R) : map (↑f) K = comap f.symm K

theorem NonUnitalSubring.comap_equiv_eq_map_symm {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R ≃+* S) (K : NonUnitalSubring S) : comap (↑f) K = map f.symm K

def NonUnitalRingHom.rangeRestrict {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (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

• f.rangeRestrict = NonUnitalRingHom.codRestrict f f.range ⋯

@[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

theorem NonUnitalRingHom.rangeRestrict_surjective {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : Function.Surjective ⇑f.rangeRestrict

theorem NonUnitalRingHom.range_eq_top {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f : R →ₙ+* S} : f.range = ⊤ ↔ Function.Surjective ⇑f

@[simp]

theorem NonUnitalRingHom.range_eq_top_of_surjective {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (hf : Function.Surjective ⇑f) : f.range = ⊤

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

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

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 = { carrier := {x : R | f x = g x}, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem NonUnitalRingHom.mem_eqLocus {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f g : R →ₙ+* S} {x : R} : x ∈ f.eqLocus g ↔ f x = g x

@[simp]

theorem NonUnitalRingHom.eqLocus_same {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : f.eqLocus f = ⊤

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) : Set.EqOn ⇑f ⇑g ↑(NonUnitalSubring.closure 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

theorem NonUnitalRingHom.closure_preimage_le {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (s : Set S) : NonUnitalSubring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubring.comap f (NonUnitalSubring.closure s)

theorem NonUnitalRingHom.map_closure {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (s : Set R) : NonUnitalSubring.map f (NonUnitalSubring.closure s) = NonUnitalSubring.closure (⇑f '' s)

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

@[simp]

theorem NonUnitalSubring.range_subtype {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : (NonUnitalSubringClass.subtype s).range = s

theorem NonUnitalSubring.range_fst {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : NonUnitalRingHom.srange (NonUnitalRingHom.fst R S) = ⊤

theorem NonUnitalSubring.range_snd {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : NonUnitalRingHom.srange (NonUnitalRingHom.snd R S) = ⊤

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

• RingEquiv.nonUnitalSubringCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯, map_add' := ⋯ }

def RingEquiv.ofLeftInverse' {R : Type u} {S : Type v} [NonUnitalRing R] [NonUnitalRing S] {g : S → R} {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

• One or more equations did not get rendered due to their size.

@[simp]

theorem RingEquiv.ofLeftInverse'_apply {R : Type u} {S : Type v} [NonUnitalRing R] [NonUnitalRing S] {g : S → R} {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 : S → R} {f : R →ₙ+* S} (h : Function.LeftInverse g ⇑f) (x : ↥f.range) : (ofLeftInverse' h).symm x = g ↑x

theorem NonUnitalSubring.closure_preimage_le {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) (s : Set S) : closure (⇑f ⁻¹' s) ≤ comap f (closure s)