Bundled subsemirings #

We define bundled subsemirings and some standard constructions: subtype and inclusion ring homomorphisms.

class AddSubmonoidWithOneClass (S : Type u_1) (R : outParam (Type u_2)) [AddMonoidWithOne R] [SetLike S R] extends AddSubmonoidClass , OneMemClass , AddMemClass , ZeroMemClass :

Prop

AddSubmonoidWithOneClass S R says S is a type of subsets s ≤ R that contain 0, 1, and are closed under (+)

Instances

SubsemiringClass.addSubmonoidWithOneClass

source

theorem natCast_mem {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] (s : S) [AddSubmonoidWithOneClass S R] (n : ℕ) :

↑n ∈ s

source

@[deprecated natCast_mem]

theorem coe_nat_mem {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] (s : S) [AddSubmonoidWithOneClass S R] (n : ℕ) :

↑n ∈ s

Alias of natCast_mem.

source

theorem ofNat_mem {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] [AddSubmonoidWithOneClass S R] (s : S) (n : ℕ) [n.AtLeastTwo] :

OfNat.ofNat n ∈ s

source

@[instance 74]

instance AddSubmonoidWithOneClass.toAddMonoidWithOne {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] (s : S) [AddSubmonoidWithOneClass S R] :

AddMonoidWithOne ↥s

Equations

AddSubmonoidWithOneClass.toAddMonoidWithOne s = AddMonoidWithOne.mk ⋯ ⋯

source

class SubsemiringClass (S : Type u_1) (R : outParam (Type u)) [NonAssocSemiring R] [SetLike S R] extends SubmonoidClass , AddSubmonoidClass , MulMemClass , OneMemClass , AddMemClass , ZeroMemClass :

Prop

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

Instances

source

@[instance 100]

instance SubsemiringClass.addSubmonoidWithOneClass (S : Type u_1) (R : Type u) :

∀ {x : NonAssocSemiring R} [inst : SetLike S R] [h : SubsemiringClass S R], AddSubmonoidWithOneClass S R

Equations

⋯ = ⋯

source

@[instance 100]

instance SubsemiringClass.nonUnitalSubsemiringClass (S : Type u_1) (R : Type u) [NonAssocSemiring R] [SetLike S R] [SubsemiringClass S R] :

NonUnitalSubsemiringClass S R

Equations

⋯ = ⋯

source

@[instance 75]

instance SubsemiringClass.toNonAssocSemiring {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) :

NonAssocSemiring ↥s

A subsemiring of a NonAssocSemiring inherits a NonAssocSemiring structure

Equations

SubsemiringClass.toNonAssocSemiring s = Function.Injective.nonAssocSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

instance SubsemiringClass.nontrivial {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) [Nontrivial R] :

Nontrivial ↥s

Equations

⋯ = ⋯

source

instance SubsemiringClass.noZeroDivisors {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) [NoZeroDivisors R] :

NoZeroDivisors ↥s

Equations

⋯ = ⋯

source

def SubsemiringClass.subtype {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) :

↥s →+* R

The natural ring hom from a subsemiring of semiring R to R.

Equations

SubsemiringClass.subtype s = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

theorem SubsemiringClass.coe_subtype {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) :

⇑(SubsemiringClass.subtype s) = Subtype.val

source

@[instance 75]

instance SubsemiringClass.toSemiring {S : Type v} (s : S) {R : Type u_1} [Semiring R] [SetLike S R] [SubsemiringClass S R] :

Semiring ↥s

A subsemiring of a Semiring is a Semiring.

Equations

SubsemiringClass.toSemiring s = Function.Injective.semiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

@[simp]

theorem SubsemiringClass.coe_pow {S : Type v} (s : S) {R : Type u_1} [Semiring R] [SetLike S R] [SubsemiringClass S R] (x : ↥s) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

instance SubsemiringClass.toCommSemiring {S : Type v} (s : S) {R : Type u_1} [CommSemiring R] [SetLike S R] [SubsemiringClass S R] :

CommSemiring ↥s

A subsemiring of a CommSemiring is a CommSemiring.

Equations

SubsemiringClass.toCommSemiring s = Function.Injective.commSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

structure Subsemiring (R : Type u) [NonAssocSemiring R] extends Submonoid , AddSubmonoid , Subsemigroup , AddSubsemigroup :

Type u

A subsemiring of a semiring R is a subset s that is both a multiplicative and an additive submonoid.

Instances For

source

@[reducible]

abbrev Subsemiring.toAddSubmonoid {R : Type u} [NonAssocSemiring R] (self : Subsemiring R) :

AddSubmonoid R

Reinterpret a Subsemiring as an AddSubmonoid.

Equations

self.toAddSubmonoid = { carrier := self.carrier, add_mem' := ⋯, zero_mem' := ⋯ }

source

instance Subsemiring.instSetLike {R : Type u} [NonAssocSemiring R] :

SetLike (Subsemiring R) R

Equations

Subsemiring.instSetLike = { coe := fun (s : Subsemiring R) => s.carrier, coe_injective' := ⋯ }

source

instance Subsemiring.instSubsemiringClass {R : Type u} [NonAssocSemiring R] :

SubsemiringClass (Subsemiring R) R

Equations

⋯ = ⋯

source

@[simp]

theorem Subsemiring.mem_toSubmonoid {R : Type u} [NonAssocSemiring R] {s : Subsemiring R} {x : R} :

x ∈ s.toSubmonoid ↔ x ∈ s

source

theorem Subsemiring.mem_carrier {R : Type u} [NonAssocSemiring R] {s : Subsemiring R} {x : R} :

x ∈ s.carrier ↔ x ∈ s

source

theorem Subsemiring.ext {R : Type u} [NonAssocSemiring R] {S : Subsemiring R} {T : Subsemiring R} (h : ∀ (x : R), x ∈ S ↔ x ∈ T) :

S = T

Two subsemirings are equal if they have the same elements.

source

def Subsemiring.copy {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = ↑S) :

Subsemiring R

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

Equations

S.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

source

@[simp]

theorem Subsemiring.coe_copy {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = ↑S) :

↑(S.copy s hs) = s

source

theorem Subsemiring.copy_eq {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = ↑S) :

S.copy s hs = S

source

theorem Subsemiring.toSubmonoid_injective {R : Type u} [NonAssocSemiring R] :

Function.Injective Subsemiring.toSubmonoid

source

theorem Subsemiring.toAddSubmonoid_injective {R : Type u} [NonAssocSemiring R] :

Function.Injective Subsemiring.toAddSubmonoid

source

def Subsemiring.mk' {R : Type u} [NonAssocSemiring R] (s : Set R) (sm : Submonoid R) (hm : ↑sm = s) (sa : AddSubmonoid R) (ha : ↑sa = s) :

Subsemiring R

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

Equations

Subsemiring.mk' s sm hm sa ha = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

source

@[simp]

theorem Subsemiring.coe_mk' {R : Type u} [NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R} (ha : ↑sa = s) :

↑(Subsemiring.mk' s sm hm sa ha) = s

source

@[simp]

theorem Subsemiring.mem_mk' {R : Type u} [NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R} (ha : ↑sa = s) {x : R} :

x ∈ Subsemiring.mk' s sm hm sa ha ↔ x ∈ s

source

@[simp]

theorem Subsemiring.mk'_toSubmonoid {R : Type u} [NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R} (ha : ↑sa = s) :

(Subsemiring.mk' s sm hm sa ha).toSubmonoid = sm

source

@[simp]

theorem Subsemiring.mk'_toAddSubmonoid {R : Type u} [NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R} (ha : ↑sa = s) :

(Subsemiring.mk' s sm hm sa ha).toAddSubmonoid = sa

source

theorem Subsemiring.one_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

1 ∈ s

A subsemiring contains the semiring's 1.

source

theorem Subsemiring.zero_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

0 ∈ s

A subsemiring contains the semiring's 0.

source

theorem Subsemiring.mul_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) {x : R} {y : R} :

x ∈ s → y ∈ s → x * y ∈ s

A subsemiring is closed under multiplication.

source

theorem Subsemiring.add_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) {x : R} {y : R} :

x ∈ s → y ∈ s → x + y ∈ s

A subsemiring is closed under addition.

source

instance Subsemiring.toNonAssocSemiring {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

NonAssocSemiring ↥s

A subsemiring of a NonAssocSemiring inherits a NonAssocSemiring structure

Equations

s.toNonAssocSemiring = SubsemiringClass.toNonAssocSemiring s

source

@[simp]

theorem Subsemiring.coe_one {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

↑1 = 1

source

@[simp]

theorem Subsemiring.coe_zero {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

↑0 = 0

source

@[simp]

theorem Subsemiring.coe_add {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) (x : ↥s) (y : ↥s) :

↑(x + y) = ↑x + ↑y

source

@[simp]

theorem Subsemiring.coe_mul {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) (x : ↥s) (y : ↥s) :

↑(x * y) = ↑x * ↑y

source

instance Subsemiring.nontrivial {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) [Nontrivial R] :

Nontrivial ↥s

Equations

⋯ = ⋯

source

theorem Subsemiring.pow_mem {R : Type u_1} [Semiring R] (s : Subsemiring R) {x : R} (hx : x ∈ s) (n : ℕ) :

x ^ n ∈ s

source

instance Subsemiring.noZeroDivisors {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) [NoZeroDivisors R] :

NoZeroDivisors ↥s

Equations

⋯ = ⋯

source

instance Subsemiring.toSemiring {R : Type u_1} [Semiring R] (s : Subsemiring R) :

Semiring ↥s

A subsemiring of a Semiring is a Semiring.

Equations

s.toSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

source

@[simp]

theorem Subsemiring.coe_pow {R : Type u_1} [Semiring R] (s : Subsemiring R) (x : ↥s) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

instance Subsemiring.toCommSemiring {R : Type u_1} [CommSemiring R] (s : Subsemiring R) :

CommSemiring ↥s

A subsemiring of a CommSemiring is a CommSemiring.

Equations

s.toCommSemiring = CommSemiring.mk ⋯

source

def Subsemiring.subtype {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

↥s →+* R

The natural ring hom from a subsemiring of semiring R to R.

Equations

s.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

theorem Subsemiring.coe_subtype {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

⇑s.subtype = Subtype.val

source

theorem Subsemiring.nsmul_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) {x : R} (hx : x ∈ s) (n : ℕ) :

n • x ∈ s

source

@[simp]

theorem Subsemiring.coe_toSubmonoid {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

↑s.toSubmonoid = ↑s

source

@[simp]

theorem Subsemiring.coe_carrier_toSubmonoid {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

s.carrier = ↑s

source

theorem Subsemiring.mem_toAddSubmonoid {R : Type u} [NonAssocSemiring R] {s : Subsemiring R} {x : R} :

x ∈ s.toAddSubmonoid ↔ x ∈ s

source

theorem Subsemiring.coe_toAddSubmonoid {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) :

↑s.toAddSubmonoid = ↑s

source

instance Subsemiring.instTop {R : Type u} [NonAssocSemiring R] :

Top (Subsemiring R)

The subsemiring R of the semiring R.

Equations

Subsemiring.instTop = { top := let __src := ⊤; let __src_1 := ⊤; { toSubmonoid := __src, add_mem' := ⋯, zero_mem' := ⋯ } }

source

@[simp]

theorem Subsemiring.mem_top {R : Type u} [NonAssocSemiring R] (x : R) :

x ∈ ⊤

source

@[simp]

theorem Subsemiring.coe_top {R : Type u} [NonAssocSemiring R] :

↑⊤ = Set.univ

source

instance Subsemiring.instInf {R : Type u} [NonAssocSemiring R] :

Inf (Subsemiring R)

The inf of two subsemirings is their intersection.

Equations

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

source

@[simp]

theorem Subsemiring.coe_inf {R : Type u} [NonAssocSemiring R] (p : Subsemiring R) (p' : Subsemiring R) :

↑(p ⊓ p') = ↑p ∩ ↑p'

source

@[simp]

theorem Subsemiring.mem_inf {R : Type u} [NonAssocSemiring R] {p : Subsemiring R} {p' : Subsemiring R} {x : R} :

x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

source

def RingHom.domRestrict {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] {σR : Type u_1} [SetLike σR R] [SubsemiringClass σR R] (f : R →+* S) (s : σR) :

↥s →+* S

Restriction of a ring homomorphism to a subsemiring of the domain.

Equations

f.domRestrict s = f.comp (SubsemiringClass.subtype s)

source

@[simp]

theorem RingHom.restrict_apply {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] {σR : Type u_1} [SetLike σR R] [SubsemiringClass σR R] (f : R →+* S) {s : σR} (x : ↥s) :

(f.domRestrict s) x = f ↑x

source

def RingHom.eqLocusS {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : R →+* S) :

Subsemiring R

The subsemiring of elements x : R such that f x = g x

Equations

f.eqLocusS g = { carrier := {x : R | f x = g x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

source

@[simp]

theorem RingHom.eqLocusS_same {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) :

f.eqLocusS f = ⊤

Documentation

Mathlib.Algebra.Ring.Subsemiring.Defs

Bundled subsemirings #